push_rel_context: do not rename section variables.

Renaming section variables is incorrect. And interacts badly with Hints and Canonical Structures in sections. (bug noticed in ssreflect)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17024 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 7 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ec22bb8fc..c8481bca7 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -326,6 +326,12 @@ let push_rel_context_to_named_context env typ =
     | Name id' when id_ord id id' = 0 -> None
     | Name id' -> Some id'
   in
+  let is_section_variable =
+    let global = Global.env () in
+    fun id ->
+      try ignore (Environ.lookup_named id global);true
+      with Not_found -> false
+  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) *)
@@ -334,18 +340,23 @@ let push_rel_context_to_named_context env typ =
       (fun (na,c,t) (subst, vsubst, avoid, env) ->
 	let id = next_name_away na avoid in
         match extract_if_neq id na with
-        | None ->
-	    let d = (id,Option.map (subst2 subst vsubst) c,subst2 subst vsubst t) in
-	    (mkVar id :: subst, vsubst, id::avoid, push_named d env)
-        | Some 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. *)
+        | 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 = (id0, Option.map (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 = (id,Option.map (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)