| Age | Commit message (Expand) | Author |
|---|
| 2013-06-21 | Splitted up Genarg in four different levels: | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-19 | Fixing argument extension. Instead of qualified names, string | ppedrot |
| 2013-06-18 | Proof-of-concept: moved four easy-to-handle generic arguments to | ppedrot |
| 2013-06-18 | Removing the various glob/subst/interp registering functions for | ppedrot |
| 2013-06-12 | Added Genarg as generic argument type. | ppedrot |
| 2013-06-06 | Uniformizing generic argument types. | ppedrot |
| 2013-05-29 | Make ist (interp_sign) available to TACTIC EXTEND code | gareuselesinge |
| 2013-05-12 | Added a generic notion of hook. Hooks are functions to be set | ppedrot |
| 2013-03-17 | Fix some camlp5 quotations , restoring compatibility with camlp5 5.x | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 8) | letouzey |
| 2013-03-12 | Updated Exninfo to the new Store type. | ppedrot |
| 2013-03-05 | More monomorphization. | ppedrot |
| 2013-02-19 | Dir_path --> DirPath | letouzey |
| 2013-02-18 | Added exception enrichment. Now one can define additional arbitrary | ppedrot |
| 2013-01-28 | Added backtrace primitives. | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2013-01-22 | New implementation of the conversion test, using normalization by evaluation to | mdenes |
| 2012-12-21 | Yet a new reduction tactic in Coq : cbn | pboutill |
| 2012-12-14 | Modulification of dir_path | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-14 | Moving hcons_string to String namespace. | ppedrot |
| 2012-12-14 | Implemented a full-fledged equality on [constr_expr]. By the way, | ppedrot |
| 2012-12-13 | Using library string functions. | ppedrot |
| 2012-11-13 | More monomorphizations | ppedrot |
| 2012-11-13 | Added a CString module. | ppedrot |
| 2012-11-08 | Added an Int module with dummy utility functions. | ppedrot |
| 2012-10-16 | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey |
| 2012-10-15 | Continue killing hidden tactics : no more generated h_xxx | letouzey |
| 2012-10-15 | Stylistic improvement: avoid a "if match List.hd" | letouzey |
| 2012-10-06 | remove useless hidden_flag in TacMutual(Co)Fix | letouzey |
| 2012-10-06 | remove Refiner.abstract_tactic and similar | letouzey |
| 2012-10-06 | Clean-up : removal of Proof_type.tactic_expr | letouzey |
| 2012-10-04 | Adding a nominal typing layer to Metasyntax in order to clarify | ppedrot |
| 2012-10-04 | Moved Compat to parsing. This permits to break the dependency of the | ppedrot |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-10-02 | Argextend: avoid useless "open Extrawit" | letouzey |
| 2012-10-01 | Added a new tactical infoH tac, that displays the names of hypothesis created... | courtieu |
| 2012-09-26 | Reusing the Hashset data structure in Hashcons. Hopefully, this should | ppedrot |
| 2012-09-18 | More cleanup of Util: utf8 aspects moved to a new file unicode.ml | letouzey |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-09-14 | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot |
| 2012-09-14 | The new ocaml compiler (4.00) has a lot of very cool warnings, | regisgia |
| 2012-09-13 | Made Pp.std_ppcmds opaque. | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-07-12 | Better exception handling in TACTIC EXTEND and VERNAC EXTEND (fix #2797) | letouzey |
| 2012-07-09 | The tactic remember now accepts a final eqn:H option (grant wish #2489) | letouzey |
| 2012-07-09 | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
