Utilisation d'une construction spéciale SECVAR pour gérer la

globalisation des variables de section (en espérant plus de robustesse
vis à vis des bugs récurrents de Infix pour les variables avec
implicites)


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

5 files changed, 34 insertions, 8 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 6d2e0cfd3b..fa44a19ac8 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -237,7 +237,7 @@ let maybe_constructor allow_var env = function
 	| _ ->
             error ("Unknown absolute constructor name: "^(string_of_path sp)))
 
-  | Node(loc,("CONST"|"EVAR"|"MUTIND"|"SYNCONST" as key), l) ->
+  | Node(loc,("CONST"|"SECVAR"|"EVAR"|"MUTIND"|"SYNCONST" as key), l) ->
       user_err_loc (loc,"ast_to_pattern",
    (str "Found a pattern involving global references which are not constructors"
 ))
@@ -250,6 +250,10 @@ let ast_to_global loc c =
 	let ref = ConstRef (ast_to_sp sp) in
 	let imps = implicits_of_global ref in
 	RRef (loc, ref), imps
+    | ("SECVAR", [Nvar (_,s)]) ->
+	let ref = VarRef s in
+	let imps = implicits_of_global ref in
+	RRef (loc, ref), imps
     | ("MUTIND", [sp;Num(_,tyi)]) -> 
 	let ref = IndRef (ast_to_sp sp, tyi) in
 	let imps = implicits_of_global ref in
@@ -469,8 +473,9 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
 	  match f with
 	    | Node(locs,"QUALID",p) ->
 		rawconstr_of_qualid env lvar locs (interp_qualid p)
+            (* For globalized references (e.g. in Infix) *) 
 	    | Node(loc,
-		   ("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),
+		   ("CONST"|"SECVAR"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),
 		   l) ->
 		ast_to_global loc (key,l)
 	    | _ -> (dbrec env f, [])
@@ -504,7 +509,7 @@ let ast_to_rawconstr sigma env allow_soapp lvar =
     | Node(loc,"TYPE", _) -> RSort(loc,RType None)
 	  
     (* This case mainly parses things build in a quotation *)
-    | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
+    | Node(loc,("CONST"|"SECVAR"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
 	fst (ast_to_global loc (key,l))
 
     | Node(loc,"CAST", [c1;c2]) ->	   
diff --git a/parsing/esyntax.ml b/parsing/esyntax.ml
index 2b801d03eb..9d83c78789 100644
--- a/parsing/esyntax.ml
+++ b/parsing/esyntax.ml
@@ -23,9 +23,10 @@ open Extend
  * according to the key of the pattern. *)
 
 type key =
-  | Cst of Names.section_path (* keys for global constants rules *)
-  | Ind of Names.section_path * int 
-  | Cstr of (Names.section_path * int) * int
+  | Cst of Names.constant (* keys for global constants rules *)
+  | SecVar of Names.variable
+  | Ind of Names.inductive
+  | Cstr of Names.constructor
   | Nod of string      (* keys for other constructed asts rules *)
   | Oth                (* key for other syntax rules *)
   | All     (* key for catch-all rules (i.e. with a pattern such as $x .. *)
@@ -35,6 +36,8 @@ let warning_verbose = ref true
 let ast_keys = function
   | Node(_,"APPLIST", Node(_,"CONST", [Path (_,sl)]) ::_) ->
       [Cst sl; Nod "APPLIST"; All]
+  | Node(_,"APPLIST", Node(_,"SECVAR", [Nvar (_,s)]) ::_) ->
+      [SecVar s; Nod "APPLIST"; All]
   | Node(_,"APPLIST", Node(_,"MUTIND", [Path (_,sl); Num (_,tyi)]) ::_) ->
       [Ind (sl,tyi); Nod "APPLIST"; All]
   | Node(_,"APPLIST", Node(_,"MUTCONSTRUCT",
@@ -50,6 +53,10 @@ let spat_key astp =
                         Pcons(Pquote(Path (_,sl)),_)), _))
       -> Cst sl
     | Pnode("APPLIST",
+            Pcons(Pnode("SECVAR",
+                        Pcons(Pquote(Nvar (_,s)),_)), _))
+      -> SecVar s
+    | Pnode("APPLIST",
             Pcons(Pnode("MUTIND",
                         Pcons(Pquote(Path (_,sl)),
 			      Pcons(Pquote(Num (_,tyi)),_))), _))
diff --git a/parsing/printer.ml b/parsing/printer.ml
index af0bcf1b28..dae3423bec 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -34,6 +34,11 @@ let global_const_name sp =
   with Not_found -> (* May happen in debug *)
     (str ("CONST("^(string_of_path sp)^")"))
 
+let global_var_name id =
+  try pr_global (VarRef id)
+  with Not_found -> (* May happen in debug *)
+    (str ("SECVAR("^(string_of_id id)^")"))
+
 let global_ind_name (sp,tyi) =
   try pr_global (IndRef (sp,tyi))
   with Not_found -> (* May happen in debug *)
@@ -50,6 +55,8 @@ let globpr gt = match gt with
   | Node(_,"EVAR", [Num (_,ev)]) -> (str ("?" ^ (string_of_int ev)))
   | Node(_,"CONST",[Path(_,sl)]) ->
       global_const_name (section_path sl)
+  | Node(_,"SECVAR",[Nvar(_,s)]) ->
+      global_var_name s
   | Node(_,"MUTIND",[Path(_,sl); Num(_,tyi)]) ->
       global_ind_name (section_path sl, tyi)
   | Node(_,"MUTCONSTRUCT",[Path(_,sl); Num(_,tyi); Num(_,i)]) ->
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 0ce85209b9..95e4b51634 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -101,6 +101,9 @@ let ast_of_constructor_ref ((sp,tyi),n) =
 let ast_of_inductive_ref (sp,tyi) =
   ope("MUTIND", [path_section dummy_loc sp; num tyi])
 
+let ast_of_section_variable_ref s =
+  ope("SECVAR", [nvar s])
+
 let ast_of_qualid p =
   let dir, s = repr_qualid p in
   let args = List.map nvar ((List.rev(repr_dirpath dir))@[s]) in
@@ -110,7 +113,7 @@ let ast_of_ref = function
   | ConstRef sp -> ast_of_constant_ref sp
   | IndRef sp -> ast_of_inductive_ref sp
   | ConstructRef sp -> ast_of_constructor_ref sp
-  | VarRef id -> nvar id
+  | VarRef id -> ast_of_section_variable_ref id
 
 (**********************************************************************)
 (* conversion of patterns                                             *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 8e5e35930b..5e718289cc 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -201,7 +201,11 @@ let rec detype tenv avoid env t =
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
 	 in RVar (dummy_loc, id_of_string s))
     | Meta n -> RMeta (dummy_loc, n)
-    | Var id -> RVar (dummy_loc, id)
+    | Var id ->
+	(try
+	  let _ = Global.lookup_named id in RRef (dummy_loc, VarRef id)
+	 with _ ->
+	  RVar (dummy_loc, id))
     | Sort (Prop c) -> RSort (dummy_loc,RProp c)
     | Sort (Type u) -> RSort (dummy_loc,RType (Some u))
     | Cast (c1,c2) ->