aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrintern.ml
Commit message (Expand)AuthorAge
* 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
* | minor: in constrintern.ml:sort_fields, clarify sfGravatar Gabriel Scherer2016-06-27
* | minor: in constrintern.ml:sort_fields, clarify build_pattGravatar Gabriel Scherer2016-06-27
* | whitespace: untabity constrinternl.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
* | minor clarifications in constrintern.ml:sort_fieldsGravatar Gabriel Scherer2016-06-27
* | Adding ability to put any pattern in binders, prefixed by a quote.Gravatar Daniel de Rauglaudre2016-06-27
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-06-16
* | A slight phase of documentation and uniformization of names ofGravatar Hugo Herbelin2016-06-02
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-04
|\|
| * Fix bug #3825: Universe annotations on notations should pass through or be re...Gravatar Pierre-Marie Pédrot2016-05-03
* | Revert "Not taking arguments given by name or position into account when"Gravatar Hugo Herbelin2016-04-27
* | Revert "Warn about possible shadowing of a name occurring in a "in" clause."Gravatar Hugo Herbelin2016-04-27
* | Warn about possible shadowing of a name occurring in a "in" clause.Gravatar Hugo Herbelin2016-04-27
* | Not taking arguments given by name or position into account whenGravatar Hugo Herbelin2016-04-27
* | Fixing a "This clause is redundant" error when interpreting the "in"Gravatar Hugo Herbelin2016-04-27
* | Reformatting + removal of some useless data + some cut-eliminationGravatar Hugo Herbelin2016-04-27
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-25 05:36:55 +0000