aboutsummaryrefslogtreecommitdiff
path: root/plugins
AgeCommit message (Expand)Author
2013-01-29Fixed synchronicity of filter with evar context in new_goal_with.herbelin
2013-01-28Uniformization of the "anomaly" command.ppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2013-01-18Unset Asymmetric Patternspboutill
2012-12-19Array.create is deprecatedpboutill
2012-12-18Modulification of nameppedrot
2012-12-18Modulification of mod_bound_idppedrot
2012-12-18Modulification of Labelppedrot
2012-12-18Extraction: qualified names in Extract Constant examples (fix #2878)letouzey
2012-12-18No more constant named "int" in Coq theories (cf bug #2878)letouzey
2012-12-17Extraction of projections: restrict a hack to ocaml only (fix #2941)letouzey
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-14Moved Intset and Intmap to Int namespace.ppedrot
2012-12-08Ensure that a function declared with a label is used with itletouzey
2012-11-17Taking into account the type of a definition (if it exists), and theherbelin
2012-11-13More monomorphizationsppedrot
2012-11-13Added a CString module.ppedrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-08 04:22:02 +0000