From 376e61185dadea415d6b7d2df45dc7236e901e5b Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 6 May 2008 18:31:25 +0000 Subject: checker deals with polymorphic constants and module aliases git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10892 85f007b7-540e-0410-9357-904b9bb8a0f7 --- checker/.depend | 166 +++++++++++++++++++++++++++----------------------------- 1 file changed, 81 insertions(+), 85 deletions(-) (limited to 'checker/.depend') diff --git a/checker/.depend b/checker/.depend index d9c48a282..dade1591b 100644 --- a/checker/.depend +++ b/checker/.depend @@ -1,9 +1,9 @@ -checker.cmo: ../lib/util.cmi univ.cmi type_errors.cmi \ +checker.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \ /usr/lib/ocaml/camlp4/token.cmi ../kernel/term.cmi ../lib/system.cmi \ /usr/lib/ocaml/camlp4/stdpp.cmi safe_typing.cmi ../lib/pp.cmi \ ../kernel/names.cmi indtypes.cmi ../lib/flags.cmi declarations.cmi \ ../config/coq_config.cmi check_stat.cmi check.cmo -checker.cmx: ../lib/util.cmx univ.cmx type_errors.cmx \ +checker.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \ /usr/lib/ocaml/camlp4/token.cmi ../kernel/term.cmx ../lib/system.cmx \ /usr/lib/ocaml/camlp4/stdpp.cmi safe_typing.cmx ../lib/pp.cmi \ ../kernel/names.cmx indtypes.cmx ../lib/flags.cmx declarations.cmx \ @@ -13,108 +13,104 @@ check.cmo: ../lib/util.cmi ../lib/system.cmi safe_typing.cmi ../lib/pp.cmi \ check.cmx: ../lib/util.cmx ../lib/system.cmx safe_typing.cmx ../lib/pp.cmi \ ../kernel/names.cmx ../lib/flags.cmx check_stat.cmo: ../lib/util.cmi ../kernel/term.cmi ../lib/system.cmi \ - safe_typing.cmi ../lib/pp.cmi ../kernel/names.cmi ../kernel/environ.cmi \ - declarations.cmi check_stat.cmi + safe_typing.cmi ../lib/pp.cmi ../kernel/names.cmi indtypes.cmi \ + ../lib/flags.cmi ../kernel/environ.cmi declarations.cmi check_stat.cmi check_stat.cmx: ../lib/util.cmx ../kernel/term.cmx ../lib/system.cmx \ - safe_typing.cmx ../lib/pp.cmi ../kernel/names.cmx ../kernel/environ.cmx \ - declarations.cmx check_stat.cmi + safe_typing.cmx ../lib/pp.cmi ../kernel/names.cmx indtypes.cmx \ + ../lib/flags.cmx ../kernel/environ.cmx declarations.cmx check_stat.cmi closure.cmo: ../lib/util.cmi ../kernel/term.cmi ../lib/pp.cmi \ - ../kernel/names.cmi esubst.cmi ../kernel/environ.cmi closure.cmi + ../kernel/names.cmi ../kernel/esubst.cmi ../kernel/environ.cmi \ + closure.cmi closure.cmx: ../lib/util.cmx ../kernel/term.cmx ../lib/pp.cmi \ - ../kernel/names.cmx esubst.cmx ../kernel/environ.cmx closure.cmi -closure.cmi: ../kernel/term.cmi ../lib/pp.cmi ../kernel/names.cmi esubst.cmi \ - ../kernel/environ.cmi -declarations.cmo: ../lib/util.cmi univ.cmi ../kernel/term.cmi \ + ../kernel/names.cmx ../kernel/esubst.cmx ../kernel/environ.cmx \ + closure.cmi +closure.cmi: ../kernel/term.cmi ../lib/pp.cmi ../kernel/names.cmi \ + ../kernel/esubst.cmi ../kernel/environ.cmi +declarations.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ ../lib/rtree.cmi ../lib/option.cmi ../kernel/names.cmi declarations.cmi -declarations.cmx: ../lib/util.cmx univ.cmx ../kernel/term.cmx \ +declarations.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \ ../lib/rtree.cmx ../lib/option.cmx ../kernel/names.cmx declarations.cmi -declarations.cmi: ../lib/util.cmi univ.cmi ../kernel/term.cmi \ +declarations.cmi: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ ../lib/rtree.cmi ../kernel/names.cmi -environ.cmo: ../lib/util.cmi univ.cmi ../kernel/term.cmi ../kernel/names.cmi \ - declarations.cmi -environ.cmx: ../lib/util.cmx univ.cmx ../kernel/term.cmx ../kernel/names.cmx \ - declarations.cmx -esubst.cmo: ../lib/util.cmi esubst.cmi -esubst.cmx: ../lib/util.cmx esubst.cmi -esubst.cmi: ../lib/util.cmi -indtypes.cmo: ../lib/util.cmi univ.cmi typeops.cmi ../kernel/term.cmi \ - ../lib/rtree.cmi reduction.cmi ../lib/pp.cmi ../kernel/names.cmi \ - inductive.cmi ../lib/flags.cmi ../kernel/environ.cmi declarations.cmi \ - indtypes.cmi -indtypes.cmx: ../lib/util.cmx univ.cmx typeops.cmx ../kernel/term.cmx \ - ../lib/rtree.cmx reduction.cmx ../lib/pp.cmi ../kernel/names.cmx \ - inductive.cmx ../lib/flags.cmx ../kernel/environ.cmx declarations.cmx \ - indtypes.cmi -indtypes.cmi: univ.cmi typeops.cmi ../kernel/term.cmi ../kernel/names.cmi \ - ../kernel/environ.cmi declarations.cmi -inductive.cmo: ../lib/util.cmi univ.cmi type_errors.cmi ../kernel/term.cmi \ - ../lib/rtree.cmi reduction.cmi ../kernel/names.cmi ../kernel/environ.cmi \ - declarations.cmi inductive.cmi -inductive.cmx: ../lib/util.cmx univ.cmx type_errors.cmx ../kernel/term.cmx \ - ../lib/rtree.cmx reduction.cmx ../kernel/names.cmx ../kernel/environ.cmx \ - declarations.cmx inductive.cmi -inductive.cmi: univ.cmi ../kernel/term.cmi ../kernel/names.cmi \ +environ.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ + ../kernel/names.cmi declarations.cmi +environ.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \ + ../kernel/names.cmx declarations.cmx +indtypes.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \ + ../kernel/term.cmi ../lib/rtree.cmi reduction.cmi ../lib/pp.cmi \ + ../kernel/names.cmi inductive.cmi ../lib/flags.cmi ../kernel/environ.cmi \ + declarations.cmi indtypes.cmi +indtypes.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \ + ../kernel/term.cmx ../lib/rtree.cmx reduction.cmx ../lib/pp.cmi \ + ../kernel/names.cmx inductive.cmx ../lib/flags.cmx ../kernel/environ.cmx \ + declarations.cmx indtypes.cmi +indtypes.cmi: ../kernel/univ.cmi typeops.cmi ../kernel/term.cmi ../lib/pp.cmi \ + ../kernel/names.cmi ../kernel/environ.cmi declarations.cmi +inductive.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \ + ../kernel/term.cmi ../lib/rtree.cmi reduction.cmi ../kernel/names.cmi \ + ../kernel/environ.cmi declarations.cmi inductive.cmi +inductive.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \ + ../kernel/term.cmx ../lib/rtree.cmx reduction.cmx ../kernel/names.cmx \ + ../kernel/environ.cmx declarations.cmx inductive.cmi +inductive.cmi: ../kernel/univ.cmi ../kernel/term.cmi ../kernel/names.cmi \ ../kernel/environ.cmi declarations.cmi main.cmo: checker.cmo main.cmx: checker.cmx -mod_checking.cmo: ../lib/util.cmi univ.cmi typeops.cmi ../kernel/term.cmi \ - subtyping.cmi reduction.cmi ../lib/pp.cmi ../kernel/names.cmi modops.cmi \ - inductive.cmi indtypes.cmi ../lib/flags.cmi ../kernel/environ.cmi \ - declarations.cmi -mod_checking.cmx: ../lib/util.cmx univ.cmx typeops.cmx ../kernel/term.cmx \ - subtyping.cmx reduction.cmx ../lib/pp.cmi ../kernel/names.cmx modops.cmx \ - inductive.cmx indtypes.cmx ../lib/flags.cmx ../kernel/environ.cmx \ - declarations.cmx -modops.cmo: ../lib/util.cmi univ.cmi ../kernel/term.cmi ../lib/pp.cmi \ - ../lib/option.cmi ../kernel/names.cmi ../kernel/environ.cmi \ +mod_checking.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \ + ../kernel/term.cmi subtyping.cmi reduction.cmi ../lib/pp.cmi \ + ../kernel/names.cmi modops.cmi inductive.cmi indtypes.cmi \ + ../lib/flags.cmi ../kernel/environ.cmi declarations.cmi +mod_checking.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \ + ../kernel/term.cmx subtyping.cmx reduction.cmx ../lib/pp.cmi \ + ../kernel/names.cmx modops.cmx inductive.cmx indtypes.cmx \ + ../lib/flags.cmx ../kernel/environ.cmx declarations.cmx +modops.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ + ../lib/pp.cmi ../lib/option.cmi ../kernel/names.cmi ../kernel/environ.cmi \ declarations.cmi modops.cmi -modops.cmx: ../lib/util.cmx univ.cmx ../kernel/term.cmx ../lib/pp.cmi \ - ../lib/option.cmx ../kernel/names.cmx ../kernel/environ.cmx \ +modops.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \ + ../lib/pp.cmi ../lib/option.cmx ../kernel/names.cmx ../kernel/environ.cmx \ declarations.cmx modops.cmi -modops.cmi: ../lib/util.cmi univ.cmi ../kernel/term.cmi ../kernel/names.cmi \ - ../kernel/environ.cmi declarations.cmi -reduction.cmo: ../lib/util.cmi univ.cmi ../kernel/term.cmi \ - ../kernel/names.cmi esubst.cmi ../kernel/environ.cmi closure.cmi \ - reduction.cmi -reduction.cmx: ../lib/util.cmx univ.cmx ../kernel/term.cmx \ - ../kernel/names.cmx esubst.cmx ../kernel/environ.cmx closure.cmx \ - reduction.cmi +modops.cmi: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ + ../kernel/names.cmi ../kernel/environ.cmi declarations.cmi +reduction.cmo: ../lib/util.cmi ../kernel/univ.cmi ../kernel/term.cmi \ + ../kernel/names.cmi ../kernel/esubst.cmi ../kernel/environ.cmi \ + closure.cmi reduction.cmi +reduction.cmx: ../lib/util.cmx ../kernel/univ.cmx ../kernel/term.cmx \ + ../kernel/names.cmx ../kernel/esubst.cmx ../kernel/environ.cmx \ + closure.cmx reduction.cmi reduction.cmi: ../kernel/term.cmi ../kernel/environ.cmi safe_typing.cmo: validate.cmo ../lib/util.cmi ../lib/pp.cmi ../lib/option.cmi \ - ../kernel/names.cmi modops.cmi mod_checking.cmo ../kernel/environ.cmi \ - declarations.cmi safe_typing.cmi + ../kernel/names.cmi modops.cmi mod_checking.cmo ../lib/flags.cmi \ + ../kernel/environ.cmi declarations.cmi safe_typing.cmi safe_typing.cmx: validate.cmx ../lib/util.cmx ../lib/pp.cmi ../lib/option.cmx \ - ../kernel/names.cmx modops.cmx mod_checking.cmx ../kernel/environ.cmx \ - declarations.cmx safe_typing.cmi -safe_typing.cmi: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi \ - declarations.cmi -subtyping.cmo: ../lib/util.cmi univ.cmi typeops.cmi ../kernel/term.cmi \ - reduction.cmi ../lib/pp.cmi ../kernel/names.cmi modops.cmi inductive.cmi \ - ../kernel/environ.cmi declarations.cmi subtyping.cmi -subtyping.cmx: ../lib/util.cmx univ.cmx typeops.cmx ../kernel/term.cmx \ - reduction.cmx ../lib/pp.cmi ../kernel/names.cmx modops.cmx inductive.cmx \ - ../kernel/environ.cmx declarations.cmx subtyping.cmi -subtyping.cmi: univ.cmi ../kernel/term.cmi ../kernel/environ.cmi \ + ../kernel/names.cmx modops.cmx mod_checking.cmx ../lib/flags.cmx \ + ../kernel/environ.cmx declarations.cmx safe_typing.cmi +safe_typing.cmi: ../kernel/term.cmi ../lib/system.cmi ../kernel/names.cmi \ + ../kernel/environ.cmi declarations.cmi +subtyping.cmo: ../lib/util.cmi ../kernel/univ.cmi typeops.cmi \ + ../kernel/term.cmi reduction.cmi ../lib/pp.cmi ../kernel/names.cmi \ + modops.cmi inductive.cmi ../kernel/environ.cmi declarations.cmi \ + subtyping.cmi +subtyping.cmx: ../lib/util.cmx ../kernel/univ.cmx typeops.cmx \ + ../kernel/term.cmx reduction.cmx ../lib/pp.cmi ../kernel/names.cmx \ + modops.cmx inductive.cmx ../kernel/environ.cmx declarations.cmx \ + subtyping.cmi +subtyping.cmi: ../kernel/univ.cmi ../kernel/term.cmi ../kernel/environ.cmi \ declarations.cmi -term.cmo: ../lib/util.cmi univ.cmi ../lib/pp.cmi ../lib/option.cmi \ - ../kernel/names.cmi esubst.cmi -term.cmx: ../lib/util.cmx univ.cmx ../lib/pp.cmi ../lib/option.cmx \ - ../kernel/names.cmx esubst.cmx +term.cmo: ../lib/util.cmi ../kernel/univ.cmi ../lib/pp.cmi ../lib/option.cmi \ + ../kernel/names.cmi ../kernel/esubst.cmi +term.cmx: ../lib/util.cmx ../kernel/univ.cmx ../lib/pp.cmi ../lib/option.cmx \ + ../kernel/names.cmx ../kernel/esubst.cmx type_errors.cmo: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi \ type_errors.cmi type_errors.cmx: ../kernel/term.cmx ../kernel/names.cmx ../kernel/environ.cmx \ type_errors.cmi type_errors.cmi: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi -typeops.cmo: ../lib/util.cmi univ.cmi type_errors.cmi ../kernel/term.cmi \ - reduction.cmi ../kernel/names.cmi inductive.cmi ../kernel/environ.cmi \ - declarations.cmi typeops.cmi -typeops.cmx: ../lib/util.cmx univ.cmx type_errors.cmx ../kernel/term.cmx \ - reduction.cmx ../kernel/names.cmx inductive.cmx ../kernel/environ.cmx \ - declarations.cmx typeops.cmi +typeops.cmo: ../lib/util.cmi ../kernel/univ.cmi type_errors.cmi \ + ../kernel/term.cmi reduction.cmi ../kernel/names.cmi inductive.cmi \ + ../kernel/environ.cmi declarations.cmi typeops.cmi +typeops.cmx: ../lib/util.cmx ../kernel/univ.cmx type_errors.cmx \ + ../kernel/term.cmx reduction.cmx ../kernel/names.cmx inductive.cmx \ + ../kernel/environ.cmx declarations.cmx typeops.cmi typeops.cmi: ../kernel/term.cmi ../kernel/names.cmi ../kernel/environ.cmi \ declarations.cmi -univ.cmo: ../lib/util.cmi ../lib/pp.cmi ../lib/option.cmi ../kernel/names.cmi \ - univ.cmi -univ.cmx: ../lib/util.cmx ../lib/pp.cmi ../lib/option.cmx ../kernel/names.cmx \ - univ.cmi -univ.cmi: ../lib/pp.cmi ../kernel/names.cmi -- cgit v1.2.3