use get_obj to retrieve cic objects instead of typecheck

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 637636e0b8b8146d62964eb8710cd7947f7bbc75..d627c76e10ccc346268614f3305e095ea8b62796 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -203,37 +203,38 @@ let interpretate ~context ~env ast =
                        raise DisambiguateChoices.Invalid_choice))
                   subst
             | None -> List.map (fun uri -> uri, Cic.Implicit None) uris)
-         in
-          (try
+          in
+          (* the try is for CicTypeChecker.typecheck *)
+          (try 
             match cic with
             | Cic.Const (uri, []) ->
                 let uris =
-                  (*match CicEnvironment.get_obj uri with*)
-                  match CicTypeChecker.typecheck uri with
+                  match CicEnvironment.get_obj uri with
+                  (*match CicTypeChecker.typecheck uri with*)
                   | Cic.Constant (_, _, _, uris) -> uris
                   | _ -> assert false
                 in
                 Cic.Const (uri, mk_subst uris)
             | Cic.Var (uri, []) ->
                 let uris =
-                  (*match CicEnvironment.get_obj uri with*)
-                  match CicTypeChecker.typecheck uri with
+                  match CicEnvironment.get_obj uri with
+                  (*match CicTypeChecker.typecheck uri with*)
                   | Cic.Variable (_, _, _, uris) -> uris
                   | _ -> assert false
                 in
                 Cic.Var (uri, mk_subst uris)
             | Cic.MutInd (uri, i, []) ->
                 let uris =
-                  (*match CicEnvironment.get_obj uri with*)
-                  match CicTypeChecker.typecheck uri with
+                  match CicEnvironment.get_obj uri with
+                  (*match CicTypeChecker.typecheck uri with*)
                   | Cic.InductiveDefinition (_, uris, _) -> uris
                   | _ -> assert false
                 in
                 Cic.MutInd (uri, i, mk_subst uris)
             | Cic.MutConstruct (uri, i, j, []) ->
                 let uris =
-                  (*match CicEnvironment.get_obj uri with*)
-                  match CicTypeChecker.typecheck uri with
+                  match CicEnvironment.get_obj uri with
+                  (*match CicTypeChecker.typecheck uri with*)
                   | Cic.InductiveDefinition (_, uris, _) -> uris
                   | _ -> assert false
                 in