Custom query (541 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (201 - 300 of 541)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Component Version
#16228 glob M computation problem with functors and inner modules for {*} Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16663 Goal window should update on tactic failure... Pierre-Yves Strub defect 2 ProofGeneral pre-1.x
#17005 Higher-order pattern matching enhancement 3 EasyCrypt pre-1.x
#17277 Higher-order pattern-matching with quantifiers Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17109 Hoare adversary rule introducess references to non-existent memories in postconditions Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#16751 hoare should work on fun. Benjamin Grégoire 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
#15922 if tactic for bd_hoare doesn't work with precondition true Santiago Zanella-Béguelin 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
#15791 import doesn't import function from module Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17369 imprecise pretty printing with functor application defect 2 EasyCrypt pre-1.x
#17244 Imprecise "uninitialized local variables" warning Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17069 Improve error messages of the (P?R)HL tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15949 Improve kill error message Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17354 In cloning, `rename` should not be allowed to create unreachable/unparsable symbols Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17375 `include` command for modules / module types Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#15980 inconsistency due to choosing from empty distribution Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17007 Inconsistent syntax for closing sections/theories enhancement 2 EasyCrypt pre-1.x
#15779 Inference during apply Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17389 inline does not inline under match statement defect 3 EasyCrypt pre-1.x
#17336 `inline` procedure selection by code position Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16811 inline * should not try to inline abstract function Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15768 Inlining with functor and cloning doesn't work Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17006 Instantiating an abstract procedure taking n-uple with a n-ary concrete procedure Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16001 Instantiating an internal theory when cloning fails 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
#17247 Interactive proof realisation for `instance` Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17243 Internal error (anomaly) on proof script Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17380 Internal "seq" of pHL tactics is unsound Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17170 Introduce theory for product distribution Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17373 introduction pattern bug somehow related to SmtMap defect 3 EasyCrypt pre-1.x
#17258 Intro pattern for hypothesis duplication Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16725 Intro pattern for substitution Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17326 `+` intro-pattern may reorder assumptions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17328 `_` intro-pattern should only check if the clear is possible once the rest of the intro-pattern has been processed enhancement 3 EasyCrypt pre-1.x
#17065 Invalid priority of `by` w.r.t `;` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17323 |> ip anomaly Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17324 |> ip expands predicates in conclusion Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17134 is_lossless F(M).f generate a parse error. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15506 Issues when cloning theories Pierre-Yves Strub defect 3 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
#16015 lack of dot in map subscripting leads to assertion failure 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
#17055 Lemma linking eq_except and in_dom in FMap enhancement 3 Libraries 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
#16749 link between hoare bdhoare equiv Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#15906 (local) opening of modules Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17293 Looping behaviour in reduction/simplification. Probably related to reals. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17172 Looping on `rewrite !/op` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16746 Losslessness annotations Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17104 Make (<>) accessible in prefix form enhancement 1 EasyCrypt pre-1.x
#17016 Make elim and case work on tuples and records. Retire the special lemmas Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17121 Make Option.witness accessible at top level enhancement 3 EasyCrypt pre-1.x
#17079 Make the test-suite pass. Pierre-Yves Strub defect 5 Libraries pre-1.x
#16628 making nested sections work enhancement 3 EasyCrypt pre-1.x
#16966 Many lexer errors related to the universal projector notation (.'n) Pierre-Yves Strub 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
#17038 Message with anomaly Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17289 Missing dependencies in OPAM package defect 3 EasyCrypt pre-1.x
#16086 Missing error message: "Abstract function <function name> cannot be inlined." Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17083 Missing eta-reduction in conversion Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17206 Missing parens in the pretty printer Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17166 missing syntax for proving all axioms of a theory, its subtheories, etc., when cloning Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17338 misspelled pragmas are not reported Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17171 mode similar to nocheck that tries smt calls and just prints the locations for the failing calls Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17144 Module type checking: Unclear error message and probably bug Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17300 Module type checks have wrong variance when dealing with some functor configurations Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17313 module types with multiple occurrences of same procedure should not be accepted Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17303 more fel peculiarities Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17248 More precise error messages when non-interactive realization fails Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17137 More tactical about goal selections Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16082 move * for adversary function outside { ... } Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17291 `move: x` should keep the body of `x` if any. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16150 Multiple import Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17139 Multiple require at once. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16104 naming issues enhancement 3 EasyCrypt pre-1.x
#17059 Negative line selectors in program logic tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16787 new conseq issues Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17371 new option for smt Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17205 New syntax for assignments should be available in immediate definitions Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16087 New view for apply: !a -> (a => false) Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#16786 Nicer treatment of datatype constructors Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17387 no error message for match Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15841 No explicit binding in equiv creates problems Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16253 Non-local modules and abstract restrictions. defect 3 EasyCrypt pre-1.x
#16560 Non-relational 'bypr' for probabilistic Hoare statements ckunz enhancement 3 EasyCrypt pre-1.x
#16965 Non-termination when expanding a procedure whose body contains a generic projector (.`n) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16141 Not catched error in split Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17165 not-to-be-proved lemmas Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17193 Obscure failure on lazy smt with higher-order stuff and booleans 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
#17306 Operator folding and unfolding not checking type parameters Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#15794 Operator not found Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17219 operators don't print the way they are declared Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17148 Operators should be subject to section restrictions Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#16963 op/pred nosmt ... Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17200 Parse error in required theories are incorrectly located. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17147 Parse error in (some) expressions involving memories Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17184 parse error involving parameterized module Pierre-Yves Strub defect 3 EasyCrypt 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.