diff options
| -rw-r--r-- | intf/tacexpr.mli | 2 | ||||
| -rw-r--r-- | ltac/eauto.ml | 2 | ||||
| -rw-r--r-- | ltac/extratactics.ml4 | 4 | ||||
| -rw-r--r-- | ltac/g_auto.ml4 | 2 | ||||
| -rw-r--r-- | ltac/tacinterp.ml | 18 | ||||
| -rw-r--r-- | ltac/tacinterp.mli | 5 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 25 | ||||
| -rw-r--r-- | pretyping/pretyping.mli | 8 |
8 files changed, 38 insertions, 28 deletions
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli index b1dc174d4..0aa3b936c 100644 --- a/intf/tacexpr.mli +++ b/intf/tacexpr.mli @@ -122,7 +122,7 @@ type open_glob_constr = unit * glob_constr_and_expr type binding_bound_vars = Id.Set.t type glob_constr_pattern_and_expr = glob_constr_and_expr * constr_pattern -type 'a delayed_open = +type 'a delayed_open = 'a Pretyping.delayed_open = { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } type delayed_open_constr_with_bindings = Term.constr with_bindings delayed_open diff --git a/ltac/eauto.ml b/ltac/eauto.ml index 044946759..9cfb805d4 100644 --- a/ltac/eauto.ml +++ b/ltac/eauto.ml @@ -60,7 +60,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true } in - List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs + List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs (************************************************************************) (* PROLOG tactic *) diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 23aa8dcb4..96abc1199 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -44,7 +44,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true } in - let c = Tacinterp.type_uconstr ~flags ist c in + let c = Pretyping.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac let replace_in_clause_maybe_by ist c1 c2 cl tac = @@ -368,7 +368,7 @@ let refine_tac ist simple c = let env = Proofview.Goal.env gl in let flags = Pretyping.all_no_fail_flags in let expected_type = Pretyping.OfType concl in - let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in + let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in let refine = Refine.refine ~unsafe:false update in if simple then refine diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index 788443944..bc98b7d6d 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -48,7 +48,7 @@ let eval_uconstrs ist cs = fail_evar = false; expand_evars = true } in - List.map (fun c -> Tacinterp.type_uconstr ~flags ist c) cs + List.map (fun c -> Pretyping.type_uconstr ~flags ist c) cs let pr_auto_using _ _ _ = Pptactic.pr_auto_using (fun _ -> mt ()) diff --git a/ltac/tacinterp.ml b/ltac/tacinterp.ml index 4506f8159..4c74984f8 100644 --- a/ltac/tacinterp.ml +++ b/ltac/tacinterp.ml @@ -723,24 +723,6 @@ let interp_open_constr_list = let pf_interp_type ist env sigma = interp_type ist env sigma -(* Fully evaluate an untyped constr *) -let type_uconstr ?(flags = constr_flags) - ?(expected_type = WithoutTypeConstraint) ist c = - { delayed = begin fun env sigma -> - let open Pretyping in - let { closure; term } = c in - let vars = { - ltac_constrs = closure.typed; - ltac_uconstrs = closure.untyped; - ltac_idents = closure.idents; - ltac_genargs = ist.lfun; - } in - let sigma = Sigma.to_evar_map sigma in - let (sigma, c) = understand_ltac flags env sigma vars expected_type term in - Sigma.Unsafe.of_pair (c, sigma) - end } - - (* Interprets a reduction expression *) let interp_unfold ist env sigma (occs,qid) = (interp_occurrences ist occs,interp_evaluable ist env sigma qid) diff --git a/ltac/tacinterp.mli b/ltac/tacinterp.mli index 31327873e..92f12fc8f 100644 --- a/ltac/tacinterp.mli +++ b/ltac/tacinterp.mli @@ -64,11 +64,6 @@ val val_interp : interp_sign -> glob_tactic_expr -> (value -> unit Proofview.tac (** Interprets an expression that evaluates to a constr *) val interp_ltac_constr : interp_sign -> glob_tactic_expr -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic -val type_uconstr : - ?flags:Pretyping.inference_flags -> - ?expected_type:Pretyping.typing_constraint -> - interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open - (** Interprets redexp arguments *) val interp_redexp : Environ.env -> Evd.evar_map -> raw_red_expr -> Evd.evar_map * red_expr diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a765d3091..8baa668c7 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -58,6 +58,8 @@ type ltac_var_map = { } type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } (************************************************************************) (* This concerns Cases *) @@ -1107,3 +1109,26 @@ let understand_tcc_evars ?(flags=all_no_fail_flags) env evdref ?(expected_type=W let understand_ltac flags env sigma lvar kind c = ise_pretype_gen flags env sigma lvar kind c + +let constr_flags = { + use_typeclasses = true; + use_unif_heuristics = true; + use_hook = None; + fail_evar = true; + expand_evars = true } + +(* Fully evaluate an untyped constr *) +let type_uconstr ?(flags = constr_flags) + ?(expected_type = WithoutTypeConstraint) ist c = + { delayed = begin fun env sigma -> + let { closure; term } = c in + let vars = { + ltac_constrs = closure.typed; + ltac_uconstrs = closure.untyped; + ltac_idents = closure.idents; + ltac_genargs = ist.Geninterp.lfun; + } in + let sigma = Sigma.to_evar_map sigma in + let (sigma, c) = understand_ltac flags env sigma vars expected_type term in + Sigma.Unsafe.of_pair (c, sigma) + end } diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 4c4c535d8..91320f20a 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -55,6 +55,9 @@ type inference_flags = { expand_evars : bool } +type 'a delayed_open = + { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } + val default_inference_flags : bool -> inference_flags val no_classes_no_fail_inference_flags : inference_flags @@ -114,6 +117,11 @@ val understand_judgment : env -> evar_map -> val understand_judgment_tcc : env -> evar_map ref -> glob_constr -> unsafe_judgment +val type_uconstr : + ?flags:inference_flags -> + ?expected_type:typing_constraint -> + Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open + (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags. *) |