diff options
42 files changed, 222 insertions, 223 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 310fb1188..843992f78 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -102,17 +102,17 @@ let pp_transparent_state s = pp (pr_transparent_state s) (* proof printers *) let ppmetas metas = pp(pr_metaset metas) -let ppevm evd = pp(pr_evar_defs evd) -let ppevd evd = pp(pr_evar_defs evd) +let ppevm evd = pp(pr_evar_map evd) +let ppevd evd = pp(pr_evar_map evd) let ppclenv clenv = pp(pr_clenv clenv) let ppgoal g = pp(db_pr_goal g) let pppftreestate p = pp(print_pftreestate p) let pr_gls gls = - hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) + hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) let ppsigmagoal g = pp(pr_goal (sig_it g)) diff --git a/interp/constrintern.mli b/interp/constrintern.mli index ee677e80a..0e66dde83 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -117,21 +117,21 @@ val interp_casted_constr : evar_map -> env -> ?impls:full_internalization_env -> (* Accepting evars and giving back the manual implicits in addition. *) -val interp_casted_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> env -> +val interp_casted_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr * manual_implicits -val interp_type_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> +val interp_type_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:full_internalization_env -> constr_expr -> types * manual_implicits -val interp_constr_evars_impls : ?evdref:(evar_defs ref) -> ?fail_evar:bool -> +val interp_constr_evars_impls : ?evdref:(evar_map ref) -> ?fail_evar:bool -> env -> ?impls:full_internalization_env -> constr_expr -> constr * manual_implicits -val interp_casted_constr_evars : evar_defs ref -> env -> +val interp_casted_constr_evars : evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr -val interp_type_evars : evar_defs ref -> env -> ?impls:full_internalization_env -> +val interp_type_evars : evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> types (*s Build a judgment *) @@ -154,7 +154,7 @@ val interp_reference : ltac_sign -> reference -> rawconstr val interp_binder : evar_map -> env -> name -> constr_expr -> types -val interp_binder_evars : evar_defs ref -> env -> name -> constr_expr -> types +val interp_binder_evars : evar_map ref -> env -> name -> constr_expr -> types (* Interpret contexts: returns extended env and context *) @@ -162,7 +162,7 @@ val interp_context : ?fail_anonymous:bool -> evar_map -> env -> local_binder list -> (env * rel_context) * manual_implicits val interp_context_evars : ?fail_anonymous:bool -> - evar_defs ref -> env -> local_binder list -> (env * rel_context) * manual_implicits + evar_map ref -> env -> local_binder list -> (env * rel_context) * manual_implicits (* Locating references of constructions, possibly via a syntactic definition *) (* (these functions do not modify the glob file) *) diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli index f45dfa1cc..406f94338 100644 --- a/plugins/subtac/eterm.mli +++ b/plugins/subtac/eterm.mli @@ -22,7 +22,7 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) -val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> +val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int -> ?status:obligation_definition_status -> constr -> types -> (identifier * types * loc * obligation_definition_status * Intset.t * tactic option) array diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index bc4d834d4..6c6918664 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -232,7 +232,7 @@ let push_history_pattern n current cont = *) type pattern_matching_problem = { env : env; - isevars : Evd.evar_defs ref; + isevars : Evd.evar_map ref; pred : predicate_signature option; tomatch : tomatch_stack; history : pattern_continuation; @@ -1892,8 +1892,8 @@ let liftn_rel_context n k sign = in liftrec (k + rel_context_length sign) sign -let nf_evars_env evar_defs (env : env) : env = - let nf t = nf_isevar evar_defs t in +let nf_evars_env sigma (env : env) : env = + let nf t = nf_isevar sigma t in let env0 : env = reset_context env in let f e (na, b, t) e' : env = Environ.push_named (na, Option.map nf b, nf t) e' diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index b96c58755..fe25dc6fc 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -132,7 +132,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p Namegen.next_global_ident_away i (Termops.ids_of_context env) in let env' = push_rel_context ctx' env in - isevars := Evarutil.nf_evar_defs !isevars; + isevars := Evarutil.nf_evar_map !isevars; isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars; let sigma = !isevars in let subst = List.map (Evarutil.nf_evar sigma) subst in @@ -192,7 +192,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p [] subst (k.cl_props @ snd k.cl_context) in let inst_constr, ty_constr = instance_constructor k subst in - isevars := Evarutil.nf_evar_defs !isevars; + isevars := Evarutil.nf_evar_map !isevars; let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx') and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') in diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli index eb9f3c8e3..4b575da90 100644 --- a/plugins/subtac/subtac_classes.mli +++ b/plugins/subtac/subtac_classes.mli @@ -24,7 +24,7 @@ open Implicit_quantifiers open Classes (*i*) -val type_ctx_instance : Evd.evar_defs ref -> +val type_ctx_instance : Evd.evar_map ref -> Environ.env -> ('a * Term.constr option * Term.constr) list -> Topconstr.constr_expr list -> diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index b61299a06..f905b605d 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -334,7 +334,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation boxed = Impargs.declare_manual_implicits false gr impls in hook, recname, typ in - let _ = isevars := Evarutil.nf_evar_defs !isevars in + let _ = isevars := Evarutil.nf_evar_map !isevars in let fullcoqc = Evarutil.nf_isevar !isevars def in let fullctyp = Evarutil.nf_isevar !isevars typ in let evm = evars_of_term !isevars Evd.empty fullctyp in @@ -445,7 +445,7 @@ let interp_recursive fixkind l boxed = let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:false env_rec evd in - let evd = Evarutil.nf_evar_defs evd in + let evd = Evarutil.nf_evar_map evd in let fixdefs = List.map (nf_evar evd) fixdefs in let fixtypes = List.map (nf_evar evd) fixtypes in let rec_sign = nf_named_context_evar evd rec_sign in diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli index 71c93266d..304aa139e 100644 --- a/plugins/subtac/subtac_command.mli +++ b/plugins/subtac/subtac_command.mli @@ -11,34 +11,34 @@ open Constrintern val interp_gen : typing_constraint -> - evar_defs ref -> + evar_map ref -> env -> ?impls:full_internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> constr_expr -> constr val interp_constr : - evar_defs ref -> + evar_map ref -> env -> constr_expr -> constr val interp_type_evars : - evar_defs ref -> + evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> constr val interp_casted_constr_evars : - evar_defs ref -> + evar_map ref -> env -> ?impls:full_internalization_env -> constr_expr -> types -> constr val interp_open_constr : - evar_defs ref -> env -> constr_expr -> constr + evar_map ref -> env -> constr_expr -> constr val interp_constr_judgment : - evar_defs ref -> + evar_map ref -> env -> constr_expr -> unsafe_judgment val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list -val interp_binder : Evd.evar_defs ref -> +val interp_binder : Evd.evar_map ref -> Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index e2910b8c4..54f7aff1b 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -69,7 +69,7 @@ let merge_evms x y = let interp env isevars c tycon = let j = pretype tycon env isevars ([],[]) c in - let _ = isevars := Evarutil.nf_evar_defs !isevars in + let _ = isevars := Evarutil.nf_evar_map !isevars in let evd,_ = consider_remaining_unif_problems env !isevars in (* let unevd = undefined_evars evd in *) let unevd' = Typeclasses.resolve_typeclasses ~onlyargs:true ~split:true ~fail:true env evd in diff --git a/plugins/subtac/subtac_pretyping.mli b/plugins/subtac/subtac_pretyping.mli index fab8eccc7..055c6df22 100644 --- a/plugins/subtac/subtac_pretyping.mli +++ b/plugins/subtac/subtac_pretyping.mli @@ -12,12 +12,12 @@ module Pretyping : Pretyping.S val interp : Environ.env -> - Evd.evar_defs ref -> + Evd.evar_map ref -> Rawterm.rawconstr -> Evarutil.type_constraint -> Term.constr * Term.constr -val subtac_process : env -> evar_defs ref -> identifier -> local_binder list -> +val subtac_process : env -> evar_map ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list -val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> env -> evar_defs ref -> identifier -> local_binder list -> +val subtac_proof : Decl_kinds.definition_kind -> Tacexpr.declaration_hook -> env -> evar_map ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> Subtac_obligations.progress diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 64f5fe9c7..0beb1e1ae 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -116,7 +116,7 @@ let my_print_context = Termops.print_rel_context let my_print_named_context = Termops.print_named_context let my_print_env = Termops.print_env let my_print_rawconstr = Printer.pr_rawconstr_env -let my_print_evardefs = Evd.pr_evar_defs +let my_print_evardefs = Evd.pr_evar_map let my_print_tycon_type = Evarutil.pr_tycon_type @@ -448,7 +448,7 @@ let pr_evar_info evi = in hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") -let pr_evar_defs sigma = +let pr_evar_map sigma = h 0 (prlist_with_sep pr_fnl (fun (ev,evi) -> @@ -464,11 +464,11 @@ let pr_constraints pbs = | Reduction.CUMUL -> "<=") ++ spc() ++ print_constr t2) pbs) -let pr_evar_defs evd = +let pr_evar_map evd = let pp_evm = let evars = evd in if evars = empty then mt() else - str"EVARS:"++brk(0,1)++pr_evar_defs evars++fnl() in + str"EVARS:"++brk(0,1)++pr_evar_map evars++fnl() in let pp_met = if meta_list evd = [] then mt() else str"METAS:"++brk(0,1)++pr_meta_map evd in diff --git a/plugins/subtac/subtac_utils.mli b/plugins/subtac/subtac_utils.mli index 81f263cc2..d0ad334d3 100644 --- a/plugins/subtac/subtac_utils.mli +++ b/plugins/subtac/subtac_utils.mli @@ -69,7 +69,7 @@ val extsort : sorts -> constr_expr val my_print_constr : env -> constr -> std_ppcmds val my_print_constr_expr : constr_expr -> std_ppcmds -val my_print_evardefs : evar_defs -> std_ppcmds +val my_print_evardefs : evar_map -> std_ppcmds val my_print_context : env -> std_ppcmds val my_print_rel_context : env -> rel_context -> std_ppcmds val my_print_named_context : env -> std_ppcmds @@ -87,11 +87,11 @@ type binders = local_binder list val app_opt : ('a -> 'a) option -> 'a -> 'a val print_args : env -> constr array -> std_ppcmds val make_existential : loc -> ?opaque:obligation_definition_status -> - env -> evar_defs ref -> types -> constr + env -> evar_map ref -> types -> constr val make_existential_expr : loc -> 'a -> 'b -> constr_expr val string_of_hole_kind : hole_kind -> string val evars_of_term : evar_map -> evar_map -> constr -> evar_map -val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map +val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map val global_kind : logical_kind val goal_kind : locality * goal_object_kind val global_proof_kind : logical_kind @@ -129,7 +129,7 @@ val solve_by_tac : evar_info -> Tacmach.tactic -> constr val string_of_list : string -> ('a -> string) -> 'a list -> string val string_of_intset : Intset.t -> string -val pr_evar_defs : evar_defs -> Pp.std_ppcmds +val pr_evar_map : evar_map -> Pp.std_ppcmds val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr diff --git a/pretyping/cases.ml b/pretyping/cases.ml index fbc8bcd07..ae7106fb3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -88,7 +88,7 @@ let coq_unit_judge = module type S = sig val compile_cases : loc -> case_style -> - (type_constraint -> env -> evar_defs ref -> rawconstr -> unsafe_judgment) * evar_defs ref -> + (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref -> type_constraint -> env -> rawconstr option * tomatch_tuples * cases_clauses -> unsafe_judgment @@ -291,14 +291,14 @@ let push_history_pattern n current cont = type 'a pattern_matching_problem = { env : env; - evdref : evar_defs ref; + evdref : evar_map ref; pred : constr; tomatch : tomatch_stack; history : pattern_continuation; mat : 'a matrix; caseloc : loc; casestyle : case_style; - typing_function: type_constraint -> env -> evar_defs ref -> 'a option -> unsafe_judgment } + typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment } (*--------------------------------------------------------------------------* * A few functions to infer the inductive type from the patterns instead of * diff --git a/pretyping/cases.mli b/pretyping/cases.mli index e6d42e10d..669240312 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -64,7 +64,7 @@ type tomatch_status = module type S = sig val compile_cases : loc -> case_style -> - (type_constraint -> env -> evar_defs ref -> rawconstr -> unsafe_judgment) * evar_defs ref -> + (type_constraint -> env -> evar_map ref -> rawconstr -> unsafe_judgment) * evar_map ref -> type_constraint -> env -> rawconstr option * tomatch_tuples * cases_clauses -> unsafe_judgment diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index 5e4e7558c..79b0c5a02 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -40,7 +40,7 @@ let pf_concl gl = gl.it.evar_concl type clausenv = { env : env; - evd : evar_defs; + evd : evar_map; templval : constr freelisted; templtyp : constr freelisted } @@ -477,4 +477,4 @@ let pr_clenv clenv = h 0 (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ - pr_evar_defs clenv.evd) + pr_evar_map clenv.evd) diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 8e4dba5b5..5571efbc5 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -32,7 +32,7 @@ open Unification *) type clausenv = { env : env; - evd : evar_defs; + evd : evar_map; templval : constr freelisted; templtyp : constr freelisted } @@ -122,12 +122,12 @@ val make_clenv_binding : [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1] and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *) val clenv_environments : - evar_defs -> int option -> types -> evar_defs * constr list * types + evar_map -> int option -> types -> evar_map * constr list * types (* [clenv_environments_evars env sigma n t] does the same but returns a list of Evar's defined in [env] and extends [sigma] accordingly *) val clenv_environments_evars : - env -> evar_defs -> int option -> types -> evar_defs * constr list * types + env -> evar_map -> int option -> types -> evar_map * constr list * types (* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *) val clenv_conv_leq : diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 2f5099c1a..9f0b43521 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -29,38 +29,38 @@ module type S = sig inserts a coercion into [j], if needed, in such a way it gets as type a product; it returns [j] if no coercion is applicable *) val inh_app_fun : - env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (* [inh_coerce_to_sort env evd j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a sort; it fails if no coercion is applicable *) val inh_coerce_to_sort : loc -> - env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment (* [inh_coerce_to_base env evd j] coerces [j] to its base type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type its base type (the notion depends on the coercion system) *) val inh_coerce_to_base : loc -> - env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (* [inh_coerce_to_prod env evars t] coerces [t] to a product type *) val inh_coerce_to_prod : loc -> - env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type + env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type (* [inh_conv_coerce_to loc env evd j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) val inh_conv_coerce_to : loc -> - env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment + env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment val inh_conv_coerce_rigid_to : loc -> - env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment + env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment (* [inh_conv_coerces_to loc env evd t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) val inh_conv_coerces_to : loc -> - env -> evar_defs -> types -> type_constraint_type -> evar_defs + env -> evar_map -> types -> type_constraint_type -> evar_map (* [inh_pattern_coerce_to loc env evd pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; @@ -231,7 +231,7 @@ module Default = struct let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true - let inh_conv_coerces_to loc env (evd : evar_defs) t (abs, t') = evd + let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = evd (* Still problematic, as it changes unification let nabsinit, nabs = match abs with diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 0329cc07c..565cf0c40 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -26,38 +26,38 @@ module type S = sig inserts a coercion into [j], if needed, in such a way it gets as type a product; it returns [j] if no coercion is applicable *) val inh_app_fun : - env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (* [inh_coerce_to_sort env isevars j] coerces [j] to a type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type a sort; it fails if no coercion is applicable *) val inh_coerce_to_sort : loc -> - env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_type_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_type_judgment (* [inh_coerce_to_base env isevars j] coerces [j] to its base type; i.e. it inserts a coercion into [j], if needed, in such a way it gets as type its base type (the notion depends on the coercion system) *) val inh_coerce_to_base : loc -> - env -> evar_defs -> unsafe_judgment -> evar_defs * unsafe_judgment + env -> evar_map -> unsafe_judgment -> evar_map * unsafe_judgment (* [inh_coerce_to_prod env isevars t] coerces [t] to a product type *) val inh_coerce_to_prod : loc -> - env -> evar_defs -> type_constraint_type -> evar_defs * type_constraint_type + env -> evar_map -> type_constraint_type -> evar_map * type_constraint_type (* [inh_conv_coerce_to loc env isevars j t] coerces [j] to an object of type [t]; i.e. it inserts a coercion into [j], if needed, in such a way [t] and [j.uj_type] are convertible; it fails if no coercion is applicable *) val inh_conv_coerce_to : loc -> - env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment + env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment val inh_conv_coerce_rigid_to : loc -> - env -> evar_defs -> unsafe_judgment -> type_constraint_type -> evar_defs * unsafe_judgment + env -> evar_map -> unsafe_judgment -> type_constraint_type -> evar_map * unsafe_judgment (* [inh_conv_coerces_to loc env isevars t t'] checks if an object of type [t] is coercible to an object of type [t'] adding evar constraints if needed; it fails if no coercion exists *) val inh_conv_coerces_to : loc -> - env -> evar_defs -> types -> type_constraint_type -> evar_defs + env -> evar_map -> types -> type_constraint_type -> evar_map (* [inh_pattern_coerce_to loc env isevars pat ind1 ind2] coerces the Cases pattern [pat] typed in [ind1] into a pattern typed in [ind2]; diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index a85f0f739..9a4247bc2 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -17,24 +17,24 @@ open Evd (*i*) (* returns exception Reduction.NotConvertible if not unifiable *) -val the_conv_x : env -> constr -> constr -> evar_defs -> evar_defs -val the_conv_x_leq : env -> constr -> constr -> evar_defs -> evar_defs +val the_conv_x : env -> constr -> constr -> evar_map -> evar_map +val the_conv_x_leq : env -> constr -> constr -> evar_map -> evar_map (* The same function resolving evars by side-effect and catching the exception *) -val e_conv : env -> evar_defs ref -> constr -> constr -> bool -val e_cumul : env -> evar_defs ref -> constr -> constr -> bool +val e_conv : env -> evar_map ref -> constr -> constr -> bool +val e_cumul : env -> evar_map ref -> constr -> constr -> bool (*i For debugging *) val evar_conv_x : - env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool + env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool val evar_eqappr_x : - env -> evar_defs -> + env -> evar_map -> conv_pb -> constr * constr list -> constr * constr list -> - evar_defs * bool + evar_map * bool (*i*) -val consider_remaining_unif_problems : env -> evar_defs -> evar_defs * bool +val consider_remaining_unif_problems : env -> evar_map -> evar_map * bool val check_conv_record : constr * types list -> constr * types list -> constr * constr list * (constr list * constr list) * diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 1357c6ce3..0613a3501 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -79,7 +79,7 @@ let nf_evar_info evc info = let nf_evars evm = Evd.fold (fun ev evi evm' -> Evd.add evm' ev (nf_evar_info evm evi)) evm Evd.empty -let nf_evar_defs evd = Evd.evars_reset_evd (nf_evars evd) evd +let nf_evar_map evd = Evd.evars_reset_evd (nf_evars evd) evd let nf_isevar evd = nf_evar evd let j_nf_isevar evd = j_nf_evar evd @@ -958,7 +958,7 @@ and evar_define ?(choose=false) env (evk,_ as ev) rhs evd = with e -> pperrnl (str "Ill-typed evar instantiation: " ++ fnl() ++ - pr_evar_defs evd' ++ fnl() ++ + pr_evar_map evd' ++ fnl() ++ str "----> " ++ int ev ++ str " := " ++ print_constr body); raise e in*) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index a5a87b9bd..4bfef7998 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -34,10 +34,10 @@ val new_untyped_evar : unit -> existential_key (***********************************************************) (* Creating a fresh evar given their type and context *) val new_evar : - evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_defs * constr + evar_map -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_map * constr (* the same with side-effects *) val e_new_evar : - evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr + evar_map ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> 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 @@ -46,7 +46,7 @@ val e_new_evar : 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_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr + named_context_val -> evar_map -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_map * constr val make_pure_subst : evar_info -> constr array -> (identifier * constr) list @@ -57,7 +57,7 @@ val make_pure_subst : evar_info -> constr array -> (identifier * constr) list possibly solving related unification problems, possibly leaving open some problems that cannot be solved in a unique way (except if choose is true); fails if the instance is not valid for the given [ev] *) -val evar_define : ?choose:bool -> env -> existential -> constr -> evar_defs -> evar_defs +val evar_define : ?choose:bool -> env -> existential -> constr -> evar_map -> evar_map (***********************************************************) (* Evars/Metas switching... *) @@ -75,24 +75,24 @@ val non_instantiated : evar_map -> (evar * evar_info) list exception NoHeadEvar val head_evar : constr -> existential_key (* may raise NoHeadEvar *) -val is_ground_term : evar_defs -> constr -> bool -val is_ground_env : evar_defs -> env -> bool +val is_ground_term : evar_map -> constr -> bool +val is_ground_env : evar_map -> env -> bool val solve_refl : - (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) - -> env -> evar_defs -> existential_key -> constr array -> constr array -> - evar_defs + (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) + -> env -> evar_map -> existential_key -> constr array -> constr array -> + evar_map val solve_simple_eqn : - (env -> evar_defs -> conv_pb -> constr -> constr -> evar_defs * bool) - -> ?choose:bool -> env -> evar_defs -> bool option * existential * constr -> - evar_defs * bool + (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool) + -> ?choose:bool -> env -> evar_map -> bool option * existential * constr -> + evar_map * bool (* [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) -val check_evars : env -> evar_map -> evar_defs -> constr -> unit +val check_evars : env -> evar_map -> evar_map -> constr -> unit -val define_evar_as_product : evar_defs -> existential -> evar_defs * types -val define_evar_as_lambda : evar_defs -> existential -> evar_defs * types -val define_evar_as_sort : evar_defs -> existential -> evar_defs * sorts +val define_evar_as_product : evar_map -> existential -> evar_map * types +val define_evar_as_lambda : evar_map -> existential -> evar_map * types +val define_evar_as_sort : evar_map -> existential -> evar_map * sorts val is_unification_pattern_evar : env -> existential -> constr list -> constr -> bool @@ -123,8 +123,8 @@ val empty_valcon : val_constraint val mk_valcon : constr -> val_constraint val split_tycon : - loc -> env -> evar_defs -> type_constraint -> - evar_defs * (name * type_constraint * type_constraint) + loc -> env -> evar_map -> type_constraint -> + evar_map * (name * type_constraint * type_constraint) val valcon_of_tycon : type_constraint -> val_constraint @@ -155,16 +155,16 @@ val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env (* Same for evar defs *) -val nf_isevar : evar_defs -> constr -> constr -val j_nf_isevar : evar_defs -> unsafe_judgment -> unsafe_judgment +val nf_isevar : evar_map -> constr -> constr +val j_nf_isevar : evar_map -> unsafe_judgment -> unsafe_judgment val jl_nf_isevar : - evar_defs -> unsafe_judgment list -> unsafe_judgment list + evar_map -> unsafe_judgment list -> unsafe_judgment list val jv_nf_isevar : - evar_defs -> unsafe_judgment array -> unsafe_judgment array + evar_map -> unsafe_judgment array -> unsafe_judgment array val tj_nf_isevar : - evar_defs -> unsafe_type_judgment -> unsafe_type_judgment + evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_evar_defs : evar_defs -> evar_defs +val nf_evar_map : evar_map -> evar_map (* Replacing all evars *) exception Uninstantiated_evar of existential_key @@ -192,7 +192,7 @@ type clear_dependency_error = exception ClearDependencyError of identifier * clear_dependency_error -val clear_hyps_in_evi : evar_defs ref -> named_context_val -> types -> +val clear_hyps_in_evi : evar_map ref -> named_context_val -> types -> identifier list -> named_context_val * types val push_rel_context_to_named_context : Environ.env -> types -> diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c96cc20cf..1c47b8b00 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -67,7 +67,7 @@ let eq_evar_info ei1 ei2 = - ExistentialMap ( Maps of existential_keys ) - EvarInfoMap ( .t = evar_info ExistentialMap.t ) - EvarMap ( .t = EvarInfoMap.t * sort_constraints ) - - evar_defs (exported) + - evar_map (exported) *) module ExistentialMap = Intmap @@ -418,7 +418,7 @@ type hole_kind = type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * Environ.env * constr * constr -type evar_defs = +type evar_map = { evars : EvarMap.t; conv_pbs : evar_constraint list; last_mods : ExistentialSet.t; @@ -426,14 +426,14 @@ type evar_defs = metas : clbinding Metamap.t } (*** Lifting primitive from EvarMap. ***) -type evar_map = evar_defs + (* spiwack: this function seems to be used only for the definition of the progress tactical. I would recommand not using it in other places. *) let eq_evar_map d1 d2 = EvarMap.eq_evar_map d1.evars d2.evars (* spiwack: tentative. It might very well not be the semantics we want - for merging evar_defs *) + for merging evar_map *) let merge d1 d2 = { (* d1 with evars = EvarMap.merge d1.evars d2.evars*) evars = EvarMap.merge d1.evars d2.evars ; @@ -447,10 +447,10 @@ let remove d e = { d with evars=EvarMap.remove d.evars e } let dom d = EvarMap.dom d.evars let find d e = EvarMap.find d.evars e let mem d e = EvarMap.mem d.evars e -(* spiwack: this function loses information from the original evar_defs +(* spiwack: this function loses information from the original evar_map it might be an idea not to export it. *) let to_list d = EvarMap.to_list d.evars -(* spiwack: not clear what folding over an evar_defs, for now we shall +(* spiwack: not clear what folding over an evar_map, for now we shall simply fold over the inner evar_map. *) let fold f d a = EvarMap.fold f d.evars a let is_evar d e = EvarMap.is_evar d.evars e @@ -462,7 +462,7 @@ let existential_opt_value d e = EvarMap.existential_opt_value d.evars e (*** /Lifting... ***) -(* evar_defs are considered empty disregarding histories *) +(* evar_map are considered empty disregarding histories *) let is_empty d = d.evars = EvarMap.empty && d.conv_pbs = [] && @@ -790,7 +790,7 @@ let pr_evar_info evi = in hov 2 (str"[" ++ phyps ++ spc () ++ str"|- " ++ pty ++ pb ++ str"]") -let pr_evar_defs_t (evars,cstrs as sigma) = +let pr_evar_map_t (evars,cstrs as sigma) = let evs = if evars = EvarInfoMap.empty then mt () else @@ -813,10 +813,10 @@ let pr_constraints pbs = | Reduction.CUMUL -> "<=") ++ spc() ++ print_constr t2) pbs) -let pr_evar_defs evd = +let pr_evar_map evd = let pp_evm = if evd.evars = EvarMap.empty then mt() else - pr_evar_defs_t evd.evars++fnl() in + pr_evar_map_t evd.evars++fnl() in let cstrs = if evd.conv_pbs = [] then mt() else str"CONSTRAINTS:"++brk(0,1)++pr_constraints evd.conv_pbs++fnl() in diff --git a/pretyping/evd.mli b/pretyping/evd.mli index bcada1fc0..bffcf1cc6 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -79,7 +79,7 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding (*********************************************************************) (*** Existential variables and unification states ***) -(* A unification state (of type [evar_defs]) is primarily a finite mapping +(* A unification state (of type [evar_map]) is primarily a finite mapping from existential variables to records containing the type of the evar ([evar_concl]), the context under which it was introduced ([evar_hyps]) and its definition ([evar_body]). [evar_extra] is used to add any other @@ -117,47 +117,47 @@ val evar_unfiltered_env : evar_info -> env val evar_env : evar_info -> env (*** Unification state ***) -type evar_defs +type evar_map (* Unification state and existential variables *) (* spiwack: this function seems to be used only for the definition of the progress tactical. I would recommand not using it in other places. *) -val eq_evar_map : evar_defs -> evar_defs -> bool +val eq_evar_map : evar_map -> evar_map -> bool -val empty : evar_defs -val is_empty : evar_defs -> bool +val empty : evar_map +val is_empty : evar_map -> bool -val add : evar_defs -> evar -> evar_info -> evar_defs +val add : evar_map -> evar -> evar_info -> evar_map -val dom : evar_defs -> evar list -val find : evar_defs -> evar -> evar_info -val remove : evar_defs -> evar -> evar_defs -val mem : evar_defs -> evar -> bool -val to_list : evar_defs -> (evar * evar_info) list -val fold : (evar -> evar_info -> 'a -> 'a) -> evar_defs -> 'a -> 'a +val dom : evar_map -> evar list +val find : evar_map -> evar -> evar_info +val remove : evar_map -> evar -> evar_map +val mem : evar_map -> evar -> bool +val to_list : evar_map -> (evar * evar_info) list +val fold : (evar -> evar_info -> 'a -> 'a) -> evar_map -> 'a -> 'a -val merge : evar_defs -> evar_defs -> evar_defs +val merge : evar_map -> evar_map -> evar_map -val define : evar -> constr -> evar_defs -> evar_defs +val define : evar -> constr -> evar_map -> evar_map -val is_evar : evar_defs -> evar -> bool +val is_evar : evar_map -> evar -> bool -val is_defined : evar_defs -> evar -> bool +val is_defined : evar_map -> evar -> bool (*s [existential_value sigma ev] raises [NotInstantiatedEvar] if [ev] has no body and [Not_found] if it does not exist in [sigma] *) exception NotInstantiatedEvar -val existential_value : evar_defs -> existential -> constr -val existential_type : evar_defs -> existential -> types -val existential_opt_value : evar_defs -> existential -> constr option +val existential_value : evar_map -> existential -> constr +val existential_type : evar_map -> existential -> types +val existential_opt_value : evar_map -> existential -> constr option (* Assume empty universe constraints in [evar_map] and [conv_pbs] *) -val subst_evar_defs_light : substitution -> evar_defs -> evar_defs +val subst_evar_defs_light : substitution -> evar_map -> evar_map (* spiwack: this function seems to somewhat break the abstraction. *) -val evars_reset_evd : evar_defs -> evar_defs -> evar_defs +val evars_reset_evd : evar_map -> evar_map -> evar_map @@ -180,81 +180,81 @@ type hole_kind = (* spiwack: [is_undefined_evar] should be considered a candidate for moving to evarutils *) -val is_undefined_evar : evar_defs -> constr -> bool -val undefined_evars : evar_defs -> evar_defs +val is_undefined_evar : evar_map -> constr -> bool +val undefined_evars : evar_map -> evar_map val evar_declare : named_context_val -> evar -> types -> ?src:loc * hole_kind -> - ?filter:bool list -> evar_defs -> evar_defs -val evar_source : existential_key -> evar_defs -> loc * hole_kind + ?filter:bool list -> evar_map -> evar_map +val evar_source : existential_key -> evar_map -> loc * hole_kind (* spiwack: this function seems to somewhat break the abstraction. *) (* [evar_merge evd ev1] extends the evars of [evd] with [evd1] *) -val evar_merge : evar_defs -> evar_defs -> evar_defs +val evar_merge : evar_map -> evar_map -> evar_map (* Unification constraints *) type conv_pb = Reduction.conv_pb type evar_constraint = conv_pb * env * constr * constr -val add_conv_pb : evar_constraint -> evar_defs -> evar_defs +val add_conv_pb : evar_constraint -> evar_map -> evar_map module ExistentialSet : Set.S with type elt = existential_key -val extract_changed_conv_pbs : evar_defs -> +val extract_changed_conv_pbs : evar_map -> (ExistentialSet.t -> evar_constraint -> bool) -> - evar_defs * evar_constraint list -val extract_all_conv_pbs : evar_defs -> evar_defs * evar_constraint list + evar_map * evar_constraint list +val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list (* Metas *) -val find_meta : evar_defs -> metavariable -> clbinding -val meta_list : evar_defs -> (metavariable * clbinding) list -val meta_defined : evar_defs -> metavariable -> bool +val find_meta : evar_map -> metavariable -> clbinding +val meta_list : evar_map -> (metavariable * clbinding) list +val meta_defined : evar_map -> metavariable -> bool (* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if meta has no value *) -val meta_value : evar_defs -> metavariable -> constr -val meta_fvalue : evar_defs -> metavariable -> constr freelisted * instance_status -val meta_opt_fvalue : evar_defs -> metavariable -> (constr freelisted * instance_status) option -val meta_type : evar_defs -> metavariable -> types -val meta_ftype : evar_defs -> metavariable -> types freelisted -val meta_name : evar_defs -> metavariable -> name -val meta_with_name : evar_defs -> identifier -> metavariable +val meta_value : evar_map -> metavariable -> constr +val meta_fvalue : evar_map -> metavariable -> constr freelisted * instance_status +val meta_opt_fvalue : evar_map -> metavariable -> (constr freelisted * instance_status) option +val meta_type : evar_map -> metavariable -> types +val meta_ftype : evar_map -> metavariable -> types freelisted +val meta_name : evar_map -> metavariable -> name +val meta_with_name : evar_map -> identifier -> metavariable val meta_declare : - metavariable -> types -> ?name:name -> evar_defs -> evar_defs -val meta_assign : metavariable -> constr * instance_status -> evar_defs -> evar_defs -val meta_reassign : metavariable -> constr * instance_status -> evar_defs -> evar_defs + metavariable -> types -> ?name:name -> evar_map -> evar_map +val meta_assign : metavariable -> constr * instance_status -> evar_map -> evar_map +val meta_reassign : metavariable -> constr * instance_status -> evar_map -> evar_map (* [meta_merge evd1 evd2] returns [evd2] extended with the metas of [evd1] *) -val meta_merge : evar_defs -> evar_defs -> evar_defs +val meta_merge : evar_map -> evar_map -> evar_map -val undefined_metas : evar_defs -> metavariable list -val metas_of : evar_defs -> meta_type_map -val map_metas_fvalue : (constr -> constr) -> evar_defs -> evar_defs +val undefined_metas : evar_map -> metavariable list +val metas_of : evar_map -> meta_type_map +val map_metas_fvalue : (constr -> constr) -> evar_map -> evar_map type metabinding = metavariable * constr * instance_status -val retract_coercible_metas : evar_defs -> metabinding list * evar_defs +val retract_coercible_metas : evar_map -> metabinding list * evar_map val subst_defined_metas : metabinding list -> constr -> constr option (**********************************************************) (* Sort variables *) -val new_sort_variable : evar_defs -> sorts * evar_defs -val is_sort_variable : evar_defs -> sorts -> bool -val whd_sort_variable : evar_defs -> constr -> constr -val set_leq_sort_variable : evar_defs -> sorts -> sorts -> evar_defs -val define_sort_variable : evar_defs -> sorts -> sorts -> evar_defs +val new_sort_variable : evar_map -> sorts * evar_map +val is_sort_variable : evar_map -> sorts -> bool +val whd_sort_variable : evar_map -> constr -> constr +val set_leq_sort_variable : evar_map -> sorts -> sorts -> evar_map +val define_sort_variable : evar_map -> sorts -> sorts -> evar_map (*********************************************************************) (* constr with holes *) -type open_constr = evar_defs * constr +type open_constr = evar_map * constr (*********************************************************************) (* The type constructor ['a sigma] adds an evar map to an object of type ['a] *) type 'a sigma = { it : 'a ; - sigma : evar_defs} + sigma : evar_map} val sig_it : 'a sigma -> 'a -val sig_sig : 'a sigma -> evar_defs +val sig_sig : 'a sigma -> evar_map (**********************************************************) (* Failure explanation *) @@ -265,16 +265,15 @@ type unsolvability_explanation = SeveralInstancesFound of int (* debug pretty-printer: *) val pr_evar_info : evar_info -> Pp.std_ppcmds -val pr_evar_defs : evar_defs -> Pp.std_ppcmds -val pr_sort_constraints : evar_defs -> Pp.std_ppcmds +val pr_evar_map : evar_map -> Pp.std_ppcmds +val pr_sort_constraints : evar_map -> Pp.std_ppcmds val pr_metaset : Metaset.t -> Pp.std_ppcmds (*** /!\Deprecated /!\ ***) -type evar_map = evar_defs -(* create an [evar_defs] with empty meta map: *) -val create_evar_defs : evar_defs -> evar_defs -val create_goal_evar_defs : evar_defs -> evar_defs -val is_defined_evar : evar_defs -> existential -> bool -val subst_evar_map : substitution -> evar_defs -> evar_defs +(* create an [evar_map] with empty meta map: *) +val create_evar_defs : evar_map -> evar_map +val create_goal_evar_defs : evar_map -> evar_map +val is_defined_evar : evar_map -> existential -> bool +val subst_evar_map : substitution -> evar_map -> evar_map (*** /Deprecaded ***) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index eaa2e6757..10d9a1c4e 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -101,7 +101,7 @@ sig evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_defs ref -> env -> typing_constraint -> rawconstr -> constr + evar_map ref -> env -> typing_constraint -> rawconstr -> constr (* More general entry point with evars from ltac *) @@ -117,7 +117,7 @@ sig val understand_ltac : evar_map -> env -> var_map * unbound_ltac_var_map -> - typing_constraint -> rawconstr -> evar_defs * constr + typing_constraint -> rawconstr -> evar_map * constr (* Standard call to get a constr from a rawconstr, resolving implicit args *) @@ -139,24 +139,24 @@ sig (* Idem but do not fail on unresolved evars *) - val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment + val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment (*i*) (* Internal of Pretyping... * Unused outside, but useful for debugging *) val pretype : - type_constraint -> env -> evar_defs ref -> + type_constraint -> env -> evar_map ref -> var_map * (identifier * identifier option) list -> rawconstr -> unsafe_judgment val pretype_type : - val_constraint -> env -> evar_defs ref -> + val_constraint -> env -> evar_map ref -> var_map * (identifier * identifier option) list -> rawconstr -> unsafe_type_judgment val pretype_gen : - bool -> bool -> evar_defs ref -> env -> + bool -> bool -> evar_map ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 7524c72a6..e3b18f73c 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -44,7 +44,7 @@ sig evar_map -> env -> ?expected_type:types -> rawconstr -> open_constr val understand_tcc_evars : ?fail_evar:bool -> ?resolve_classes:bool -> - evar_defs ref -> env -> typing_constraint -> rawconstr -> constr + evar_map ref -> env -> typing_constraint -> rawconstr -> constr (* More general entry point with evars from ltac *) @@ -60,7 +60,7 @@ sig val understand_ltac : evar_map -> env -> var_map * unbound_ltac_var_map -> - typing_constraint -> rawconstr -> evar_defs * constr + typing_constraint -> rawconstr -> evar_map * constr (* Standard call to get a constr from a rawconstr, resolving implicit args *) @@ -81,23 +81,23 @@ sig val understand_judgment : evar_map -> env -> rawconstr -> unsafe_judgment (* Idem but do not fail on unresolved evars *) - val understand_judgment_tcc : evar_defs ref -> env -> rawconstr -> unsafe_judgment + val understand_judgment_tcc : evar_map ref -> env -> rawconstr -> unsafe_judgment (*i*) (* Internal of Pretyping... *) val pretype : - type_constraint -> env -> evar_defs ref -> + type_constraint -> env -> evar_map ref -> var_map * (identifier * identifier option) list -> rawconstr -> unsafe_judgment val pretype_type : - val_constraint -> env -> evar_defs ref -> + val_constraint -> env -> evar_map ref -> var_map * (identifier * identifier option) list -> rawconstr -> unsafe_type_judgment val pretype_gen : - bool -> bool -> evar_defs ref -> env -> + bool -> bool -> evar_map ref -> env -> var_map * (identifier * identifier option) list -> typing_constraint -> rawconstr -> constr diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 3c3190484..1268a3f3b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -217,6 +217,6 @@ val head_unfold_under_prod : transparent_state -> reduction_function val whd_betaiota_deltazeta_for_iota_state : state_reduction_function (*s Meta-related reduction functions *) -val meta_instance : evar_defs -> constr freelisted -> constr -val nf_meta : evar_defs -> constr -> constr -val meta_reducible_instance : evar_defs -> constr freelisted -> constr +val meta_instance : evar_map -> constr freelisted -> constr +val nf_meta : evar_map -> constr -> constr +val meta_reducible_instance : evar_map -> constr freelisted -> constr diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 19ec47cf4..997b28c10 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -87,7 +87,7 @@ val mark_unresolvables : evar_map -> evar_map val is_class_evar : evar_map -> evar_info -> bool val resolve_typeclasses : ?onlyargs:bool -> ?split:bool -> ?fail:bool -> - env -> evar_defs -> evar_defs + env -> evar_map -> evar_map val resolve_one_typeclass : env -> evar_map -> types -> open_constr val register_set_typeclass_transparency : (evaluable_global_reference -> bool -> unit) -> unit @@ -96,5 +96,5 @@ val set_typeclass_transparency : evaluable_global_reference -> bool -> unit val register_add_instance_hint : (global_reference -> int option -> unit) -> unit val add_instance_hint : global_reference -> int option -> unit -val solve_instanciations_problem : (env -> evar_defs -> bool -> bool -> bool -> evar_defs) ref +val solve_instanciations_problem : (env -> evar_map -> bool -> bool -> bool -> evar_map) ref val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index ae9dec97f..1de8b7a5f 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -28,7 +28,7 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * identifier located (* Class name, method *) | NoInstance of identifier located * constr list - | UnsatisfiableConstraints of evar_defs * (existential_key * hole_kind) option + | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *) exception TypeClassError of env * typeclass_error diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 5cf850890..7fd04e225 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -28,7 +28,7 @@ type typeclass_error = | NotAClass of constr | UnboundMethod of global_reference * identifier located (* Class name, method *) | NoInstance of identifier located * constr list - | UnsatisfiableConstraints of evar_defs * (existential_key * hole_kind) option + | UnsatisfiableConstraints of evar_map * (existential_key * hole_kind) option | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *) exception TypeClassError of env * typeclass_error @@ -39,7 +39,7 @@ val unbound_method : env -> global_reference -> identifier located -> 'a val no_instance : env -> identifier located -> constr list -> 'a -val unsatisfiable_constraints : env -> evar_defs -> evar option -> 'a +val unsatisfiable_constraints : env -> evar_map -> evar option -> 'a val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a diff --git a/pretyping/typing.mli b/pretyping/typing.mli index 0aa65bef3..9a40d01ec 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -25,10 +25,10 @@ val sort_of : env -> evar_map -> types -> sorts val check : env -> evar_map -> constr -> types -> unit (* The same but with metas... *) -val mtype_of : env -> evar_defs -> constr -> types -val msort_of : env -> evar_defs -> types -> sorts -val mcheck : env -> evar_defs -> constr -> types -> unit -val meta_type : evar_defs -> metavariable -> types +val mtype_of : env -> evar_map -> constr -> types +val msort_of : env -> evar_map -> types -> sorts +val mcheck : env -> evar_map -> constr -> types -> unit +val meta_type : evar_map -> metavariable -> types (* unused typing function... *) -val mtype_of_type : env -> evar_defs -> types -> types +val mtype_of_type : env -> evar_map -> types -> types diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 2df1c648a..cc62a9bb8 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -27,23 +27,23 @@ val default_no_delta_unify_flags : unify_flags (* The "unique" unification fonction *) val w_unify : - bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_defs -> evar_defs + bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map (* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a subterm of [t]. Constraints are added to [m] and the matched subterm of [t] is also returned. *) val w_unify_to_subterm : - env -> ?flags:unify_flags -> constr * constr -> evar_defs -> evar_defs * constr + env -> ?flags:unify_flags -> constr * constr -> evar_map -> evar_map * constr val w_unify_to_subterm_all : - env -> ?flags:unify_flags -> constr * constr -> evar_defs -> (evar_defs * constr) list + env -> ?flags:unify_flags -> constr * constr -> evar_map -> (evar_map * constr) list -val w_unify_meta_types : env -> ?flags:unify_flags -> evar_defs -> evar_defs +val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map (* [w_coerce_to_type env evd c ctyp typ] tries to coerce [c] of type [ctyp] so that its gets type [typ]; [typ] may contain metavariables *) -val w_coerce_to_type : env -> evar_defs -> constr -> types -> types -> - evar_defs * constr +val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> + evar_map * constr (*i This should be in another module i*) @@ -51,4 +51,4 @@ val w_coerce_to_type : env -> evar_defs -> constr -> types -> types -> (* abstracts the terms in l over c to get a term of type t *) (* (exported for inv.ml) *) val abstract_list_all : - env -> evar_defs -> constr -> constr -> constr list -> constr + env -> evar_map -> constr -> constr -> constr list -> constr diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index ab0fdf831..0bd616809 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.mli @@ -21,7 +21,7 @@ open Rawterm (* Refinement of existential variables. *) val w_refine : evar * evar_info -> - (var_map * unbound_ltac_var_map) * rawconstr -> evar_defs -> evar_defs + (var_map * unbound_ltac_var_map) * rawconstr -> evar_map -> evar_map val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate diff --git a/proofs/refiner.ml b/proofs/refiner.ml index c66e9c84b..c9c956a1c 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -939,4 +939,4 @@ let print_pftreestate {tpf = pf; tpfsigma = sigma; tstack = stack } = prlist_with_sep (fun () -> str ";") (fun (n,_) -> int n) (List.rev stack) ++ str "] is:")) ++ fnl() ++ !pp_proof sigma (Global.named_context()) pf ++ - Evd.pr_evar_defs sigma + Evd.pr_evar_map sigma diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index acccfb812..9e35abfc8 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -244,9 +244,9 @@ let rec pr_list f = function | a::l1 -> (f a) ++ pr_list f l1 let pr_gls gls = - hov 0 (pr_evar_defs (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) + hov 0 (pr_evar_map (sig_sig gls) ++ fnl () ++ db_pr_goal (sig_it gls)) let pr_glls glls = - hov 0 (pr_evar_defs (sig_sig glls) ++ fnl () ++ + hov 0 (pr_evar_map (sig_sig glls) ++ fnl () ++ prlist_with_sep pr_fnl db_pr_goal (sig_it glls)) diff --git a/tactics/decl_proof_instr.ml b/tactics/decl_proof_instr.ml index 8c47497a1..9c58f06ee 100644 --- a/tactics/decl_proof_instr.ml +++ b/tactics/decl_proof_instr.ml @@ -327,7 +327,7 @@ type stackd_elt = se_type:types; se_last_meta:metavariable; se_meta_list:(metavariable*types) list; - se_evd: evar_defs} + se_evd: evar_map} let rec replace_in_list m l = function [] -> raise Not_found diff --git a/tactics/equality.mli b/tactics/equality.mli index 8c43888fb..e79254ce2 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -49,7 +49,7 @@ val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic val register_general_rewrite_clause : (identifier option -> orientation -> occurrences -> open_constr with_bindings -> new_goals:constr list -> tactic) -> unit -val register_is_applied_rewrite_relation : (env -> evar_defs -> rel_context -> constr -> open_constr option) -> unit +val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> open_constr option) -> unit val general_rewrite_ebindings_clause : identifier option -> orientation -> occurrences -> ?tac:(tactic * conditions) -> open_constr with_bindings -> evars_flag -> tactic diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index d3d488183..1ba25fc60 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -429,7 +429,7 @@ type rewrite_flags = { under_lambdas : bool; on_morphisms : bool } let default_flags = { under_lambdas = true; on_morphisms = true; } -type evars = evar_defs * evar_defs (* goal evars, constraint evars *) +type evars = evar_map * evar_map (* goal evars, constraint evars *) type rewrite_result_info = { rew_car : constr; @@ -442,7 +442,7 @@ type rewrite_result_info = { type rewrite_result = rewrite_result_info option -type strategy = Environ.env -> evar_defs -> constr -> types -> +type strategy = Environ.env -> evar_map -> constr -> types -> constr option -> evars -> rewrite_result option let resolve_subrelation env sigma car rel rel' res = @@ -525,7 +525,7 @@ let apply_rule hypinfo loccs : strategy = | Some (env', (prf, (car, rel, c1, c2))) when is_occ !occ -> begin let goalevars = Evd.evar_merge (fst evars) - (Evd.undefined_evars (Evarutil.nf_evar_defs env'.evd)) + (Evd.undefined_evars (Evarutil.nf_evar_map env'.evd)) in let res = { rew_car = ty; rew_rel = rel; rew_from = c1; rew_to = c2; rew_prf = prf; rew_evars = goalevars, snd evars } diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index 307e3a97d..ce8cfa7db 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -43,7 +43,7 @@ and interp_sign = debug : debug_info; trace : ltac_trace } -val extract_ltac_vars : interp_sign -> Evd.evar_defs -> Environ.env -> +val extract_ltac_vars : interp_sign -> Evd.evar_map -> Environ.env -> Pretyping.var_map * Pretyping.unbound_ltac_var_map (* Transforms an id into a constr if possible *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 48e45e8d8..70e8557db 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -887,7 +887,7 @@ let check_evars sigma evm gl = if rest <> Evd.empty then errorlabstrm "apply" (str"Uninstantiated existential "++ str(plural (List.length (Evd.to_list rest)) "variable")++str": " ++ - fnl () ++ pr_evar_defs rest);; + fnl () ++ pr_evar_map rest);; let get_bindings_evars = function | ImplicitBindings largs -> List.map fst largs diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index f4ea23215..b45e45c80 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -55,7 +55,7 @@ let subst_evar_in_evm evar def evm = let rec safe_define evm ev c = if not (closedn (-1) c) then raise Termops.CannotFilter else -(* msgnl(str"safe_define "++pr_evar_defs evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*) +(* msgnl(str"safe_define "++pr_evar_map evm++spc()++str" |- ?"++Util.pr_int ev++str" := "++pr_constr c);*) let evi = (Evd.find evm ev) in let define_subst evm sigma = Util.Intmap.fold @@ -111,7 +111,7 @@ let complete_evar (cl,gen,evm:signature) (ev,evi) (k:signature -> unit) = let def = applistc (Libnames.constr_of_global gr) argl in (* msgnl(str"essayons ?"++Util.pr_int ev++spc()++str":="++spc() ++pr_constr def++spc()++str":"++spc()++pr_constr (Global.type_of_global gr)*) - (*++spc()++str"dans"++spc()++pr_evar_defs evm++spc());*) + (*++spc()++str"dans"++spc()++pr_evar_map evm++spc());*) try let evm = safe_define evm ev def in k (cl,gen,evm); @@ -147,7 +147,7 @@ let complete_with_evars_permut (cl,gen,evm:signature) evl c (k:signature -> unit let tyl = List.map (fun (_,_,t) -> t) ctx in let ((cl,gen,evm),argl) = add_gen_ctx (cl,gen,evm) tyl in let def = applistc c argl in -(* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_defs evm);*) +(* msgnl(str"trouvé def ?"++Util.pr_int ev++str" := "++pr_constr def++str " dans "++pr_evar_map evm);*) try if not (Evd.is_defined evm ev) then let evm = safe_define evm ev def in @@ -220,7 +220,7 @@ let complete_signature_with_def gr deftyp (k:instance_decl_function -> signature ( fun ctx typ -> List.iter (fun ((cl,ev,evm),_,_) -> -(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_defs evm);*) +(* msgnl(pr_global gr++str" : "++pr_constr typ++str" matche ?"++Util.pr_int ev++str " dans "++pr_evar_map evm);*) smap := Gmapl.add (cl,evm) (ctx,ev) !smap) (Recordops.methods_matching typ) ) [] deftyp; @@ -263,7 +263,7 @@ let declare_instance (k:global_reference -> rel_context -> constr list -> unit) then Evd.remove evm ev,gen else evm,(ev::gen)) gen (evm,[]) in -(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_defs evm);*) +(* msgnl(str"instance complète : ["++Util.prlist_with_sep (fun _ -> str";") Util.pr_int gen++str"] : "++spc()++pr_evar_map evm);*) let ngen = List.length gen in let (_,ctx,evm) = List.fold_left ( fun (i,ctx,evm) ev -> diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 8412a39f3..9c4f759c9 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -173,7 +173,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) Namegen.next_global_ident_away i (Termops.ids_of_context env) in let env' = push_rel_context ctx' env in - evars := Evarutil.nf_evar_defs !evars; + evars := Evarutil.nf_evar_map !evars; evars := resolve_typeclasses env !evars; let sigma = !evars in let subst = List.map (Evarutil.nf_evar sigma) subst in @@ -244,7 +244,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) Evarutil.nf_isevar !evars t in let term = Termops.it_mkLambda_or_LetIn app ctx' in - evars := Evarutil.nf_evar_defs !evars; + evars := Evarutil.nf_evar_map !evars; let term = Evarutil.nf_isevar !evars term in let evm = undefined_evars !evars in Evarutil.check_evars env Evd.empty !evars termtype; diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index c769e8930..852e7588a 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -522,7 +522,7 @@ let pr_constraints printenv env evm = prlist_with_sep (fun () -> fnl ()) (fun (ev, evi) -> str(string_of_existential ev)++ str " == " ++ pr_constr evi.evar_concl) l else - pr_evar_defs evm + pr_evar_map evm let explain_unsatisfiable_constraints env evd constr = let evm = Evarutil.nf_evars evd in |