aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.ml
diff options
context:
space:
mode:
authorletouzey2001-11-12 09:37:43 +0000
committerletouzey2001-11-12 09:37:43 +0000
commit9d478de763bbc2088cd7250309b2a811a5bf8c57 (patch)
tree862fb8d645713160bc0214d4f764107401df2edf /pretyping/pretype_errors.ml
parent9fd56d7a7281edece40240d52d25b9144d12439e (diff)
Refonte de extraction.ml. Traitement dans mlutil.ml des Empty Inductive (Texn)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2181 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions