Custom query (551 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (201 - 300 of 551)

1 2 3 4 5 6

Status: closed (100 matches)

Ticket Summary Owner Type Priority Component Version
#16775 EasyCrypt insists on typing boolean-returning fixpoints as predicates Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16780 Change the test script so the test suites can be run in weak check mode Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16786 Nicer treatment of datatype constructors Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16787 new conseq issues Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#16788 Another stack overflow during unification Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16789 Pattern matching should to some top-level delta-unfolding Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16790 Bug when cloning and instantiating an abstract type Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16811 inline * should not try to inline abstract function Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16840 @ can be used to define infix operators, but cannot be used to apply them Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16849 Broken proc (in branch 1.0) Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#16856 Blocker typing bug in rnd (master) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16885 Support for type annotations in let expressions Pierre-Yves Strub enhancement 1 EasyCrypt pre-1.x
#16918 selection tactical "all n" Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16963 op/pred nosmt ... Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#16964 Warn when a variable is used before being initialized Pierre-Yves Strub 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
#16966 Many lexer errors related to the universal projector notation (.'n) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16983 equiv generates ill-typed formulas on ill-typed input (instead of an error) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16984 Anomaly due to inlining functions with tuple arguments Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#16986 "while >=" generates invalid goals ckunz defect 3 EasyCrypt pre-1.x
#16990 Generalization does not cross tuple projections. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17005 Higher-order pattern matching enhancement 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
#17007 Inconsistent syntax for closing sections/theories enhancement 2 EasyCrypt pre-1.x
#17009 1.x error messages Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17011 Pretty-printer in adding too much scoping annotation Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17012 pr_false is badly implemented (unsoundness) Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17013 EasyCrypt toolchain does not compile anymore on OSX Pierre-Yves Strub defect 5 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
#17018 splitwhile syntax is still weird Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17021 Some judgment-combining variants of conseq do not apply to procedures Benjamin Grégoire defect 3 EasyCrypt pre-1.x
#17026 EasyCrypt does not compile on Windows (win32 / cygwin) Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17027 [Unsoundness] The HL and pHL tactics for abstract function calls do not quantify over variables that may be modified in the postcondition Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17033 Some program logic tactics that modify the precondition use bad associativity Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17035 Alt-Ergo succeeds on false obligations in weird circumstances Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17038 Message with anomaly Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17044 Bad inlining when giving an argument of type unit to a procedure that expects no arguments Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17047 pretty printing of module type uses old notation for "*" defect 3 EasyCrypt pre-1.x
#17049 "restart scripting" not working in ProofGeneral defect 2 ProofGeneral pre-1.x
#17050 elim/let anomaly Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17051 Pretty-printing regression defect 3 EasyCrypt pre-1.x
#17052 Parse error on (**) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17053 Bogus goal when variable shadows a module Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17054 Finiteness of product of finite types enhancement 3 Libraries pre-1.x
#17055 Lemma linking eq_except and in_dom in FMap enhancement 3 Libraries pre-1.x
#17057 Add the possibility to rule out the prover filtering mecanism from the command line. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17059 Negative line selectors in program logic tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17060 pretty printer still using "lambda" instead of "fun" defect 3 EasyCrypt pre-1.x
#17061 when arguments to seq are too big, anomaly rather than error message defect 3 EasyCrypt pre-1.x
#17065 Invalid priority of `by` w.r.t `;` Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17066 Better error message when operator selection failed. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17067 Syntax for chained case analysis of the top-assumption Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17068 Possible bug in the union-find algorithm Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17069 Improve error messages of the (P?R)HL tactics Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17071 Error message for [expect] <default> enhancement 1 EasyCrypt pre-1.x
#17072 Pretty Printer Glitches for !(_ = _) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17073 `case` intro-pattern does not try to head-reduce if the goal is not subject to intro. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17074 Option to destruct disjunctive hypotheses in [progress] Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17075 [sp] should fail when given code positions that cannot be reached Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17078 EasyCrypt should use big integers internally. Pierre-Yves Strub defect 3 Internals pre-1.x
#17079 Make the test-suite pass. Pierre-Yves Strub defect 5 Libraries pre-1.x
#17080 `t_generalize_hyps` does not work when given a non-singleton list. Pierre-Yves Strub defect 4 Internals pre-1.x
#17083 Missing eta-reduction in conversion Benjamin Grégoire enhancement 3 EasyCrypt pre-1.x
#17084 syntax for non-flat proof-terms Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17087 [conseq*] should be the default behaviour of [conseq] Pierre-Yves Strub enhancement 4 EasyCrypt pre-1.x
#17089 anomaly in [sim] Benjamin Grégoire defect 4 EasyCrypt pre-1.x
#17091 [rewrite] should head-reduce created b-redexes Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17092 Chaining [apply] Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17093 Add the possibility to declare several operators/predicates in 1 command. Pierre-Yves Strub enhancement 2 EasyCrypt pre-1.x
#17094 Refactoring: code for operators addition. Pierre-Yves Strub enhancement 3 Internals pre-1.x
#17095 anomaly raised by invariant form of [call upto] defect 3 EasyCrypt pre-1.x
#17096 Unfolding should work even in the presence of several matching operators. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17097 Bad pretty-printing of lists. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17098 Add a search facility Pierre-Yves Strub enhancement 4 Documentation pre-1.x
#17099 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17100 Forward `apply` should be accessible for the top-assumption in intro-patterns Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17101 [anomaly] when defining an operator over a concrete module's globals Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17102 [anomaly] when pHL => pRHL variant of conseq is used with a bound different from [=1%r] Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17104 Make (<>) accessible in prefix form enhancement 1 EasyCrypt pre-1.x
#17106 Unification should work modulo delta-unfolding / simplification. enhancement 3 EasyCrypt pre-1.x
#17107 Potential mismatch between spec and lemma versions of the "pHL + HL => pHL" variant of [conseq] defect 3 EasyCrypt pre-1.x
#17108 require clone enhancement 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
#17110 [anomaly] on using [call] with a lemma referring to the wrong procedure Pierre-Yves Strub defect 2 EasyCrypt pre-1.x
#17112 `unknown symbol Top.o` when importing a theory including objects referring to `Top.o` Pierre-Yves Strub defect 5 EasyCrypt pre-1.x
#17114 Unsoundness of module system Benjamin Grégoire defect 5 EasyCrypt pre-1.x
#17115 [exfalso] tactic for ambient logic enhancement 3 EasyCrypt pre-1.x
#17116 Bad error message for [swap] Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17118 Add the ability to print the axioms of the environment enhancement 3 EasyCrypt pre-1.x
#17119 Give the ability to print subgoals Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17120 [rnd] allows to prove false Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17121 Make Option.witness accessible at top level enhancement 3 EasyCrypt pre-1.x
#17122 Clone ignores provided proof Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17123 Bad parsing on call (_: B, I) Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17124 allows to specify timeout only for smt. Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17125 Cannot clear variables referring to memory Pierre-Yves Strub defect 3 EasyCrypt pre-1.x
#17126 Command and command line option for global timeout multiplier. Pierre-Yves Strub enhancement 3 EasyCrypt pre-1.x
#17127 Bug in typing of instruction x.[y] = e; Pierre-Yves Strub defect 4 EasyCrypt pre-1.x
#17128 assert false in rnd. Benjamin Grégoire 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.