From 9f175bbeb19175a1e422225986f139e8f1a1b56c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Fri, 4 May 2018 14:36:18 +0200 Subject: Use evd_combX in Cases. --- engine/evarutil.ml | 10 +++++----- engine/evarutil.mli | 22 +++++++++++++--------- 2 files changed, 18 insertions(+), 14 deletions(-) (limited to 'engine') diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 52610f6f3..2b202ef3e 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -436,7 +436,7 @@ let new_pure_evar_full evd evi = let evd = Evd.declare_future_goal evk evd in (evd, evk) -let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) typ = +let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ = let default_naming = Misctypes.IntroAnonymous in let naming = Option.default default_naming naming in let name = match naming with @@ -463,14 +463,14 @@ let new_pure_evar sign evd ?(src=default_source) ?(filter = Filter.identity) ?ca in (evd, newevk) -let new_evar_instance sign evd typ ?src ?filter ?candidates ?store ?naming ?principal instance = +let new_evar_instance ?src ?filter ?candidates ?store ?naming ?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 ?candidates ?store ?naming ?principal typ in evd, mkEvar (newevk,Array.of_list instance) -let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?principal typ = +let new_evar_from_context ?src ?filter ?candidates ?store ?naming ?principal sign evd typ = let instance = List.map (NamedDecl.get_id %> EConstr.mkVar) (named_context_of_val sign) in let instance = match filter with @@ -480,7 +480,7 @@ let new_evar_from_context sign evd ?src ?filter ?candidates ?store ?naming ?prin (* [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 env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming typ = +let new_evar ?src ?filter ?candidates ?store ?naming ?principal ?hypnaming env evd typ = let sign,typ',instance,subst = push_rel_context_to_named_context ?hypnaming env evd typ in let map c = csubst_subst subst c in let candidates = Option.map (fun l -> List.map map l) candidates in @@ -490,7 +490,7 @@ let new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal ?hypnami | Some filter -> Filter.filter_list filter instance in new_evar_instance sign evd typ' ?src ?filter ?candidates ?store ?naming ?principal instance -let new_type_evar env evd ?src ?filter ?naming ?principal ?hypnaming rigid = +let new_type_evar ?src ?filter ?naming ?principal ?hypnaming env evd rigid = let (evd', s) = new_sort_variable rigid evd in let (evd', e) = new_evar env evd' ?src ?filter ?naming ?principal ?hypnaming (EConstr.mkSort s) in evd', (e, s) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index c24660f5b..7dd98bac9 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -25,10 +25,11 @@ val mk_new_meta : unit -> constr (** {6 Creating a fresh evar given their type and context} *) val new_evar_from_context : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * EConstr.t + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * EConstr.t type naming_mode = | KeepUserNameAndRenameExistingButSectionNames @@ -37,25 +38,28 @@ type naming_mode = | FailIfConflict val new_evar : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> types -> evar_map * EConstr.t + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> types -> evar_map * EConstr.t val new_pure_evar : - named_context_val -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> types -> evar_map * Evar.t + ?principal:bool -> + named_context_val -> evar_map -> types -> evar_map * Evar.t val new_pure_evar_full : evar_map -> 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 : - env -> evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> + ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> - ?principal:bool -> ?hypnaming:naming_mode -> rigid -> + ?principal:bool -> ?hypnaming:naming_mode -> + env -> evar_map -> rigid -> evar_map * (constr * Sorts.t) val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr @@ -74,10 +78,10 @@ val new_global : evar_map -> GlobRef.t -> evar_map * constr of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_map -> types -> ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t -> ?candidates:constr list -> ?store:Store.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> + named_context_val -> evar_map -> types -> constr list -> evar_map * constr val make_pure_subst : evar_info -> 'a array -> (Id.t * 'a) list -- cgit v1.2.3