aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* Merge branch 'master' into ltac2-hooksGravatar Pierre-Marie Pédrot2017-05-19
|\
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-05-17
| |\
| * \ Merge PR#630: [interp] [ast] Make raw_cases_pattern_expr private + small cleanupGravatar Maxime Dénès2017-05-17
| |\ \
| | | * Fixing bug #5222 (anomaly with "`pat" in the presence of scope delimiters).Gravatar Hugo Herbelin2017-05-16
| | | * Fixing a bug with nested "as" clauses in "match".Gravatar Hugo Herbelin2017-05-16
| | * | [interp] Rework check for casts inside patterns.Gravatar Emilio Jesus Gallego Arias2017-05-15
| | * | [interp] [ast] Make raw_cases_pattern_expr private.Gravatar Emilio Jesus Gallego Arias2017-05-15
| * | | Typo in comments of constrintern.Gravatar Hugo Herbelin2017-05-15
| |/ /
* / / Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
|/ /
* | Warning 29: non escaped end of line may be non portableGravatar Gaetan Gilbert2017-04-27
* | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | 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
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 07:57:28 +0000