Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge branch 'master' into econstr | 2017-04-07 | |
|\ | |||
| * | Merge PR#508: Optimize pending evars | 2017-04-06 | |
| |\ | |||
* | | | Merge branch 'trunk' into pr379 | 2017-04-04 | |
|\| | | |||
* | | | Using delayed universe instances in EConstr. | 2017-04-01 | |
* | | | Fix call to broken unsafe_type_of in apply tactic. | 2017-03-29 | |
* | | | Merge branch 'trunk' into pr379 | 2017-03-24 | |
|\ \ \ | |||
| | * | | [nit] Fix a couple incorrect uses of msg_error. | 2017-03-24 | |
| |/ / | |||
| | * | Fast path for implicit tactic solving. | 2017-03-23 | |
| |/ | |||
| * | [pp] [ide] Minor cleanups in pp code. | 2017-03-21 | |
| * | Remove a dead exception catching code. | 2017-03-13 | |
| * | [stm] Break stm/toplevel dependency loop. | 2017-02-15 | |
* | | 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 | |
* | | Moving printing code from Evd to Termops. | 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 various compatibility layers of tactics. | 2017-02-14 | |
* | | Funind API using EConstr. | 2017-02-14 | |
* | | Ltac now uses evar-based constrs. | 2017-02-14 | |
* | | Removing compatibility layers in Retyping | 2017-02-14 | |
* | | Quote API using EConstr. | 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 | |
* | | Rewrite API using EConstr. | 2017-02-14 | |
* | | Eqdecide API using EConstr. | 2017-02-14 | |
* | | Hints API using EConstr. | 2017-02-14 | |
* | | Tactics 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 | |
* | | 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 | |
* | | Coercion API using EConstr. | 2017-02-14 | |
* | | Tacred API using EConstr. | 2017-02-14 | |
* | | Constr_matching API using EConstr. | 2017-02-14 | |
* | | Typing API using EConstr. | 2017-02-14 | |
* | | Evarconv API using EConstr. | 2017-02-14 | |
* | | Retyping API using EConstr. | 2017-02-14 | |
* | | Nativenorm API using EConstr. | 2017-02-14 | |
* | | Vnorm API using EConstr. | 2017-02-14 | |
* | | Reductionops API using EConstr. | 2017-02-14 | |
* | | Termops API using EConstr. | 2017-02-14 |