diff options
| author | herbelin | 2006-10-25 13:02:22 +0000 |
|---|---|---|
| committer | herbelin | 2006-10-25 13:02:22 +0000 |
| commit | 0def214a2e9fb473d0f137598d5ee38d36c47c86 (patch) | |
| tree | 655ee826fad9111a98b0a70333c66ecc071f1fbd /tactics | |
| parent | 8b4637c2a5ff1b6774be4f40665ccc03b687a47e (diff) | |
Correction d'une tentative incorrecte (révision 9266) de clarification
du rôle de l'argument (-1) de make_clenv_binding_apply; nouvelle
correction qui évite ce codage.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9277 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 66de55a1d8..be1d52a6c9 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -46,7 +46,7 @@ END let e_resolve_with_bindings_tac (c,lbind) gl = let t = pf_hnf_constr gl (pf_type_of gl c) in - let clause = make_clenv_binding_apply gl (-1) (c,t) lbind in + let clause = make_clenv_binding_apply gl None (c,t) lbind in Clenvtac.e_res_pf clause gl let e_resolve_constr c gls = e_resolve_with_bindings_tac (c,NoBindings) gls diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d0e8645453..8d9d9e0308 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -518,7 +518,7 @@ let apply_with_bindings (c,lbind) gl = try let n = nb_prod thm_ty - nb_prod (pf_concl gl) in if n<0 then error "Apply: theorem has not enough premisses."; - let clause = make_clenv_binding_apply gl n (c,thm_ty) lbind in + let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause gl with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) as exn -> let red_thm = @@ -529,7 +529,7 @@ let apply_with_bindings (c,lbind) gl = with (Pretype_errors.PretypeError _|RefinerError _|UserError _|Failure _) -> (* Last chance: if the head is a variable, apply may try second order unification *) - let clause = make_clenv_binding gl (c,thm_ty0) lbind in + let clause = make_clenv_binding_apply gl None (c,thm_ty0) lbind in Clenvtac.res_pf clause gl let apply c = apply_with_bindings (c,NoBindings) |