aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarsolve.ml
Commit message (Expand)AuthorAge
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Merge PR #6064: [api] Deprecate all legacy uses of Name.Id in core.Gravatar Maxime Dénès2017-11-06
|\
* | Refining PR#924 (insensitivity of projection heuristics to alphabet).Gravatar Hugo Herbelin2017-11-05
| * [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
|/
* Merge PR #924: Fixing part of #5669: unification heuristics sensitive to alph...Gravatar Maxime Dénès2017-11-03
|\
* | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
* | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| * Fixing one part of #5669 (unification heuristics sensitive to choice of names).Gravatar Hugo Herbelin2017-07-27
* | Removing template polymorphism for definitions.Gravatar Pierre-Marie Pédrot2017-07-26
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-07-04
|\
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| * Merge PR#713: Bump year in headers.Gravatar Maxime Dénès2017-06-15
| |\
* | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| * | Univs: fix bug #5365, generation of u+k <= v constraintsGravatar Matthieu Sozeau2017-06-05
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
| | * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| |/
* | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | Upgrading some local function as a general-purpose combinator Option.List.map.Gravatar Hugo Herbelin2017-05-05
* | Fix 4.04 warningsGravatar Gaetan Gilbert2017-04-27
* | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\ \
* | | Dedicated datatype for aliases in Evarsolve.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Chasing a few unsafe constr coercions.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Evar-normalizing functions now act on EConstrs.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
* | | 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
* | | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Tactics 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
* | | Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Evarsolve API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Retyping 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 branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
| |\|
| | * Document changesGravatar Matthieu Sozeau2016-12-02
| | * Fix UGraph.check_eq!Gravatar Matthieu Sozeau2016-11-30
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| | | |/
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\ \
| | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| |/
| * Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-10-21
| |\
| | * Revert "unification.ml: fix for bug #4763, unif regression"Gravatar Maxime Dénès2016-10-21
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\| |
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-18
| |\|
| | * Fixing to #3209 (Not_found due to an occur-check cycle).Gravatar Hugo Herbelin2016-10-17