From 05afd04095e35d77ca135bd2c1cb8d303ea2d6a8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 24 Nov 2016 18:18:17 +0100 Subject: Ltac now uses evar-based constrs. --- engine/evd.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 5c9effd4be..4e8284675e 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -607,7 +607,7 @@ val pr_evar_suggested_name : existential_key -> evar_map -> Id.t (** {5 Debug pretty-printers} *) -val print_constr_hook : (Environ.env -> constr -> Pp.std_ppcmds) Hook.t +val print_constr_hook : (Environ.env -> evar_map -> constr -> Pp.std_ppcmds) Hook.t val pr_evar_info : evar_info -> Pp.std_ppcmds val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds -- cgit v1.2.3 From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 25 Nov 2016 18:34:53 +0100 Subject: Removing various compatibility layers of tactics. --- engine/evd.mli | 4 ---- 1 file changed, 4 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 4e8284675e..699b52c2b2 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -420,10 +420,6 @@ val loc_of_conv_pb : evar_map -> evar_constraint -> Loc.t contained in the object; need the term to be evar-normal otherwise defined evars are returned too. *) -val evar_list : constr -> existential list - (** excluding evars in instances of evars and collected with - redundancies from right to left (used by tactic "instantiate") *) - val evars_of_term : constr -> Evar.Set.t (** including evars in instances of evars *) -- cgit v1.2.3 From 390fd4ac0a969103caeb5db3e5138e26f9a533de Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 17:49:11 +0100 Subject: Chasing a few unsafe constr coercions. --- engine/evd.mli | 13 ------------- 1 file changed, 13 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index 699b52c2b2..eeb9fd8618 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -569,19 +569,6 @@ val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> Globnames.global_reference -> evar_map * constr -(******************************************************************** - Conversion w.r.t. an evar map, not unifying universes. See - [Reductionops.infer_conv] for conversion up-to universes. *) - -val test_conversion : env -> evar_map -> conv_pb -> constr -> constr -> bool -(** WARNING: This does not allow unification of universes *) - -val eq_constr_univs : evar_map -> constr -> constr -> evar_map * bool -(** Syntactic equality up to universes, recording the associated constraints *) - -val e_eq_constr_univs : evar_map ref -> constr -> constr -> bool -(** Syntactic equality up to universes. *) - (********************************************************************) (* constr with holes and pending resolution of classes, conversion *) (* problems, candidates, etc. *) -- cgit v1.2.3 From 27fbf069ccd846383bcfb35ba1ea5bd1d95090a0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Nov 2016 23:48:28 +0100 Subject: Moving printing code from Evd to Termops. --- engine/evd.mli | 16 ---------------- 1 file changed, 16 deletions(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index eeb9fd8618..fc1d4a5142 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -584,22 +584,6 @@ type open_constr = evar_map * constr (* Special case when before is empty *) type unsolvability_explanation = SeveralInstancesFound of int (** Failure explanation. *) -val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds - -val pr_evar_suggested_name : existential_key -> evar_map -> Id.t - -(** {5 Debug pretty-printers} *) - -val print_constr_hook : (Environ.env -> evar_map -> constr -> Pp.std_ppcmds) Hook.t -val pr_evar_info : evar_info -> Pp.std_ppcmds -val pr_evar_constraints : evar_constraint list -> Pp.std_ppcmds -val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds -val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> - evar_map -> Pp.std_ppcmds -val pr_metaset : Metaset.t -> Pp.std_ppcmds -val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds -val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds - (** {5 Deprecated functions} *) val create_evar_defs : evar_map -> evar_map -- cgit v1.2.3 From 1683b718f85134fdb0d49535e489344e1a7d56f5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 30 Nov 2016 00:33:08 +0100 Subject: Making Evd independent from Namegen. --- engine/evd.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'engine/evd.mli') diff --git a/engine/evd.mli b/engine/evd.mli index fc1d4a5142..2151000b60 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -149,7 +149,7 @@ val has_undefined : evar_map -> bool there are uninstantiated evars in [sigma]. *) val new_evar : evar_map -> - ?naming:Misctypes.intro_pattern_naming_expr -> evar_info -> evar_map * evar + ?name:Id.t -> evar_info -> evar_map * evar (** Creates a fresh evar mapping to the given information. *) val add : evar_map -> evar -> evar_info -> evar_map -- cgit v1.2.3