index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
grammar
Commit message (
Expand
)
Author
Age
*
Adding a possible DEPRECATED flag to VERNAC EXTEND statements.
Pierre-Marie Pédrot
2015-02-19
*
Record type for VERNAC EXTEND rules and a bit of documentation.
Pierre-Marie Pédrot
2015-02-19
*
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
*
Fixing CAMLP4 compilation.
Pierre-Marie Pédrot
2014-12-16
*
Extend the syntax of simpl with a delta flag.
Arnaud Spiwack
2014-12-12
*
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
*
Continuing 3741c46fe134 on reporting ltac error.
Hugo Herbelin
2014-11-08
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
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
*
Parsing evar instances.
Hugo Herbelin
2014-09-12
*
VernacExtend does not dispatch on type anymore.
Pierre-Marie Pédrot
2014-09-10
*
Parsing of Type@{max(i,j)}.
Matthieu Sozeau
2014-09-08
*
Renaming goal-entering functions.
Pierre-Marie Pédrot
2014-09-06
*
Moving code of tactic interpretation from Tacenv to Vernacentries.
Pierre-Marie Pédrot
2014-08-31
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Moving the TacExtend node from atomic to plain tactics.
Pierre-Marie Pédrot
2014-08-18
*
Removing simple induction / destruct from the AST.
Pierre-Marie Pédrot
2014-08-07
*
Instead of relying on a trick to make the constructor tactic parse, put
Pierre-Marie Pédrot
2014-08-07
*
Removing the "constructor" tactic from the AST.
Pierre-Marie Pédrot
2014-08-07
*
Removing "intros untils" from the AST.
Pierre-Marie Pédrot
2014-08-06
*
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-08-05
*
Adding a syntax "enough" for the variant of "assert" with the order of
Hugo Herbelin
2014-08-05
*
STM: encapsulate Pp.message in Feedback.feedback
Carst Tankink
2014-08-04
*
Qualified ML tactic names. The plugin name is used to discriminate
Pierre-Marie Pédrot
2014-07-27
*
Removing dead code relative to or_metaid.
Pierre-Marie Pédrot
2014-07-25
*
Distinguish tactics t1;t2 and t1;[t2..].
Arnaud Spiwack
2014-07-24
*
Fix g_coqast for explicit applications.
Matthieu Sozeau
2014-07-07
*
all coqide specific files moved into ide/
Enrico Tassi
2014-06-25
*
Moving the [split] tactic out of the AST.
Pierre-Marie Pédrot
2014-06-06
*
Fixing TACTIC EXTEND for arguments-free tactics that may modify the whole
Pierre-Marie Pédrot
2014-05-24
*
Removing useless use of metaids in tactic AST.
Pierre-Marie Pédrot
2014-05-22
*
Moving left & right tactics out of the AST.
Pierre-Marie Pédrot
2014-05-21
*
Moving (e)transitivity out of the AST.
Pierre-Marie Pédrot
2014-05-20
*
Tactics declared through TACTIC EXTEND that are of the form
Pierre-Marie Pédrot
2014-05-20
*
Tentative to add constr-using primitive tactics without grammar rules.
Pierre-Marie Pédrot
2014-05-20
*
Fixing Camlp4 compilation
Pierre-Marie Pédrot
2014-05-17
*
Moving argument-free tactics out of the AST into a dedicated
Pierre-Marie Pédrot
2014-05-16
*
Tactics defined through TACTIC EXTEND that are only defined as a string do
Pierre-Marie Pédrot
2014-05-16
*
Now parsing rules of ML-declared tactics are only made available after the
Pierre-Marie Pédrot
2014-05-12
*
Moving the ML tactic extension mechanism to a Libobject-based one.
Pierre-Marie Pédrot
2014-05-12
*
Plugin names must be declared in the header of .ml4 file, be they static or
Pierre-Marie Pédrot
2014-05-12
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Adding a canary library. This canary is imperfect. It allows serialization
Pierre-Marie Pédrot
2014-03-05
*
Added a new module HMap. It works (almost) like Map, except that it expects
Pierre-Marie Pédrot
2014-03-05
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
[next]