aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/coqlib.mli
Commit message (Expand)AuthorAge
* 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
* 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
* 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
* Hipattern : consider jmeq only when Logic.JMeq is loadedGravatar letouzey2013-03-12
* Dir_path --> DirPathGravatar letouzey2013-02-19
* Modulification of dir_pathGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* remove many excessive open Util & Errors in mli'sGravatar 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
* Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...Gravatar herbelin2011-07-16
* 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
* New script dev/tools/change-header to automatically update Coq files headers.Gravatar herbelin2010-06-22
* Various minor improvements of comments in mli for ocamldocGravatar letouzey2010-04-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Move from ocamlweb to ocamdoc to generate mli documentationGravatar pboutill2010-04-29
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Added "etransitivity".Gravatar herbelin2009-08-03
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Switched to "standardized" names for the properties of eq andGravatar herbelin2009-01-01
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
* Addition of a "Combined Scheme" vernacular command for building the conjuncti...Gravatar msozeau2006-12-23
* - Documentation of the Program tactics.Gravatar msozeau2006-04-07
* Ajout nat_path et find_referenceGravatar herbelin2006-02-04
* exporting the global reference to the inductive " \/ " in coqlib andGravatar bertot2006-01-25
* Ajout booléens; nettoyageGravatar herbelin2005-12-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Nettoyage et documentation de LibraryGravatar herbelin2005-02-06
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* Nouvelle en-têteGravatar herbelin2004-07-16
* Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...Gravatar herbelin2003-11-01
* Un peu plus de souplesse dans la globalisation des noms utilises par les tact...Gravatar herbelin2003-09-26
* Restructuration des procédures de filtrageGravatar herbelin2003-05-19
* factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )Gravatar corbinea2003-03-31
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14