Suppression Rel de rawconstr et correction de bugs d'affichage

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

4 files changed, 23 insertions, 6 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 083b94df0e..a88eeb7e27 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -9,6 +9,9 @@ open Rawterm
 
 exception PretypeError of loc * path_kind * context * type_error
 
+let error_var_not_found_loc loc k s =
+  raise (PretypeError (loc,k, Global.context() (*bidon*), VarNotFound s))
+
 let error_cant_find_case_type_loc loc env expr =
   raise (PretypeError (loc,CCI,context env,CantFindCaseType expr))
 
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 6d39fdd31b..4671d097dd 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -15,6 +15,9 @@ open Rawterm
 
 exception PretypeError of loc * path_kind * context * type_error
 
+val error_var_not_found_loc :
+  loc -> path_kind -> identifier -> 'a
+
 val error_cant_find_case_type_loc : 
   loc -> env -> constr -> 'a
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 05d73ffa1b..6b4b3320ec 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -204,6 +204,22 @@ let evar_type_case isevars env ct pt lft p c =
   in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
 *)
 
+let pretype_var loc env id = 
+  try
+    match lookup_id id (context env) with
+      | RELNAME (n,{body=typ;typ=s}) ->
+	  { uj_val  = Rel n;
+	    uj_type = lift n typ;
+	    uj_kind = DOP0 (Sort s) }
+      | GLOBNAME (id,{body=typ;typ=s}) ->
+	  { uj_val  = VAR id;
+	    uj_type = typ;
+	    uj_kind = DOP0 (Sort s) }
+    with Not_found ->
+      error_var_not_found_loc loc CCI id
+
+(*************************************************************************)
+(* Main pretyping function                                               *)
 
 let trad_metamap = ref []
 let trad_nocheck = ref false
@@ -225,9 +241,7 @@ let pretype_ref loc isevars env = function
           uj_kind=failwith "should be casted"})
 	   (* hnf_constr !isevars (exemeta_hack metaty).uj_type}) *)
 
-| RVar id ->
-    let {body=typ;typ=s} = snd(lookup_glob id (context env)) in
-    {uj_val=VAR id; uj_type=typ; uj_kind = DOP0 (Sort s)}
+| RVar id -> pretype_var loc env id
 
 | RConst (sp,ids) ->
     let cstr = mkConst sp (ctxt_of_ids ids) in
@@ -279,8 +293,6 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
 | RRef (loc,ref) -> 
     pretype_ref loc isevars env ref
 
-| RRel (loc,n) -> relative env n
-
 | RHole loc ->
   if !compter then nbimpl:=!nbimpl+1;
   (match vtcon with
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 29fdf560c0..440d9ed442 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -33,7 +33,6 @@ type cases_style = PrintLet | PrintIf | PrintCases
 
 type rawconstr = 
   | RRef of loc * reference
-  | RRel of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RBinder of loc * binder_kind * name * rawconstr * rawconstr
   | RCases of loc * cases_style * rawconstr option * rawconstr list *