From 82306753608353e9aed7e1b9c03b96787f1ec5eb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 13 Sep 2006 12:53:01 +0000 Subject: [PATCH] Bug fixed in injection: a missing lift bugged the tactic when the constructor had more than one argument. The tactic is still bugged when the inductive type has either right or left parameters! --- helm/software/components/tactics/discriminationTactics.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/discriminationTactics.ml b/helm/software/components/tactics/discriminationTactics.ml index 4c7f5148d..9c9998907 100644 --- a/helm/software/components/tactics/discriminationTactics.ml +++ b/helm/software/components/tactics/discriminationTactics.ml @@ -37,7 +37,8 @@ let rec injection_tac ~term = let _,metasenv,_,_ = proof in let _,context,_ = CicUtil.lookup_meta goal metasenv in let termty,_ = (* TASSI: FIXME *) - CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph in + CicTypeChecker.type_of_aux' metasenv context term CicUniv.empty_ugraph + in ProofEngineTypes.apply_tactic (match termty with (C.Appl [(C.MutInd (equri, 0, [])) ; tty ; t1 ; t2]) @@ -59,7 +60,9 @@ let rec injection_tac ~term = [],[] -> T.id_tac | hd1::tl1,hd2::tl2 -> T.then_ - ~start:(injection1_tac ~i ~term) + ~start: + (injection1_tac ~i + ~term:(CicSubstitution.lift (i-1) term)) ~continuation:(traverse_list (i+1) tl1 tl2) | _ -> raise (ProofEngineTypes.Fail (lazy "Discriminate: i 2 termini hanno in testa lo stesso costruttore, ma applicato a un numero diverso di termini. possibile???")) in traverse_list 1 applist1 applist2 -- 2.39.2