diff options
| -rw-r--r-- | engine/evarutil.ml | 22 |
1 files changed, 16 insertions, 6 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml index 7c2ecca89e..4bff98c0c2 100644 --- a/engine/evarutil.ml +++ b/engine/evarutil.ml @@ -331,11 +331,21 @@ let push_rel_decl_to_named_context let map_decl f d = NamedDecl.map_constr f d in - let replace_var_named_declaration id0 id decl = - let id' = NamedDecl.get_id decl in - let id' = if Id.equal id0 id' then id else id' in - let vsubst = [id0 , mkVar id] in - decl |> NamedDecl.set_id id' |> map_decl (replace_vars vsubst) + let replace_var_named_declaration id0 id nc = + let rec replace = function + | [] -> false, [] + | decl :: nc -> + let seen, nc = replace nc in + if seen then + let vsubst = [id0 , mkVar id] in + true, (map_decl (fun c -> replace_vars vsubst c) decl) :: nc + else if Id.equal id0 (NamedDecl.get_id decl) then + true, (NamedDecl.set_id id decl) :: nc + else + false, decl :: nc + in + let (_, nc) = replace nc in + nc in let extract_if_neq id = function | Anonymous -> None @@ -366,7 +376,7 @@ let push_rel_decl_to_named_context context. Unless [id] is a section variable. *) 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 = List.map (replace_var_named_declaration id0 id) nc in + let nc = replace_var_named_declaration id0 id nc in (push_var id0 subst, Id.Set.add id avoid, d :: nc) | Some id0 when hypnaming = FailIfConflict -> user_err Pp.(Id.print id0 ++ str " is already used.") |