Custom query (527 matches)

Filters
 
or
 
  
 
Columns

Show under each result:


Results (501 - 527 of 527)

1 2 3 4 5 6

Status: new (25 matches)

Ticket Summary Owner Type Priority Version Severity
#17346 have access to notation in ml defect 3 pre-1.x normal
#17348 Intro-pattern `|>` might transform a provable goal to a non-provable one defect 3 pre-1.x normal
#17349 call tactic for aequiv conclusions enhancement 3 pre-1.x normal
#17351 sp for aqeuiv goals enhancement 3 pre-1.x normal
#17353 `&&` could disappear from internal code, and be replaced by distinct splitting lemmas for `/\` enhancement 1 pre-1.x normal
#17356 Two-sided `rcondx` enhancement 1 pre-1.x normal
#17357 rnd tactic for aprhl enhancement 3 pre-1.x normal
#17358 A normalization operator enhancement 3 pre-1.x normal
#17363 Conseq: do not how to combine equivF and hoareS and hoareS into equivS enhancement 3 pre-1.x normal
#17366 crush losing some context on intermediate substitutions defect 3 pre-1.x normal
#17367 abbreviations involving modules and memories enhancement 3 pre-1.x normal
#17368 atomic formula of ambient logic expressing disjoint globals of modules enhancement 3 pre-1.x normal
#17370 checking memory initialisation constraints enhancement 3 pre-1.x normal
#17382 glob M should reduce to a record enhancement 3 pre-1.x normal
#17383 abstract operators in section should be generalized enhancement 3 pre-1.x normal
#17384 module parametrised by expressions enhancement 3 pre-1.x normal
#17386 crush reduces goal whose conclusion is `y1 = y2 <=> x1 = x2` to false goal defect 3 pre-1.x normal
#17388 allows _ in pattern enhancement 3 pre-1.x normal
#17390 problem with use of match on expression involving polymorphic operator/abbreviation defect 3 pre-1.x normal
#17395 when cloning operators, lemmas may need to be turned into axioms defect 3 pre-1.x normal
#17396 automated lemmas and simplification hints for match's get_as_X operators enhancement 3 pre-1.x normal
#17037 Poor error message for module restriction example Pierre-Yves Strub enhancement 2 pre-1.x minor
#17307 Coq style Locate enhancement 1 pre-1.x minor
#17399 `sim: (<eqs>)` could use `conseq (: <eqs>)` internally as frame enhancement 3 pre-1.x minor
#16103 scoping issue with theories enhancement 3 pre-1.x

Status: reopened (2 matches)

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