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
*
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
*
Adding a CSet module in Coq lib.
Pierre-Marie Pédrot
2014-03-05
*
Grammar.cma with less deps (Glob_ops and Nameops) after moving minor code
Pierre Letouzey
2014-03-02
*
Removing non-marshallable data from the Agram constructor. Instead of
Pierre-Marie Pédrot
2014-02-16
*
Tactic extensions do not need to be classified by the STM, as
Pierre-Marie Pédrot
2014-02-05
*
Removing the useless pattern ident genarg.
Pierre-Marie Pédrot
2013-12-19
*
Removing RefArgType generic argument.
Pierre-Marie Pédrot
2013-12-01
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Tacinterp: fewer use of old-style goals.
Arnaud Spiwack
2013-11-25
*
Centralizing the Ltac-defining functions in Tacenv.
ppedrot
2013-11-10
*
Removing the dependency of every level of tactic ATSs on glob_tactic_expr.
ppedrot
2013-11-10
*
Added the tactical "tac1 + tac2".
aspiwack
2013-11-02
*
CList.factorize_left with a parametric equality
letouzey
2013-10-23
*
Fixing CAMLP4 compilation.
ppedrot
2013-10-09
*
At least made the evar type opaque! There are still 5 remaining unsafe
ppedrot
2013-09-18
*
Moving Searchstack to CStack, and normalizing names a bit.
ppedrot
2013-09-06
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Vernac classification streamlined (handles VERNAC EXTEND)
gareuselesinge
2013-08-08
*
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-07-09
*
Removing SortArgType.
ppedrot
2013-07-05
*
Expurgating the useless difference between List0 and List1 at the
ppedrot
2013-07-05
*
Removing the use of leveled tactics wit_tacticn. It is now handled
ppedrot
2013-07-02
*
Removed the ad-hod handling of wit_tacticn.
ppedrot
2013-07-02
*
Fixing Camlp4 compilation.
ppedrot
2013-06-30
*
Getting rid of IntroPatternArgType.
ppedrot
2013-06-27
*
Splitted up Genarg in four different levels:
ppedrot
2013-06-21
*
Cutting the dependency of Genarg in constr_expr, glob_constr
ppedrot
2013-06-21
*
Fixing argument extension. Instead of qualified names, string
ppedrot
2013-06-19
[next]