aboutsummaryrefslogtreecommitdiff
path: root/plugins/setoid_ring/newring.ml4
AgeCommit message (Expand)Author
2013-06-10Hiding tactic value representations.ppedrot
2013-06-06Uniformizing generic argument types.ppedrot
2013-05-29newring.ml4: interp constr arg at interp time (not parse time)gareuselesinge
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-03-23Minor code cleaning in CArray / CList.ppedrot
2013-03-12Allowing different types of, not to be mixed, generic Stores throughppedrot
2013-02-19Dir_path --> DirPathletouzey
2013-02-18Minor code cleanups, especially take advantage of Dir_path.is_emptyletouzey
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
2012-10-02Remove some more "open" and dead code thanks to OCaml4 warningsletouzey
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-06-01Getting rid of Pp.msgnl and Pp.message.ppedrot
2012-05-30Getting rid of Pp.msgppedrot
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-29New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstrletouzey
2012-05-29locus.mli for occurrences+clauses, misctypes.mli for various little thingsletouzey
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-11-17Fixing bug #2640 and variants of it (inconsistency between when andherbelin
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-08-08Esubst: make types of substitutions & lifts privatepuech
2011-07-29Newring: generic = on constr replaced by eq_constrpuech
2011-07-29replaced some generic = on constr by eq_constrpuech
2011-07-29Newring: replaced some generic = on constr by eq_constrpuech
2011-07-29Newring: replaced generic = on constr by eq_constrpuech
2011-07-29Newring: generic Pervasives.compare on constr replaced by constr_ordpuech
2011-07-29Newring: generic equality on constr replaced by constr_equalpuech
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-09-30Simplify tactic(_)-bound arguments in TACTIC EXTEND rulesglondu
2010-09-28Remove some occurrences of "open Termops"glondu
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-19Reverting partial fix for #2335 committed by mistake in r13435. Sorry.herbelin
2010-09-19Patch solving the bug but leaving open design choicesherbelin
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:29:27 +0000