From: Stefano Zacchiroli Date: Fri, 21 Jan 2005 09:33:11 +0000 (+0000) Subject: attributes support X-Git-Tag: V_0_1_0~104 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=d62461c7f4d79e6f87aa454dab636c2db3a3e7bc;p=helm.git attributes support --- diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml index b39d35f07..7237c8fb7 100644 --- a/helm/ocaml/cic_disambiguation/disambiguate.ml +++ b/helm/ocaml/cic_disambiguation/disambiguate.ml @@ -230,44 +230,23 @@ let interpretate ~context ~env ast = subst | None -> List.map (fun uri -> uri, Cic.Implicit None) uris) in - (* the try is for CicTypeChecker.typecheck *) (try match cic with | Cic.Const (uri, []) -> - let uris = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - (*match CicTypeChecker.typecheck uri with*) - | Cic.Constant (_, _, _, uris) -> uris - | _ -> assert false - in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o in Cic.Const (uri, mk_subst uris) | Cic.Var (uri, []) -> - let uris = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - (*match CicTypeChecker.typecheck uri with*) - | Cic.Variable (_, _, _, uris) -> uris - | _ -> assert false - in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o in Cic.Var (uri, mk_subst uris) | Cic.MutInd (uri, i, []) -> - let uris = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - (*match CicTypeChecker.typecheck uri with*) - | Cic.InductiveDefinition (_, uris, _) -> uris - | _ -> assert false - in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o in Cic.MutInd (uri, i, mk_subst uris) | Cic.MutConstruct (uri, i, j, []) -> - let uris = - let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in - match o with - (*match CicTypeChecker.typecheck uri with*) - | Cic.InductiveDefinition (_, uris, _) -> uris - | _ -> assert false - in + let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in + let uris = CicUtil.params_of_obj o in Cic.MutConstruct (uri, i, j, mk_subst uris) | Cic.Meta _ | Cic.Implicit _ as t -> (* @@ -623,6 +602,6 @@ module Make (C: Callbacks) = res with CicEnvironment.CircularDependency s -> - raise (Failure "e chi la becca sta CircularDependency?"); + failwith "Disambiguate: circular dependency" end