diff options
Diffstat (limited to 'engine')
| -rw-r--r-- | engine/eConstr.ml | 5 | ||||
| -rw-r--r-- | engine/eConstr.mli | 3 | ||||
| -rw-r--r-- | engine/evarutil.ml | 22 | ||||
| -rw-r--r-- | engine/evarutil.mli | 2 |
4 files changed, 20 insertions, 12 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 |