index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
proofs
/
proof_type.mli
Commit message (
Expand
)
Author
Age
*
Nouvelle tactique primitive ThinBody et nouvelles tactiques utilisateurs 'Cle...
herbelin
2001-10-05
*
Ajout tactique TrueCut qui fait la coupure du calcul des séquents; nouvelle ...
herbelin
2001-08-07
*
Les réduction dans les hypothèses s'appliquent maintenant au corps de la dÃ...
herbelin
2001-06-25
*
Ajout de _ dans les patterns d'intro
mohring
2001-04-12
*
amelioration de la structure des univers
barras
2001-03-28
*
entetes
filliatr
2001-03-15
*
Déplacement de qualid dans Nametab, hors du noyau
herbelin
2001-03-01
*
Prise en compte noms longs dans SuperAuto
herbelin
2001-02-16
*
Documentation
herbelin
2000-12-18
*
syntaxe AST Inversion + commentaires ocamlweb autour de $
filliatr
2000-12-12
*
Portage d'AutoRewrite
delahaye
2000-12-02
*
Renommage canonique :
herbelin
2000-10-18
*
Nettoyage pretyping; ise_resolve_* devient understand_*; Ajout d'une notion d...
herbelin
2000-09-26
*
Pattern matching de sous-termes
delahaye
2000-08-17
*
Modifs de presentation.
delahaye
2000-06-28
*
portage EAuto et Ring
filliatr
2000-06-21
*
diverses modifs pour ocamlweb
filliatr
2000-05-03
*
Ajout du langage de tactiques
delahaye
2000-05-03