aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Expand)AuthorAge
...
| | | * 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
* | | | Merge PR#393: Replace Typeops with Fast_typeopsGravatar Maxime Dénès2017-02-08
|\ \ \ \
* \ \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\ \ \ \ \ | | |_|/ / | |/| | |
* | | | | Adding a new evar source to remember the name of evars which wereGravatar Hugo Herbelin2017-01-22
| * | | | Fixing bugs in typing "match" (regressions #5322 and #5324 + bugs with let-ins).Gravatar Hugo Herbelin2017-01-22
| | | * | Improve unification debug trace.Gravatar Théo Zimmermann2016-12-13
| |_|/ / |/| | |
| | * | Replace Typeops by Fast_typeopsGravatar Gaetan Gilbert2016-12-12
| |/ / |/| |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
|\| |
| * | Merge remote-tracking branch 'github/pr/366' into v8.6Gravatar Maxime Dénès2016-12-04
| |\ \
| | * | Document changesGravatar Matthieu Sozeau2016-12-02
| * | | Univs: fix bug #5180Gravatar Matthieu Sozeau2016-11-30
| | * | Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
| |/ /
* | / Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|\| | | |/ |/|
| * Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
| * \ Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\ \
| | * | More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07