Custom query (559 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (501 - 559 of 559)

1 2 3 4 5 6

Status: new (57 matches)

Ticket Summary Owner Type Priority Component Version
#17215 Issues with module typing when functor parameters are themselves functors defect 3 EasyCrypt pre-1.x
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment enhancement 3 EasyCrypt pre-1.x
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate enhancement 3 EasyCrypt pre-1.x
#17225 Explore reproducible smt calls enhancement 3 EasyCrypt pre-1.x
#17239 Mutual inductive types. enhancement 3 EasyCrypt pre-1.x
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 EasyCrypt pre-1.x
#17246 `rewrite`, apply, ... in contracts defect 3 EasyCrypt pre-1.x
#17251 print Self enhancement 3 EasyCrypt pre-1.x
#17257 `/=` is too weak. defect 5 EasyCrypt pre-1.x
#17259 Theory of distribution (iso)morphisms task 3 Libraries pre-1.x
#17267 `auto` with `call` enhancement 3 EasyCrypt pre-1.x
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 EasyCrypt pre-1.x
#17281 Several problems with `apply` in program logics enhancement 3 EasyCrypt pre-1.x
#17283 pattern matching complexity problem defect 3 EasyCrypt pre-1.x
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 EasyCrypt pre-1.x
#17286 pRHL `apply` should have a framing variant enhancement 3 EasyCrypt pre-1.x
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 3 EasyCrypt pre-1.x
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 EasyCrypt pre-1.x
#17295 local ops enhancement 3 EasyCrypt pre-1.x
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 EasyCrypt pre-1.x
#17301 Applicative view for `if then else` enhancement 3 EasyCrypt pre-1.x
#17305 proc* in eager case needlessly assigns result of procedures returning unit to variables enhancement 3 EasyCrypt pre-1.x
#17307 Coq style Locate enhancement 1 EasyCrypt pre-1.x
#17311 `smt (@Self)` enhancement 3 EasyCrypt pre-1.x
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 3 EasyCrypt pre-1.x
#17322 use of side with HL version of while tactic should be syntax error defect 3 EasyCrypt pre-1.x
#17325 syntax marking end of cloning realization enhancement 3 EasyCrypt pre-1.x
#17337 substitutions should complain when substituting a locally defined variable enhancement 3 EasyCrypt pre-1.x
#17340 cfold should support variables (and more general terms). enhancement 3 EasyCrypt pre-1.x
#17341 for loops enhancement 3 EasyCrypt pre-1.x
#17342 Better support for rewriting with equivalences enhancement 3 EasyCrypt pre-1.x
#17344 Trees and polynomials enhancement 3 EasyCrypt pre-1.x
#17346 have access to notation in ml enhancement 3 EasyCrypt pre-1.x
#17349 call tactic for aequiv conclusions enhancement 3 EasyCrypt pre-1.x
#17351 sp for aqeuiv goals enhancement 3 EasyCrypt pre-1.x
#17353 `&&` could disappear from internal code, and be replaced by distinct splitting lemmas for `/\` enhancement 1 EasyCrypt pre-1.x
#17356 Two-sided `rcondx` enhancement 1 EasyCrypt pre-1.x
#17357 rnd tactic for aprhl enhancement 3 EasyCrypt pre-1.x
#17358 A normalization operator enhancement 3 EasyCrypt pre-1.x
#17363 Conseq: do not how to combine equivF and hoareS and hoareS into equivS enhancement 3 EasyCrypt pre-1.x
#17367 abbreviations involving modules and memories enhancement 3 EasyCrypt pre-1.x
#17368 atomic formula of ambient logic expressing disjoint globals of modules enhancement 3 EasyCrypt pre-1.x
#17370 checking memory initialisation constraints enhancement 3 EasyCrypt pre-1.x
#17374 pre-/post- should be implemented with an explicit memory enhancement 3 Internals pre-1.x
#17382 glob M should reduce to a record enhancement 3 EasyCrypt pre-1.x
#17383 abstract operators in section should be generalized enhancement 3 EasyCrypt pre-1.x
#17384 module parametrised by expressions enhancement 3 EasyCrypt pre-1.x
#17388 allows _ in pattern enhancement 3 EasyCrypt pre-1.x
#17390 problem with use of match on expression involving polymorphic operator/abbreviation defect 3 EasyCrypt pre-1.x
#17395 potential unsoundness when cloning concrete operators defect 3 EasyCrypt pre-1.x
#17396 automated lemmas and simplification hints for match's get_as_X operators enhancement 3 EasyCrypt pre-1.x
#17399 `sim: (<eqs>)` could use `conseq (: <eqs>)` internally as frame enhancement 3 EasyCrypt pre-1.x
#17404 rename procedure name when cloning enhancement 3 EasyCrypt pre-1.x
#17406 FEL tactic should take memory reads into account when deciding what counts as an oracle defect 3 EasyCrypt pre-1.x
#17407 Alt-Ergo + IntDiv proves false defect 3 EasyCrypt pre-1.x
#17410 .eco should include information about provers used defect 3 EasyCrypt pre-1.x
#17413 rewrite /Top.f needed instead of /f to avoid going two levels deep, when op f = T.f defect 3 EasyCrypt pre-1.x

Status: reopened (2 matches)

Ticket Summary Owner Type Priority Component Version
#17182 Renaming internal symbols on cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17186 using [bypr] in odd way can result in badly formed goal Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
1 2 3 4 5 6
Note: See TracQuery for help on using queries.