From 0c7a77321a043a27645b6ec13b39b45aa7de28e7 Mon Sep 17 00:00:00 2001 From: aspiwack Date: Sat, 2 Nov 2013 15:40:55 +0000 Subject: 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 --- pretyping/evarutil.ml | 25 ++++++++++++++++++------- 1 file 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) -- cgit v1.2.3