aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2012-11-08Monomorphized a lot of equalities over OCaml integers, thanks toppedrot
2012-10-31correcting a little bug in Functionjforest
2012-10-30Extraction Implicit: consider the parameters of a constructor (fix #2905)letouzey
2012-10-30Extraction: avoid initial strange empty comments after Arnaud's hackletouzey
2012-10-30Fix Separate extraction when a module-as-file is aliased (#2917)letouzey
2012-10-26Change Hint Resolve, Immediate to take a global reference as argumentmsozeau
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-06still some more dead code removalletouzey
2012-10-06remove useless hidden_flag in TacMutual(Co)Fixletouzey
2012-10-06remove dumptree.ml4letouzey
2012-10-06Clean-up : removal of Proof_type.tactic_exprletouzey
2012-10-06Proof_type: rule now degenerates to prim_ruleletouzey
2012-10-06Clean-up : no more Proof_type.proof_treeletouzey
2012-10-06Clean-up of proof_type.ml : no more Nested nor abstract_tactic_boxletouzey
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:12:42 +0000