aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/equality.ml
Commit message (Expand)AuthorAge
* Fix program cases and inversion tactic to correctly record universe constraints.Gravatar Matthieu Sozeau2014-06-24
* Removing opens to Clenvtac to track its use more easily.Gravatar Pierre-Marie Pédrot2014-06-23
* More on injection over a projectable "existT". - Fixing syntax "injection ......Gravatar Hugo Herbelin2014-05-31
* Fixing introduction patterns * and ** when used in a branch so that they do n...Gravatar Hugo Herbelin2014-05-31
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
* When discrimination is not possible, try to project.Gravatar Maxime Dénès2014-05-18
* Suggest Set Injection On Proofs in error message for injection.Gravatar Maxime Dénès2014-05-18
* Restored old behavior of injection on proofs by default.Gravatar Maxime Dénès2014-05-18
* Code cleaning & factorizing functions in Equality.Gravatar Pierre-Marie Pédrot2014-05-09
* Encapsulating some clausenv uses. This simplifies the control flow of someGravatar Pierre-Marie Pédrot2014-05-08
* Revert "Avoid "revert" to retype-check the goal, and move it to a "new" tactic."Gravatar Hugo Herbelin2014-05-08
* Avoid "revert" to retype-check the goal, and move it to a "new" tactic.Gravatar Hugo Herbelin2014-05-08
* Simplification and improvement of "subst x" in such a way that itGravatar Hugo Herbelin2014-05-08
* Fixes after rebase. The use of pf_constr_of_global is problematic in presence...Gravatar Matthieu Sozeau2014-05-06
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt Y. Bertot's path on private inductives (now the keyword is "Private").Gravatar Yves Bertot2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Trying to improve the error messages of injection.Gravatar Maxime Dénès2014-04-30
* Injection: do not fail when arguments have sort Prop.Gravatar Maxime Dénès2014-04-29
* Removing useless try-with clauses in Goal.enter variants.Gravatar Pierre-Marie Pédrot2014-04-25
* Fixing various backtrace recordings.Gravatar Pierre-Marie Pédrot2014-04-25
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Cosmetic changes in Equality.Gravatar Pierre-Marie Pédrot2014-03-27
* Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing Tacmach compatibility layer in Equality.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing tactic compatibility layer in Equality.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing Tacmach compatibility layer in Inv.Gravatar Pierre-Marie Pédrot2014-03-26
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Fix test-suite 2255.vGravatar Pierre Boutillier2014-03-17
* Remove some dead-code (thanks to ocaml warnings)Gravatar Pierre Letouzey2014-03-05
* Matching --> ConstrMatching (was clashing with OCaml's compiler-libs)Gravatar Pierre Letouzey2014-03-02
* Fixing pervasive comparisonsGravatar Pierre-Marie Pédrot2014-03-01
* Code refactoring thanks to the new Monad module.Gravatar Arnaud Spiwack2014-02-27
* Writing [cut] tactic using the new monad.Gravatar Pierre-Marie Pédrot2013-12-02
* Porting Tactics.assumption to the new engine.Gravatar ppedrot2013-11-08
* Made Proofview.Goal.hyps a named_context.Gravatar aspiwack2013-11-02
* Less use of the list-based interface for goal-bound tactics.Gravatar aspiwack2013-11-02
* Tachmach.New is now in Proofview.Goal.enter style.Gravatar aspiwack2013-11-02
* More Proofview.Goal.enter.Gravatar aspiwack2013-11-02
* Removed spurious try/with in Proofview.Notation.(>>=) and (>>==).Gravatar aspiwack2013-11-02
* Clean up a warning.Gravatar aspiwack2013-11-02
* Cleanup of comments.Gravatar aspiwack2013-11-02
* Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.Gravatar aspiwack2013-11-02
* Getting rid of Goal.here, and all the related exceptions and combinators.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Moving side effects into evar_map. There was no reason to keep anotherGravatar ppedrot2013-10-05
* Fixing potential evar leak in Equality.Gravatar ppedrot2013-10-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 16:24:18 +0000