diff options
| author | msozeau | 2009-04-10 19:23:58 +0000 |
|---|---|---|
| committer | msozeau | 2009-04-10 19:23:58 +0000 |
| commit | e2655d38d11b072da0e5f4d40b05adbea73c8b8d (patch) | |
| tree | 7fa52c241089222050a84d2b47576e58d6e8492e /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index fa0dd6e0c4..9940f04b5a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2173,8 +2173,8 @@ let abstract_args gl id = let liftargty = lift (List.length ctx) argty in let convertible = Reductionops.is_conv_leq ctxenv sigma liftargty ty in match kind_of_term arg with - | Var _ | Rel _ | Ind _ when convertible -> - (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env) +(* | Var _ | Rel _ | Ind _ when convertible -> *) +(* (subst1 arg arity, ctx, ctxenv, mkApp (c, [|arg|]), args, eqs, refls, vars, env) *) | _ -> let name = get_id name in let decl = (Name name, None, ty) in |