snapshot

[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 47f422f52dbbd0c3801784314334dc0b83cc9822..16aa6d3b2d5925a10b1ab3bf7e47583885365c2f 100644 (file)
--- a/helm/software/components/tactics/equalityTactics.ml
+++ b/helm/software/components/tactics/equalityTactics.ml
@@ -46,8 +46,6 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   let proof,goal = status in
   let curi, metasenv, _subst, pbo, pty, attrs = proof in
   let (metano,context,gty) = CicUtil.lookup_meta goal metasenv in
-  let gsort,_ =
-   CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in
   match hyps_pat with
      he::(_::_ as tl) ->
        PET.apply_tactic
@@ -70,15 +68,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 ->
@@ -97,6 +87,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
          Some pat,gty
     | _::_ -> assert false
   in
+  let gsort,_ =
+   CicTypeChecker.type_of_aux' metasenv context gty CicUniv.oblivion_ugraph in
   let if_right_to_left do_not_change a b = 
     match direction with
     | `RightToLeft -> if do_not_change then a else b
@@ -206,8 +198,8 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
     in
      (proof',goals)
   with (* FG: this should be PET.Fail _ *)
-     TC.TypeCheckerFailure _ -> 
-      let msg = lazy "rewrite: nothing to rewrite" in
+     TC.TypeCheckerFailure m -> 
+      let msg = lazy ("rewrite: "^ Lazy.force m) in
       raise (PET.Fail msg)
  in    
   PET.mk_tactic _rewrite_tac