aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\
* \ Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| | * Replacing "cast surgery" in LetIn by a proper field (see PR #404).Gravatar Hugo Herbelin2017-03-24
| | * Using the same type of binders for interning and externing.Gravatar Hugo Herbelin2017-03-24
| | * Unifying standard "constr_level" names for constructors of local_binder_expr.Gravatar Hugo Herbelin2017-03-24
| | * Type extended_glob_local_binder now contains only glob_constr.Gravatar Hugo Herbelin2017-03-24
| | * Standardized the order of constructors for binders: Assum then Def.Gravatar Hugo Herbelin2017-03-24
| | * Cleaning phase around local binder at glob level:Gravatar Hugo Herbelin2017-03-24
| | * "Standardizing" the name LocalPatten into LocalRawPattern.Gravatar Hugo Herbelin2017-03-24
| |/
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-22
| |\
* | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| |
* | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| | * Fixing an anomaly with 'pat after cofix.Gravatar Hugo Herbelin2017-02-02
| * | Adding a new evar source to remember the name of evars which wereGravatar Hugo Herbelin2017-01-22
|/ /
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\|
| * Fix #5048 - Casts in pattern raise an anomaly in Constrintern.Gravatar Maxime Dénès2016-10-04
| * Quick fix to #4595 (making notations containing "ltac:" unused for printing).Gravatar Hugo Herbelin2016-10-04
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\|
| * Fix bug #5087: Improve the error message on record with duplicated fields.Gravatar Pierre-Marie Pédrot2016-10-02
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\|
| * typosGravatar Enrico Tassi2016-09-22
* | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | Merge remote-tracking branch 'github/pr/283' into trunkGravatar Maxime Dénès2016-09-22
|\ \
* | | Fix an error-prone error API.Gravatar Pierre-Marie Pédrot2016-09-21
| * | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
|/ /
* | Generalizing the notion of constr substitution to generic arguments.Gravatar Pierre-Marie Pédrot2016-09-15
* | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ | |/ |/|
* | Fix anomaly on user-inputted projection name (bug #5029).Gravatar Guillaume Melquiond2016-08-19
| * Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
| * Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
| * Unify location handling of error functions.Gravatar Emilio Jesus Gallego Arias2016-08-19
|/
* Removing dead unsafe debugging code in Constrintern.Gravatar Pierre-Marie Pédrot2016-08-16
* Removing a source of clash with multiple recursive patterns in notations.Gravatar Hugo Herbelin2016-07-19
* Fixing #4932 (anomaly when using binders as terms in recursive notations).Gravatar Hugo Herbelin2016-07-17
* Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-07-16
* Merge remote-tracking branch 'github/bug4653' into v8.6Gravatar Matthieu Sozeau2016-07-07
|\
| * Do not use implicit type info for (x := t) bindingsGravatar Matthieu Sozeau2016-07-07
* | Program: fix #4873: transparency option not usedGravatar Matthieu Sozeau2016-07-07
| * Univs: fix internalization of (x := T) and castsGravatar Matthieu Sozeau2016-07-06
|/
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
|\
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
| * Univs: allowing notations to take univ instancesGravatar Matthieu Sozeau2016-06-27
| * Forbidding silently dropped universes instances inGravatar Matthieu Sozeau2016-06-27
* | minor: comment on the meaning of the 'boolean' variableGravatar Gabriel Scherer2016-06-27
* | minor: documentation comment for constrintern.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
* | minor: interp/constrintern.ml, clarify field completionGravatar Gabriel Scherer2016-06-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 05:05:03 +0000