aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.mli38
-rw-r--r--plugins/setoid_ring/newring.ml53
-rw-r--r--pretyping/cases.ml18
-rw-r--r--pretyping/coercion.ml4
-rw-r--r--pretyping/evarconv.ml10
-rw-r--r--pretyping/evarconv.mli3
-rw-r--r--pretyping/program.ml4
-rw-r--r--pretyping/unification.ml4
-rw-r--r--tactics/equality.ml36
-rw-r--r--tactics/tactics.ml3
10 files changed, 105 insertions, 68 deletions
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 3bbd2923c..7595de04c 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -50,13 +50,6 @@ val new_pure_evar :
val new_pure_evar_full : evar_map -> evar_info -> evar_map * Evar.t
-(** the same with side-effects *)
-val e_new_evar :
- env -> evar_map ref -> ?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 -> constr
-
(** Create a new Type existential variable, as we keep track of
them during type-checking and unification. *)
val new_type_evar :
@@ -65,13 +58,7 @@ val new_type_evar :
?principal:bool -> ?hypnaming:naming_mode -> rigid ->
evar_map * (constr * Sorts.t)
-val e_new_type_evar : env -> evar_map ref ->
- ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
- ?naming:Misctypes.intro_pattern_naming_expr ->
- ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
-
val new_Type : ?rigid:rigid -> env -> evar_map -> evar_map * constr
-val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
val restrict_evar : evar_map -> Evar.t -> Filter.t ->
?src:Evar_kinds.t Loc.located -> constr list option -> evar_map * Evar.t
@@ -79,7 +66,6 @@ val restrict_evar : evar_map -> Evar.t -> Filter.t ->
(** Polymorphic constants *)
val new_global : evar_map -> GlobRef.t -> evar_map * constr
-val e_new_global : evar_map ref -> GlobRef.t -> 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
@@ -187,8 +173,6 @@ val nf_evars_universes : evar_map -> Constr.constr -> Constr.constr
val nf_evars_and_universes : evar_map -> evar_map * (Constr.constr -> Constr.constr)
[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
-val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
-[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
(** Normalize the evar map w.r.t. universes, after simplification of constraints.
Return the substitution function for constrs as well. *)
@@ -276,3 +260,25 @@ type type_constraint = types option
[@@ocaml.deprecated "use the version in Evardefine"]
type val_constraint = constr option
[@@ocaml.deprecated "use the version in Evardefine"]
+
+val e_new_evar :
+ env -> evar_map ref -> ?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 -> constr
+[@@ocaml.deprecated "Use [Evd.new_evar]"]
+
+val e_new_type_evar : env -> evar_map ref ->
+ ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
+ ?naming:Misctypes.intro_pattern_naming_expr ->
+ ?principal:bool -> ?hypnaming:naming_mode -> rigid -> constr * Sorts.t
+[@@ocaml.deprecated "Use [Evd.new_type_evar]"]
+
+val e_new_Type : ?rigid:rigid -> env -> evar_map ref -> constr
+[@@ocaml.deprecated "Use [Evd.new_Type]"]
+
+val e_new_global : evar_map ref -> GlobRef.t -> constr
+[@@ocaml.deprecated "Use [Evd.new_global]"]
+
+val e_nf_evars_and_universes : evar_map ref -> (Constr.constr -> Constr.constr) * Universes.universe_opt_subst
+[@@ocaml.deprecated "Use Evd.minimize_universes and nf_evars_universes"]
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 5facf2a80..b2ac3b5a4 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -247,9 +247,10 @@ let coq_nil = coq_reference "nil"
let lapp f args = mkApp(Lazy.force f,args)
-let plapp evd f args =
- let fc = Evarutil.e_new_global evd (Lazy.force f) in
- mkApp(fc,args)
+let plapp evdref f args =
+ let evd, fc = Evarutil.new_global !evdref (Lazy.force f) in
+ evdref := evd;
+ mkApp(fc,args)
let dest_rel0 sigma t =
match EConstr.kind sigma t with
@@ -586,48 +587,52 @@ let make_hyp env evd c =
let t = Retyping.get_type_of env !evd c in
plapp evd coq_mkhypo [|t;c|]
-let make_hyp_list env evd lH =
- let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let make_hyp_list env evdref lH =
+ let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+ evdref := evd;
let l =
List.fold_right
- (fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
- (plapp evd coq_nil [|carrier|])
+ (fun c l -> plapp evdref coq_cons [|carrier; (make_hyp env evdref c); l|]) lH
+ (plapp evdref coq_nil [|carrier|])
in
- let l' = Typing.e_solve_evars env evd l in
+ let l' = Typing.e_solve_evars env evdref l in
let l' = EConstr.Unsafe.to_constr l' in
- Evarutil.nf_evars_universes !evd l'
+ Evarutil.nf_evars_universes !evdref l'
-let interp_power env evd pow =
- let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_power env evdref pow =
+ let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+ evdref := evd;
match pow with
| None ->
let t = ArgArg(Loc.tag (Lazy.force ltac_inv_morph_nothing)) in
- (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evd coq_None [|carrier|])
+ (TacArg(Loc.tag (TacCall(Loc.tag (t,[])))), plapp evdref coq_None [|carrier|])
| Some (tac, spec) ->
let tac =
match tac with
| CstTac t -> Tacintern.glob_tactic t
| Closed lc ->
closed_term_ast (List.map Smartlocate.global_with_alias lc) in
- let spec = make_hyp env evd (ic_unsafe spec) in
- (tac, plapp evd coq_Some [|carrier; spec|])
+ let spec = make_hyp env evdref (ic_unsafe spec) in
+ (tac, plapp evdref coq_Some [|carrier; spec|])
-let interp_sign env evd sign =
- let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_sign env evdref sign =
+ let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+ evdref := evd;
match sign with
- | None -> plapp evd coq_None [|carrier|]
+ | None -> plapp evdref coq_None [|carrier|]
| Some spec ->
- let spec = make_hyp env evd (ic_unsafe spec) in
- plapp evd coq_Some [|carrier;spec|]
+ let spec = make_hyp env evdref (ic_unsafe spec) in
+ plapp evdref coq_Some [|carrier;spec|]
(* Same remark on ill-typed terms ... *)
-let interp_div env evd div =
- let carrier = Evarutil.e_new_global evd (Lazy.force coq_hypo) in
+let interp_div env evdref div =
+ let evd, carrier = Evarutil.new_global !evdref (Lazy.force coq_hypo) in
+ evdref := evd;
match div with
- | None -> plapp evd coq_None [|carrier|]
+ | None -> plapp evdref coq_None [|carrier|]
| Some spec ->
- let spec = make_hyp env evd (ic_unsafe spec) in
- plapp evd coq_Some [|carrier;spec|]
+ let spec = make_hyp env evdref (ic_unsafe spec) in
+ plapp evdref coq_Some [|carrier;spec|]
(* Same remark on ill-typed terms ... *)
let add_theory0 name (sigma, rth) eqth morphth cst_tac (pre,post) power sign div =
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4c87b4e7e..16244d8c0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -295,7 +295,8 @@ let inductive_template evdref env tmloc ind =
| LocalAssum (na,ty) ->
let ty = EConstr.of_constr ty in
let ty' = substl subst ty in
- let e = e_new_evar env evdref ~src:(hole_source n) ty' in
+ let evd, e = Evarutil.new_evar env !evdref ~src:(hole_source n) ty' in
+ evdref := evd;
(e::subst,e::evarl,n+1)
| LocalDef (na,b,ty) ->
let b = EConstr.of_constr b in
@@ -396,7 +397,9 @@ let coerce_to_indtype typing_fun evdref env lvar matx tomatchl =
(* Utils *)
let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref =
- let e, u = e_new_type_evar env evdref univ_flexible_alg ~src:src in e
+ let evd, (e, u) = new_type_evar env !evdref univ_flexible_alg ~src:src in
+ evdref := evd;
+ e
let evd_comb2 f evdref x y =
let (evd',y) = f !evdref x y in
@@ -1681,7 +1684,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
(fun i _ ->
try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
1 (rel_context env) in
- let ev' = e_new_evar env evdref ~src ty in
+ let evd, ev' = Evarutil.new_evar env !evdref ~src ty in
+ evdref := evd;
begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with
| Success evd -> evdref := evd
| UnifFailure _ -> assert false
@@ -1712,7 +1716,8 @@ let abstract_tycon ?loc env evdref subst tycon extenv t =
(named_context extenv) in
let filter = Filter.make (rel_filter @ named_filter) in
let candidates = u :: List.map mkRel vl in
- let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in
+ let evd, ev = Evarutil.new_evar extenv !evdref ~src ~filter ~candidates ty in
+ evdref := evd;
lift k ev
in
aux (0,extenv,subst0) t0
@@ -1724,8 +1729,9 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
we are in an impossible branch *)
let n = Context.Rel.length (rel_context env) in
let n' = Context.Rel.length (rel_context tycon_env) in
- let impossible_case_type, u =
- e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in
+ let evd, (impossible_case_type, u) =
+ new_type_evar (reset_context env) !evdref univ_flexible_alg ~src:(Loc.tag ?loc Evar_kinds.ImpossibleCase) in
+ evdref := evd;
(lift (n'-n) impossible_case_type, mkSort u)
| Some t ->
let t = abstract_tycon ?loc tycon_env evdref subst tycon extenv t in
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 6dc3687a0..e8b17d694 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -94,7 +94,9 @@ open Program
let make_existential ?loc ?(opaque = not (get_proofs_transparency ())) na env evdref c =
let src = Loc.tag ?loc (Evar_kinds.QuestionMark (Evar_kinds.Define opaque,na)) in
- Evarutil.e_new_evar env evdref ~src c
+ let evd, v = Evarutil.new_evar env !evdref ~src c in
+ evdref := evd;
+ v
let app_opt env evdref f t =
whd_betaiota !evdref (app_opt f t)
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 144166a34..2144639d5 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1394,6 +1394,16 @@ let the_conv_x_leq env ?(ts=default_transparent_state env) t1 t2 evd =
| Success evd' -> evd'
| UnifFailure (evd',e) -> raise (UnableToUnify (evd',e))
+let make_opt = function
+ | Success evd -> Some evd
+ | UnifFailure _ -> None
+
+let conv env ?(ts=default_transparent_state env) evd t1 t2 =
+ make_opt(evar_conv_x ts env evd CONV t1 t2)
+
+let cumul env ?(ts=default_transparent_state env) evd t1 t2 =
+ make_opt(evar_conv_x ts env evd CUMUL t1 t2)
+
let e_conv env ?(ts=default_transparent_state env) evdref t1 t2 =
match evar_conv_x ts env !evdref CONV t1 t2 with
| Success evd' -> evdref := evd'; true
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 9270d6e3a..da2b4d1b8 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -30,6 +30,9 @@ val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_ma
val e_conv : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr -> bool
+val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+
(** {6 Unification heuristics. } *)
(** Try heuristics to solve pending unification problems and to solve
diff --git a/pretyping/program.ml b/pretyping/program.ml
index 52d940d8e..8cfb7966c 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -16,7 +16,9 @@ let init_reference dir s () = Coqlib.coq_reference "Program" dir s
let papp evdref r args =
let open EConstr in
let gr = delayed_force r in
- mkApp (Evarutil.e_new_global evdref gr, args)
+ let evd, hd = Evarutil.new_global !evdref gr in
+ evdref := evd;
+ mkApp (hd, args)
let sig_typ = init_reference ["Init"; "Specif"] "sig"
let sig_intro = init_reference ["Init"; "Specif"] "exist"
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d98ce9aba..1caa629ff 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -198,8 +198,8 @@ let pose_all_metas_as_evars env evd t =
then nf_betaiota env evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
let src = Evd.evar_source_of_meta mv !evdref in
- let ev = Evarutil.e_new_evar env evdref ~src ty in
- evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) !evdref;
+ let evd, ev = Evarutil.new_evar env !evdref ~src ty in
+ evdref := meta_assign mv (ev,(Conv,TypeNotProcessed)) evd;
ev)
| _ ->
EConstr.map !evdref aux t in
diff --git a/tactics/equality.ml b/tactics/equality.ml
index b6bbd0be4..d142e10a4 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1176,34 +1176,35 @@ let minimal_free_rels_rec env sigma =
let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
let sigdata = find_sigma_data env sort_of_ty in
- let evdref = ref (Evd.clear_metas sigma) in
- let rec sigrec_clausal_form siglen p_i =
+ let rec sigrec_clausal_form sigma siglen p_i =
if Int.equal siglen 0 then
(* is the default value typable with the expected type *)
let dflt_typ = unsafe_type_of env sigma dflt in
try
- let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in
- let () =
- evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in
- dflt
+ let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in
+ let sigma =
+ Evarconv.solve_unif_constraints_with_heuristics env sigma in
+ sigma, dflt
with Evarconv.UnableToUnify _ ->
user_err Pp.(str "Cannot solve a unification problem.")
else
- let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with
+ let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with
| (_sigS,[a;p]) -> (a, p)
| _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in
- let ev = Evarutil.e_new_evar env evdref a in
+ let sigma, ev = Evarutil.new_evar env sigma a in
let rty = beta_applist sigma (p_i_minus_1,[ev]) in
- let tuple_tail = sigrec_clausal_form (siglen-1) rty in
- let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in
+ let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in
+ let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in
match evopt with
| Some w ->
- let w_type = unsafe_type_of env !evdref w in
- if Evarconv.e_cumul env evdref w_type a then
- let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in
- applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
- else
+ let w_type = unsafe_type_of env sigma w in
+ begin match Evarconv.cumul env sigma w_type a with
+ | Some sigma ->
+ let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in
+ sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail])
+ | None ->
user_err Pp.(str "Cannot solve a unification problem.")
+ end
| None ->
(* This at least happens if what has been detected as a
dependency is not one; use an evasive error message;
@@ -1213,8 +1214,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt =
unsolved evars would mean not binding rel *)
user_err Pp.(str "Cannot solve a unification problem.")
in
- let scf = sigrec_clausal_form siglen ty in
- !evdref, Evarutil.nf_evar !evdref scf
+ let sigma = Evd.clear_metas sigma in
+ let sigma, scf = sigrec_clausal_form sigma siglen ty in
+ sigma, Evarutil.nf_evar sigma scf
(* The problem is to build a destructor (a generalization of the
predecessor) which, when applied to a term made of constructors
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index ee76ad077..178c10815 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3840,7 +3840,8 @@ let specialize_eqs id =
| _ ->
if in_eqs then acc, in_eqs, ctx, ty
else
- let e = e_new_evar (push_rel_context ctx env) evars t in
+ let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in
+ evars := sigma;
aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b)
| t -> acc, in_eqs, ctx, ty
in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-15 07:36:01 +0000