Added universes handling. The PRE_UNIVERSES tag may help ;)

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

diff --git a/helm/ocaml/tactics/equalityTactics.ml b/helm/ocaml/tactics/equalityTactics.ml
index fe566ab74f779a5e8ed27ab8a5f4ed2c020ea2ee..718a1bac21cb8902daf6f7519a038cfea1fee2b7 100644 (file)
--- a/helm/ocaml/tactics/equalityTactics.ml
+++ b/helm/ocaml/tactics/equalityTactics.ml
@@ -24,13 +24,16 @@
  *)
 
 let rewrite_tac ~term:equality =
- let rewrite_tac ~term:equality (proof,goal) =
-  let module C = Cic in
-  let module U = UriManager in
-   let curi,metasenv,pbo,pty = proof in
-   let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+  let rewrite_tac ~term:equality (proof,goal) =
+    let module C = Cic in
+    let module U = UriManager in
+    let curi,metasenv,pbo,pty = proof in
+    let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+    let ty_eq,_ = 
+      CicTypeChecker.type_of_aux' metasenv context equality 
+       CicUniv.empty_ugraph in 
     let eq_ind_r,ty,t1,t2 =
-     match CicTypeChecker.type_of_aux' metasenv context equality with
+      match ty_eq with
         C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
          when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
           let eq_ind_r =
@@ -66,9 +69,9 @@ let rewrite_tac ~term:equality =
           [eq_ind_r ; ty ; t2 ; pred ; C.Meta (fresh_meta,irl) ; t1 ;equality]))        ((curi,metasenv',pbo,pty),goal)
       in
        assert (List.length goals = 0) ;
-       (proof',[fresh_meta])
- in
-  ProofEngineTypes.mk_tactic (rewrite_tac ~term:equality)
+       (proof',[fresh_meta])
+  in
+    ProofEngineTypes.mk_tactic (rewrite_tac ~term:equality)
 ;;
 
 
@@ -81,7 +84,7 @@ let rewrite_simpl_tac ~term =
     (ReductionTactics.simpl_tac ~also_in_hypotheses:false ~terms:None))
    status
  in
-  ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
+   ProofEngineTypes.mk_tactic (rewrite_simpl_tac ~term)
 ;;
 
 
@@ -91,8 +94,11 @@ let rewrite_back_tac ~term:equality =
   let module U = UriManager in
    let curi,metasenv,pbo,pty = proof in
    let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+   let ty_eq,_ = 
+     CicTypeChecker.type_of_aux' metasenv context equality 
+       CicUniv.empty_ugraph in
     let eq_ind_r,ty,t1,t2 =
-     match CicTypeChecker.type_of_aux' metasenv context equality with
+     match ty_eq with
         C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
          when U.eq uri HelmLibraryObjects.Logic.eq_URI ->
           let eq_ind_r =
@@ -154,34 +160,35 @@ let replace_tac ~what ~with_what =
   let module U = UriManager in
   let module P = PrimitiveTactics in
   let module T = Tacticals in
-   let _,metasenv,_,_ = proof in
-    let _,context,_ = CicUtil.lookup_meta goal metasenv in
-     let wty = CicTypeChecker.type_of_aux' metasenv context what in
-      try
-      if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
-       then
+  let _,metasenv,_,_ = proof in
+  let _,context,_ = CicUtil.lookup_meta goal metasenv in
+  let wty,u = (* TASSI: FIXME *)
+    CicTypeChecker.type_of_aux' metasenv context what CicUniv.empty_ugraph in
+  let wwty,_ = CicTypeChecker.type_of_aux' metasenv context with_what u in
+    try
+      if (wty = wwty) then
         ProofEngineTypes.apply_tactic
-         (T.thens
-          ~start:(
-            P.cut_tac 
-             (C.Appl [
-               (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
-                 wty ; 
-                 what ; 
-                 with_what]))
-          ~continuations:[
-            T.then_
-               ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
-               ~continuation:(
-                 ProofEngineStructuralRules.clear
-                  ~hyp:(List.hd context)) ;
-            T.id_tac])
+          (T.thens
+             ~start:(
+               P.cut_tac 
+                      (C.Appl [
+                         (C.MutInd (HelmLibraryObjects.Logic.eq_URI, 0, [])) ;
+                         wty ; 
+                         what ; 
+                         with_what]))
+             ~continuations:[            
+              
+              T.then_     ~start:(rewrite_simpl_tac ~term:(C.Rel 1))
+                          ~continuation:(
+                                ProofEngineStructuralRules.clear
+                                               ~hyp:(List.hd context)) ;
+               T.id_tac])
           status
-       else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
-       with (Failure "hd") -> 
-            raise (ProofEngineTypes.Fail "Replace: empty context")
+      else raise (ProofEngineTypes.Fail "Replace: terms not replaceable")
+    with (Failure "hd") -> 
+      raise (ProofEngineTypes.Fail "Replace: empty context")
  in
-  ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
+   ProofEngineTypes.mk_tactic (replace_tac ~what ~with_what)
 ;;