aboutsummaryrefslogtreecommitdiff
path: root/interp/coqlib.ml
AgeCommit message (Expand)Author
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2015-12-22Do not compose "str" and "to_string" whenever possible.Guillaume Melquiond
2015-04-23Remove almost all the uses of string concatenation when building error messages.Guillaume Melquiond
2015-03-11admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Enrico Tassi
2015-01-12Update headers.Maxime Dénès
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-06-17Removing dead code.Pierre-Marie Pédrot
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-04-02Better error message when found more than once object of name ...Pierre Boutillier
2013-10-23cList: a few alternative to hashtbl-based uniquize, distinct, subsetletouzey
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-22Less "Coq" strings everywhereletouzey
2013-08-08Side effect free implementation of admit (Isabelle's oracle)gareuselesinge
2013-06-02Modest protection against "injection" and co raising anomaly inherbelin
2013-03-12Hipattern : consider jmeq only when Logic.JMeq is loadedletouzey
2013-02-27Coqlib: minor simplificationsletouzey
2013-02-19Dir_path --> DirPathletouzey
2013-02-18use List.rev_map whenever possibleletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-14Modulification of dir_pathppedrot
2012-12-14Modulification of identifierppedrot
2012-11-25Monomorphization (interp)ppedrot
2012-09-14Moving Utils.list_* to a proper CList module, which includes stdlibppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-06-22Added an indirection with respect to Loc in Compat. As many [open Compat]ppedrot
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-02Noise for nothingpboutill
2011-07-16Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...herbelin
2011-05-26Fixing discriminate for identity.herbelin
2011-05-05Definitions of positive, N, Z moved in Numbers/BinNums.vletouzey
2011-01-31Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"letouzey
2010-11-02Move stuff about positive into a distinct PArith subdirletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-30Move [delayed] to util and use [force_delayed] everywhere to forcemsozeau
2010-06-12Fixing spelling: pr_coma -> pr_commaherbelin
2010-05-20Fix bug 2307pboutill
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-10-21This big commit addresses two problems:soubiran
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-09-11Generalized the possibility to refer to a global name by a notationherbelin
2009-08-06- Cleaning phase of the interfaces of libnames.ml and nametab.mlherbelin
2009-08-03Added "etransitivity".herbelin
2009-05-09- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceherbelin
2009-01-01Switched to "standardized" names for the properties of eq andherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 12:29:02 +0000