Custom query (541 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (401 - 500 of 541)

1 2 3 4 5 6

Status: closed (52 matches)

Ticket Summary Owner Type Priority Component Version
#15893 Call in adversary call is not working properly Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#15892 It should not be possible to close a theory where not all proofs are finished Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15891 Instantiating axioms and sub-theories when cloning theories Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#15884 Repeat tactic broken Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15882 tuple and memory misprinted Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15881 Complete path for local variable in printer Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15880 Constant propagation with module variable Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15879 While one sided ckunz enhancement 3 EasyCrypt pre-1.x
#15877 Apply is not working when trying to use it to instantiate a lemma that is quantified on modules Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15874 Add support for chaining relations Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#15873 Bug Printer Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#15872 fun stopped working ckunz defect 5 EasyCrypt pre-1.x
#15871 Stack Overflow Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15859 Omit path when it can be inferred from context Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15854 Allow sequences of variable declarations in procedure definitions Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15853 timeout and prover settings are not undone Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#15852 Undo immediately after 'save.' does not work Pierre-Yves Strub defect 1 ProofGeneral pre-1.x
#15851 [rnd] for map update produces confusing post-conditions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15849 Ignoring proof that are already done in a file Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15842 Bug in lambda translation Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15841 No explicit binding in equiv creates problems Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15827 memory restriction for adversary does not take inner modules into account Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#15817 Lighten EC syntax by removing the clumsy "<:" && "&" notations for modules / memories introductions / applications Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#15815 Search path for theories should include path of currently active file Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#15814 call tactic accepts variable defined in left game ({1}) defined for right game Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15813 call tactic signals an "unknown symbol" error Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15809 Parsing/Printing scope for operator overloading "(x op y)%Scope" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15808 Declaring/defining mixfix operators, using them when not in scope Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15794 Operator not found Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15791 import doesn't import function from module Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15786 Swap with call to the adversary defect 3 EasyCrypt pre-1.x
#15781 Bug into env insertion of a specific axiom Pr[] Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15779 Inference during apply Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15769 ProofGeneral issue with new EasyCrypt: undo step at EOF give Emacs type error Pierre-Yves Strub defect 3 ProofGeneral pre-1.x
#15768 Inlining with functor and cloning doesn't work Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15764 Result not introduce after call in hoare logic Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15762 Tactic to transform a tuple equality into a conjonction Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15744 require import causes name collisions in sub theories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15742 Strange error raised during a call to trivial Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15738 Typing functor applications inside modules Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15737 Type-soundness issue when implementing module signatures Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15716 Problem with introduction of Module in Proof Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15715 Can't access a variable from a functor in probability formula Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15702 Error with multiple require if they contain the same game Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#15676 Zeta tactics takes too much time to end(infinite loop ?) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15651 lambda in operator doesn't work Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15647 Can't extract easily function from tuple Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15612 require Theory issues misleading "added" messages Pierre-Yves Strub defect 1 EasyCrypt pre-1.x
#15520 request for more loop manipulation tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15506 Issues when cloning theories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15502 "Ident <top>_[...] is not yet declared" when cloning a theory with operators Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15106 Consider probability quantities as real-valued expressions enhancement 2 EasyCrypt pre-1.x

Status: new (48 matches)

Ticket Summary Owner Type Priority Component Version
#17391 case works with tuple corresponding to glob M, but not with glob M defect 3 EasyCrypt pre-1.x
#17390 problem with use of match on expression involving polymorphic operator/abbreviation defect 3 EasyCrypt pre-1.x
#17388 allows _ in pattern enhancement 3 EasyCrypt pre-1.x
#17386 crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal defect 3 EasyCrypt pre-1.x
#17384 module parametrised by expressions enhancement 3 EasyCrypt pre-1.x
#17383 abstract operators in section should be generalized enhancement 3 EasyCrypt pre-1.x
#17382 glob M should reduce to a record enhancement 3 EasyCrypt pre-1.x
#17374 pre-/post- should be implemented with an explicit memory enhancement 3 Internals pre-1.x
#17370 checking memory initialisation constraints enhancement 3 EasyCrypt pre-1.x
#17368 atomic formula of ambient logic expressing disjoint globals of modules enhancement 3 EasyCrypt pre-1.x
#17367 abbreviations involving modules and memories enhancement 3 EasyCrypt pre-1.x
#17366 crush losing some context on intermediate substitutions defect 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
#17358 A normalization operator enhancement 3 EasyCrypt pre-1.x
#17357 rnd tactic for aprhl enhancement 3 EasyCrypt pre-1.x
#17356 Two-sided `rcondx` enhancement 1 EasyCrypt pre-1.x
#17353 `&&` could disappear from internal code, and be replaced by distinct splitting lemmas for `/\` enhancement 1 EasyCrypt pre-1.x
#17351 sp for aqeuiv goals enhancement 3 EasyCrypt pre-1.x
#17349 call tactic for aequiv conclusions enhancement 3 EasyCrypt pre-1.x
#17348 Intro-pattern `|>` might transform a provable goal to a non-provable one defect 3 EasyCrypt pre-1.x
#17346 have access to notation in ml defect 3 EasyCrypt pre-1.x
#17344 Trees and polynomials enhancement 3 EasyCrypt pre-1.x
#17342 Better support for rewriting with equivalences enhancement 3 EasyCrypt pre-1.x
#17341 for loops enhancement 3 EasyCrypt pre-1.x
#17340 cfold should support variables (and more general terms). enhancement 3 EasyCrypt pre-1.x
#17337 substitutions should complain when substituting a locally defined variable enhancement 3 EasyCrypt pre-1.x
#17325 syntax marking end of cloning realization enhancement 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
#17317 `search` should work somewhat better with abbreviations enhancement 3 EasyCrypt pre-1.x
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 3 EasyCrypt pre-1.x
#17311 `smt (@Self)` enhancement 3 EasyCrypt pre-1.x
#17307 Coq style Locate enhancement 1 EasyCrypt pre-1.x
#17305 proc* in eager case needlessly assigns result of procedures returning unit to variables enhancement 3 EasyCrypt pre-1.x
#17301 Applicative view for `if then else` enhancement 3 EasyCrypt pre-1.x
#17298 Super rnd enhancement 4 EasyCrypt phl
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 EasyCrypt pre-1.x
#17295 local ops enhancement 3 EasyCrypt pre-1.x
#17290 `n!->>` should work enhancement 3 EasyCrypt pre-1.x
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 EasyCrypt pre-1.x
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 3 EasyCrypt pre-1.x
#17286 pRHL `apply` should have a framing variant enhancement 3 EasyCrypt pre-1.x
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 EasyCrypt pre-1.x
#17283 pattern matching complexity problem defect 3 EasyCrypt pre-1.x
#17282 call should not work task 3 EasyCrypt phl
#17281 Several problems with `apply` in program logics enhancement 3 EasyCrypt pre-1.x
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 EasyCrypt pre-1.x
#17267 `auto` with `call` enhancement 3 EasyCrypt pre-1.x
#17259 Theory of distribution (iso)morphisms task 3 Libraries pre-1.x
(more results for this group on next page)
1 2 3 4 5 6
Note: See TracQuery for help on using queries.