From e2655d38d11b072da0e5f4d40b05adbea73c8b8d Mon Sep 17 00:00:00 2001 From: msozeau Date: Fri, 10 Apr 2009 19:23:58 +0000 Subject: Fix premature optimisation in dependent induction: even variable args need to be generalized as they may appear in other arguments or their types. Try to keep the original names around as well, using the ones found in the goal. This only requires that interning a pattern [forall x, _] properly declares [x] as a metavariable, binding instances are already part of the substitutions computed by [extended_matches]. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12079 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pattern.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) (limited to 'pretyping/pattern.ml') diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index ba53d127e..d4b21fba5 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -221,12 +221,15 @@ let rec pat_of_raw metas vars = function PApp (pat_of_raw metas vars c, Array.of_list (List.map (pat_of_raw metas vars) cl)) | RLambda (_,na,bk,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PLambda (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) - | RProd (_,na,bk,c1,c2) -> + | RProd (_,na,bk,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PProd (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | RLetIn (_,na,c1,c2) -> + name_iter (fun n -> metas := n::!metas) na; PLetIn (na, pat_of_raw metas vars c1, pat_of_raw metas (na::vars) c2) | RSort (_,s) -> -- cgit v1.2.3