added aps generation

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

diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml
index bd73865af94ffcf050498704a9be1be71543ff23..47f422f52dbbd0c3801784314334dc0b83cc9822 100644 (file)
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -104,7 +104,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   in
   let ty_eq,ugraph = 
     CicTypeChecker.type_of_aux' metasenv context equality 
-      CicUniv.empty_ugraph in 
+      CicUniv.oblivion_ugraph in 
   let (ty_eq,metasenv',arguments,fresh_meta) =
    TermUtil.saturate_term
     (ProofEngineHelpers.new_meta_of_proof proof) metasenv context ty_eq 0 in  
@@ -174,6 +174,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   let abstr_gty =
    ProofEngineReduction.replace_lifting_csc 0
     ~equality:(==) ~what ~with_what:with_what ~where:lifted_gty in
+  if lifted_gty = abstr_gty then 
+    raise (ProofEngineTypes.Fail (lazy "nothing to do"));
   let abstr_gty = CicMetaSubst.apply_subst subst abstr_gty in
   let pred = C.Lambda (fresh_name, ty, abstr_gty) in
   (* The argument is either a meta if we are rewriting in the conclusion
@@ -239,7 +241,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   in
   let context_len = List.length context in
   let subst,metasenv,u,_,selected_terms_with_context =
-   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph
+   ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.oblivion_ugraph
     ~conjecture ~pattern in
   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
   let with_what, metasenv, u = with_what context metasenv u in
@@ -249,7 +251,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
   let ty_of_with_what,u =
    CicTypeChecker.type_of_aux'
-    metasenv context with_what CicUniv.empty_ugraph in
+    metasenv context with_what CicUniv.oblivion_ugraph in
   let whats =
    match selected_terms_with_context with
       [] -> raise (ProofEngineTypes.Fail (lazy "Replace: no term selected"))
@@ -276,7 +278,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
              (lazy "Replace: one of the selected terms is not closed")) in
          let ty_of_t_in_context,u = (* TASSI: FIXME *)
           CicTypeChecker.type_of_aux' metasenv context t_in_context
-           CicUniv.empty_ugraph in
+           CicUniv.oblivion_ugraph in
          let b,u = CicReduction.are_convertible ~metasenv context
           ty_of_with_what ty_of_t_in_context u in
          if b then