From 55c78a59b2127ecead99bb814a3ca519f8087053 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 2 Jul 2008 09:13:12 +0000 Subject: [PATCH] calculation of the sort user to choose the rewriting principle fixed (the one of the goal was used also to rewrite in an hypothesis) --- helm/software/components/tactics/equalityTactics.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/helm/software/components/tactics/equalityTactics.ml b/helm/software/components/tactics/equalityTactics.ml index 82c339ae2..16aa6d3b2 100644 --- 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 @@ -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 -- 2.39.2