From 7ba8eaf750689ab14910069a806233b7635bec91 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 4 Jul 2020 19:42:33 +0200 Subject: Small code simplification in Evarutil.new_evar. --- engine/evarutil.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) (limited to 'engine') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 423af1d4ec..a60e521923 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -414,10 +414,8 @@ let new_pure_evar_full evd ?typeclass_candidate evi = let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity) - ?candidates ?naming ?typeclass_candidate ?(principal=false) sign evd typ = - let default_naming = IntroAnonymous in - let naming = Option.default default_naming naming in +let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity) + ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ = let name = match naming with | IntroAnonymous -> None | IntroIdentifier id -> Some id -- cgit v1.2.3 From c6391a7edfd12a876f663bbac6d24386c021d148 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 4 Jul 2020 19:49:37 +0200 Subject: Remove Evarutil.new_pure_evar_full from the API. --- engine/evarutil.ml | 5 ----- engine/evarutil.mli | 2 -- 2 files changed, 7 deletions(-) (limited to 'engine') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index a60e521923..e30f908df0 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -409,11 +409,6 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ = let default_source = Loc.tag @@ Evar_kinds.InternalHole -let new_pure_evar_full evd ?typeclass_candidate evi = - let (evd, evk) = Evd.new_evar evd ?typeclass_candidate evi in - let evd = Evd.declare_future_goal evk evd in - (evd, evk) - let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_arguments = Abstraction.identity) ?candidates ?(naming = IntroAnonymous) ?typeclass_candidate ?(principal=false) sign evd typ = let name = match naming with diff --git a/engine/evarutil.mli b/engine/evarutil.mli index b3c94e6b3b..c463415b6a 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -56,8 +56,6 @@ val new_pure_evar : ?principal:bool -> named_context_val -> evar_map -> types -> evar_map * Evar.t -val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t - (** Create a new Type existential variable, as we keep track of them during type-checking and unification. *) val new_type_evar : -- cgit v1.2.3 From aba870c6b58b18bc1bd4711c379863a87bbf6d33 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 4 Jul 2020 19:54:19 +0200 Subject: Remove Evarutil.new_evar_from_context from the API. --- engine/evarutil.ml | 8 -------- engine/evarutil.mli | 8 -------- 2 files changed, 16 deletions(-) (limited to 'engine') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index e30f908df0..9bfe3e21f3 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -444,14 +444,6 @@ let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?type let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in evd, mkEvar (newevk, instance) -let new_evar_from_context ?src ?filter ?candidates ?naming ?typeclass_candidate ?principal sign evd typ = - let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in - let instance = - match filter with - | None -> instance - | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ ?src ?filter ?candidates ?naming ?principal instance - (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c463415b6a..c592a4f5d1 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -25,14 +25,6 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) -val new_evar_from_context : - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?candidates:constr list -> - ?naming:intro_pattern_naming_expr -> - ?typeclass_candidate:bool -> - ?principal:bool -> - named_context_val -> evar_map -> types -> evar_map * EConstr.t - type naming_mode = | KeepUserNameAndRenameExistingButSectionNames | KeepUserNameAndRenameExistingEvenSectionNames -- cgit v1.2.3 From 834c64015b608b8152e160d37e6f07a3106ff26b Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 4 Jul 2020 20:02:42 +0200 Subject: Remove Evarutil.new_evar_instance from the API. --- engine/evarutil.ml | 13 +++---------- engine/evarutil.mli | 15 --------------- 2 files changed, 3 insertions(+), 25 deletions(-) (limited to 'engine') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 9bfe3e21f3..b4b2032dd2 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -436,14 +436,6 @@ let new_pure_evar ?(src=default_source) ?(filter = Filter.identity) ?(abstract_a in (evd, newevk) -let new_evar_instance ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate - ?principal sign evd typ instance = - let open EConstr in - assert (not !Flags.debug || - List.distinct (ids_of_named_context (named_context_of_val sign))); - let (evd, newevk) = new_pure_evar sign evd ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate ?principal typ in - evd, mkEvar (newevk, instance) - (* [new_evar] declares a new existential in an env env with type typ *) (* Converting the env into the sign of the evar to define *) let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_candidate @@ -455,8 +447,9 @@ let new_evar ?src ?filter ?abstract_arguments ?candidates ?naming ?typeclass_can match filter with | None -> instance | Some filter -> Filter.filter_list filter instance in - new_evar_instance sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming - ?typeclass_candidate ?principal instance + let (evd, evk) = new_pure_evar sign evd typ' ?src ?filter ?abstract_arguments ?candidates ?naming + ?typeclass_candidate ?principal in + (evd, EConstr.mkEvar (evk, instance)) let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c592a4f5d1..41b58d38b0 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -63,21 +63,6 @@ val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr val new_global : evar_map -> GlobRef.t -> evar_map * constr -(** Create a fresh evar in a context different from its definition context: - [new_evar_instance sign evd ty inst] creates a new evar of context - [sign] and type [ty], [inst] is a mapping of the evar context to - the context where the evar should occur. This means that the terms - of [inst] are typed in the occurrence context and their type (seen - as a telescope) is [sign] *) -val new_evar_instance : - ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> - ?abstract_arguments:Abstraction.t -> ?candidates:constr list -> - ?naming:intro_pattern_naming_expr -> - ?typeclass_candidate:bool -> - ?principal:bool -> - named_context_val -> evar_map -> types -> - constr list -> evar_map * constr - val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option -- cgit v1.2.3