index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
inv.ml
Commit message (
Expand
)
Author
Age
*
print_id, print_sp -> pr_id, pr_sp
herbelin
2000-11-23
*
suppression des (* open Generic *)
filliatr
2000-11-02
*
Renommage canonique :
herbelin
2000-10-18
*
Prise en compte de Let à certains endroits
herbelin
2000-10-11
*
Bug ordre dans push_rels
herbelin
2000-10-10
*
Code mort
herbelin
2000-10-01
*
Abstraction de constr
herbelin
2000-09-14
*
Correction pour make doc
herbelin
2000-09-10
*
Ajout d'un LetIn primitif.
herbelin
2000-09-10
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Plus de env et sigma dans get_arity, plus de sigma dans make_arity
herbelin
2000-07-01
*
Extension de find_inductive aux co-inductifs et renommage en find_rectype
herbelin
2000-07-01
*
Retrait des lam_and_pop and co
herbelin
2000-06-03
*
suppression de l'env/sigma dans les fonctions de reduction beta et iota seuls
herbelin
2000-05-22
*
bugs
herbelin
2000-05-18
*
Nettoyage
herbelin
2000-05-18
*
Intégration de leminv
herbelin
2000-05-05
*
les erreurs
herbelin
2000-05-04
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
Intégration progressive
herbelin
2000-04-30
*
Inversion (pas termine)
filliatr
2000-03-27