Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| * | | | Merge branch 'v8.6' | 2017-03-22 | ||
| |\| | | ||||
| * | | | Attempt to improve error message when "apply in" fail. | 2017-03-15 | ||
| | | * | Show unused-intro-pattern warning. | 2017-03-14 | ||
| | * | | Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correc... | 2017-03-10 | ||
| | |\ \ | | | |/ | | |/| | ||||
* | | | | Merge branch 'master'. | 2017-02-14 | ||
|\| | | | ||||
* | | | | Quick hack to fix interpretation of patterns in Ltac. | 2017-02-14 | ||
* | | | | Removing a subtle nf_enter in Class_tactics. | 2017-02-14 | ||
* | | | | Removing most nf_enter in tactics. | 2017-02-14 | ||
* | | | | Namegen primitives now apply on evar constrs. | 2017-02-14 | ||
* | | | | Chasing a few unsafe constr coercions. | 2017-02-14 | ||
* | | | | Do not ask for a normalized goal to get hypotheses and conclusions. | 2017-02-14 | ||
* | | | | Definining EConstr-based contexts. | 2017-02-14 | ||
* | | | | Introducing contexts parameterized by the inner term type. | 2017-02-14 | ||
* | | | | Evar-normalizing functions now act on EConstrs. | 2017-02-14 | ||
* | | | | Removing compatibility layers from Tacticals | 2017-02-14 | ||
* | | | | Cleaning up interfaces. | 2017-02-14 | ||
* | | | | Removing various compatibility layers of tactics. | 2017-02-14 | ||
* | | | | Removing compatibility layers related to printing. | 2017-02-14 | ||
* | | | | Ltac now uses evar-based constrs. | 2017-02-14 | ||
* | | | | Removing compatibility layers in Retyping | 2017-02-14 | ||
* | | | | Removing some return type compatibility layers in Termops. | 2017-02-14 | ||
* | | | | Reductionops now return EConstrs. | 2017-02-14 | ||
* | | | | Proofview.Goal primitive now return EConstrs. | 2017-02-14 | ||
* | | | | Eliminating parts of the right-hand side compatibility layer | 2017-02-14 | ||
* | | | | Tactic_matching API using EConstr. | 2017-02-14 | ||
* | | | | Eqdecide API using EConstr. | 2017-02-14 | ||
* | | | | Class_tactics API using EConstr. | 2017-02-14 | ||
* | | | | Eauto API using EConstr. | 2017-02-14 | ||
* | | | | Auto API using EConstr. | 2017-02-14 | ||
* | | | | Hints API using EConstr. | 2017-02-14 | ||
* | | | | Leminv API using EConstr. | 2017-02-14 | ||
* | | | | Inv API using EConstr. | 2017-02-14 | ||
* | | | | Contradiction API using EConstr. | 2017-02-14 | ||
* | | | | Equality API using EConstr. | 2017-02-14 | ||
* | | | | Elim API using EConstr. | 2017-02-14 | ||
* | | | | Tactics API using EConstr. | 2017-02-14 | ||
* | | | | Hipattern API using EConstr. | 2017-02-14 | ||
* | | | | Tacticals API using EConstr. | 2017-02-14 | ||
* | | | | Clenv API using EConstr. | 2017-02-14 | ||
* | | | | Tacmach API using EConstr. | 2017-02-14 | ||
* | | | | Refine API using EConstr. | 2017-02-14 | ||
* | | | | Goal API using EConstr. | 2017-02-14 | ||
* | | | | Cleaning up opening of the EConstr module in pretyping folder. | 2017-02-14 | ||
* | | | | Making judgment type generic over the type of inner constrs. | 2017-02-14 | ||
* | | | | Unification API using EConstr. | 2017-02-14 | ||
* | | | | Pretyping API using EConstr. | 2017-02-14 | ||
* | | | | Cases API using EConstr. | 2017-02-14 | ||
* | | | | Typeclasses API using EConstr. | 2017-02-14 | ||
* | | | | Tacred API using EConstr. | 2017-02-14 | ||
* | | | | Constr_matching API using EConstr. | 2017-02-14 |