aboutsummaryrefslogtreecommitdiff
path: root/grammar
AgeCommit message (Expand)Author
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
2012-09-14The new ocaml compiler (4.00) has a lot of very cool warnings,regisgia
2012-09-13Made Pp.std_ppcmds opaque.ppedrot
2012-08-08Updating headers.herbelin
2012-07-12Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797)letouzey
2012-07-09The tactic remember now accepts a final eqn:H option (grant wish #2489)letouzey
2012-07-09induction/destruct : nicer syntax for generating equations (solves #2741)letouzey
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-01More cleaningppedrot
2012-05-29Extend become a mli-only file in intf/letouzey
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 18:14:53 +0000