index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
intf
/
vernacexpr.mli
Commit message (
Expand
)
Author
Age
*
Revert "Process Next Obligation proofs in parallel (fix #5314)"
Enrico Tassi
2017-01-21
*
Process Next Obligation proofs in parallel (fix #5314)
Enrico Tassi
2017-01-20
*
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
*
Lets Hints/Instances take an optional pattern
Matthieu Sozeau
2016-11-03
*
Complete overhaul of the Arguments vernacular.
Maxime Dénès
2016-10-27
*
Add command 'Set foo Append "bar"' for appending to an option (bug #5109).
Guillaume Melquiond
2016-10-01
*
Merge remote-tracking branch 'github/pr/299' into v8.6
Maxime Dénès
2016-09-30
|
\
*
|
Fix bug #4798: compat notations should not modify the parser.
Pierre-Marie Pédrot
2016-09-29
*
|
Arguments: cleanup + detect discrepancy rename/implicit (#3753)
Enrico Tassi
2016-09-29
|
*
Fix bug #4869, allow Prop, Set, and level names in constraints.
Matthieu Sozeau
2016-09-29
|
/
*
Support qualified identifiers in Show Match (bug #5050).
Guillaume Melquiond
2016-08-27
*
COMMENTS: Vernacexpr.extend_name
Matej Kosik
2016-06-20
*
par: like all: but in parallel
Enrico Tassi
2016-06-17
*
Extend Hint Mode to handle the no-head-evar case
Matthieu Sozeau
2016-06-16
*
Merge 'pr/191' into trunk
Enrico Tassi
2016-06-16
|
\
*
\
Merge remote-tracking branch 'github/pr/194' into trunk
Maxime Dénès
2016-06-16
|
\
\
|
|
*
Goal selectors are now tacticals and can be used as such.
Cyprien Mangin
2016-06-14
|
|
*
Add goal range selectors.
Cyprien Mangin
2016-06-14
|
*
|
Adding an only printing flag to notations.
Pierre-Marie Pédrot
2016-06-07
|
|
/
*
/
STM: proof block detection/error resilience API
Enrico Tassi
2016-06-06
|
/
*
Moving and enhancing the grammar_tactic_prod_item_expr type.
Pierre-Marie Pédrot
2016-04-14
*
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into...
Matthieu Sozeau
2016-04-04
|
\
*
|
Moving the Ltac definition command to an EXTEND based command.
Pierre-Marie Pédrot
2016-03-20
*
|
Moving Print Ltac 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
*
|
Moving Autorewrite to Hightatctic.
Pierre-Marie Pédrot
2016-03-06
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-21
|
\
\
|
*
|
Update copyright headers.
Maxime Dénès
2016-01-20
*
|
|
CLEANUP: removing unnecessary wrapper
Matej Kosik
2016-01-11
*
|
|
Simplification of grammar_prod_item type.
Pierre-Marie Pédrot
2016-01-02
*
|
|
CLEANUP: removing unnecessary alias
Matej Kosik
2015-12-18
*
|
|
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
|
/
/
*
|
Adding syntax "Show id" to show goal named id (shelved or not).
Hugo Herbelin
2015-11-02
*
|
Axioms now support the universe binding syntax.
Pierre-Marie Pédrot
2015-10-08
*
|
Proof using: let-in policy, optional auto-clear, forward closure*
Enrico Tassi
2015-10-08
*
|
Goptions: new value type: optional string
Enrico Tassi
2015-10-08
*
|
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
|
Documentation by giving a name to a large type.
Pierre-Marie Pédrot
2015-08-19
|
*
Revert commit 18796b6aea453bdeef1ad12ce80eeb220bf01e67, close 3080
Jason Gross
2015-08-14
|
/
*
Code documentation of the TACTIC/VERNAC EXTEND macros.
Pierre-Marie Pédrot
2015-06-29
*
Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"
Lionel Rieg
2015-06-26
*
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-05-04
*
Putting the From parameter of the Require command into the AST.
Pierre-Marie Pédrot
2015-03-27
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
Update headers.
Maxime Dénès
2015-01-12
*
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-18
[next]