From: Stefano Zacchiroli <zack@upsilon.cc>
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