generate HTML templates using XSLT starting from a bunch of .src files

[helm.git] / helm / ocaml / tactics / proofEngineReduction.ml

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index e7975793fa748d8d4f8cd46720f0aa7ec0b015ee..e43f9221c2d0a503cb46b6a2c145d4fac3438cc9 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -389,15 +389,15 @@ let reduce context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-       (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+       (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
         match o with
            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))
        )
@@ -430,16 +430,16 @@ let reduce context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph 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
@@ -492,9 +492,9 @@ let reduce context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+              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
@@ -615,15 +615,15 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
          match o with
             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)
         )
@@ -656,17 +656,17 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph 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) ->
@@ -715,9 +715,9 @@ let simpl context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+              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