aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf
Commit message (Expand)AuthorAge
* Merge PR #6960: [api] Move some types to their proper module.Gravatar Pierre-Marie Pédrot2018-04-06
|\
* \ Merge PR #7016: Make parsing independent of the cumulativity flag.Gravatar Enrico Tassi2018-04-05
|\ \
* \ \ Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"Gravatar Enrico Tassi2018-04-05
|\ \ \
* \ \ \ Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.Gravatar Enrico Tassi2018-04-04
|\ \ \ \
| | | | * [api] Move some types to their proper module.Gravatar Emilio Jesus Gallego Arias2018-04-02
| |_|_|/ |/| | |
* | | | Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)Gravatar Pierre-Marie Pédrot2018-04-01
|\ \ \ \
| | | * | [stm] More cleanup of "classification is not an interpreter"Gravatar Emilio Jesus Gallego Arias2018-04-01
| | |/ /
| | * | [stm] Move VernacBacktrack to the toplevel.Gravatar Emilio Jesus Gallego Arias2018-04-01
* | | | Remove deprecated commands Arguments Scope and Implicit ArgumentsGravatar Jasper Hugunin2018-03-30
| |/ / |/| |
| * | Patterns: Accepting patterns in PFix and PCofix and not only constr.Gravatar Hugo Herbelin2018-03-28
* | | Merge PR #7062: Slightly refining some error messages about unresolvable evars.Gravatar Pierre-Marie Pédrot2018-03-27
|\ \ \
| * | | Slightly refining some error messages about unresolvable evars.Gravatar Hugo Herbelin2018-03-24
| |/ /
| | * bool option -> (VernacCumulative | VernacNonCumulative) optionGravatar Gaëtan Gilbert2018-03-22
| | * Make parsing independent of the cumulativity flag.Gravatar Gaëtan Gilbert2018-03-21
| |/
* / [vernac] Move `Quit` and `Drop` to the toplevel layer.Gravatar Emilio Jesus Gallego Arias2018-03-11
|/
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Implement the Export Set/Unset feature.Gravatar Pierre-Marie Pédrot2018-03-09
* Make most of TACTIC EXTEND macros runtime calls.Gravatar Maxime Dénès2018-03-08
* Merge PR #6905: Fix make ml-docGravatar Maxime Dénès2018-03-07
|\
* \ Merge PR #6790: Allow universe declarations for [with Definition].Gravatar Maxime Dénès2018-03-07
|\ \
| | * Change non-documentation comment from ocamldoc styleGravatar mrmr19932018-03-05
| | * Fix formatting of some ocamldoc comments to reduce warningsGravatar mrmr19932018-03-05
| |/ |/|
| * Allow universe declarations for [with Definition].Gravatar Gaëtan Gilbert2018-03-05
* | Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
* Change default for notations with variables bound to both terms and binders.Gravatar Hugo Herbelin2018-02-20
* Notations: Adding modifiers to tell which kind of binder a constr can parse.Gravatar Hugo Herbelin2018-02-20
* Notations: A step in cleaning constr_entry_key.Gravatar Hugo Herbelin2018-02-20
* Adding general support for irrefutable disjunctive patterns.Gravatar Hugo Herbelin2018-02-20
* Respecting the ident/pattern distinction in notation modifiers.Gravatar Hugo Herbelin2018-02-20
* Adding support for parsing subterms of a notation as "pattern".Gravatar Hugo Herbelin2018-02-20
* Allows recursive patterns for binders to be associative on the left.Gravatar Hugo Herbelin2018-02-20
* A bit of miscellaneous code documentation around notations.Gravatar Hugo Herbelin2018-02-20
* Introducing an intermediary type "constr_prod_entry_key" for grammar producti...Gravatar Hugo Herbelin2018-02-20
* Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.Gravatar Hugo Herbelin2018-02-20
* Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.Gravatar Hugo Herbelin2018-02-20
* More precise explanation when a notation is not reversible for printing.Gravatar Hugo Herbelin2018-02-20
* Merge PR #6651: Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-02-12
|\
* | [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
* | [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
| * Use r.(p) syntax to print primitive projections.Gravatar Maxime Dénès2018-01-30
|/
* Merge PR #6499: [vernac] Move the flags/attributes out of vernac_exprGravatar Maxime Dénès2018-01-16
|\
| * [vernac] vernac_expr no longer recursiveGravatar Vincent Laporte2018-01-08
* | Brackets support single numbered goal selectors.Gravatar Théo Zimmermann2018-01-05
| * [vernac] Define types in orderGravatar Vincent Laporte2017-12-29
|/
* Merge PR #6433: [flags] Move global time flag into an attribute.Gravatar Maxime Dénès2017-12-29
|\
* | [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| * [flags] Move global time flag into an attribute.Gravatar Emilio Jesus Gallego Arias2017-12-23
|/
* Separate vernac controls and regular commands.Gravatar Maxime Dénès2017-12-20
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-23 20:47:00 +0000