aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation_ops.ml
Commit message (Expand)AuthorAge
...
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\| |
* | | Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* | | Merge PR#561: Improving the Name APIGravatar Maxime Dénès2017-06-01
|\ \ \
| | | * Bump year in headers.Gravatar Maxime Dénès2017-06-01
| | |/
| * | Creating a module Nameops.Name extending module Names.Name.Gravatar Hugo Herbelin2017-05-31
* | | Fixing #5523 (missing support for complex constructions in recursive notations).Gravatar Hugo Herbelin2017-05-31
* | | Fixing a too lax constraint for finding recursive binder part of a notation.Gravatar Hugo Herbelin2017-05-31
|/ /
* | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
* | | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | | [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
|/ /
| * Better support for printing constructors with let-ins.Gravatar Hugo Herbelin2017-04-07
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-04-04
|\ \
| * | 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
* | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
|/ /
* | 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
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-05
|\| |
| * | 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
|\| |
| * | Warning about similar notations now up to alpha-conversion.Gravatar Hugo Herbelin2016-09-28
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-09-23
|\| |
* | | Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Gravatar Maxime Dénès2016-09-22
* | | 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
* | | 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
|\ \ \ | |/ / |/| |
* | | 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
| * | 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
|/ /
* | Make it a bit more obvious when variables are of type unit.Gravatar Guillaume Melquiond2016-08-10
* | Some extra fixes in printing patterns in binders.Gravatar Hugo Herbelin2016-07-19
* | Taking into account binding patterns when agglutinating sequences of binders.Gravatar Hugo Herbelin2016-07-19
* | Notations with multiple recursive binders: fixing use of alpha-conversion.Gravatar Hugo Herbelin2016-07-19
* | Notations: fixing multiple binders used as terms in reverse order.Gravatar Hugo Herbelin2016-07-19
* | Removing a source of clash with multiple recursive patterns in notations.Gravatar Hugo Herbelin2016-07-19
* | A new step on using alpha-conversion in printing notations.Gravatar Hugo Herbelin2016-07-18
* | Partial fix to #4592 (notation requiring alpha-conversion for printing).Gravatar Hugo Herbelin2016-07-17
* | Fixing a bug in recognizing a recursive pattern of notationsGravatar Hugo Herbelin2016-07-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 12:12:59 +0000