From e6005301fcbccbca31571795ed6071283f45d5a8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 8 Jul 2005 12:15:48 +0000 Subject: [PATCH] Elim generalized: the term to eliminate is now saturated (i.e. it is applied to as many ? as needed to make its type become something different from a product). --- helm/ocaml/tactics/primitiveTactics.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml index 2b67b521f..c43034f93 100644 --- a/helm/ocaml/tactics/primitiveTactics.ml +++ b/helm/ocaml/tactics/primitiveTactics.ml @@ -455,6 +455,10 @@ let elim_tac ~term = let (curi,metasenv,proofbo,proofty) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in + let (termty,metasenv',arguments,fresh_meta) = + ProofEngineHelpers.saturate_term + (ProofEngineHelpers.new_meta_of_proof proof) metasenv context termty in + let term = if arguments = [] then term else Cic.Appl (term::arguments) in let uri,exp_named_subst,typeno,args = match termty with C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[]) @@ -472,7 +476,7 @@ let elim_tac ~term = name | _ -> assert false in - let ty_ty,_ = T.type_of_aux' metasenv context ty CicUniv.empty_ugraph in + let ty_ty,_ = T.type_of_aux' metasenv' context ty CicUniv.empty_ugraph in let ext = match ty_ty with C.Sort C.Prop -> "_ind" @@ -486,7 +490,7 @@ let elim_tac ~term = in let eliminator_ref = C.Const (eliminator_uri,exp_named_subst) in let ety,_ = - T.type_of_aux' metasenv context eliminator_ref CicUniv.empty_ugraph in + T.type_of_aux' metasenv' context eliminator_ref CicUniv.empty_ugraph in let rec find_args_no = function C.Prod (_,_,t) -> 1 + find_args_no t @@ -504,7 +508,7 @@ let elim_tac ~term = C.Appl (eliminator_ref :: make_tl term (args_no - 1)) in let metasenv', term_to_refine' = - CicMkImplicit.expand_implicits metasenv [] context term_to_refine in + CicMkImplicit.expand_implicits metasenv' [] context term_to_refine in let refined_term,_,metasenv'',_ = CicRefine.type_of_aux' metasenv' context term_to_refine' CicUniv.empty_ugraph -- 2.39.2