From bb19a912c9d3d470163e88722e3abbd548b8bdb9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Sat, 9 Jul 2005 07:38:59 +0000 Subject: [PATCH] Generalize ported to the new select up to unification. --- helm/ocaml/tactics/variousTactics.ml | 33 ++++++++++++++++++---------- 1 file changed, 21 insertions(+), 12 deletions(-) diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml index 8bbe05dcb..1f2e6b13c 100644 --- a/helm/ocaml/tactics/variousTactics.ml +++ b/helm/ocaml/tactics/variousTactics.ml @@ -72,7 +72,6 @@ let generalize_tac ?(mk_fresh_name_callback = FreshNamesGenerator.mk_fresh_name ~subst:[]) pattern = -(* let module PET = ProofEngineTypes in let generalize_tac mk_fresh_name_callback ~pattern:(term,hyps_pat,concl_pat) status @@ -82,20 +81,31 @@ let generalize_tac let module C = Cic in let module P = PrimitiveTactics in let module T = Tacticals in - let _,metasenv,_,_ = proof in + let uri,metasenv,pbo,pty = proof in let (_,context,ty) as conjecture = CicUtil.lookup_meta goal metasenv in - let selected_hyps,terms_with_context = - ProofEngineHelpers.select ~metasenv ~conjecture ~pattern in - let typ,term = + let subst,metasenv,u,selected_hyps,terms_with_context = + ProofEngineHelpers.select ~metasenv ~ugraph:CicUniv.empty_ugraph + ~conjecture ~pattern in + let context = CicMetaSubst.apply_subst_context subst context in + 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 + | Some term -> Some (CicMetaSubst.apply_subst subst term) in + let u,typ,term = match terms_with_context, term with [], None -> raise UnableToDetectTheTermThatMustBeGeneralizedYouMustGiveItExplicitly | _, Some term | (_,term)::_, None -> - fst - (CicTypeChecker.type_of_aux' metasenv context term - CicUniv.empty_ugraph), - term in + let typ,u = + CicTypeChecker.type_of_aux' ~subst metasenv context term u + in + u,typ,term + in (* We need to check: 1. whether they live in the context of the goal; if they do they are also well-typed since they are closed subterms @@ -118,12 +128,12 @@ let generalize_tac raise TheSelectedTermsMustLiveInTheGoalContext end; (* 2 *) - let b,u1 = CicReduction.are_convertible context term t u in + let b,u1 = CicReduction.are_convertible ~subst context term t u in if not b then raise AllSelectedTermsMustBeConvertible else u1 - ) CicUniv.empty_ugraph terms_with_context) ; + ) u terms_with_context) ; PET.apply_tactic (T.thens ~start: @@ -143,5 +153,4 @@ let generalize_tac status in PET.mk_tactic (generalize_tac mk_fresh_name_callback ~pattern) -*) assert false ;; -- 2.39.2