aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
* 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
* Cc API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops 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
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Class_tactics 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
* Tactics 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
* 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
* Coercion API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Classops 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
* Recordops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evardefine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Find_subterm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Cbv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Nativenorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Vnorm API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Stronger static invariant in equality upto universes.Gravatar Pierre-Marie Pédrot2016-10-31
* Moving Universes to the engine/ folder.Gravatar Pierre-Marie Pédrot2016-10-30
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * Fixing error localisation bug introduced in fixing #5142 (21e1d501e17c).Gravatar Hugo Herbelin2016-10-29
| * Merge remote-tracking branch 'github/pr/337' into v8.6Gravatar Maxime Dénès2016-10-28
| |\
| | * Complete overhaul of the Arguments vernacular.Gravatar Maxime Dénès2016-10-27
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\ \
| | * \ Merge remote-tracking branch 'github/pr/333' into v8.5Gravatar Maxime Dénès2016-10-25
| | |\ \
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\| | | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-17 00:32:52 +0000