aboutsummaryrefslogtreecommitdiffhomepage
path: root/intf/vernacexpr.ml
Commit message (Expand)AuthorAge
* [vernac] Mutual theorems (VernacStartTheoremProof) always have namesGravatar Vincent Laporte2018-02-01
* [vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinitionGravatar Vincent Laporte2018-02-01
* 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
|/
* [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
* Merge PR #1150: [stm] Remove all but one use of VtUnknown.Gravatar Maxime Dénès2017-12-11
|\
* | [api] Remove kernel dependency on intf (Decl_kind)Gravatar Emilio Jesus Gallego Arias2017-12-10
| * [stm] Remove all but one use of VtUnknown.Gravatar Emilio Jesus Gallego Arias2017-12-09
|/
* Remove "obsolete_locality" and fix STM vernac classification.Gravatar Maxime Dénès2017-11-29
* Allow local universe renaming in Print.Gravatar Gaëtan Gilbert2017-11-25
* Finish removing Show Goal uidGravatar Gaëtan Gilbert2017-11-04
* [stm] Remove VtBack from public classification.Gravatar Emilio Jesus Gallego Arias2017-10-17
* [stm] First step to move interpretation of Undo commands out of the classifier.Gravatar Emilio Jesus Gallego Arias2017-10-17
* Parse [Proof using Type] without translating Type to an id.Gravatar Gaëtan Gilbert2017-10-10
* Implementing a generic mechanism for locating named objects from Coq side.Gravatar Pierre-Marie Pédrot2017-10-03
* [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
* Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\
* | Remove STM vernaculars.Gravatar Maxime Dénès2017-09-19
| * Allow declaring universe constraints at definition level.Gravatar Matthieu Sozeau2017-09-19
|/
* Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...Gravatar Maxime Dénès2017-09-15
|\
* | Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| * [vernac] Store Infix Modifier in Vernac Notation.Gravatar Pierre-Marie Pédrot2017-08-29
|/
* Improve errors for cumulativity when monomorphicGravatar Amin Timany2017-07-31
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* [vernac] Remove stale bool parameter from `VernacStartTheoremProof`Gravatar Emilio Jesus Gallego Arias2017-06-21
* Merge PR#774: [ide] Add route_id parameter to query call.Gravatar Maxime Dénès2017-06-20
|\
| * [ide] Add route_id parameter to query call.Gravatar Emilio Jesus Gallego Arias2017-06-18
* | Fix bugs and add an option for cumulativityGravatar Amin Timany2017-06-16
|/
* Remove Show Thesis command which was never implemented.Gravatar Théo Zimmermann2017-06-12
* Remove non-working Show Tree and Show Node commands.Gravatar Théo Zimmermann2017-06-12
* Remove Show Implicit Arguments command.Gravatar Théo Zimmermann2017-06-12
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 05:50:20 +0000