aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins
Commit message (Expand)AuthorAge
* correcting a little bug in FunctionGravatar jforest2012-10-31
* Extraction Implicit: consider the parameters of a constructor (fix #2905)Gravatar letouzey2012-10-30
* Extraction: avoid initial strange empty comments after Arnaud's hackGravatar letouzey2012-10-30
* Fix Separate extraction when a module-as-file is aliased (#2917)Gravatar letouzey2012-10-30
* Change Hint Resolve, Immediate to take a global reference as argumentGravatar msozeau2012-10-26
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* still some more dead code removalGravatar letouzey2012-10-06
* remove useless hidden_flag in TacMutual(Co)FixGravatar letouzey2012-10-06
* remove dumptree.ml4Gravatar letouzey2012-10-06
* Clean-up : removal of Proof_type.tactic_exprGravatar letouzey2012-10-06
* Proof_type: rule now degenerates to prim_ruleGravatar letouzey2012-10-06
* Clean-up : no more Proof_type.proof_treeGravatar letouzey2012-10-06
* Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxGravatar letouzey2012-10-06
* Moved Compat to parsing. This permits to break the dependency of theGravatar ppedrot2012-10-04
* 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