From 30e8924209af6a016681d9edbf65cbb567ff35d6 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 28 Jun 2004 11:17:06 +0000 Subject: [PATCH] use get_obj to retrieve cic objects instead of typecheck --- helm/ocaml/cic_disambiguation/disambiguate.ml | 21 ++++++++++--------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index 637636e0b..d627c76e1 100644 --- 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 -- 2.39.2