diff options
| -rw-r--r-- | tactics/tactics.ml | 24 |
1 files changed, 7 insertions, 17 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d058ad543b..02c0e65918 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -753,23 +753,13 @@ let exact_proof c gl = let (assumption : tactic) = fun gl -> let concl = pf_concl gl in - if occur_existential concl then - let rec arec = function - | [] -> error "No such assumption" - | (id,_,t)::rest -> - (try tclTHEN (unify t) (exact_check (mkVar id)) gl - with UserError _ | Logic.RefinerError _ -> arec rest) - in - arec (pf_hyps gl) - else - let rec arec = function - | [] -> error "No such assumption" - | (id,_,t)::rest -> - if pf_conv_x_leq gl t concl then refine_no_check (mkVar id) gl - else arec rest - in - arec (pf_hyps gl) - + let rec arec = function + | [] -> error "No such assumption" + | (id,c,t)::rest -> + if pf_conv_x_leq gl t concl then refine_no_check (mkVar id) gl + else arec rest + in + arec (pf_hyps gl) (*****************************************************************) (* Modification of a local context *) |