aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Expand)AuthorAge
...
* | | Clenv 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
* | | Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Evarconv 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
* | | 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
| | * Improve unification debug trace.Gravatar Théo Zimmermann2016-12-13
| |/
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/|
| * Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
| |\
* | | Stronger static invariant in equality upto universes.Gravatar Pierre-Marie Pédrot2016-10-31
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\| |
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-26
| |\ \
| | | * Renamings to avoid confusion deprecating old namesGravatar Matthieu Sozeau2016-10-22
| | |/ | |/|
| | * Fix a bug in error printing of unif constraintsGravatar Matthieu Sozeau2016-10-22
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-18
|\| |
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-18
| |\|
| * | Quick fix to unification regression #4955.Gravatar Hugo Herbelin2016-10-17
| | * Fixing a missing constraint in consider_remaining_unif_constraints.Gravatar Hugo Herbelin2016-10-17
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\| |
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-08
| |\|
| | * evarconv.ml: Fix bug #4529, primproj unfoldingGravatar Matthieu Sozeau2016-10-06
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\| |
| * | no-refold patchGravatar Paul Steckler2016-09-09
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* | | | CLEANUP: using |> operator more consistentlyGravatar Matej Kosik2016-08-30
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | | CLEANUP: removing calls of the "Context.Named.Declaration.to_tuple" functionGravatar Matej Kosik2016-08-24
| |/ / |/| |
| * | Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/ /
* | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Univs: add source locations of levelsGravatar Matthieu Sozeau2016-06-29
* | Refine 9cc95f5, unification of Let-In's, bug #3929Gravatar Matthieu Sozeau2016-06-16
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\|
| * evar_conv: Refine occur_rigidlyGravatar Matthieu Sozeau2016-06-13
| * Minor simplification in evarconv.Gravatar Hugo Herbelin2016-06-12
| * Protecting eta-expansion in evarconv.ml against ill-typed problems.Gravatar Hugo Herbelin2016-06-12
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-09
|\|
| * Fixing #4644 (regression of unification on evar-evar problems with a match).Gravatar Hugo Herbelin2016-06-09
| * Minor simplification in evarconv.ml.Gravatar Hugo Herbelin2016-06-09
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Splitting Evarutil in two distinct files.Gravatar Pierre-Marie Pédrot2016-03-20
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-20
|\|
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-03-18
|\ \
| | * Fix incorrect behavior of CS resolutionGravatar Matthieu Sozeau2016-03-16
| |/