X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=0610504c4faeaa389c8c65e6ea804acb1542d6fe;hb=fdd8107cc53f5e862004aa5fcd48593ee5634234;hp=e456a1731b226d3e66cd4718a12aeb19dab0f165;hpb=218c0062f93dd3221b0266cfbc26fd9cf787ad18;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index e456a1731..0610504c4 100644
--- 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