aboutsummaryrefslogtreecommitdiff
path: root/intf
AgeCommit message (Expand)Author
2018-04-23[api] Relocate `intf` modules according to dependency-order.Emilio Jesus Gallego Arias
2018-04-23Merge PR #7152: [api] Remove dependency of library on Vernacexpr.Pierre-Marie Pédrot
2018-04-06Merge PR #6960: [api] Move some types to their proper module.Pierre-Marie Pédrot
2018-04-06[api] Remove dependency of library on Vernacexpr.Emilio Jesus Gallego Arias
2018-04-05Merge PR #7016: Make parsing independent of the cumulativity flag.Enrico Tassi
2018-04-05Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Enrico Tassi
2018-04-04Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Enrico Tassi
2018-04-02[api] Move some types to their proper module.Emilio Jesus Gallego Arias
2018-04-01Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Pierre-Marie Pédrot
2018-04-01[stm] More cleanup of "classification is not an interpreter"Emilio Jesus Gallego Arias
2018-04-01[stm] Move VernacBacktrack to the toplevel.Emilio Jesus Gallego Arias
2018-03-30Remove deprecated commands Arguments Scope and Implicit ArgumentsJasper Hugunin
2018-03-28Patterns: Accepting patterns in PFix and PCofix and not only constr.Hugo Herbelin
2018-03-27Merge PR #7062: Slightly refining some error messages about unresolvable evars.Pierre-Marie Pédrot
2018-03-24Slightly refining some error messages about unresolvable evars.Hugo Herbelin
2018-03-22bool option -> (VernacCumulative | VernacNonCumulative) optionGaëtan Gilbert
2018-03-21Make parsing independent of the cumulativity flag.Gaëtan Gilbert
2018-03-11[vernac] Move `Quit` and `Drop` to the toplevel layer.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-09Implement the Export Set/Unset feature.Pierre-Marie Pédrot
2018-03-08Make most of TACTIC EXTEND macros runtime calls.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-05Change non-documentation comment from ocamldoc stylemrmr1993
2018-03-05Fix formatting of some ocamldoc comments to reduce warningsmrmr1993
2018-03-05Allow universe declarations for [with Definition].Gaëtan Gilbert
2018-02-27Update headers following #6543.Théo Zimmermann
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-20Adding general support for irrefutable disjunctive patterns.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-20Allows recursive patterns for binders to be associative on the left.Hugo Herbelin
2018-02-20A bit of miscellaneous code documentation around notations.Hugo Herbelin
2018-02-20Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Hugo Herbelin
2018-02-20Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Hugo Herbelin
2018-02-20Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Hugo Herbelin
2018-02-20More precise explanation when a notation is not reversible for printing.Hugo Herbelin
2018-02-12Merge PR #6651: Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-02-01[vernac] Mutual theorems (VernacStartTheoremProof) always have namesVincent Laporte
2018-02-01[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionVincent Laporte
2018-01-30Use r.(p) syntax to print primitive projections.Maxime Dénès
2018-01-16Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprMaxime Dénès
2018-01-08[vernac] vernac_expr no longer recursiveVincent Laporte
2018-01-05Brackets support single numbered goal selectors.Théo Zimmermann
2017-12-29[vernac] Define types in orderVincent Laporte
2017-12-29Merge PR #6433: [flags] Move global time flag into an attribute.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:53:58 +0000