index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
pretyping
/
detyping.ml
Age
Commit message (
Expand
)
Author
2000-09-14
Abstraction de constr
herbelin
2000-09-12
Modification mkAppL; abstraction via kind_of_term; changement dans Reduction
herbelin
2000-09-10
Correction pour make doc
herbelin
2000-09-10
Suppression de Abst
herbelin
2000-09-10
Ajout d'un LetIn primitif.
herbelin
2000-07-24
Passage à des contextes de vars et de rels pouvant contenir des déclarations
herbelin
2000-05-31
Nettoyage de Generic
herbelin
2000-05-26
Modification messages d'erreurs, possibilité de n'importe quel constr dans l...
herbelin
2000-05-22
Suite restructuration inductifs; changement nom module Constant en Declarations
herbelin
2000-05-18
Effets de bords suite à la restructuration des inductives (cf Inductive)
herbelin
2000-05-02
Bug redondance entre 'RRef (RMeta _)' et 'PMeta _'
herbelin
2000-04-28
Changement de représentation du contexte des réf dans rawconstr et pattern
herbelin
2000-04-26
N'importe quel rawconstr maintenant dans le contexte d'une référence
herbelin
2000-03-21
Prise en compte nouveau case_info
herbelin
2000-01-26
Abstraction de l'implémentation des signatures de Sign en vue intégration d...
herbelin
2000-01-07
Traduction constr->rawconstr (avant dans Termast
herbelin