index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
Commit message (
Expand
)
Author
Age
*
Add a [Redirect] vernacular command
Clément Pit--Claudel
2015-05-04
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Inlining "fun" and "forall" tokens in parser, so that alternative notations for
Hugo Herbelin
2015-04-20
*
grammar: export constr_eval
Enrico Tassi
2015-03-30
*
grammar: export hypident
Enrico Tassi
2015-03-30
*
Putting the From parameter of the Require command into the AST.
Pierre-Marie Pédrot
2015-03-27
*
Qed export -> Qed exporting
Enrico Tassi
2015-03-22
*
Fixed 3233 (fresh does not work with a qualid).
Pierre Courtieu
2015-02-23
*
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Enrico Tassi
2015-02-14
*
Fixing #3982 (conflict with max notation for universes).
Hugo Herbelin
2015-02-12
*
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
*
Better doc and a few fixes for Proof using.
Enrico Tassi
2014-12-19
*
Proof using: New vernacular to name sets of section variables
Enrico Tassi
2014-12-18
*
Fixing CAMLP4 compilation.
Pierre-Marie Pédrot
2014-12-16
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
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
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
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
*
Fixing bugs #3723 and #3787 (reinitialization of camlp5 empty levels)
Hugo Herbelin
2014-11-06
*
Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".
Hugo Herbelin
2014-11-02
*
Add [Info] command.
Arnaud Spiwack
2014-11-01
*
Reorganization of the test for generic selection of occurrences in
Hugo Herbelin
2014-10-31
*
Dead code
Hugo Herbelin
2014-10-27
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Emit a warning for void Arguments statement (Close 3713)
Enrico Tassi
2014-10-13
*
Parsing of "?[" as two tokens (makes ssr compile).
Enrico Tassi
2014-10-13
*
Fixing #3687 (inconsistent lexer state after a bullet).
Hugo Herbelin
2014-10-07
*
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
*
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
Matthieu Sozeau
2014-09-15
*
Checking typability of evar instances. Using ";" to separate bindings
Hugo Herbelin
2014-09-13
*
Add syntax [id]: to apply tactic to goal named id.
Hugo Herbelin
2014-09-12
*
Parsing evar instances.
Hugo Herbelin
2014-09-12
*
Referring to evars by names. Added a parser for evars (but parsing of
Hugo Herbelin
2014-09-12
*
VernacExtend does not dispatch on type anymore.
Pierre-Marie Pédrot
2014-09-10
*
Removing dead code relative to the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Removing the XML plugin.
Pierre-Marie Pédrot
2014-09-08
*
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-09-08
*
Factorize the parsing rules of [Record] and the other kind of type definitions.
Arnaud Spiwack
2014-09-04
*
Remove [Infer] option of records.
Arnaud Spiwack
2014-09-04
*
Add a [Variant] declaration which allows to write non-recursive variant types.
Arnaud Spiwack
2014-09-04
[next]