From ba0975d00f49684e33f763e171f9578a702eec85 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Sep 2016 16:51:19 +0200 Subject: Move glob_constr_ltac_closure to evar_refiner. --- API/API.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index a0e77edd1..f7cc7ced3 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4008,7 +4008,6 @@ sig } type pure_open_constr = Evd.evar_map * EConstr.constr - type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr val understand_ltac : inference_flags -> Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> @@ -4387,8 +4386,10 @@ end module Evar_refiner : sig + type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr + val w_refine : Evar.t * Evd.evar_info -> - Pretyping.glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map + glob_constr_ltac_closure -> Evd.evar_map -> Evd.evar_map end -- cgit v1.2.3 From cd0a6070d9627cdf335c4be0a03b9bbb81f7a738 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Sep 2016 16:53:23 +0200 Subject: Remove pure_open_constr (now open_constr) --- API/API.mli | 4 +--- pretyping/pretyping.ml | 1 - pretyping/pretyping.mli | 4 +--- 3 files changed, 2 insertions(+), 7 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index f7cc7ced3..9dc78cbe4 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4007,11 +4007,9 @@ sig expand_evars : bool } - type pure_open_constr = Evd.evar_map * EConstr.constr - val understand_ltac : inference_flags -> Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> - typing_constraint -> Glob_term.glob_constr -> pure_open_constr + typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr val type_uconstr : diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 3fae20bcb..32daa0d89 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -47,7 +47,6 @@ open Misctypes module NamedDecl = Context.Named.Declaration type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type pure_open_constr = evar_map * EConstr.constr (************************************************************************) (* This concerns Cases *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 1bde4b44c..002e84a49 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -27,8 +27,6 @@ val search_guard : type typing_constraint = OfType of types | IsType | WithoutTypeConstraint -type pure_open_constr = evar_map * constr - type inference_hook = env -> evar_map -> evar -> evar_map * constr type inference_flags = { @@ -77,7 +75,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> val understand_ltac : inference_flags -> env -> evar_map -> ltac_var_map -> - typing_constraint -> glob_constr -> pure_open_constr + typing_constraint -> glob_constr -> evar_map * EConstr.t (** Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; -- cgit v1.2.3 From a92b0e3abb476743f6f12ce828a0d82eb3c98e98 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 15 Sep 2016 17:31:51 +0200 Subject: Move type_uconstr to Tacinterp. --- API/API.mli | 4 ---- plugins/ltac/extratactics.ml4 | 4 ++-- plugins/ltac/g_auto.ml4 | 2 +- plugins/ltac/tacinterp.ml | 14 ++++++++++++++ plugins/ltac/tacinterp.mli | 5 +++++ pretyping/pretyping.ml | 21 --------------------- pretyping/pretyping.mli | 5 ----- 7 files changed, 22 insertions(+), 33 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 9dc78cbe4..f4a7be2a3 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4012,10 +4012,6 @@ sig typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.t val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr - val type_uconstr : - ?flags:inference_flags -> - ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> Environ.env -> Evd.evar_map -> Glob_term.glob_constr -> Constr.t Evd.in_evar_universe_context val check_evars : Environ.env -> Evd.evar_map -> Evd.evar_map -> EConstr.constr -> unit diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index f3f2f27e9..b847aadf2 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -40,7 +40,7 @@ let with_delayed_uconstr ist c tac = fail_evar = false; expand_evars = true } in - let c = Pretyping.type_uconstr ~flags ist c in + let c = Tacinterp.type_uconstr ~flags ist c in Tacticals.New.tclDELAYEDWITHHOLES false c tac let replace_in_clause_maybe_by ist c1 c2 cl tac = @@ -359,7 +359,7 @@ let refine_tac ist simple with_classes c = let flags = { constr_flags () with Pretyping.use_typeclasses = with_classes } in let expected_type = Pretyping.OfType concl in - let c = Pretyping.type_uconstr ~flags ~expected_type ist c in + let c = Tacinterp.type_uconstr ~flags ~expected_type ist c in let update = begin fun sigma -> c env sigma end in diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 301943a50..5baa0d5c1 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -48,7 +48,7 @@ let eval_uconstrs ist cs = expand_evars = true } in let map c env sigma = c env sigma in - List.map (fun c -> map (Pretyping.type_uconstr ~flags ist c)) cs + List.map (fun c -> map (Tacinterp.type_uconstr ~flags ist c)) cs let pr_auto_using_raw _ _ _ = Pptactic.pr_auto_using Ppconstr.pr_constr_expr let pr_auto_using_glob _ _ _ = Pptactic.pr_auto_using (fun (c,_) -> Printer.pr_glob_constr c) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index d3e625e73..51eed2f4e 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1108,6 +1108,20 @@ let rec read_match_rule lfun ist env sigma = function :: read_match_rule lfun ist env sigma tl | [] -> [] +(* Fully evaluate an untyped constr *) +let type_uconstr ?(flags = {(constr_flags ()) with use_hook = None }) + ?(expected_type = WithoutTypeConstraint) ist c = + 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 = Id.Map.empty; + } in + understand_ltac flags env sigma vars expected_type term + end + let warn_deprecated_info = CWarnings.create ~name:"deprecated-info-tactical" ~category:"deprecated" (fun () -> diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 73e4f3d6a..c1ab2b4c4 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -54,6 +54,11 @@ val set_debug : debug_info -> unit (** Gives the state of debug *) val get_debug : unit -> debug_info +val type_uconstr : + ?flags:Pretyping.inference_flags -> + ?expected_type:Pretyping.typing_constraint -> + Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open + (** Adds an interpretation function for extra generic arguments *) val interp_genarg : interp_sign -> glob_generic_argument -> Value.t Ftactic.t diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 156e61ab6..7362b57fe 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1203,27 +1203,6 @@ let understand_ltac flags env sigma lvar kind c = let (sigma, c) = ise_pretype_gen flags env sigma lvar kind c in (sigma, c) -let constr_flags = { - use_typeclasses = true; - solve_unification_constraints = 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 = - 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 = Id.Map.empty; - } in - understand_ltac flags env sigma vars expected_type term - end - let pretype k0 resolve_tc typcon env evdref lvar t = pretype k0 resolve_tc typcon (make_env env !evdref) evdref lvar t diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index c475bcf7e..aa25e3604 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -84,11 +84,6 @@ val understand_ltac : inference_flags -> val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context -val type_uconstr : - ?flags:inference_flags -> - ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open - (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver hook depending on given flags. *) -- cgit v1.2.3