index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
coqlib.mli
Commit message (
Expand
)
Author
Age
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Misc changes around coqtop.ml :
letouzey
2013-08-22
*
Less "Coq" strings everywhere
letouzey
2013-08-22
*
Side effect free implementation of admit (Isabelle's oracle)
gareuselesinge
2013-08-08
*
Hipattern : consider jmeq only when Logic.JMeq is loaded
letouzey
2013-03-12
*
Dir_path --> DirPath
letouzey
2013-02-19
*
Modulification of dir_path
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...
herbelin
2011-07-16
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Move [delayed] to util and use [force_delayed] everywhere to force
msozeau
2010-06-30
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
*
Various minor improvements of comments in mli for ocamldoc
letouzey
2010-04-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Move from ocamlweb to ocamdoc to generate mli documentation
pboutill
2010-04-29
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
Added "etransitivity".
herbelin
2009-08-03
*
- Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence
herbelin
2009-05-09
*
Switched to "standardized" names for the properties of eq and
herbelin
2009-01-01
*
Added the automatic generation of the boolean equality if possible and the
vsiles
2007-10-05
*
Addition of a "Combined Scheme" vernacular command for building the conjuncti...
msozeau
2006-12-23
*
- Documentation of the Program tactics.
msozeau
2006-04-07
*
Ajout nat_path et find_reference
herbelin
2006-02-04
*
exporting the global reference to the inductive " \/ " in coqlib and
bertot
2006-01-25
*
Ajout booléens; nettoyage
herbelin
2005-12-30
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
Nouvelle en-tête
herbelin
2004-07-16
*
Controle par le prefixe et plus par le nom absolu pour la recherche d'objets ...
herbelin
2003-11-01
*
Un peu plus de souplesse dans la globalisation des noms utilises par les tact...
herbelin
2003-09-26
*
Restructuration des procédures de filtrage
herbelin
2003-05-19
*
factorisation des "constant" dans les contrib/* ( maintenant dans coqlib )
corbinea
2003-03-31
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14