From e46b614f187e3be3d5c38a99a7258bc1c8205a04 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 31 Jan 2006 17:56:28 +0000 Subject: [PATCH] Bug fixed in generalize: a status was generated with an old metasenv. --- helm/ocaml/tactics/variousTactics.ml | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index fc6413eb5..0e43cb1da 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -92,7 +92,6 @@ let generalize_tac let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in let pbo = CicMetaSubst.apply_subst subst pbo in let pty = CicMetaSubst.apply_subst subst pty in - let status = (uri,metasenv,pbo,pty),goal in let term = match term with None -> None @@ -118,13 +117,14 @@ let generalize_tac (List.length context_of_t - List.length context) t with CicMetaSubst.DeliftingARelWouldCaptureAFreeVariable -> - raise TheSelectedTermsMustLiveInTheGoalContext in - (*CSC: I am not sure about the following two assertions; - maybe I need to propagate the new subst and metasenv *) - assert (subst = []); - assert (metasenv' = metasenv); - let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in - u,typ,t,metasenv + raise TheSelectedTermsMustLiveInTheGoalContext + in + (*CSC: I am not sure about the following two assertions; + maybe I need to propagate the new subst and metasenv *) + assert (subst = []); + assert (metasenv' = metasenv); + let typ,u = CicTypeChecker.type_of_aux' ~subst metasenv context t u in + u,typ,t,metasenv in (* We need to check: 1. whether they live in the context of the goal; @@ -156,6 +156,7 @@ let generalize_tac else u1 ) u terms_with_context) ; + let status = (uri,metasenv,pbo,pty),goal in PET.apply_tactic (T.thens ~start: -- 2.39.2