aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.ml
Commit message (Expand)AuthorAge
* Make the user_err header an optional parameter.Gravatar Emilio Jesus Gallego Arias2016-08-19
* Remove errorlabstrm in favor of user_errGravatar Emilio Jesus Gallego Arias2016-08-19
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Do not compose "str" and "to_string" whenever possible.Gravatar Guillaume Melquiond2015-12-22
|/
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Update headers.Gravatar Maxime Dénès2015-01-12
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Better error message when found more than once object of name ...Gravatar Pierre Boutillier2014-04-02
* cList: a few alternative to hashtbl-based uniquize, distinct, subsetGravatar letouzey2013-10-23
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
* Modest protection against "injection" and co raising anomaly inGravatar herbelin2013-06-02
* Hipattern : consider jmeq only when Logic.JMeq is loadedGravatar letouzey2013-03-12
* Coqlib: minor simplificationsGravatar letouzey2013-02-27
* Dir_path --> DirPathGravatar letouzey2013-02-19
* use List.rev_map whenever possibleGravatar letouzey2013-02-18
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (interp)Gravatar ppedrot2012-11-25
* Moving Utils.list_* to a proper CList module, which includes stdlibGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...Gravatar herbelin2011-07-16
* Fixing discriminate for identity.Gravatar herbelin2011-05-26
* Definitions of positive, N, Z moved in Numbers/BinNums.vGravatar letouzey2011-05-05
* Coqlib.gen_constant_in_modules can take a qualid string "Foo.bar"Gravatar letouzey2011-01-31
* Move stuff about positive into a distinct PArith subdirGravatar letouzey2010-11-02
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Move [delayed] to util and use [force_delayed] everywhere to forceGravatar msozeau2010-06-30
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Fix bug 2307Gravatar pboutill2010-05-20
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03