From aced6734a7e68bf561c1ad3ca7e1d465a1feaf70 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 23 Jan 2004 17:09:18 +0000 Subject: Bug induction lors de types inductives avec parametres git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5241 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/tactics.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d739cb225..a1d6a0435 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1343,6 +1343,8 @@ let cook_sign hyp0 indvars env = before:=false; None (* fake value *) end else if List.mem hyp indvars then begin + (* warning: hyp can still occur after induction *) + (* e.g. if the goal (t hyp hyp0) with other occs of hyp in t *) indhyps := hyp::!indhyps; rhyp end else @@ -1580,9 +1582,10 @@ let induction_from_context isrec elim_info hyp0 (names,b_rnames) gl = [ if deps = [] then tclIDTAC else apply_type tmpcl args; thin dephyps; (if isrec then tclTHENFIRSTn else tclTHENLASTn) - (tclTHEN - (induction_tac hyp0 typ0 (elimc,elimt)) - (thin (hyp0::indhyps))) + (tclTHENLIST + [ induction_tac hyp0 typ0 (elimc,elimt); + thin [hyp0]; + tclTRY (thin indhyps) ]) (array_map2 (induct_discharge statlists lhyp0 (List.rev dephyps)) indsign names) ] -- cgit v1.2.3