we tranlate an Automath book in an itermediate format where:

[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..82c339ae2b3d13381b6f1fee090eb1721f190fb9 100644 (file)
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -70,15 +70,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
    match hyps_pat with
       [] -> None,true,(fun ~term _ -> P.exact_tac term),concl_pat,gty
     | [name,pat] ->
-      let rec find_hyp n =
-       function
-          [] -> assert false
-        | Some (Cic.Name s,Cic.Decl ty)::_ when name = s ->
-           Cic.Rel n, S.lift n ty
-        | Some (Cic.Name s,Cic.Def _)::_ when name = s -> assert false (*CSC: not implemented yet! But does this make any sense?*)
-        | _::tl -> find_hyp (n+1) tl
-      in
-       let arg,gty = find_hyp 1 context in
+       let arg,gty = ProofEngineHelpers.find_hyp name context in
        let dummy = "dummy" in
         Some arg,false,
          (fun ~term typ ->
@@ -104,7 +96,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 +166,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 +233,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 +243,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 +270,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