attributes support

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

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e456a1731b226d3e66cd4718a12aeb19dab0f165..0610504c4faeaa389c8c65e6ea804acb1542d6fe 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -38,7 +38,7 @@ let debug t env s =
  let rec debug_aux t i =
   let module C = Cic in
   let module U = UriManager in
-   CicPp.ppobj (C.Variable ("DEBUG", None, t, [])) ^ "\n" ^ i
+   CicPp.ppobj (C.Variable ("DEBUG", None, t, [], [])) ^ "\n" ^ i
  in
   if !fdebug = 0 then
    prerr_endline (s ^ "\n" ^ List.fold_right debug_aux (t::env) "")
@@ -358,7 +358,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
            in
            (match o with
                C.Constant _ -> raise ReferenceToConstant
-             | C.Variable (_,_,_,params) -> params
+             | C.Variable (_,_,_,params,_) -> params
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
@@ -389,9 +389,9 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
              CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
            in
            (match o with
-               C.Constant (_,_,_,params) -> params
+               C.Constant (_,_,_,params,_) -> params
              | C.Variable _ -> raise ReferenceToVariable
-             | C.CurrentProof (_,_,_,_,params) -> params
+             | C.CurrentProof (_,_,_,_,params,_) -> params
              | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
            )
           in
@@ -408,7 +408,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_) -> params
+             | C.InductiveDefinition (_,params,_,_) -> params
            )
           in
            let exp_named_subst' =
@@ -424,7 +424,7 @@ prerr_endline ("%%%%%UWVAR " ^ String.concat " ; " (List.map (function (uri,t) -
                C.Constant _ -> raise ReferenceToConstant
              | C.Variable _ -> raise ReferenceToVariable
              | C.CurrentProof _ -> raise ReferenceToCurrentProof
-             | C.InductiveDefinition (_,params,_) -> params
+             | C.InductiveDefinition (_,params,_,_) -> params
            )
           in
            let exp_named_subst' =
@@ -549,11 +549,11 @@ if List.mem uri params then prerr_endline "---- OK2" ;
               C.Constant _ -> raise ReferenceToConstant
             | C.CurrentProof _ -> raise ReferenceToCurrentProof
             | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-            | C.Variable (_,None,_,_) ->
+            | C.Variable (_,None,_,_,_) ->
                let t' = unwind k e ens t in
                 if s = [] then t' else
                  C.Appl (t'::(RS.from_stack_list ~unwind s))
-            | C.Variable (_,Some body,_,_) ->
+            | C.Variable (_,Some body,_,_,_) ->
                let ens' = push_exp_named_subst k e ens exp_named_subst in
                 reduce (0, [], ens', body, s)
           )
@@ -604,15 +604,15 @@ if List.mem uri params then prerr_endline "---- OK2" ;
           CicEnvironment.get_cooked_obj CicUniv.empty_ugraph uri
         in
          match o with
-            C.Constant (_,Some body,_,_) ->
+            C.Constant (_,Some body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s) 
-          | C.Constant (_,None,_,_) ->
+          | C.Constant (_,None,_,_,_) ->
              let t' = unwind k e ens t in
               if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))
           | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,body,_,_) ->
+          | C.CurrentProof (_,_,body,_,_,_) ->
              let ens' = push_exp_named_subst k e ens exp_named_subst in
               (* constants are closed *)
               reduce (0, [], ens', body, s)
@@ -662,7 +662,7 @@ if List.mem uri params then prerr_endline "---- OK2" ;
                  CicEnvironment.get_cooked_obj CicUniv.empty_ugraph mutind 
                in
                  match o with
-                      C.InductiveDefinition (tl,ingredients,r) ->
+                      C.InductiveDefinition (tl,ingredients,r,_) ->
                        let (_,_,arity,_) = List.nth tl i in
                          (arity,r)
                     | _ -> raise WrongUriToInductiveDefinition