aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/subtac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/subtac')
-rw-r--r--plugins/subtac/eterm.mli2
-rw-r--r--plugins/subtac/subtac_cases.ml6
-rw-r--r--plugins/subtac/subtac_classes.ml4
-rw-r--r--plugins/subtac/subtac_classes.mli2
-rw-r--r--plugins/subtac/subtac_command.ml4
-rw-r--r--plugins/subtac/subtac_command.mli14
-rw-r--r--plugins/subtac/subtac_pretyping.ml2
-rw-r--r--plugins/subtac/subtac_pretyping.mli6
-rw-r--r--plugins/subtac/subtac_utils.ml8
-rw-r--r--plugins/subtac/subtac_utils.mli8
10 files changed, 28 insertions, 28 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-02 09:09:50 +0000