ident au lieu de string pour le nom de base de qualid

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

4 files changed, 20 insertions, 16 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 1e33ea049..a915148a3 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -129,7 +129,11 @@ let interp_qualid p =
     | [] -> anomaly "interp_qualid: empty qualified identifier"
     | l -> 
 	let p, r = list_chop (List.length l -1) (List.map outnvar l) in
-	make_qualid p (List.hd r)
+	make_qualid p (id_of_string (List.hd r))
+
+let maybe_variable = function
+  | [Nvar (_,s)] -> Some s
+  | _ -> None
 
 let ids_of_ctxt ctxt =
   Array.to_list
@@ -153,16 +157,16 @@ let maybe_constructor env = function
 	  | IsMutConstruct ((spi,j),cl) -> 
 	      IsConstrPat (loc,((spi,j),ids_of_ctxt cl))
 	  | _ -> 
-	      (match repr_qualid qid with
-		 | [], s -> 
+	      (match maybe_variable l with
+		 | Some s -> 
 		     warning ("Defined reference "^(string_of_qualid qid)
 			      ^" is here considered as a matching variable");
 		     IsVarPat (loc,s)
 		 | _ -> error ("This reference does not denote a constructor: "
 			       ^(string_of_qualid qid)))
       with Not_found -> 
-	match repr_qualid qid with
-	  | [], s -> IsVarPat (loc,s)
+	match maybe_variable l with
+	  | Some s -> IsVarPat (loc,s)
 	  | _ -> error ("Unknown qualified constructor: "
 			^(string_of_qualid qid)))
 
@@ -230,7 +234,7 @@ let ast_to_var (env,impls) (vars1,vars2) loc s =
       let _ = lookup_id id vars2 in
       (* Car Fixpoint met les fns définies tmporairement comme vars de sect *)
       try
-	let ref = Nametab.locate (make_qualid [] s) in
+	let ref = Nametab.locate (make_qualid [] (id_of_string s)) in
 	implicits_of_global ref
       with _ -> []
   in RVar (loc, id), [], imps
@@ -249,7 +253,7 @@ let translate_qualid act qid =
   (* Is it a bound variable? *)
   try
     match repr_qualid qid with
-      | [],s -> act.parse_var s, []
+      | [],s -> act.parse_var (string_of_id s), []
       | _ -> raise Not_found
   with Not_found ->
   (* Is it a global reference? *)
@@ -276,7 +280,7 @@ let rawconstr_of_qualid env vars loc qid =
   (* Is it a bound variable? *)
   try
     match repr_qualid qid with
-      | [],s -> ast_to_var env vars loc s
+      | [],s -> ast_to_var env vars loc (string_of_id s)
       | _ -> raise Not_found
   with Not_found ->
   (* Is it a global reference? *)
@@ -589,7 +593,7 @@ let ast_adjust_consts sigma =
         let id = id_of_string s in
         if isMeta s then ast
         else if Idset.mem id env then ast
-        else adjust_qualid env loc ast (make_qualid [] s)
+        else adjust_qualid env loc ast (make_qualid [] (id_of_string s))
     | Node (loc, "QUALID", p) as ast ->
 	adjust_qualid env loc ast (interp_qualid p)
     | Slam (loc, None, t) -> Slam (loc, None, dbrec env t)
diff --git a/parsing/coqlib.ml b/parsing/coqlib.ml
index 94c23ef19..b0a7f3a8a 100644
--- a/parsing/coqlib.ml
+++ b/parsing/coqlib.ml
@@ -20,10 +20,11 @@ let glob_My_special_variable_nat = ConstRef myvar_path
 
 let reference dir s =
   let dir = "Coq"::"Init"::[dir] in
+  let id = id_of_string s in
   try 
-    Nametab.locate_in_absolute_module dir (id_of_string s)
+    Nametab.locate_in_absolute_module dir id
   with Not_found ->
-    anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir s)))
+    anomaly ("Coqlib: cannot find "^(string_of_qualid (make_qualid dir id)))
 
 let constant dir s =
   Declare.constr_of_reference Evd.empty (Global.env()) (reference dir s)
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index af94577af..34d3d2980 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -416,9 +416,8 @@ let print_name qid =
   try  (* Var locale de but, pas var de section... donc pas d'implicits *)
     let dir,str = repr_qualid qid in 
     if dir <> [] then raise Not_found;
-    let name = id_of_string str in
-    let (c,typ) = Global.lookup_named name in 
-    [< print_named_decl (name,c,typ) >]
+    let (c,typ) = Global.lookup_named str in 
+    [< print_named_decl (str,c,typ) >]
   with Not_found ->
   try
     let sp = Syntax_def.locate_syntactic_definition qid in
diff --git a/parsing/termast.ml b/parsing/termast.ml
index b1a2d18d1..026e79324 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -94,7 +94,7 @@ let ast_of_ref = function
 
 let ast_of_qualid p =
   let dir, s = repr_qualid p in
-  let args = List.map nvar (dir@[s]) in
+  let args = List.map nvar (dir@[string_of_id s]) in
   ope ("QUALID", args)
 
 (**********************************************************************)
@@ -179,7 +179,7 @@ let rec ast_of_raw = function
 	 | RVar (_,id) ->
 	     let imp =
 	       try 
-		 let ref = Nametab.locate (make_qualid [] (string_of_id id)) in
+		 let ref = Nametab.locate (make_qualid [] id) in
 		 implicits_of_global ref
 	       with Not_found -> [] in
 	     ast_of_app imp astf astargs