Commit message (Expand) | Author | Age | |
---|---|---|---|
* | 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 | |
* | 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 | |
* | Refine 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 | |
* | Cases API using EConstr. | 2017-02-14 | |
* | Typeclasses API using EConstr. | 2017-02-14 | |
* | Tacred API using EConstr. | 2017-02-14 | |
* | Evarconv API using EConstr. | 2017-02-14 | |
* | Evarsolve API using EConstr. | 2017-02-14 | |
* | Reductionops API using EConstr. | 2017-02-14 | |
* | Termops API using EConstr. | 2017-02-14 | |
* | Introducing a new EConstr.t type to perform the nf_evar operation on demand. | 2016-11-08 | |
* | Moving unused code out of the kernel into Termops. | 2016-10-31 | |
* | Stronger static invariant in equality upto universes. | 2016-10-31 | |
* | Code factorization in Universes. | 2016-10-31 | |
* | Moving Universes to the engine/ folder. | 2016-10-30 | |
* | Reordering Termops w.r.t. Evd and Namegen in engine folder. | 2016-10-30 | |
* | Merge branch 'v8.6' | 2016-10-29 | |
|\ | |||
| * | Merge remote-tracking branch 'github/pr/321' into v8.6 | 2016-10-28 | |
| |\ | |||
| * | | Merge branch 'v8.5' into v8.6 | 2016-10-26 | |
* | | | COMMENT: Namegen.next_ident_away | 2016-10-26 | |
* | | | COMMENT: Proofview.entry | 2016-10-26 | |
* | | | Merge branch 'v8.6' | 2016-10-24 | |
|\| | | |||
| * | | Oops, my bad, didn't expect a merge issue! | 2016-10-21 | |
| * | | Merge remote-tracking branch 'gforge/v8.5' into v8.6 | 2016-10-21 | |
| | * | sections/hints: prevent Not_found in get_type_of | 2016-10-21 | |
| |/ | |||
* | | CLEANUP: Namegen.to_avoid | 2016-10-20 | |
* | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript". | 2016-10-19 | |
* | | Merge branch 'v8.6' | 2016-10-17 | |
|\| | |||
| * | Fix bug #5145: Anomaly: index to an anonymous variable. | 2016-10-15 | |
* | | Merge branch 'v8.6' | 2016-10-12 | |
|\| | |||
| * | Merge branch 'v8.5' into v8.6 | 2016-10-12 | |
| * | Merge branch 'v8.5' into v8.6 | 2016-10-12 | |
* | | Merge branch 'v8.6' | 2016-10-05 | |
|\| | |||
| * | Merge remote-tracking branch 'github/pr/263' into v8.6 | 2016-10-03 | |
| |\ | |||
* | | | Merge branch 'v8.6' | 2016-09-23 | |
|\| | | |||
| * | | Adding variants enter_one and refine_one which assume that exactly one | 2016-09-16 | |
| | * | Tracking careless uses of slow name lookup. | 2016-09-09 | |
| |/ | |||
* | | Merge PR #244. | 2016-09-08 | |
|\ \ | |||
* \ \ | Merge branch 'v8.6' | 2016-09-07 | |
|\ \ \ | | |/ | |/| | |||
| * | | Fast path in push_rel_context_to_named_context. | 2016-09-05 |