Custom query (536 matches)

Filters
 
or
 
  
 
Columns

Show under each result:

Results (401 - 500 of 536)

← 1 2 3 4 5 6 →

Status: closed (51 matches)

Ticket Summary Owner Type Priority Version Severity
#15879 While one sided ckunz enhancement 3 pre-1.x
#15921 A strongest post-condition tactic [sp n m], like in trunk ckunz enhancement 3 pre-1.x
#16174 Bug in bdhoare call ckunz defect 3 pre-1.x normal
#16292 Side-conditions for the rnd rule in pHL should be proved under some precondition ckunz defect 3 pre-1.x
#16560 Non-relational 'bypr' for probabilistic Hoare statements ckunz enhancement 3 pre-1.x
#16986 "while >=" generates invalid goals ckunz defect 3 pre-1.x normal
#15827 memory restriction for adversary does not take inner modules into account Benjamin Grégoire defect 3 pre-1.x
#15841 No explicit binding in equiv creates problems Benjamin Grégoire defect 3 pre-1.x minor
#15842 Bug in lambda translation Benjamin Grégoire defect 3 pre-1.x
#15893 Call in adversary call is not working properly Benjamin Grégoire defect 4 pre-1.x
#15919 [case] tactic for bd_hoare is useless Benjamin Grégoire defect 3 pre-1.x
#15950 tactics for fundamental lemma Benjamin Grégoire enhancement 4 pre-1.x major
#15968 assertion failure when fun tactic for abstract function isn't given argument Benjamin Grégoire defect 3 pre-1.x normal
#15974 The following example generates an anomaly Benjamin Grégoire defect 3 pre-1.x
#15980 inconsistency due to choosing from empty distribution Benjamin Grégoire defect 3 pre-1.x critical
#15981 "delta cpEq" causes an untypable goal to be produced Benjamin Grégoire defect 3 pre-1.x
#15982 Printer bug for partially applied infix operators in prefix form Benjamin Grégoire defect 3 pre-1.x
#16000 repeated instantiation and losslessness of 3-argument fun don't work well together Benjamin Grégoire defect 3 pre-1.x major
#16137 universal elimination doesn't enforce { ... } restriction on module Benjamin Grégoire defect 3 pre-1.x major
#16138 assertion failure when call tactic not given { ... } module restriction Benjamin Grégoire defect 3 pre-1.x normal
#16228 glob M computation problem with functors and inner modules for {*} Benjamin Grégoire defect 3 pre-1.x normal
#16231 General issues with computation of globals for nested modules Benjamin Grégoire defect 3 pre-1.x major
#16306 Bug in cloning ? Benjamin Grégoire defect 5 pre-1.x major
#16362 Assertion failure when cloning a theory with let expressions Benjamin Grégoire defect 3 pre-1.x
#16416 FEL completeness - initialization Benjamin Grégoire enhancement 3 pre-1.x normal
#16622 Functor-level "lambdas" Benjamin Grégoire enhancement 2 pre-1.x
#16723 Subtyping for abstract modules and functors Benjamin Grégoire enhancement 3 pre-1.x
#16727 bd_hoare should work on >=, rather than forcing us to swap arguments Benjamin Grégoire defect 3 pre-1.x minor
#16729 Tactic swap causes inconsistent dependencies Benjamin Grégoire defect 3 pre-1.x blocker
#16732 Problem with functor aliases when outermost module is a parameter Benjamin Grégoire defect 3 pre-1.x
#16749 link between hoare bdhoare equiv Benjamin Grégoire enhancement 3 pre-1.x
#16751 hoare should work on fun. Benjamin Grégoire defect 3 pre-1.x normal
#16787 new conseq issues Benjamin Grégoire defect 5 pre-1.x blocker
#16849 Broken proc (in branch 1.0) Benjamin Grégoire defect 3 pre-1.x blocker
#16965 Non-termination when expanding a procedure whose body contains a generic projector (.`n) Benjamin Grégoire defect 3 pre-1.x critical
#17021 Some judgment-combining variants of conseq do not apply to procedures Benjamin Grégoire defect 3 pre-1.x normal
#17046 possible tactic renaming: [proc *] -> [eager proc *] Benjamin Grégoire enhancement 3 pre-1.x normal
#17083 Missing eta-reduction in conversion Benjamin Grégoire enhancement 3 pre-1.x normal
#17089 anomaly in [sim] Benjamin Grégoire defect 4 pre-1.x normal
#17109 Hoare adversary rule introducess references to non-existent memories in postconditions Benjamin Grégoire defect 5 pre-1.x normal
#17114 Unsoundness of module system Benjamin Grégoire defect 5 pre-1.x blocker
#17128 assert false in rnd. Benjamin Grégoire defect 3 pre-1.x normal
#17129 bug in alias, the introduced variable has not the good type. Benjamin Grégoire defect 3 pre-1.x normal
#17130 "alias i" works only on random instruction. Benjamin Grégoire enhancement 3 pre-1.x normal
#17133 seq for phoare do not check the type of the arguments. Benjamin Grégoire defect 3 pre-1.x normal
#17142 Anomaly (related to SMT and memories) Benjamin Grégoire defect 3 pre-1.x normal
#17300 Module type checks have wrong variance when dealing with some functor configurations Benjamin Grégoire defect 3 pre-1.x normal
#17302 fel can generate subgoal with undefined memory Benjamin Grégoire defect 3 pre-1.x normal
#17303 more fel peculiarities Benjamin Grégoire defect 3 pre-1.x normal
#17376 behaviour of module type include in functor types Benjamin Grégoire enhancement 3 pre-1.x normal
#17380 Internal "seq" of pHL tactics is unsound Benjamin Grégoire defect 5 pre-1.x critical

Status: new (49 matches)
Ticket Summary Owner Type Priority Version Severity
#16103 scoping issue with theories enhancement 3 pre-1.x
#16912 Lifting the "collection update" statements to tuples enhancement 1 pre-1.x normal
#16987 Move facts from precondition to context enhancement 3 pre-1.x normal
#17022 Pattern-matching on variables in judgments and probability expressions enhancement 3 pre-1.x normal
#17036 Instantiating abstract modules: warnings and interactive justification enhancement 1 pre-1.x normal
#17045 Rewriting procedures in probability expressions directly from an equivalence enhancement 1 pre-1.x normal
#17086 Generalize [rewrite Pr] enhancement 3 pre-1.x normal
#17090 Selecting procedure(s) to [inline] by position enhancement 2 pre-1.x normal
#17105 [transitivity] for phoare and hoare enhancement 3 pre-1.x normal
#17113 Decide what to do on rewrite with defined head symbols enhancement 3 pre-1.x normal
#17140 Pattern matching should make use of simplification rules. enhancement 3 pre-1.x normal
#17149 Expand glob A for concrete module enhancement 3 pre-1.x normal
#17156 New vernacular command: `print axiom` enhancement 3 pre-1.x normal
#17163 Check that `phoare` tactics are forcing the input bounds to be in [0..1]. task 4 pre-1.x major
#17164 behavior of -check-all enhancement 3 pre-1.x normal
#17169 Anonymous functor arguments: passing procedures to functors directly enhancement 3 pre-1.x normal
#17175 Direct intro on negative goals enhancement 3 pre-1.x normal
#17183 Variant of `sim` that works modulo inlining. enhancement 1 pre-1.x normal
#17192 Problem with `glob` and type inference defect 3 pre-1.x normal
#17197 Asserts in equivalence proofs enhancement 3 pre-1.x normal
#17202 Add seq* tactic enhancement 3 pre-1.x major
#17210 Pattern-matching for pairs in operator arguments enhancement 3 pre-1.x normal
#17215 Issues with module typing when functor parameters are themselves functors defect 3 pre-1.x normal
#17217 need better error message when attempting to apply lemma to goal that isn't a judgment enhancement 3 pre-1.x normal
#17218 proposal for expressing goal of two-sided PRHL rnd tactic using isomorphism of bijections predicate enhancement 3 pre-1.x normal
#17225 Explore reproducible smt calls enhancement 3 pre-1.x normal
#17239 Mutual inductive types. enhancement 3 pre-1.x normal
#17245 Formula manipulation commands (for `conseq` and `seq`) enhancement 3 pre-1.x normal
#17246 `rewrite`, apply, ... in contracts defect 3 pre-1.x normal
#17251 print Self enhancement 3 pre-1.x normal
#17257 `/=` is too weak. defect 5 pre-1.x normal
#17267 `auto` with `call` enhancement 3 pre-1.x normal
#17279 Improve `invalid goal shape` error messages for variants of `byequiv` enhancement 3 pre-1.x normal
#17281 Several problems with `apply` in program logics enhancement 3 pre-1.x normal
#17282 call should not work task 3 phl normal
#17283 pattern matching complexity problem defect 3 pre-1.x normal
#17285 Transitivity on procedures should support inferring contracts from `equiv` lemmas. enhancement 3 pre-1.x normal
#17286 pRHL `apply` should have a framing variant enhancement 3 pre-1.x normal
#17287 Program transformation tactics should not `anomaly` without a side in pRHL defect 3 pre-1.x normal
#17288 EasyCrypt crashes when printing required abstract theory IterProc defect 3 pre-1.x normal
#17295 local ops enhancement 3 pre-1.x normal
#17297 Allow the optional use of undeclared variables in procedures enhancement 1 pre-1.x normal
#17298 Super rnd enhancement 4 phl blocker
#17301 Applicative view for `if then else` enhancement 3 pre-1.x normal
#17305 proc* in eager case needlessly assigns result of procedures returning unit to variables enhancement 3 pre-1.x normal
#17307 Coq style Locate enhancement 1 pre-1.x minor
#17311 `smt (@Self)` enhancement 3 pre-1.x normal
#17316 [smt (@Theory)] should force the use of axioms marked as `nosmt` defect 3 pre-1.x normal
#17322 use of side with HL version of while tactic should be syntax error defect 3 pre-1.x normal
(more results for this group on next page)
← 1 2 3 4 5 6 →
Note: See TracQuery for help on using queries.