aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Ltac repeat is in fact already doing progressGravatar letouzey2012-10-01
* Cleaning, renaming obscure functions and documenting in Hashcons.Gravatar ppedrot2012-09-26
* Fixing a bug introduced in Funind plugin when reorganizing the CListGravatar ppedrot2012-09-24
* More cleaning in CArray...Gravatar ppedrot2012-09-18
* More cleanup of Util: utf8 aspects moved to a new file unicode.mlGravatar letouzey2012-09-18
* Cleaning interface of Util.Gravatar ppedrot2012-09-18
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Some documentation and cleaning of CList and Util interfaces.Gravatar ppedrot2012-09-15
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Made Pp.std_ppcmds opaque.Gravatar ppedrot2012-09-13
* Fix Extraction Implicit on axioms.Gravatar aspiwack2012-08-24
* Experimental support for a comment in the files' preamble in extraction.Gravatar aspiwack2012-08-24
* Add option Set/Unset Extraction Conservative Types.Gravatar aspiwack2012-08-24
* Updating headers.Gravatar herbelin2012-08-08
* Fixup for macOS 10.8 & Ocaml 4.0Gravatar pboutill2012-08-08
* Vecnacentries.dump_global silently ignores exceptionsGravatar pboutill2012-08-06
* Try to make the use of Unix.lockf in micromega compatible with Win32Gravatar letouzey2012-08-06
* Dump references in ExtractionGravatar pboutill2012-08-05
* Dump referencesGravatar pboutill2012-08-05
* Bigint: new functions of_int and to_int, 2nd arg of pow in intGravatar letouzey2012-08-02
* Getting rid of the undocumented [complete] tactic, which wasGravatar ppedrot2012-07-19
* Fixes r15610 (A new status Unsafe in Interface).Gravatar aspiwack2012-07-13
* Ring_polynom : a restricted simpl instead of a unfold;foldGravatar letouzey2012-07-07
* Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)Gravatar letouzey2012-07-05
* Legacy Ring and Legacy Field migrated to contribsGravatar letouzey2012-07-05
* rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteGravatar letouzey2012-07-05
* More cleanup in Ring_polynom and EnvRingGravatar letouzey2012-07-05
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* Open Local Scope ---> Local Open Scope, same with Notation and aliiGravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Cleaning opening of the standard List module.Gravatar ppedrot2012-06-28
* Replace nat indices with positive one in Btauto.Gravatar ppedrot2012-06-28
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Internalization of pattern is done in two phases.Gravatar pboutill2012-06-14
* Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.Gravatar ppedrot2012-06-12
* More cleaningGravatar ppedrot2012-06-01
* Cleaning Pp.ppnl useGravatar ppedrot2012-06-01
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* remove many excessive open Util & Errors in mli'sGravatar letouzey2012-05-29
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Basic stuff about constr_expr migrated from topconstr to constrexpr_opsGravatar letouzey2012-05-29
* Stuff about notation_constr (ex-aconstr) now in notation_ops.mlGravatar letouzey2012-05-29