parameter sintax added to axiom statement

[helm.git] / helm / software / components / tactics / proofEngineReduction.ml

diff --git a/helm/software/components/tactics/proofEngineReduction.ml b/helm/software/components/tactics/proofEngineReduction.ml
index 3892ace35a14e49b9ad834b2f9de08ee5c93bc14..d5dbf9f35b51760559b50e78328dcaf9daa06595 100644 (file)
--- a/helm/software/components/tactics/proofEngineReduction.ml
+++ b/helm/software/components/tactics/proofEngineReduction.ml
@@ -417,7 +417,7 @@ let unfold ?what context where =
       with
          Failure _ -> assert false)
   | Cic.Const (uri,exp_named_subst) as t ->
-     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+     let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
       (match o with
           Cic.Constant (_,Some body,_,_,_) ->
            CicReduction.head_beta_reduce
@@ -428,7 +428,7 @@ let unfold ?what context where =
         | Cic.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
       )
   | Cic.Var (uri,exp_named_subst) as t ->
-     let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+     let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
       (match o with
           Cic.Constant _ -> raise ReferenceToConstant
         | Cic.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -512,7 +512,7 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
          match o with
             C.Constant _ -> raise ReferenceToConstant
           | C.CurrentProof _ -> raise ReferenceToCurrentProof
@@ -553,7 +553,7 @@ let simpl context =
        let exp_named_subst' =
         reduceaux_exp_named_subst context l exp_named_subst
        in
-        (let o,_ = CicEnvironment.get_obj CicUniv.empty_ugraph uri in
+        (let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
          match o with
            C.Constant (_,Some body,_,_,_) ->
             if List.exists is_active l then
@@ -612,7 +612,7 @@ 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 CicUniv.empty_ugraph mutind in
+              let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph mutind in
                 match o with
                      C.InductiveDefinition (tl,ingredients,r,_) ->
                        let (_,_,arity,_) = List.nth tl i in
@@ -870,7 +870,7 @@ let simpl context =
                        prerr_endline (CicPp.ppterm t2 ^ "\n");
                        let subst1, _, _ = 
                          CicUnification.fo_unif metasenv ctx t1 t2
-                           CicUniv.empty_ugraph
+                           CicUniv.oblivion_ugraph
                        in
                        prerr_endline "UNIFICANO\n\n\n";
                        subst := subst1;