X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineReduction.ml;h=e43f9221c2d0a503cb46b6a2c145d4fac3438cc9;hb=eac74259f5a0aaa8056791876284c897a6827c24;hp=e53d69048dd0261210b71aee19bff913305467a5;hpb=218c0062f93dd3221b0266cfbc26fd9cf787ad18;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index e53d69048..e43f9221c 100644
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -394,10 +394,10 @@ let reduce context =
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-         | C.Variable (_,None,_,_) ->
+         | C.Variable (_,None,_,_,_) ->
             let t' = C.Var (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)
-         | C.Variable (_,Some body,_,_) ->
+         | C.Variable (_,Some body,_,_,_) ->
             (reduceaux context l
               (CicSubstitution.subst_vars exp_named_subst' body))
        )
@@ -432,14 +432,14 @@ let reduce context =
        in
         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	  match o with
-            C.Constant (_,Some body,_,_) ->
+            C.Constant (_,Some body,_,_,_) ->
              (reduceaux context l
                (CicSubstitution.subst_vars exp_named_subst' body))
-          | C.Constant (_,None,_,_) ->
+          | C.Constant (_,None,_,_,_) ->
              let t' = C.Const (uri,exp_named_subst') in
               if l = [] then t' else C.Appl (t'::l)
           | C.Variable _ -> raise ReferenceToVariable
-          | C.CurrentProof (_,_,body,_,_) ->
+          | C.CurrentProof (_,_,body,_,_,_) ->
              (reduceaux context l
                (CicSubstitution.subst_vars exp_named_subst' body))
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -494,7 +494,7 @@ let reduce context =
              let (arity, r) =
 	       let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph mutind in
 		 match o with
-                     C.InductiveDefinition (tl,_,r) ->
+                     C.InductiveDefinition (tl,_,r,_) ->
                        let (_,_,arity,_) = List.nth tl i in
 			 (arity,r)
 		   | _ -> raise WrongUriToInductiveDefinition
@@ -620,10 +620,10 @@ let simpl context =
             C.Constant _ -> raise ReferenceToConstant
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
-          | C.Variable (_,None,_,_) ->
+          | C.Variable (_,None,_,_,_) ->
             let t' = C.Var (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)
-          | C.Variable (_,Some body,_,_) ->
+          | C.Variable (_,Some body,_,_,_) ->
              reduceaux context l
               (CicSubstitution.subst_vars exp_named_subst' body)
         )
@@ -658,15 +658,15 @@ let simpl context =
        in
         (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
 	  match o with
-           C.Constant (_,Some body,_,_) ->
+           C.Constant (_,Some body,_,_,_) ->
             try_delta_expansion l
              (C.Const (uri,exp_named_subst'))
              (CicSubstitution.subst_vars exp_named_subst' body)
-         | C.Constant (_,None,_,_) ->
+         | C.Constant (_,None,_,_,_) ->
             let t' = C.Const (uri,exp_named_subst') in
              if l = [] then t' else C.Appl (t'::l)
          | C.Variable _ -> raise ReferenceToVariable
-         | C.CurrentProof (_,_,body,_,_) -> reduceaux context l body
+         | C.CurrentProof (_,_,body,_,_,_) -> reduceaux context l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
     | C.MutInd (uri,i,exp_named_subst) ->
@@ -717,7 +717,7 @@ let simpl context =
              let (arity, r) =
 	       let o,_ = CicEnvironment.get_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