aboutsummaryrefslogtreecommitdiff
path: root/intf
AgeCommit message (Expand)Author
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
2017-12-23[api] Also deprecate constructors of Decl_kinds.Emilio Jesus Gallego Arias
2017-12-23[flags] Move global time flag into an attribute.Emilio Jesus Gallego Arias
2017-12-20Separate vernac controls and regular commands.Maxime Dénès
2017-12-14Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...Maxime Dénès
2017-12-12In printing, factorizing "match" clauses with same right-hand side.Hugo Herbelin
2017-12-12Removing cumbersome location in multiple patterns.Hugo Herbelin
2017-12-11Merge PR #1150: [stm] Remove all but one use of VtUnknown.Maxime Dénès
2017-12-10[api] Remove kernel dependency on intf (Decl_kind)Emilio Jesus Gallego Arias
2017-12-09[stm] Remove all but one use of VtUnknown.Emilio Jesus Gallego Arias
2017-12-01Proper nametab handling of global universe namesMatthieu Sozeau
2017-11-29Remove "obsolete_locality" and fix STM vernac classification.Maxime Dénès
2017-11-28Merge PR #1033: Universe binder improvementsMaxime Dénès
2017-11-26[api] Remove aliases of `Evar.t`Emilio Jesus Gallego Arias
2017-11-25Allow local universe renaming in Print.Gaëtan Gilbert
2017-11-13Merge PR #6098: [api] Move structures deprecated in the API to the core.Maxime Dénès
2017-11-13Merge PR #6052: [general] Move Tactypes to `interp` + API reordering.Maxime Dénès
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-11-04Finish removing Show Goal uidGaëtan Gilbert
2017-11-01[general] Move Tactypes to `interp`Emilio Jesus Gallego Arias
2017-10-25[general] Remove Econstr dependency from `intf`Emilio Jesus Gallego Arias
2017-10-17[stm] Remove VtBack from public classification.Emilio Jesus Gallego Arias
2017-10-17[stm] First step to move interpretation of Undo commands out of the classifier.Emilio Jesus Gallego Arias
2017-10-10Parse [Proof using Type] without translating Type to an id.Gaëtan Gilbert
2017-10-03Implementing a generic mechanism for locating named objects from Coq side.Pierre-Marie Pédrot
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
2017-09-26Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Maxime Dénès
2017-09-19Remove STM vernaculars.Maxime Dénès
2017-09-19Allow declaring universe constraints at definition level.Matthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 04:02:43 +0000