attributes support

[helm.git] / helm / ocaml / cic_unification / cicRefine.ml

diff --git a/helm/ocaml/cic_unification/cicRefine.ml b/helm/ocaml/cic_unification/cicRefine.ml
index 24171327c80adce776de9ada770c26ffd62e43fc..fe70f250aa89999161824cf26d08639dc18739a7 100644 (file)
--- a/helm/ocaml/cic_unification/cicRefine.ml
+++ b/helm/ocaml/cic_unification/cicRefine.ml
@@ -76,8 +76,8 @@ let rec type_of_constant uri ugraph =
     *)
   let obj,u= CicEnvironment.get_obj ugraph uri in
     match obj with
-       C.Constant (_,_,ty,_) -> ty,u
-      | C.CurrentProof (_,_,_,ty,_) -> ty,u
+       C.Constant (_,_,ty,_,_) -> ty,u
+      | C.CurrentProof (_,_,_,ty,_,_) -> ty,u
       | _ ->
          raise
            (RefineFailure ("Unknown constant definition " ^  U.string_of_uri uri))
@@ -95,7 +95,7 @@ and type_of_variable uri ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-       C.Variable (_,_,ty,_) -> ty,u
+       C.Variable (_,_,ty,_,_) -> ty,u
       |  _ ->
           raise
            (RefineFailure
@@ -114,7 +114,7 @@ and type_of_mutual_inductive_defs uri i ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-       C.InductiveDefinition (dl,_,_) ->
+       C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,arity,_) = List.nth dl i in
            arity,u
       | _ ->
@@ -135,7 +135,7 @@ and type_of_mutual_inductive_constr uri i j ugraph =
     *)
   let obj,u = CicEnvironment.get_obj ugraph uri in
     match obj with
-       C.InductiveDefinition (dl,_,_) ->
+       C.InductiveDefinition (dl,_,_,_) ->
          let (_,_,_,cl) = List.nth dl i in
           let (_,ty) = List.nth cl (j-1) in
             ty,u
@@ -366,7 +366,7 @@ and type_of_aux' metasenv context t ugraph =
              *)
              let obj,u = CicEnvironment.get_obj ugraph uri in
               match obj with
-                 C.InductiveDefinition (l,expl_params,parsno) -> 
+                 C.InductiveDefinition (l,expl_params,parsno,_) -> 
                    List.nth l i , expl_params, parsno, u
                | _ ->
                    raise