aboutsummaryrefslogtreecommitdiff
path: root/interp/notation_ops.ml
AgeCommit message (Expand)Author
2017-09-12Fixing bugs of a67bd7f9 and c6d9d4fb in recognizing a 'pat binding.Hugo Herbelin
2017-09-12Fixing a typo in printing notations with recursive binders.Hugo Herbelin
2017-09-12Fixing a bug of recursive notations introduced in dfdaf4de.Hugo Herbelin
2017-09-04Making detyping potentially lazy.Pierre-Marie Pédrot
2017-08-29Adapting code to renaming Array.fold_map -> Array.fold_left_map.Hugo Herbelin
2017-08-29Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_mapHugo Herbelin
2017-07-04Merge branch 'v8.6'Pierre-Marie Pédrot
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-15Merge PR#713: Bump year in headers.Maxime Dénès
2017-06-09Fix Bug #5568, no dup notation warnings on repeated module importsPaul Steckler
2017-06-08Merge branch 'v8.6'Pierre-Marie Pédrot
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-06-01Merge PR#561: Improving the Name APIMaxime Dénès
2017-06-01Bump year in headers.Maxime Dénès
2017-05-31Creating a module Nameops.Name extending module Names.Name.Hugo Herbelin
2017-05-31Fixing #5523 (missing support for complex constructions in recursive notations).Hugo Herbelin
2017-05-31Fixing a too lax constraint for finding recursive binder part of a notation.Hugo Herbelin
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-04-27Remove some unused values and typesGaetan Gilbert
2017-04-25[location] [ast] Port module AST to CAstEmilio Jesus Gallego Arias
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-25[location] Remove Loc.ghost.Emilio Jesus Gallego Arias
2017-04-24[location] Switch glob_constr to Loc.locatedEmilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.predicate_pattern to located.Emilio Jesus Gallego Arias
2017-04-24[location] Move Glob_term.cases_pattern to located.Emilio Jesus Gallego Arias
2017-04-07Better support for printing constructors with let-ins.Hugo Herbelin
2017-04-04Merge branch 'trunk' into pr379Maxime Dénès
2017-03-24Replacing "cast surgery" in LetIn by a proper field (see PR #404).Hugo Herbelin
2017-03-24Using the same type of binders for interning and externing.Hugo Herbelin
2017-02-14Namegen primitives now apply on evar constrs.Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-29Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-27Fixing #5161 (case of a notation with unability to detect a recursive binder).Hugo Herbelin
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-04Quick fix to #4595 (making notations containing "ltac:" unused for printing).Hugo Herbelin
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-28Warning about similar notations now up to alpha-conversion.Hugo Herbelin
2016-09-23Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-22Revert "Merge remote-tracking branch 'github/pr/283' into trunk"Maxime Dénès
2016-09-20Rename Decl_kinds.binding_kind into Decls_kind.implicit_status.Maxime Dénès
2016-09-16Addressing OCaml compilation warnings.Hugo Herbelin
2016-09-14Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-14Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-09-12Fixing a recursive notation bug raised on coq-club on Sep 12, 2016.Hugo Herbelin
2016-09-08Merge PR #244.Pierre-Marie Pédrot
2016-09-01Notation_ops.subst_glob_vars: substituting also in evar kind forHugo Herbelin
2016-08-28Fix bug #4764: Syntactic notation externalization breaks.Pierre-Marie Pédrot
2016-08-19Make the user_err header an optional parameter.Emilio Jesus Gallego Arias
2016-08-19Remove errorlabstrm in favor of user_errEmilio Jesus Gallego Arias
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 11:48:34 +0000