diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 10 | ||||
| -rw-r--r-- | proofs/goal.ml | 11 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 2 |
4 files changed, 16 insertions, 9 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index fff4f67b12..0e317e68e5 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -41,8 +41,14 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = error "Instantiate called on already-defined evar"; let env = Evd.evar_filtered_env evi in let sigma',typed_c = - try Pretyping.understand_ltac ~resolve_classes:true true - sigma env ltac_var (Pretyping.OfType (Some evi.evar_concl)) rawc + let flags = { + Pretyping.use_typeclasses = true; + Pretyping.use_unif_heuristics = true; + Pretyping.use_hook = None; + Pretyping.fail_evar = false; + Pretyping.expand_evars = true } in + try Pretyping.understand_ltac flags + sigma env ltac_var (Pretyping.OfType evi.evar_concl) rawc with e when Errors.noncritical e -> let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc diff --git a/proofs/goal.ml b/proofs/goal.ml index 6b794c1479..67cd414125 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -111,9 +111,7 @@ let return v _ _ _ _ = v In an ideal world, this could/should be the other way round. As of now, though, it seems at least quite useful to build tactics. *) let interp_constr cexpr env rdefs _ _ = - let (defs,c) = Constrintern.interp_open_constr !rdefs env cexpr in - rdefs := defs ; - c + Constrintern.interp_constr_evars rdefs env cexpr (* Type of constr with holes used by refine. *) (* The list of evars doesn't necessarily contain all the evars in the constr, @@ -217,11 +215,14 @@ module Refinable = struct let init_defs = !rdefs in (* if [check_type] is true, then creates a type constraint for the proof-to-be *) - let tycon = Pretyping.OfType (Option.init check_type (Evd.evar_concl info)) in + let tycon = if check_type then Pretyping.OfType (Evd.evar_concl info) else Pretyping.WithoutTypeConstraint in (* call to [understand_tcc_evars] returns a constr with undefined evars these evars will be our new goals *) + let flags = + if resolve_classes then Pretyping.all_no_fail_flags + else Pretyping.no_classes_no_fail_inference_flags in let open_constr = - Pretyping.understand_tcc_evars ~resolve_classes rdefs env tycon rawc + Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc in ignore(update_handle handle init_defs !rdefs); open_constr diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index c07db32b75..90f20a7385 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -171,7 +171,7 @@ let implicit_tactic = ref None let declare_implicit_tactic tac = implicit_tactic := Some tac -let solve_by_implicit_tactic env sigma (evk,args) = +let solve_by_implicit_tactic env sigma evk = let evi = Evd.find_undefined sigma evk in match (!implicit_tactic, snd (evar_source evk sigma)) with | Some tac, (Evar_kinds.ImplicitArg _ | Evar_kinds.QuestionMark _) diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 4ca23e7116..73850c6f07 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -174,4 +174,4 @@ val build_by_tactic : env -> types -> tactic -> constr val declare_implicit_tactic : tactic -> unit (* Raise Exit if cannot solve *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> existential -> constr +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr |