aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
Commit message (Expand)AuthorAge
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-02-01
|\
| * Fixing #5326 (anomaly on some unsupported case of 'pat).Gravatar Hugo Herbelin2017-01-26
* | 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-29
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-29
| |\
| | * Fixing #5161 (case of a notation with unability to detect a recursive binder).Gravatar Hugo Herbelin2016-10-27
* | | CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".Gravatar Matej Kosik2016-10-19
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\| |
| | * Merge PR #310 into v8.5Gravatar Pierre-Marie Pédrot2016-10-17
| | |\
| * | \ Merge PR #310 into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
| |\ \ \ | | | |/ | | |/|
| * | | Merge PR #289 into v8.6.Gravatar Pierre-Marie Pédrot2016-10-12
| |\ \ \
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| | | |
| | | | * Fixing a collision about the meta-variable ".." in recursive notations.Gravatar Hugo Herbelin2016-10-12
| * | | | Shorter message for "Test Asymmetric Patterns".Gravatar Hugo Herbelin2016-10-12
| * | | | Fixing a few confusions on the name of the beautify flag.Gravatar Hugo Herbelin2016-10-12
* | | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\| | | |
| | | * | Revert "Make the pretty printer resilient to incomplete nametab (progress on ...Gravatar Théo Zimmermann2016-10-06
| | | |/
| * | | Disable compatibility notations warnings.Gravatar Maxime Dénès2016-10-06
| * | | Remove the Set Verbose Compat option and turn the warning on by default.Gravatar Maxime Dénès2016-10-06
* | | | 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
| * | | Warning about similar notations now up to alpha-conversion.Gravatar Hugo Herbelin2016-09-28
| | * | [notation] Allow to retrieve defined notations.Gravatar Emilio Jesus Gallego Arias2016-09-25
| |/ /
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| |
| * | coqc -o now places .glob file near .vo fileGravatar Enrico Tassi2016-09-22
| * | 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
* | | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
| * | | Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Gravatar Maxime Dénès2016-09-20
|/ / /
| * | Addressing OCaml compilation warnings.Gravatar Hugo Herbelin2016-09-16
* | | Make the Coq codebase independent from Ltac-related code.Gravatar Pierre-Marie Pédrot2016-09-16
|\ \ \
| * | | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
| * | | Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Gravatar Pierre-Marie Pédrot2016-09-15
| * | | Generalizing the notion of constr substitution to generic arguments.Gravatar Pierre-Marie Pédrot2016-09-15
* | | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-14
|\ \ \ \ | |/ / / |/| / / | |/ /
| * | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-09-14
| |\|
| | * Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Gravatar Hugo Herbelin2016-09-12
* | | Merge PR #244.Gravatar Pierre-Marie Pédrot2016-09-08
|\ \ \
* \ \ \ Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-02
|\ \ \ \ | | |/ / | |/| |
| * | | Notation_ops.subst_glob_vars: substituting also in evar kind forGravatar Hugo Herbelin2016-09-01
| * | | Fix bug #4764: Syntactic notation externalization breaks.Gravatar Pierre-Marie Pédrot2016-08-28
* | | | Merge remote-tracking branch 'v8.6' into trunkGravatar Matej Kosik2016-08-25
|\| | |
* | | | CLEANUP: minor readability improvementsGravatar Matej Kosik2016-08-24
* | | | Changing the definition of the "Lib.variable.info" type to enable us to do mo...Gravatar Matej Kosik2016-08-24
| * | | Fix bug #4904: [Import] does not load intermediately unqualified names of ali...Gravatar Pierre-Marie Pédrot2016-08-23
|/ / /