diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-10 19:23:58 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-10 19:23:58 +0000 |
| commit | e2655d38d11b072da0e5f4d40b05adbea73c8b8d (patch) | |
| tree | 7fa52c241089222050a84d2b47576e58d6e8492e /pretyping | |
| parent | 4cc6bd53bca5441c9960ba55818b5ddfa8c8d13b (diff) | |
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
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pattern.ml | 5 |
1 files changed, 4 insertions, 1 deletions
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) -> |