aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Quick hack to fix interpretation of patterns in Ltac.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing a subtle nf_enter in Class_tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
* | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
* | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Eqdecide API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Eauto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Auto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Leminv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hipattern API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cleaning up opening of the EConstr module in pretyping folder.Gravatar Pierre-Marie Pédrot2017-02-14
* | Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Patternops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 20:59:44 +0000