aboutsummaryrefslogtreecommitdiff
path: root/interp
AgeCommit message (Expand)Author
2018-05-10Fixes #7462, part 2 (only-printing not make believe parsing rule is declared).Hugo Herbelin
2018-05-10Fixes part 1 of #7462 (only-printing not to override existing interp rule).Hugo Herbelin
2018-05-08[api] Move universe syntax to `Glob_term`Emilio Jesus Gallego Arias
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-04-13Merge PR #7231: Fixing the 3 cases of a "Stream.Error" ended with two periods.Enrico Tassi
2018-04-12Merge PR #6972: [api] Deprecate a couple of aliases that we missed.Maxime Dénès
2018-04-12Fixing the 3 cases of a "Stream.Error" ended with two periods.Hugo Herbelin
2018-04-09Merge PR #7116: Fixes #7110: missing test on the absence of a "as" while look...Emilio Jesus Gallego Arias
2018-04-06Merge PR #7129: Fix #7124: Warning "Ignoring implicit status" does not provid...Hugo Herbelin
2018-04-05Refactor impargs code.Jasper Hugunin
2018-04-05Fix #7124: Warning "Ignoring implicit status" does not provide line numberMaxime Dénès
2018-04-04Merge PR #7127: Fix #6257: anomaly with Printing Projections and Context.Hugo Herbelin
2018-03-30Fix #6257: anomaly with Printing Projections and Context.Gaëtan Gilbert
2018-03-29Fixes #7110 ("as" untested while looking for notation for nested patterns).Hugo Herbelin
2018-03-28Patterns: Accepting patterns in PFix and PCofix and not only constr.Hugo Herbelin
2018-03-28[api] Deprecate a couple of aliases that we missed.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-09[located] More work towards using CAst.tEmilio Jesus Gallego Arias
2018-03-09Revert "Merge PR #873: New strategy based on open scopes for deciding which n...Maxime Dénès
2018-03-07Merge PR #6905: Fix make ml-docMaxime Dénès
2018-03-07Merge PR #6790: Allow universe declarations for [with Definition].Maxime Dénès
2018-03-05Fix formatting of some ocamldoc comments to reduce warningsmrmr1993
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Merge PR #6791: Removing compatibility support for versions older than 8.5.Maxime Dénès
2018-03-02Turn warning for deprecated notations on.Théo Zimmermann
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-28Merge PR #6823: Fixes #6821 (bug in protecting notation printing from infinit...Maxime Dénès
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-23Fixes #6821 (bug in protecting notation printing from infinite eta-expansion).Hugo Herbelin
2018-02-22[ast] Improve precision of Ast location recognition in serialization.Emilio Jesus Gallego Arias
2018-02-20Change default for notations with variables bound to both terms and binders.Hugo Herbelin
2018-02-20Notations: Adding modifiers to tell which kind of binder a constr can parse.Hugo Herbelin
2018-02-20Notations: A step in cleaning constr_entry_key.Hugo Herbelin
2018-02-20More flexibility in locating or referring to a notation.Hugo Herbelin
2018-02-20When printing a notation with "match", more flexibility in matching equations.Hugo Herbelin
2018-02-20Adding general support for irrefutable disjunctive patterns.Hugo Herbelin
2018-02-20Using an "as" clause when needed for printing irrefutable patterns.Hugo Herbelin
2018-02-20Refining the strategy for glueing let-ins to a sequence of binders.Hugo Herbelin
2018-02-20A (significant) simplification in printing notations with recursive binders.Hugo Herbelin
2018-02-20Respecting the ident/pattern distinction in notation modifiers.Hugo Herbelin
2018-02-20Adding support for parsing subterms of a notation as "pattern".Hugo Herbelin
2018-02-20Adding patterns in the category of binders for notations.Hugo Herbelin
2018-02-20Preliminary work before adding general support for patterns in notations II.Hugo Herbelin
2018-02-20Preliminary work before adding general support for patterns in notations I.Hugo Herbelin
2018-02-20Preliminary work before extending support for binders in notationsHugo Herbelin
2018-02-20Preliminary steps before adding general support for patterns in notations.Hugo Herbelin
2018-02-20In printing notations with "match", reasoning up to the order of clauses.Hugo Herbelin
2018-02-20Preliminary work before extending support for binders in notationsHugo Herbelin