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
*
Type delayed_open_constr is now monotonic.
Pierre-Marie Pédrot
2015-10-19
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-12
|
\
|
*
Fixing untimely unexpected warning "Collision between bound variables" (#4317).
Hugo Herbelin
2015-10-11
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-10-09
|
\
|
|
*
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 Strict Universe Declaration option (on by default)
Matthieu Sozeau
2015-10-07
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-09-17
|
\
|
|
*
Univs: Add universe binding lists to definitions
Matthieu Sozeau
2015-09-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-08-22
|
\
|
|
*
Documentation by giving a name to a large type.
Pierre-Marie Pédrot
2015-08-19
*
|
Merge branch 'v8.5' into trunk
Maxime Dénès
2015-07-02
|
\
|
|
*
Code documentation of the TACTIC/VERNAC EXTEND macros.
Pierre-Marie Pédrot
2015-06-29
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-28
|
\
|
|
*
Introduction of a "Undelimit Scope" command, undoing "Delimit Scope"
Lionel Rieg
2015-06-26
*
|
Remove other types not carried by interpretations in `Tacexpr`.
Arnaud Spiwack
2015-06-25
*
|
Remove useless `and_short_name` in interpreted level in `Tacexpr`.
Arnaud Spiwack
2015-06-25
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-05
|
\
|
|
*
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-05-04
*
|
Merge branch 'v8.5' into trunk
Enrico Tassi
2015-03-30
|
\
|
|
*
Putting the From parameter of the Require command into the AST.
Pierre-Marie Pédrot
2015-03-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-02-15
|
\
|
|
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-02-10
|
\
|
|
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
|
Embedding the index of the ML tactic entry in the Tacexpr AST.
Pierre-Marie Pédrot
2015-01-21
|
/
*
Update headers.
Maxime Dénès
2015-01-12
*
A global [gfail] tactic which works like [fail] except that it fails even if ...
Arnaud Spiwack
2014-12-23
*
Fix compilation error in some configurations.
Arnaud Spiwack
2014-12-23
*
Add a backtracking version of Ltac's [match].
Arnaud Spiwack
2014-12-19
*
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-18
*
About now accepts hypothesis names and goal selector.
Pierre Courtieu
2014-12-15
*
Add Ltac syntax for the [tclIFCATCH] primitive.
Arnaud Spiwack
2014-12-12
*
Extend the syntax of simpl with a delta flag.
Arnaud Spiwack
2014-12-12
*
Searchxxx now search also the hypothesis and support goal selector.
Pierre Courtieu
2014-12-12
*
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-11
*
Improved tracking of the origin of evars.
Hugo Herbelin
2014-12-07
*
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-16
*
Removing a unused boolean in the TacMove node of tacexpr AST.
Pierre-Marie Pédrot
2014-11-09
*
Add a interpreted level [tacexpr] to [Tacexpr] together with its printer.
Arnaud Spiwack
2014-11-01
*
Add [Info] command.
Arnaud Spiwack
2014-11-01
*
Feedback message: hold extra info to help routing
Enrico Tassi
2014-10-31
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
A patch for printing "match" when constructors are defined with let-in
Hugo Herbelin
2014-10-20
*
Emit a warning for void Arguments statement (Close 3713)
Enrico Tassi
2014-10-13
*
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-30
*
Add syntax for naming new goals in refine: writing ?[id] instead of _
Hugo Herbelin
2014-09-30
*
Notation: option to attach extra pretty printing rules to notations
Enrico Tassi
2014-09-29
*
Using an or_var rather than the hack with loc for coding a pure ident
Hugo Herbelin
2014-09-24
[next]