aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/eConstr.ml5
-rw-r--r--engine/eConstr.mli3
-rw-r--r--engine/evarutil.ml22
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/evd.ml31
-rw-r--r--engine/univSubst.ml6
6 files changed, 45 insertions, 24 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index ca681e58f8..42c9359ff0 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -733,6 +733,11 @@ let map_rel_context_in_env f env sign =
in
aux env [] (List.rev sign)
+let match_named_context_val :
+ named_context_val -> (named_declaration * lazy_val * named_context_val) option =
+ match unsafe_eq with
+ | Refl -> match_named_context_val
+
let fresh_global ?loc ?rigid ?names env sigma reference =
let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
evd, t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9a73c3e3f5..aea441b90b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -322,6 +322,9 @@ val lookup_named_val : variable -> named_context_val -> named_declaration
val map_rel_context_in_env :
(env -> constr -> constr) -> env -> rel_context -> rel_context
+val match_named_context_val :
+ named_context_val -> (named_declaration * lazy_val * named_context_val) option
+
(* XXX Missing Sigma proxy *)
val fresh_global :
?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 5fcadfcef7..eea7e38f87 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -287,7 +287,7 @@ let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c =
EConstr.of_constr c
type ext_named_context =
- csubst * Id.Set.t * EConstr.named_context
+ csubst * Id.Set.t * named_context_val
let push_var id { csubst_len = n; csubst_var = v; csubst_rel = s; csubst_rev = r } =
let s = Int.Map.add n (Constr.mkVar id) s in
@@ -325,22 +325,22 @@ type naming_mode =
let push_rel_decl_to_named_context
?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
- sigma decl (subst, avoid, nc) =
+ sigma decl ((subst, avoid, nc) : ext_named_context) =
let open EConstr in
let open Vars in
let map_decl f d =
NamedDecl.map_constr f d
in
- let rec replace_var_named_declaration id0 id = function
- | [] -> []
- | decl :: nc ->
+ let rec replace_var_named_declaration id0 id nc = match match_named_context_val nc with
+ | None -> empty_named_context_val
+ | Some (decl, _, nc) ->
if Id.equal id0 (NamedDecl.get_id decl) then
(* Stop here, the variable cannot occur before its definition *)
- (NamedDecl.set_id id decl) :: nc
+ push_named_context_val (NamedDecl.set_id id decl) nc
else
let nc = replace_var_named_declaration id0 id nc in
let vsubst = [id0 , mkVar id] in
- map_decl (fun c -> replace_vars vsubst c) decl :: nc
+ push_named_context_val (map_decl (fun c -> replace_vars vsubst c) decl) nc
in
let extract_if_neq id = function
| Anonymous -> None
@@ -372,7 +372,7 @@ let push_rel_decl_to_named_context
let subst = update_var id0 id subst in
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
let nc = replace_var_named_declaration id0 id nc in
- (push_var id0 subst, Id.Set.add id avoid, d :: nc)
+ (push_var id0 subst, Id.Set.add id avoid, push_named_context_val d nc)
| Some id0 when hypnaming = FailIfConflict ->
user_err Pp.(Id.print id0 ++ str " is already used.")
| _ ->
@@ -381,7 +381,7 @@ let push_rel_decl_to_named_context
the new binder has name [id]. Which amounts to the same
behaviour than when [id=id0]. *)
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in
- (push_var id subst, Id.Set.add id avoid, d :: nc)
+ (push_var id subst, Id.Set.add id avoid, push_named_context_val d nc)
let push_rel_context_to_named_context ?hypnaming env sigma typ =
(* compute the instances relative to the named context and rel_context *)
@@ -399,8 +399,8 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
(* We do keep the instances corresponding to local definition (see above) *)
let (subst, _, env) =
Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc)
- (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
- (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst)
+ (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
+ (env, csubst_subst subst typ, inst_rels@inst_vars, subst)
(*------------------------------------*
* Entry points to define new evars *
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index b5c7ccb283..b3c94e6b3b 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -268,7 +268,7 @@ val empty_csubst : csubst
val csubst_subst : csubst -> constr -> constr
type ext_named_context =
- csubst * Id.Set.t * named_context
+ csubst * Id.Set.t * named_context_val
val push_rel_decl_to_named_context : ?hypnaming:naming_mode ->
evar_map -> rel_declaration -> ext_named_context -> ext_named_context
diff --git a/engine/evd.ml b/engine/evd.ml
index ff13676818..f0ee8ae68f 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1174,12 +1174,34 @@ let meta_declare mv v ?(name=Anonymous) evd =
let metas = Metamap.add mv (Cltyp(name,mk_freelisted v)) evd.metas in
set_metas evd metas
+(* If the meta is defined then forget its name *)
+let meta_name evd mv =
+ try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
+
+let evar_source_of_meta mv evd =
+ match meta_name evd mv with
+ | Anonymous -> Loc.tag Evar_kinds.GoalEvar
+ | Name id -> Loc.tag @@ Evar_kinds.VarInstance id
+
+let use_meta_source evd mv v =
+ match Constr.kind v with
+ | Evar (evk,_) ->
+ let f = function
+ | None -> None
+ | Some evi as x ->
+ match evi.evar_source with
+ | None, Evar_kinds.GoalEvar -> Some { evi with evar_source = evar_source_of_meta mv evd }
+ | _ -> x in
+ { evd with undf_evars = EvMap.update evk f evd.undf_evars }
+ | _ -> evd
+
let meta_assign mv (v, pb) evd =
let modify _ = function
| Cltyp (na, ty) -> Clval (na, (mk_freelisted v, pb), ty)
| _ -> anomaly ~label:"meta_assign" (Pp.str "already defined.")
in
let metas = Metamap.modify mv modify evd.metas in
+ let evd = use_meta_source evd mv v in
set_metas evd metas
let meta_reassign mv (v, pb) evd =
@@ -1190,10 +1212,6 @@ let meta_reassign mv (v, pb) evd =
let metas = Metamap.modify mv modify evd.metas in
set_metas evd metas
-(* If the meta is defined then forget its name *)
-let meta_name evd mv =
- try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
-
let clear_metas evd = {evd with metas = Metamap.empty}
let meta_merge ?(with_univs = true) evd1 evd2 =
@@ -1217,11 +1235,6 @@ let retract_coercible_metas evd =
let metas = Metamap.Smart.mapi map evd.metas in
!mc, set_metas evd metas
-let evar_source_of_meta mv evd =
- match meta_name evd mv with
- | Anonymous -> Loc.tag Evar_kinds.GoalEvar
- | Name id -> Loc.tag @@ Evar_kinds.VarInstance id
-
let dependent_evar_ident ev evd =
let evi = find evd ev in
match evi.evar_source with
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index a691239ee2..92211d5f3d 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -131,9 +131,9 @@ let nf_evars_and_universes_opt_subst f subst =
let rec aux c =
match kind c with
| Evar (evk, args) ->
- let args = List.map aux args in
- (match try f (evk, args) with Not_found -> None with
- | None -> mkEvar (evk, args)
+ let args' = List.Smart.map aux args in
+ (match try f (evk, args') with Not_found -> None with
+ | None -> if args == args' then c else mkEvar (evk, args')
| Some c -> aux c)
| Const pu ->
let pu' = subst_univs_fn_puniverses lsubst pu in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 01:44:03 +0000