Commit message (Expand) | Author | Age | |
---|---|---|---|
* | [location] Make location optional in Loc.located | 2017-04-25 | |
* | [location] Remove Loc.ghost. | 2017-04-25 | |
* | Merge branch 'master' into econstr | 2017-04-07 | |
|\ | |||
| * | Merge PR#508: Optimize pending evars | 2017-04-06 | |
| |\ | |||
* | | | Using delayed universe instances in EConstr. | 2017-04-01 | |
* | | | Merge branch 'trunk' into pr379 | 2017-03-24 | |
|\| | | |||
| * | | Merge branch 'v8.6' into trunk | 2017-03-23 | |
| |\ \ | |||
| | | * | Fast path for implicit tactic solving. | 2017-03-23 | |
| | | * | Ensuring static invariants about handling of pending evars in Pretyping. | 2017-03-23 | |
| | |/ | |/| | |||
| * | | Attempt to improve error message when "apply in" fail. | 2017-03-15 | |
| | * | Show unused-intro-pattern warning. | 2017-03-14 | |
* | | | Merge branch 'master'. | 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 | |
* | | | Class_tactics API using EConstr. | 2017-02-14 | |
* | | | Leminv API using EConstr. | 2017-02-14 | |
* | | | Inv API using EConstr. | 2017-02-14 | |
* | | | Tactics API using EConstr. | 2017-02-14 | |
* | | | Hipattern 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 | |
* | | | Cleaning up opening of the EConstr module in pretyping folder. | 2017-02-14 | |
* | | | Unification API using EConstr. | 2017-02-14 | |
* | | | Pretyping API using EConstr. | 2017-02-14 | |
* | | | Typeclasses API using EConstr. | 2017-02-14 | |
* | | | Tacred API using EConstr. | 2017-02-14 | |
* | | | Typing API using EConstr. | 2017-02-14 | |
* | | | Evarconv API using EConstr. | 2017-02-14 | |
* | | | Evarsolve API using EConstr. | 2017-02-14 | |
* | | | Find_subterm API using EConstr. | 2017-02-14 | |
* | | | Retyping API using EConstr. | 2017-02-14 | |
* | | | Reductionops API using EConstr. | 2017-02-14 | |
* | | | Termops API using EConstr. | 2017-02-14 |