]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_disambiguation/disambiguate.ml
new cicEnvironment implementation
[helm.git] / helm / ocaml / cic_disambiguation / disambiguate.ml
index 2eafc81f309d165ba136f48d61759b76fea5602f..b39d35f070f68bce422c3ded19ecc7b729a9ed50 100644 (file)
@@ -235,7 +235,7 @@ let interpretate ~context ~env ast =
             match cic with
             | Cic.Const (uri, []) ->
                 let uris =
-                 let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                   match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.Constant (_, _, _, uris) -> uris
@@ -244,7 +244,7 @@ let interpretate ~context ~env ast =
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
                 let uris =
-                 let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                   match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.Variable (_, _, _, uris) -> uris
@@ -253,7 +253,7 @@ let interpretate ~context ~env ast =
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                 let uris =
-                 let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                   match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.InductiveDefinition (_, uris, _) -> uris
@@ -262,7 +262,7 @@ let interpretate ~context ~env ast =
                 Cic.MutInd (uri, i, mk_subst uris)
             | Cic.MutConstruct (uri, i, j, []) ->
                 let uris =
-                 let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+                 let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
                   match o with
                   (*match CicTypeChecker.typecheck uri with*)
                   | Cic.InductiveDefinition (_, uris, _) -> uris