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
*
- 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