index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
stm
/
vernac_classifier.ml
Commit message (
Expand
)
Author
Age
*
Merge PR #7139: [stm] More cleanup of "classification is not an interpreter"
Enrico Tassi
2018-04-05
|
\
*
\
Merge PR #7138: [stm] Move VernacBacktrack to the toplevel.
Enrico Tassi
2018-04-04
|
\
\
|
|
*
[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-04-01
*
|
Remove deprecated commands Arguments Scope and Implicit Arguments
Jasper Hugunin
2018-03-30
|
/
*
[vernac] Move `Quit` and `Drop` to the toplevel layer.
Emilio Jesus Gallego Arias
2018-03-11
*
Implement the Export Set/Unset feature.
Pierre-Marie Pédrot
2018-03-09
*
Update headers following #6543.
Théo Zimmermann
2018-02-27
*
[ast] Improve precision of Ast location recognition in serialization.
Emilio Jesus Gallego Arias
2018-02-22
*
[vernac] Mutual theorems (VernacStartTheoremProof) always have names
Vincent Laporte
2018-02-01
*
[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition
Vincent Laporte
2018-02-01
*
[vernac] vernac_expr no longer recursive
Vincent Laporte
2018-01-08
*
[flags] Move global time flag into an attribute.
Emilio Jesus Gallego Arias
2017-12-23
*
Separate vernac controls and regular commands.
Maxime Dénès
2017-12-20
*
[stm] Remove all but one use of VtUnknown.
Emilio Jesus Gallego Arias
2017-12-09
*
Remove "obsolete_locality" and fix STM vernac classification.
Maxime Dénès
2017-11-29
*
[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-17
*
Remove STM vernaculars.
Maxime Dénès
2017-09-19
*
Bump year in headers.
Pierre-Marie Pédrot
2017-07-04
*
[vernac] Remove stale bool parameter from `VernacStartTheoremProof`
Emilio Jesus Gallego Arias
2017-06-21
*
Merge PR#774: [ide] Add route_id parameter to query call.
Maxime Dénès
2017-06-20
|
\
|
*
[ide] Add route_id parameter to query call.
Emilio Jesus Gallego Arias
2017-06-18
*
|
Fix bugs and add an option for cumulativity
Amin Timany
2017-06-16
|
/
*
Merge PR#717: [proof] Deprecate "proof mode" API
Maxime Dénès
2017-06-07
|
\
*
|
Drop '.' from CErrors.anomaly, insert it in args
Jason Gross
2017-06-02
|
*
[proof] Deprecate "proof mode" API
Emilio Jesus Gallego Arias
2017-05-31
|
/
*
Remove VernacError
Gaetan Gilbert
2017-04-21
*
Merge branch 'v8.6' into trunk
Maxime Dénès
2017-04-15
|
\
|
*
Fix anomaly when doing [all:Check _.] during a proof.
Gaetan Gilbert
2017-04-14
*
|
[stm] Remove some obsolete vernacs/classification.
Emilio Jesus Gallego Arias
2017-03-24
|
*
Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"
Maxime Dénès
2016-11-18
|
*
[stm] Remove STM-related vernaculars
Emilio Jesus Gallego Arias
2016-11-17
|
/
*
Add command 'Set foo Append "bar"' for appending to an option (bug #5109).
Guillaume Melquiond
2016-10-01
*
errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...
Pierre Letouzey
2016-07-03
*
par: like all: but in parallel
Enrico Tassi
2016-06-17
*
Documentation
Enrico Tassi
2016-06-07
*
STM: proof block detection for bullets and { block }
Enrico Tassi
2016-06-06
*
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-06
*
Proof_global, STM: cleanup + use default_proof_mode instead of "Classic"
Enrico Tassi
2016-05-10
*
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
Moving Tactic Notation to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
Moving VernacSolve to an EXTEND-based definition.
Pierre-Marie Pédrot
2016-03-19
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
|
*
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
Remove useless recursive flags.
Guillaume Melquiond
2016-01-01
*
|
CLEANUP: Vernacexpr.VernacDeclareTacticDefinition
Matej Kosik
2015-12-18
*
|
CLEANUP: Removing "Vernacexpr.VernacNop" variant to which no Vernacular comma...
Matej Kosik
2015-12-18
*
|
CLEANUP: Vernacexpr.vernac_expr
Matej Kosik
2015-12-18
|
/
*
Axioms now support the universe binding syntax.
Pierre-Marie Pédrot
2015-10-08
[next]