diff options
| -rw-r--r-- | proofs/clenv.ml | 12 | ||||
| -rw-r--r-- | proofs/clenv.mli | 1 | ||||
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 37 |
4 files changed, 39 insertions, 13 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 70f4f7080..94d3c1b69 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -352,6 +352,14 @@ let clenv_environments bound c = in clrec (Intmap.empty,Intmap.empty,[]) bound c +let mk_clenv_from_n wc n (c,cty) = + let (namenv,env,args,concl) = clenv_environments n cty in + { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); + templtyp = mk_freelisted concl; + namenv = namenv; + env = env; + hook = wc } + let mk_clenv_from wc (c,cty) = let (namenv,env,args,concl) = clenv_environments (-1) cty in { templval = mk_freelisted (match args with [] -> c | _ -> applist (c,args)); @@ -1060,11 +1068,11 @@ let e_res_pf kONT clenv gls = let collect_com lbind = map_succeed (function (Com,c)->c | _ -> failwith "Com") lbind -let make_clenv_binding_apply wc (c,t) lbind = +let make_clenv_binding_apply wc n (c,t) lbind = let largs = collect_com lbind in let lcomargs = List.length largs in if lcomargs = List.length lbind then - let clause = mk_clenv_from wc (c,t) in + let clause = mk_clenv_from_n wc n (c,t) in clenv_constrain_missing_args largs clause else if lcomargs = 0 then let clause = mk_clenv_rename_from wc (c,t) in diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 106369d33..20eae8111 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -97,6 +97,7 @@ val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv val make_clenv_binding_apply : walking_constraints -> + int -> constr * constr -> (bindOcc * types) list -> walking_constraints clausenv diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 38bb22342..24beccf3b 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -42,7 +42,7 @@ let registered_e_assumption gl = let e_resolve_with_bindings_tac (c,lbind) gl = let (wc,kONT) = startWalk gl in let t = w_hnf_constr wc (w_type_of wc c) in - let clause = make_clenv_binding_apply wc (c,t) lbind in + let clause = make_clenv_binding_apply wc (-1) (c,t) lbind in e_res_pf kONT clause gl let e_resolve_with_bindings = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index bb34e96de..5ef73e5c4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -33,6 +33,15 @@ open Coqlib exception Bound +let rec nb_prod x = + let rec count n c = + match kind_of_term c with + IsProd(_,_,t) -> count (n+1) t + | IsLetIn(_,a,_,t) -> count n (subst1 a t) + | IsCast(c,_) -> count n c + | _ -> n + in count 0 x + (*********************************************) (* Tactics *) (*********************************************) @@ -482,6 +491,7 @@ let bring_hyps clsl gl = (* Resolution with missing arguments *) + let apply_with_bindings (c,lbind) gl = let apply = match kind_of_term c with @@ -489,20 +499,27 @@ let apply_with_bindings (c,lbind) gl = | _ -> res_pf in let (wc,kONT) = startWalk gl in + (* The actual type of the theorem. It will be matched against the + goal. If this fails, then the head constant will be unfolded step by + step. *) + let thm_ty0 = (w_type_of wc c) in let rec try_apply thm_ty = try - let clause = make_clenv_binding_apply wc (c,thm_ty) lbind in + 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 wc n (c,thm_ty) lbind in apply kONT clause gl with (RefinerError _|UserError _|Failure _) as exn -> - let ored = - try Some (Tacred.red_product (w_env wc) (w_Underlying wc) thm_ty) - with Tacred.Redelimination -> None - in - (match ored with - Some rty -> - try_apply rty - | None -> raise exn) in - try_apply (w_type_of wc c) + let red_thm = + try red_product (w_env wc) (w_Underlying wc) thm_ty + with (Redelimination | UserError _) -> raise exn in + try_apply red_thm in + try try_apply thm_ty0 + with (RefinerError _|UserError _|Failure _) -> + (* Last chance: if the head is a variable, apply may try + second order unification *) + let clause = make_clenv_binding_apply wc (-1) (c,thm_ty0) lbind in + apply kONT clause gl let apply c = apply_with_bindings (c,[]) |