aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/romega
Commit message (Expand)AuthorAge
* Switch the few remaining iso-latin-1 files to utf8Gravatar Pierre Letouzey2014-12-09
* Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.Gravatar Hugo Herbelin2014-12-07
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* Clean up a comment in plugins/romega/ReflOmegaCoreGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* 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