attributes support

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index b39d35f070f68bce422c3ded19ecc7b729a9ed50..7237c8fb72d0d5acc664e438ac2a0795618dd4a3 100644 (file)
--- 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