index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
intf
/
vernacexpr.ml
Age
Commit message (
Expand
)
Author
2017-12-11
Merge 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-11-29
Remove "obsolete_locality" and fix STM vernac classification.
Maxime Dénès
2017-11-25
Allow local universe renaming in Print.
Gaëtan Gilbert
2017-11-04
Finish removing Show Goal uid
Gaëtan Gilbert
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-10
Parse [Proof using Type] without translating Type to an id.
Gaëtan Gilbert
2017-10-03
Implementing 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-26
Merge PR #688: Binding universe constraints in Definition/Inductive/etc...
Maxime Dénès
2017-09-19
Remove STM vernaculars.
Maxime Dénès
2017-09-19
Allow declaring universe constraints at definition level.
Matthieu Sozeau
2017-09-15
Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...
Maxime Dénès
2017-09-08
Parse directly to Sorts.family when appropriate.
Gaëtan Gilbert
2017-08-29
[vernac] Store Infix Modifier in Vernac Notation.
Pierre-Marie Pédrot
2017-07-31
Improve errors for cumulativity when monomorphic
Amin Timany
2017-07-04
Bump year in headers.
Pierre-Marie Pédrot
2017-06-21
[vernac] Remove stale bool parameter from `VernacStartTheoremProof`
Emilio Jesus Gallego Arias
2017-06-20
Merge PR#774: [ide] Add route_id parameter to query call.
Maxime Dénès
2017-06-18
[ide] Add route_id parameter to query call.
Emilio Jesus Gallego Arias
2017-06-16
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-12
Remove Show Thesis command which was never implemented.
Théo Zimmermann
2017-06-12
Remove non-working Show Tree and Show Node commands.
Théo Zimmermann
2017-06-12
Remove Show Implicit Arguments command.
Théo Zimmermann
2017-06-07
Put all plugins behind an "API".
Matej Kosik
