aboutsummaryrefslogtreecommitdiff
path: root/grammar
AgeCommit message (Expand)Author
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Adding a canary library. This canary is imperfect. It allows serializationPierre-Marie Pédrot
2014-03-05Added a new module HMap. It works (almost) like Map, except that it expectsPierre-Marie Pédrot
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2014-03-05Adding a CSet module in Coq lib.Pierre-Marie Pédrot
2014-03-02Grammar.cma with less deps (Glob_ops and Nameops) after moving minor codePierre Letouzey
2014-02-16Removing non-marshallable data from the Agram constructor. Instead ofPierre-Marie Pédrot
2014-02-05Tactic extensions do not need to be classified by the STM, asPierre-Marie Pédrot
2013-12-19Removing the useless pattern ident genarg.Pierre-Marie Pédrot
2013-12-01Removing RefArgType generic argument.Pierre-Marie Pédrot
2013-11-30Getting rid of casted_open_constr. It was only used by thePierre-Marie Pédrot
2013-11-27Adding generic solvers to term holes. For now, no resolution mechanism norPierre-Marie Pédrot
2013-11-25Tacinterp: fewer use of old-style goals.Arnaud Spiwack
2013-11-10Centralizing the Ltac-defining functions in Tacenv.ppedrot
2013-11-10Removing the dependency of every level of tactic ATSs on glob_tactic_expr.ppedrot
2013-11-02Added the tactical "tac1 + tac2".aspiwack
2013-10-23CList.factorize_left with a parametric equalityletouzey
2013-10-09Fixing CAMLP4 compilation.ppedrot
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-07-05Removing SortArgType.ppedrot
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-07-02Removed the ad-hod handling of wit_tacticn.ppedrot
2013-06-30Fixing Camlp4 compilation.ppedrot
2013-06-27Getting rid of IntroPatternArgType.ppedrot
2013-06-21Splitted up Genarg in four different levels:ppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-19Fixing argument extension. Instead of qualified names, stringppedrot
2013-06-18Proof-of-concept: moved four easy-to-handle generic arguments toppedrot
2013-06-18Removing the various glob/subst/interp registering functions forppedrot
2013-06-12Added Genarg as generic argument type.ppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-05-29Make ist (interp_sign) available to TACTIC EXTEND codegareuselesinge
2013-05-12Added a generic notion of hook. Hooks are functions to be setppedrot
2013-03-17Fix some camlp5 quotations , restoring compatibility with camlp5 5.xletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 8)letouzey
2013-03-12Updated Exninfo to the new Store type.ppedrot
2013-03-05More monomorphization.ppedrot
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Added exception enrichment. Now one can define additional arbitraryppedrot
2013-01-28Added backtrace primitives.ppedrot
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-21Yet a new reduction tactic in Coq : cbnpboutill
2012-12-14Modulification of dir_pathppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 16:01:54 +0000