aboutsummaryrefslogtreecommitdiff
path: root/grammar
AgeCommit message (Expand)Author
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
2012-12-14Modulification of identifierppedrot
2012-12-14Moving hcons_string to String namespace.ppedrot
2012-12-14Implemented a full-fledged equality on [constr_expr]. By the way,ppedrot
2012-12-13Using library string functions.ppedrot
2012-11-13More monomorphizationsppedrot
2012-11-13Added a CString module.ppedrot
2012-11-08Added an Int module with dummy utility functions.ppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-15Continue killing hidden tactics : no more generated h_xxxletouzey
2012-10-15Stylistic improvement: avoid a "if match List.hd"letouzey
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-10-06remove Refiner.abstract_tactic and similarletouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-04Adding a nominal typing layer to Metasyntax in order to clarifyppedrot
2012-10-04Moved Compat to parsing. This permits to break the dependency of theppedrot
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-10-02Argextend: avoid useless "open Extrawit"letouzey
2012-10-01Added a new tactical infoH tac, that displays the names of hypothesis created...courtieu
2012-09-26Reusing the Hashset data structure in Hashcons. Hopefully, this shouldppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 08:46:05 +0000