aboutsummaryrefslogtreecommitdiffhomepage
path: root/grammar
Commit message (Expand)AuthorAge
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a canary library. This canary is imperfect. It allows serializationGravatar Pierre-Marie Pédrot2014-03-05
* Added a new module HMap. It works (almost) like Map, except that it expectsGravatar Pierre-Marie Pédrot2014-03-05
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Adding a CSet module in Coq lib.Gravatar Pierre-Marie Pédrot2014-03-05
* Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codeGravatar Pierre Letouzey2014-03-02
* Removing non-marshallable data from the Agram constructor. Instead ofGravatar Pierre-Marie Pédrot2014-02-16
* Tactic extensions do not need to be classified by the STM, asGravatar Pierre-Marie Pédrot2014-02-05
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
* Adding generic solvers to term holes. For now, no resolution mechanism norGravatar Pierre-Marie Pédrot2013-11-27
* Tacinterp: fewer use of old-style goals.Gravatar Arnaud Spiwack2013-11-25
* Centralizing the Ltac-defining functions in Tacenv.Gravatar ppedrot2013-11-10
* Removing the dependency of every level of tactic ATSs on glob_tactic_expr.Gravatar ppedrot2013-11-10
* Added the tactical "tac1 + tac2".Gravatar aspiwack2013-11-02
* CList.factorize_left with a parametric equalityGravatar letouzey2013-10-23
* Fixing CAMLP4 compilation.Gravatar ppedrot2013-10-09
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Moving Searchstack to CStack, and normalizing names a bit.Gravatar ppedrot2013-09-06
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Removing SortArgType.Gravatar ppedrot2013-07-05
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Removing the use of leveled tactics wit_tacticn. It is now handledGravatar ppedrot2013-07-02
* Removed the ad-hod handling of wit_tacticn.Gravatar ppedrot2013-07-02
* Fixing Camlp4 compilation.Gravatar ppedrot2013-06-30
* Getting rid of IntroPatternArgType.Gravatar ppedrot2013-06-27
* Splitted up Genarg in four different levels:Gravatar ppedrot2013-06-21
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Fixing argument extension. Instead of qualified names, stringGravatar ppedrot2013-06-19
* Proof-of-concept: moved four easy-to-handle generic arguments toGravatar ppedrot2013-06-18
* Removing the various glob/subst/interp registering functions forGravatar ppedrot2013-06-18
* Added Genarg as generic argument type.Gravatar ppedrot2013-06-12
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* Make ist (interp_sign) available to TACTIC EXTEND codeGravatar gareuselesinge2013-05-29
* Added a generic notion of hook. Hooks are functions to be setGravatar ppedrot2013-05-12
* Fix some camlp5 quotations , restoring compatibility with camlp5 5.xGravatar letouzey2013-03-17
* Restrict (try...with...) to avoid catching critical exn (part 13)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 8)Gravatar letouzey2013-03-13
* Updated Exninfo to the new Store type.Gravatar ppedrot2013-03-12
* More monomorphization.Gravatar ppedrot2013-03-05
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Added exception enrichment. Now one can define additional arbitraryGravatar ppedrot2013-02-18
* Added backtrace primitives.Gravatar ppedrot2013-01-28
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Yet a new reduction tactic in Coq : cbnGravatar pboutill2012-12-21
* Modulification of dir_pathGravatar ppedrot2012-12-14