aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
Commit message (Expand)AuthorAge
...
* Ring_polynom : shorter proof for Psub_okGravatar letouzey2013-08-22
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Expurgating the useless difference between List0 and List1 at theGravatar ppedrot2013-07-05
* Now, idtac closures use maps instead of association list.Gravatar ppedrot2013-06-22
* Cutting the dependency of Genarg in constr_expr, glob_constrGravatar ppedrot2013-06-21
* Hiding tactic value representations.Gravatar ppedrot2013-06-10
* Uniformizing generic argument types.Gravatar ppedrot2013-06-06
* newring.ml4: interp constr arg at interp time (not parse time)Gravatar gareuselesinge2013-05-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* code simplifications concerning SummaryGravatar letouzey2013-04-22
* Minor code cleaning in CArray / CList.Gravatar ppedrot2013-03-23
* Allowing different types of, not to be mixed, generic Stores throughGravatar ppedrot2013-03-12
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Minor code cleanups, especially take advantage of Dir_path.is_emptyGravatar letouzey2013-02-18
* New implementation of the conversion test, using normalization by evaluation toGravatar mdenes2013-01-22
* Unset Asymmetric PatternsGravatar pboutill2013-01-18
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Moved Stringset and Stringmap to String namespace.Gravatar ppedrot2012-12-14
* 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
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* As r15801: putting everything from Util.array_* to CArray.*.Gravatar ppedrot2012-09-14
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Getting rid of the undocumented [complete] tactic, which wasGravatar ppedrot2012-07-19
* Ring_polynom : a restricted simpl instead of a unfold;foldGravatar letouzey2012-07-07
* 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
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* Changed encoding from ISO-8859-1 to UTF-8 for some remaining gallina files.Gravatar ppedrot2012-06-12
* Getting rid of Pp.msgnl and Pp.message.Gravatar ppedrot2012-06-01
* Getting rid of Pp.msgGravatar ppedrot2012-05-30
* place all files specific to camlp4 syntax extensions in grammar/Gravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* New files intf/constrexpr.mli and intf/notation_term.mli out of TopconstrGravatar letouzey2012-05-29
* locus.mli for occurrences+clauses, misctypes.mli for various little thingsGravatar letouzey2012-05-29
* Everything compiles again.Gravatar msozeau2012-03-14
* Noise for nothingGravatar pboutill2012-03-02
* Proof using ...Gravatar gareuselesinge2011-12-12
* Fixing bug #2640 and variants of it (inconsistency between when andGravatar herbelin2011-11-17
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Esubst: make types of substitutions & lifts privateGravatar puech2011-08-08
* moins de reification inutile, noatations standardsGravatar pottier2011-08-04