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.ml
Commit message (
Expand
)
Author
Age
...
*
Suppression des stamps et donc des *_constraints
clrenard
2001-11-12
*
Suite de la suppression : enamed_declaration est remplace par evar_map.
clrenard
2001-11-06
*
Suppression des local_constraints, des ctxtty et du focus.
clrenard
2001-11-06
*
GROS COMMIT:
barras
2001-11-05
*
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
*
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
*
Ajout du langage de tactiques
delahaye
2000-05-03
[prev]