the passive set and passive list are expected to have the same cardinality, that...

[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 82c339ae2b3d13381b6f1fee090eb1721f190fb9..6eae445313304922677231b3aa0f518f108fb9d4 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
@@ -89,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
@@ -160,7 +160,7 @@ let rec rewrite_tac ~direction ~pattern:(wanted,hyps_pat,concl_pat) equality =
   let t1 = CicMetaSubst.apply_subst subst t1 in
   let t2 = CicMetaSubst.apply_subst subst t2 in
   let ty = CicMetaSubst.apply_subst subst ty in
-  let pbo = CicMetaSubst.apply_subst subst pbo in
+  let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in
   let pty = CicMetaSubst.apply_subst subst pty in
   let equality = CicMetaSubst.apply_subst subst equality in
   let abstr_gty =
@@ -198,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 
@@ -238,7 +238,7 @@ let replace_tac ~(pattern: ProofEngineTypes.lazy_pattern) ~with_what =
   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
   let with_what, metasenv, u = with_what context metasenv u in
   let with_what = CicMetaSubst.apply_subst subst with_what in
-  let pbo = CicMetaSubst.apply_subst subst pbo in
+  let pbo = lazy (CicMetaSubst.apply_subst subst (Lazy.force pbo)) in
   let pty = CicMetaSubst.apply_subst subst pty in
   let status = (uri,metasenv,_subst,pbo,pty, attrs),goal in
   let ty_of_with_what,u =