1 files changed, 83 insertions, 54 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index b63391913..bd86f4bd2 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -290,78 +290,107 @@ let make_pure_subst evi args =
  *   we have the property that u and phi(t) are convertible in env.
  *)
 
+let csubst_subst (k, s) c =
+  let rec subst n c = match Constr.kind c with
+  | Rel m ->
+    if m <= n then c
+    else if m - n <= k then Int.Map.find (k - m + n) s
+    else mkRel (m - k)
+  | _ -> Constr.map_with_binders succ subst n c
+  in
+  if k = 0 then c else subst 0 c
+
 let subst2 subst vsubst c =
-  substl subst (replace_vars vsubst c)
+  csubst_subst subst (replace_vars vsubst c)
 
-let push_rel_context_to_named_context env typ =
-  (* compute the instances relative to the named context and rel_context *)
+let next_ident_away id avoid =
+  let avoid id = Id.Set.mem id avoid in
+  next_ident_away_from id avoid
+
+let next_name_away na avoid =
+  let avoid id = Id.Set.mem id avoid in
+  let id = match na with Name id -> id | Anonymous -> default_non_dependent_ident in
+  next_ident_away_from id avoid
+
+type csubst = int * Constr.t Int.Map.t
+
+let empty_csubst = (0, Int.Map.empty)
+
+type ext_named_context =
+  csubst * (Id.t * Constr.constr) list *
+  Id.Set.t * Context.Named.t
+
+let push_var id (n, s) =
+  let s = Int.Map.add n (mkVar id) s in
+  (succ n, s)
+
+let push_rel_decl_to_named_context decl (subst, vsubst, avoid, nc) =
   let open Context.Named.Declaration in
-  let ids = List.map get_id (named_context env) in
-  let inst_vars = List.map mkVar ids in
-  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
   let replace_var_named_declaration id0 id decl =
     let id' = get_id decl in
     let id' = if Id.equal id0 id' then id else id' in
     let vsubst = [id0 , mkVar id] in
     decl |> set_id id' |> map_constr (replace_vars vsubst)
   in
-  let replace_var_named_context id0 id  env =
-    let nc = Environ.named_context env in
-    let nc' = List.map (replace_var_named_declaration id0 id) nc in
-    Environ.reset_with_named_context (val_of_named_context nc') env
-  in
   let extract_if_neq id = function
     | Anonymous -> None
     | Name id' when id_ord id id' = 0 -> None
     | Name id' -> Some id'
   in
+  let open Context.Rel.Declaration in
+  let (na, c, t) = to_tuple decl in
+  let open Context.Named.Declaration in
+  let id =
+    (* ppedrot: we want to infer nicer names for the refine tactic, but
+        keeping at the same time backward compatibility in other code
+        using this function. For now, we only attempt to preserve the
+        old behaviour of Program, but ultimately, one should do something
+        about this whole name generation problem. *)
+    if Flags.is_program_mode () then next_name_away na avoid
+    else
+      (** id_of_name_using_hdchar only depends on the rel context which is empty
+          here *)
+      next_ident_away (id_of_name_using_hdchar empty_env t na) avoid
+  in
+  match extract_if_neq id na with
+  | Some id0 when not (is_section_variable id0) ->
+      (* spiwack: if [id<>id0], rather than introducing a new
+          binding named [id], we will keep [id0] (the name given
+          by the user) and rename [id0] into [id] in the named
+          context. Unless [id] is a section variable. *)
+      let subst = (fst subst, Int.Map.map (replace_vars [id0,mkVar id]) (snd subst)) in
+      let vsubst = (id0,mkVar id)::vsubst in
+      let d = match c with
+        | None -> LocalAssum (id0, subst2 subst vsubst t)
+        | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
+      in
+      let nc = List.map (replace_var_named_declaration id0 id) nc in
+      (push_var id0 subst, vsubst, Id.Set.add id avoid, d :: nc)
+  | _ ->
+      (* spiwack: if [id0] is a section variable renaming it is
+          incorrect. We revert to a less robust behaviour where
+          the new binder has name [id]. Which amounts to the same
+          behaviour than when [id=id0]. *)
+      let d = match c with
+        | None -> LocalAssum (id, subst2 subst vsubst t)
+        | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
+      in
+      (push_var id subst, vsubst, Id.Set.add id avoid, d :: nc)
+
+let push_rel_context_to_named_context env typ =
+  (* compute the instances relative to the named context and rel_context *)
+  let open Context.Named.Declaration in
+  let ids = List.map get_id (named_context env) in
+  let avoid = List.fold_right Id.Set.add ids Id.Set.empty in
+  let inst_vars = List.map mkVar ids in
+  let inst_rels = List.rev (rel_list 0 (nb_rel env)) in
   (* move the rel context to a named context and extend the named instance *)
   (* with vars of the rel context *)
   (* We do keep the instances corresponding to local definition (see above) *)
   let (subst, vsubst, _, env) =
-    Context.Rel.fold_outside
-      (fun decl (subst, vsubst, avoid, env) ->
-        let open Context.Rel.Declaration in
-        let na = get_name decl in
-	let c = get_value decl in
-	let t = get_type decl in
-        let open Context.Named.Declaration in
-        let id =
-          (* ppedrot: we want to infer nicer names for the refine tactic, but
-             keeping at the same time backward compatibility in other code
-             using this function. For now, we only attempt to preserve the
-             old behaviour of Program, but ultimately, one should do something
-             about this whole name generation problem. *)
-          if Flags.is_program_mode () then next_name_away na avoid
-          else next_ident_away (id_of_name_using_hdchar env t na) avoid
-        in
-        match extract_if_neq id na with
-        | Some id0 when not (is_section_variable id0) ->
-            (* spiwack: if [id<>id0], rather than introducing a new
-               binding named [id], we will keep [id0] (the name given
-               by the user) and rename [id0] into [id] in the named
-               context. Unless [id] is a section variable. *)
-            let subst = List.map (replace_vars [id0,mkVar id]) subst in
-            let vsubst = (id0,mkVar id)::vsubst in
-            let d = match c with
-              | None -> LocalAssum (id0, subst2 subst vsubst t)
-              | Some c -> LocalDef (id0, subst2 subst vsubst c, subst2 subst vsubst t)
-            in
-            let env = replace_var_named_context id0  id env in
-            (mkVar id0 :: subst, vsubst, id::avoid, push_named d env)
-        | _ ->
-            (* spiwack: if [id0] is a section variable renaming it is
-               incorrect. We revert to a less robust behaviour where
-               the new binder has name [id]. Which amounts to the same
-               behaviour than when [id=id0]. *)
-            let d = match c with
-              | None -> LocalAssum (id, subst2 subst vsubst t)
-              | Some c -> LocalDef (id, subst2 subst vsubst c, subst2 subst vsubst t)
-            in
-	    (mkVar id :: subst, vsubst, id::avoid, push_named d env)
-      )
-      (rel_context env) ~init:([], [], ids, env) in
-  (named_context_val env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
+    Context.Rel.fold_outside push_rel_decl_to_named_context
+      (rel_context env) ~init:(empty_csubst, [], avoid, named_context env) in
+  (val_of_named_context env, subst2 subst vsubst typ, inst_rels@inst_vars, subst, vsubst)
 
 (*------------------------------------*
  * Entry points to define new evars   *