aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
...
* | | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | | [location] More located use.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
* | | | [location] Move Glob_term.predicate_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | [location] Move Glob_term.cases_pattern to located.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | [location] Use Loc.located for constr_expr.Gravatar Emilio Jesus Gallego Arias2017-04-24
* | | | [constrexpr] Make patterns use Loc.located for location informationGravatar Emilio Jesus Gallego Arias2017-04-24
|/ / /
| | * Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
| |/
* | 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
|/
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 23:57:01 +0000