attributes support

[helm.git] / helm / ocaml / cic_proof_checking / cicUnivUtils.ml

diff --git a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
index c027194543abc4cc0d4bc5aa4aa448eb7d996bf4..a7861444ef5c43d4961d5a7f790fea67b8acfa08 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
+++ b/helm/ocaml/cic_proof_checking/cicUnivUtils.ml
@@ -54,7 +54,7 @@ let universes_of_obj uri t =
            don := u::!don;
             (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u)
               with
-               | C.InductiveDefinition (l,_,_) -> 
+               | C.InductiveDefinition (l,_,_,_) -> 
                   List.fold_left (
                     fun y (_,_,t,l') -> 
                       y @ (aux t) @ 
@@ -72,7 +72,7 @@ let universes_of_obj uri t =
          begin
            don := u::!don;
            (match fst(CicEnvironment.get_obj CicUniv.empty_ugraph u) with
-              | C.InductiveDefinition (l,_,_) -> 
+              | C.InductiveDefinition (l,_,_,_) -> 
                   List.fold_left (
                     fun x (_,_,_t,l') ->
                       x @ aux t @  
@@ -113,37 +113,37 @@ let universes_of_obj uri t =
        List.fold_left (fun x (_,b,c) -> x @ (aux b) @ (aux c)) [] funs
   and aux_obj ?(boo=false) (t,_)  = 
     (match t with
-        C.Constant (_,Some te,ty,v) -> aux te @ aux ty @
+        C.Constant (_,Some te,ty,v,_) -> aux te @ aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
           [] v
-       | C.Constant (_,None,ty,v) -> aux ty @
+       | C.Constant (_,None,ty,v,_) -> aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
             [] v
-       | C.CurrentProof (_,conjs,te,ty,v) -> aux te @ aux ty @
+       | C.CurrentProof (_,conjs,te,ty,v,_) -> aux te @ aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
             [] v
-       | C.Variable (_,Some bo,ty,v) -> aux bo @ aux ty @
+       | C.Variable (_,Some bo,ty,v,_) -> aux bo @ aux ty @
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
             [] v
-       | C.Variable (_,None ,ty,v) -> aux ty @ 
+       | C.Variable (_,None ,ty,v,_) -> aux ty @ 
            List.fold_left (
              fun l u ->
                l @ if eq u uri then [] else 
                  (aux_obj (CicEnvironment.get_obj CicUniv.empty_ugraph u)))
             [] v
-       | C.InductiveDefinition (l,v,_) -> 
+       | C.InductiveDefinition (l,v,_,_) -> 
           (List.fold_left (
              fun x (_,_,t,l') ->
                x @ aux t @ List.fold_left (