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/evarutil.ml') 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 ----- 1 file changed, 5 deletions(-) (limited to 'engine/evarutil.ml') 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 -- 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 -------- 1 file changed, 8 deletions(-) (limited to 'engine/evarutil.ml') 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 -- 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 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) (limited to 'engine/evarutil.ml') 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 -- cgit v1.2.3