aboutsummaryrefslogtreecommitdiff
path: root/grammar
AgeCommit message (Expand)Author
2014-05-24Fixing TACTIC EXTEND for arguments-free tactics that may modify the wholePierre-Marie Pédrot
2014-05-22Removing useless use of metaids in tactic AST.Pierre-Marie Pédrot
2014-05-21Moving left & right tactics out of the AST.Pierre-Marie Pédrot
2014-05-20Moving (e)transitivity out of the AST.Pierre-Marie Pédrot
2014-05-20Tactics declared through TACTIC EXTEND that are of the formPierre-Marie Pédrot
2014-05-20Tentative to add constr-using primitive tactics without grammar rules.Pierre-Marie Pédrot
2014-05-17Fixing Camlp4 compilationPierre-Marie Pédrot
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
2014-05-16Tactics defined through TACTIC EXTEND that are only defined as a string doPierre-Marie Pédrot
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-12Moving the ML tactic extension mechanism to a Libobject-based one.Pierre-Marie Pédrot
2014-05-12Plugin names must be declared in the header of .ml4 file, be they static orPierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-11 12:37:22 +0000