aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
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-01Ltac repeat is in fact already doing progressletouzey
2012-09-26Cleaning, renaming obscure functions and documenting in Hashcons.ppedrot
2012-09-24Fixing a bug introduced in Funind plugin when reorganizing the CListppedrot
2012-09-18More cleaning in CArray...ppedrot
2012-09-18More cleanup of Util: utf8 aspects moved to a new file unicode.mlletouzey
2012-09-18Cleaning interface of Util.ppedrot
2012-09-17More cleaning on Utils and CList. Some parts of the code beingppedrot
2012-09-15Some documentation and cleaning of CList and Util interfaces.ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
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-24Fix Extraction Implicit on axioms.aspiwack
2012-08-24Experimental support for a comment in the files' preamble in extraction.aspiwack
2012-08-24Add option Set/Unset Extraction Conservative Types.aspiwack
2012-08-08Updating headers.herbelin
2012-08-08Fixup for macOS 10.8 & Ocaml 4.0pboutill
2012-08-06Vecnacentries.dump_global silently ignores exceptionspboutill
2012-08-06Try to make the use of Unix.lockf in micromega compatible with Win32letouzey
2012-08-05Dump references in Extractionpboutill
2012-08-05Dump referencespboutill
2012-08-02Bigint: new functions of_int and to_int, 2nd arg of pow in intletouzey
2012-07-19Getting rid of the undocumented [complete] tactic, which wasppedrot
2012-07-13Fixes r15610 (A new status Unsafe in Interface).aspiwack
2012-07-07Ring_polynom : a restricted simpl instead of a unfold;foldletouzey
2012-07-05Extraction: Hashtbl.replace uses less ressources than Hashtbl.add (fix #2824)letouzey
2012-07-05Legacy Ring and Legacy Field migrated to contribsletouzey
2012-07-05rewrite_db : a first attempt at using rewrite_strat for a quicker autorewriteletouzey
2012-07-05More cleanup in Ring_polynom and EnvRingletouzey
2012-07-05Kills the useless tactic annotations "in |- *"letouzey
2012-07-05Open Local Scope ---> Local Open Scope, same with Notation and aliiletouzey
2012-07-05ZArith + other : favor the use of modern names instead of compat notationsletouzey
2012-06-28Cleaning opening of the standard List module.ppedrot
2012-06-28Replace nat indices with positive one in Btauto.ppedrot
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-14Internalization of pattern is done in two phases.pboutill
2012-06-12Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.ppedrot
2012-06-01More cleaningppedrot
2012-06-01Cleaning Pp.ppnl useppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30Getting rid of Pp.msgppedrot
2012-05-30More uniformisation in Pp.warn functions.ppedrot
2012-05-29remove many excessive open Util & Errors in mli'sletouzey
2012-05-29place all files specific to camlp4 syntax extensions in grammar/letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-05-29Basic stuff about constr_expr migrated from topconstr to constrexpr_opsletouzey