Added universes handling. The PRE_UNIVERSES tag may help ;)

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

diff --git a/helm/ocaml/tactics/proofEngineReduction.ml b/helm/ocaml/tactics/proofEngineReduction.ml
index 99eb43f6a56e65e8419b090e43a0d2016dd6651b..e7975793fa748d8d4f8cd46720f0aa7ec0b015ee 100644 (file)
--- a/helm/ocaml/tactics/proofEngineReduction.ml
+++ b/helm/ocaml/tactics/proofEngineReduction.ml
@@ -389,7 +389,8 @@ let reduce context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-       (match CicEnvironment.get_obj uri with
+       (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+        match o with
            C.Constant _ -> raise ReferenceToConstant
          | C.CurrentProof _ -> raise ReferenceToCurrentProof
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -429,7 +430,8 @@ let reduce context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (match CicEnvironment.get_obj uri with
+        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+         match o with
             C.Constant (_,Some body,_,_) ->
              (reduceaux context l
                (CicSubstitution.subst_vars exp_named_subst' body))
@@ -490,11 +492,12 @@ let reduce context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              match CicEnvironment.get_obj mutind with
-                 C.InductiveDefinition (tl,_,r) ->
-                   let (_,_,arity,_) = List.nth tl i in
-                    (arity,r)
-               | _ -> raise WrongUriToInductiveDefinition
+              let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+                match o with
+                     C.InductiveDefinition (tl,_,r) ->
+                       let (_,_,arity,_) = List.nth tl i in
+                        (arity,r)
+                  | _ -> raise WrongUriToInductiveDefinition
              in
               let ts =
                let rec eat_first =
@@ -612,7 +615,8 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (match CicEnvironment.get_obj uri with
+        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+         match o with
             C.Constant _ -> raise ReferenceToConstant
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
           | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
@@ -652,7 +656,8 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (match CicEnvironment.get_obj uri with
+        (let o,_ = CicEnvironment.get_obj uri CicUniv.empty_ugraph in
+         match o with
            C.Constant (_,Some body,_,_) ->
             try_delta_expansion l
              (C.Const (uri,exp_named_subst'))
@@ -710,11 +715,12 @@ let simpl context =
             C.MutConstruct (_,_,j,_) -> reduceaux context l (List.nth pl (j-1))
           | C.Appl (C.MutConstruct (_,_,j,_) :: tl) ->
              let (arity, r) =
-              match CicEnvironment.get_obj mutind with
-                 C.InductiveDefinition (tl,ingredients,r) ->
-                   let (_,_,arity,_) = List.nth tl i in
-                    (arity,r)
-               | _ -> raise WrongUriToInductiveDefinition
+              let o,_ = CicEnvironment.get_obj mutind CicUniv.empty_ugraph in
+                match o with
+                     C.InductiveDefinition (tl,ingredients,r) ->
+                       let (_,_,arity,_) = List.nth tl i in
+                        (arity,r)
+                  | _ -> raise WrongUriToInductiveDefinition
              in
               let ts =
                let rec eat_first =