aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/evarconv.ml
Commit message (Expand)AuthorAge
* Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
|\
* \ 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.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.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-08
|\|
| * evarconv.ml: Fix bug #4529, primproj unfoldingGravatar Matthieu Sozeau2016-10-06
* | no-refold patchGravatar Paul Steckler2016-09-09
* | 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
| |/
| * Primitive projections: protect kernel from erroneous definitions.Gravatar Matthieu Sozeau2016-03-10
* | Slightly contracting code of evarconv.ml.Gravatar Hugo Herbelin2016-02-28
* | merging conflicts with the original "trunk__CLEANUP__Context__2" branchGravatar Matej Kosik2016-02-15
|\ \
* | | Monotonizing the Evarutil module.Gravatar Pierre-Marie Pédrot2016-02-15
| * | CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
|/ /
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | CLEANUP: in the Reductionops moduleGravatar Matej Kosik2015-12-17
* | Making Evarutil.new_evar monotonous.Gravatar Pierre-Marie Pédrot2015-10-18
* | Hardening the API of evarmaps.Gravatar Pierre-Marie Pédrot2015-09-26
| * Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully more regular names and formGravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully more regular form andGravatar Hugo Herbelin2015-08-02
| * Cosmetic changes in evarconv.ml: hopefully using better self-documenting names.Gravatar Hugo Herbelin2015-08-02
| * Evarconv.ml: small cut-elimination, saving useless zip.Gravatar Hugo Herbelin2015-08-02
| * Cosmetic in evarconv.ml: naming a local function for better readibility.Gravatar Hugo Herbelin2015-08-02
|/
* Continuing 93579407, spotting other potential sources of anomalyGravatar Hugo Herbelin2015-07-16
* Fixing anomaly #3743 while printing an error message involving evar constraints.Gravatar Hugo Herbelin2015-07-16
* Some dead code.Gravatar Hugo Herbelin2015-04-21
* Fix bug #3532, providing universe inconsistency information when aGravatar Matthieu Sozeau2015-03-04
* Making unification of LetIn's expressions more consistent (see #3920).Gravatar Hugo Herbelin2015-01-19
* Update headers.Gravatar Maxime Dénès2015-01-12
* Reverting the tentative try to restore the use of second-orderGravatar Hugo Herbelin2015-01-07
* Propagating the relaxing of filtering started in 48509b6, fixed inGravatar Hugo Herbelin2015-01-06