index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
pretyping
/
retyping.ml
Commit message (
Expand
)
Author
Age
...
*
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-07-24
*
Modifs d'interpretation de patterns
delahaye
2000-07-21
*
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
*
Achèvement abstraction du mécanisme (optionnel) de cast
herbelin
2000-06-29
*
Mise en place d'un choix constr/typed_type en remplacement de certains Cast
herbelin
2000-06-01
*
Nettoyage de Generic
herbelin
2000-05-31
*
Effets de bords suite à la restructuration des inductives (cf Inductive)
herbelin
2000-05-18
*
Réorganisation
herbelin
2000-05-05
*
Renommage try_mutind_of en find_inductive (on fait ce qu'on peut !)
herbelin
2000-05-04
*
Ajout du langage de tactiques
delahaye
2000-05-03
*
Extension du case_info : ajout du nombre de vrais args de chaque constr pour ...
herbelin
2000-03-21
*
MAJ nouveau try_mutind_of
herbelin
2000-03-08
*
Nouveaux types 'constructor' et 'inductive' dans Term;
herbelin
1999-12-15
*
Intégration initiale du Cases
herbelin
1999-12-11
*
Ajout des messages d'erreurs de Cases
herbelin
1999-12-09
*
Retour dans pretyping
herbelin
1999-12-01
[prev]