aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega
Commit message (Expand)AuthorAge
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* More monomorphic List.mem + List.assoc + ...Gravatar letouzey2013-10-24
* Turn many List.assoc into List.assoc_fGravatar letouzey2013-10-24
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* cList.index is now cList.index_f, same for index0Gravatar letouzey2013-10-23
* cList: set-as-list functions are now with an explicit comparisonGravatar letouzey2013-10-23
* Removing a bunch of generic equalities.Gravatar ppedrot2013-09-27
* Get rid of the uses of deprecated OCaml elements (still remaining compatible ...Gravatar xclerc2013-09-19
* Restrict (try...with...) to avoid catching critical exn (part 15)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 11)Gravatar letouzey2013-03-13
* Restrict (try...with...) to avoid catching critical exn (part 7)Gravatar letouzey2013-03-13
* Dir_path --> DirPathGravatar letouzey2013-02-19
* No more constant named "int" in Coq theories (cf bug #2878)Gravatar letouzey2012-12-18
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* More cleaning on Utils and CList. Some parts of the code beingGravatar ppedrot2012-09-17
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* The new ocaml compiler (4.00) has a lot of very cool warnings,Gravatar regisgia2012-09-14
* Kills the useless tactic annotations "in |- *"Gravatar letouzey2012-07-05
* ZArith + other : favor the use of modern names instead of compat notationsGravatar letouzey2012-07-05
* Cleaning Pp.ppnl useGravatar ppedrot2012-06-01
* 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
* Noise for nothingGravatar pboutill2012-03-02
* theories/, plugins/ and test-suite/ ported to the Arguments vernacularGravatar gareuselesinge2011-11-21
* Bug 2589: Documentation patch of Hendrik TewsGravatar pboutill2011-09-02
* New proposition "rewrite Heq in H" for eq_rect (assuming that there isGravatar herbelin2011-08-08
* Refl_omega: replaced generic = on constr by eq_constrGravatar puech2011-07-29
* Refl_omega: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
* Const_omega: replaced some generic = on constr by eq_constrGravatar puech2011-07-29
* Additionnal fix of romega after modularisation of ZArithGravatar letouzey2011-05-06
* Modularization of BinInt, related fixes in the stdlibGravatar letouzey2011-05-05
* Const_omega: look for S in Init only (avoid future clash with S of Numbers)Gravatar letouzey2009-12-18
* Factorisation between Makefile and ocamlbuild systems : .vo to compile are in...Gravatar letouzey2009-12-09
* OrderedType implementation for various numerical datatypes + min/max structuresGravatar letouzey2009-11-03
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Many changes in the Makefile infrastructure + a beginning of ocamlbuildGravatar letouzey2009-03-20
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20