From 2ebeb9ef9ea716c4b6e39199d85cb64c218afa82 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 18 Jul 2007 16:07:11 +0000 Subject: [PATCH] the predicate for elim was not built correctly when more than one right parameter was found --- components/tactics/primitiveTactics.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml index 70502d1b2..47acc7c58 100644 --- a/components/tactics/primitiveTactics.ml +++ b/components/tactics/primitiveTactics.ml @@ -517,12 +517,12 @@ let mk_predicate_for_elim | _ -> assert false in (* let _, upto = PEH.split_with_whd (List.nth splits pred_pos) in *) - let rec mk_pred metasenv context' pred arg' = function + let rec mk_pred metasenv context' pred arg' cpattern' = function | [] -> metasenv, pred, arg' | arg :: tail -> (* FG: we find the predicate for the eliminator as in the rewrite tactic ****) - let argty, _ugraph = TC.type_of_aux' metasenv context' arg ugraph in - let argty = CicReduction.whd context' argty in + let argty, _ugraph = TC.type_of_aux' metasenv context arg ugraph in + let argty = CicReduction.whd context argty in let fresh_name = FreshNamesGenerator.mk_fresh_name ~subst:[] metasenv context' C.Anonymous ~typ:argty @@ -532,7 +532,7 @@ let mk_predicate_for_elim let distance = List.length c - List.length context in S.lift distance arg, m, u in - let pattern = Some lazy_term, [], Some cpattern in + let pattern = Some lazy_term, [], Some cpattern' in let subst, metasenv, _ugraph, _conjecture, selected_terms = ProofEngineHelpers.select ~metasenv ~ugraph ~conjecture:(0, context, pred) ~pattern @@ -545,10 +545,13 @@ let mk_predicate_for_elim let pred = PER.replace_with_rel_1_from ~equality:(==) ~what 1 pred in let pred = MS.apply_subst subst pred in let pred = C.Lambda (fresh_name, argty, pred) in - mk_pred metasenv (hyp :: context') pred arg' tail + let cpattern' = C.Lambda (C.Anonymous, C.Implicit None, cpattern') in + mk_pred metasenv (hyp :: context') pred arg' cpattern' tail in - let metasenv, pred, arg = mk_pred metasenv context goal arg actual_args in - HLog.debug ("PRED: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args)); + let metasenv, pred, arg = + mk_pred metasenv context goal arg cpattern (List.rev actual_args) + in + HLog.debug ("PREDICATE: " ^ CicPp.ppterm ~metasenv pred ^ " ARGS: " ^ String.concat " " (List.map (CicPp.ppterm ~metasenv) actual_args)); metasenv, pred, arg, actual_args let beta_after_elim_tac upto predicate = -- 2.39.2