index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
intf
Commit message (
Expand
)
Author
Age
*
Merge PR #7016: Make parsing independent of the cumulativity flag.
Enrico Tassi
2018-04-05
|
\
*
\
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
|
\
\
\
*
\
\
\
Merge PR #7106: Supporting fix and cofix in Ltac pattern-matching (wish #7092)
Pierre-Marie Pédrot
2018-04-01
|
\
\
\
\
|
|
|
*
|
[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
|
|
/
/
|
/
|
|
|
*
|
Patterns: Accepting patterns in PFix and PCofix and not only constr.
Hugo Herbelin
2018-03-28
*
|
|
Merge PR #7062: Slightly refining some error messages about unresolvable evars.
Pierre-Marie Pédrot
2018-03-27
|
\
\
\
|
*
|
|
Slightly refining some error messages about unresolvable evars.
Hugo Herbelin
2018-03-24
|
|
/
/
|
|
*
bool option -> (VernacCumulative | VernacNonCumulative) option
Gaëtan Gilbert
2018-03-22
|
|
*
Make parsing independent of the cumulativity flag.
Gaëtan Gilbert
2018-03-21
|
|
/
*
/
[vernac] Move `Quit` and `Drop` to the toplevel layer.
Emilio Jesus Gallego Arias
2018-03-11
|
/
*
[located] Push inner locations in `reference` to a CAst.t node.
Emilio Jesus Gallego Arias
2018-03-09
*
[located] More work towards using CAst.t
Emilio Jesus Gallego Arias
2018-03-09
*
Implement the Export Set/Unset feature.
Pierre-Marie Pédrot
2018-03-09
*
Make most of TACTIC EXTEND macros runtime calls.
Maxime Dénès
2018-03-08
*
Merge PR #6905: Fix make ml-doc
Maxime Dénès
2018-03-07
|
\
*
\
Merge PR #6790: Allow universe declarations for [with Definition].
Maxime Dénès
2018-03-07
|
\
\
|
|
*
Change non-documentation comment from ocamldoc style
mrmr1993
2018-03-05
|
|
*
Fix formatting of some ocamldoc comments to reduce warnings
mrmr1993
2018-03-05
|
|
/
|
/
|
|
*
Allow universe declarations for [with Definition].
Gaëtan Gilbert
2018-03-05
*
|
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
*
Change default for notations with variables bound to both terms and binders.
Hugo Herbelin
2018-02-20
*
Notations: Adding modifiers to tell which kind of binder a constr can parse.
Hugo Herbelin
2018-02-20
*
Notations: A step in cleaning constr_entry_key.
Hugo Herbelin
2018-02-20
*
Adding general support for irrefutable disjunctive patterns.
Hugo Herbelin
2018-02-20
*
Respecting the ident/pattern distinction in notation modifiers.
Hugo Herbelin
2018-02-20
*
Adding support for parsing subterms of a notation as "pattern".
Hugo Herbelin
2018-02-20
*
Allows recursive patterns for binders to be associative on the left.
Hugo Herbelin
2018-02-20
*
A bit of miscellaneous code documentation around notations.
Hugo Herbelin
2018-02-20
*
Introducing an intermediary type "constr_prod_entry_key" for grammar producti...
Hugo Herbelin
2018-02-20
*
Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.
Hugo Herbelin
2018-02-20
*
Rephrasing ETBinderList with a self-documenting and invariant-carrying argument.
Hugo Herbelin
2018-02-20
*
More precise explanation when a notation is not reversible for printing.
Hugo Herbelin
2018-02-20
*
Merge PR #6651: Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-02-12
|
\
*
|
[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
|
*
Use r.(p) syntax to print primitive projections.
Maxime Dénès
2018-01-30
|
/
*
Merge PR #6499: [vernac] Move the flags/attributes out of vernac_expr
Maxime Dénès
2018-01-16
|
\
|
*
[vernac] vernac_expr no longer recursive
Vincent Laporte
2018-01-08
*
|
Brackets support single numbered goal selectors.
Théo Zimmermann
2018-01-05
|
*
[vernac] Define types in order
Vincent Laporte
2017-12-29
|
/
*
Merge PR #6433: [flags] Move global time flag into an attribute.
Maxime Dénès
2017-12-29
|
\
*
|
[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-23
|
/
*
Separate vernac controls and regular commands.
Maxime Dénès
2017-12-20
*
Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...
Maxime Dénès
2017-12-14
|
\
|
*
In printing, factorizing "match" clauses with same right-hand side.
Hugo Herbelin
2017-12-12
[next]