From 72ac4b32ac26fdba751ae48568d28b4dbb8edd14 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Sep 2016 18:11:54 +0200 Subject: Untangling Tacexpr from lower strata. --- pretyping/pretyping.ml | 4 +--- pretyping/pretyping.mli | 7 +------ 2 files changed, 2 insertions(+), 9 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 0d9bde2ec..7d79de268 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -43,6 +43,7 @@ open Glob_ops open Evarconv open Pattern open Misctypes +open Tactypes open Sigma.Notations module NamedDecl = Context.Named.Declaration @@ -59,9 +60,6 @@ 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 } -type delayed_open_constr = constr delayed_open (************************************************************************) (* This concerns Cases *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7cb256e4f..f015813af 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -55,11 +55,6 @@ type inference_flags = { expand_evars : bool } -type 'a delayed_open = - { delayed : 'r. Environ.env -> 'r Sigma.t -> ('a, 'r) Sigma.sigma } - -type delayed_open_constr = constr delayed_open - val default_inference_flags : bool -> inference_flags val no_classes_no_fail_inference_flags : inference_flags @@ -122,7 +117,7 @@ val understand_judgment_tcc : env -> evar_map ref -> val type_uconstr : ?flags:inference_flags -> ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr delayed_open + 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 -- cgit v1.2.3