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

15 files changed, 276 insertions, 242 deletions

diff --git a/.depend b/.depend
index 61f230160b..da97bf9913 100644
--- a/.depend
+++ b/.depend
@@ -411,16 +411,18 @@ parsing/astterm.cmo: parsing/ast.cmi kernel/closure.cmi parsing/coqast.cmi \
     library/declare.cmi kernel/environ.cmi pretyping/evarutil.cmi \
     kernel/evd.cmi kernel/generic.cmi library/global.cmi library/impargs.cmi \
     kernel/names.cmi library/nametab.cmi parsing/pcoq.cmi lib/pp.cmi \
-    pretyping/pretyping.cmi pretyping/rawterm.cmi kernel/reduction.cmi \
-    kernel/sign.cmi pretyping/syntax_def.cmi pretyping/tacred.cmi \
-    kernel/term.cmi pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi 
+    pretyping/pretype_errors.cmi pretyping/pretyping.cmi \
+    pretyping/rawterm.cmi kernel/reduction.cmi kernel/sign.cmi \
+    pretyping/syntax_def.cmi pretyping/tacred.cmi kernel/term.cmi \
+    pretyping/typing.cmi lib/util.cmi parsing/astterm.cmi 
 parsing/astterm.cmx: parsing/ast.cmx kernel/closure.cmx parsing/coqast.cmx \
     library/declare.cmx kernel/environ.cmx pretyping/evarutil.cmx \
     kernel/evd.cmx kernel/generic.cmx library/global.cmx library/impargs.cmx \
     kernel/names.cmx library/nametab.cmx parsing/pcoq.cmx lib/pp.cmx \
-    pretyping/pretyping.cmx pretyping/rawterm.cmi kernel/reduction.cmx \
-    kernel/sign.cmx pretyping/syntax_def.cmx pretyping/tacred.cmx \
-    kernel/term.cmx pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi 
+    pretyping/pretype_errors.cmx pretyping/pretyping.cmx \
+    pretyping/rawterm.cmi kernel/reduction.cmx kernel/sign.cmx \
+    pretyping/syntax_def.cmx pretyping/tacred.cmx kernel/term.cmx \
+    pretyping/typing.cmx lib/util.cmx parsing/astterm.cmi 
 parsing/coqast.cmo: lib/dyn.cmi lib/hashcons.cmi parsing/coqast.cmi 
 parsing/coqast.cmx: lib/dyn.cmx lib/hashcons.cmx parsing/coqast.cmi 
 parsing/egrammar.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/extend.cmi \
@@ -472,15 +474,15 @@ parsing/pretty.cmx: pretyping/classops.cmx kernel/constant.cmx \
     pretyping/syntax_def.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
     parsing/pretty.cmi 
 parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
-    parsing/esyntax.cmi parsing/extend.cmi library/global.cmi \
-    kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \
-    kernel/sign.cmi kernel/term.cmi parsing/termast.cmi lib/util.cmi \
-    parsing/printer.cmi 
+    kernel/environ.cmi parsing/esyntax.cmi parsing/extend.cmi \
+    library/global.cmi kernel/names.cmi library/nametab.cmi lib/options.cmi \
+    lib/pp.cmi kernel/sign.cmi kernel/term.cmi parsing/termast.cmi \
+    lib/util.cmi parsing/printer.cmi 
 parsing/printer.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
-    parsing/esyntax.cmx parsing/extend.cmx library/global.cmx \
-    kernel/names.cmx library/nametab.cmx lib/options.cmx lib/pp.cmx \
-    kernel/sign.cmx kernel/term.cmx parsing/termast.cmx lib/util.cmx \
-    parsing/printer.cmi 
+    kernel/environ.cmx parsing/esyntax.cmx parsing/extend.cmx \
+    library/global.cmx kernel/names.cmx library/nametab.cmx lib/options.cmx \
+    lib/pp.cmx kernel/sign.cmx kernel/term.cmx parsing/termast.cmx \
+    lib/util.cmx parsing/printer.cmi 
 parsing/termast.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \
     kernel/generic.cmi library/global.cmi library/goptions.cmi \
     library/impargs.cmi kernel/inductive.cmi kernel/names.cmi \
@@ -491,6 +493,18 @@ parsing/termast.cmx: parsing/ast.cmx parsing/coqast.cmx library/declare.cmx \
     library/impargs.cmx kernel/inductive.cmx kernel/names.cmx \
     library/nametab.cmx lib/pp.cmx pretyping/rawterm.cmi kernel/sign.cmx \
     kernel/term.cmx kernel/univ.cmx lib/util.cmx parsing/termast.cmi 
+pretyping/cases-provisoire.cmo: parsing/ast.cmi kernel/environ.cmi \
+    pretyping/evarconv.cmi pretyping/evarutil.cmi kernel/evd.cmi \
+    kernel/generic.cmi library/global.cmi library/indrec.cmi \
+    kernel/inductive.cmi kernel/names.cmi pretyping/rawterm.cmi \
+    kernel/reduction.cmi pretyping/retyping.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/typeops.cmi lib/util.cmi 
+pretyping/cases-provisoire.cmx: parsing/ast.cmx kernel/environ.cmx \
+    pretyping/evarconv.cmx pretyping/evarutil.cmx kernel/evd.cmx \
+    kernel/generic.cmx library/global.cmx library/indrec.cmx \
+    kernel/inductive.cmx kernel/names.cmx pretyping/rawterm.cmi \
+    kernel/reduction.cmx pretyping/retyping.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/typeops.cmx lib/util.cmx 
 pretyping/cases.cmo: pretyping/cases.cmi 
 pretyping/cases.cmx: pretyping/cases.cmi 
 pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \
@@ -527,12 +541,12 @@ pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
     library/indrec.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
     pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \
     kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/evarutil.cmi 
-pretyping/pretype_errors.cmo: kernel/environ.cmi kernel/names.cmi \
-    pretyping/rawterm.cmi kernel/sign.cmi kernel/type_errors.cmi \
-    pretyping/pretype_errors.cmi 
-pretyping/pretype_errors.cmx: kernel/environ.cmx kernel/names.cmx \
-    pretyping/rawterm.cmi kernel/sign.cmx kernel/type_errors.cmx \
-    pretyping/pretype_errors.cmi 
+pretyping/pretype_errors.cmo: kernel/environ.cmi library/global.cmi \
+    kernel/names.cmi pretyping/rawterm.cmi kernel/sign.cmi \
+    kernel/type_errors.cmi pretyping/pretype_errors.cmi 
+pretyping/pretype_errors.cmx: kernel/environ.cmx library/global.cmx \
+    kernel/names.cmx pretyping/rawterm.cmi kernel/sign.cmx \
+    kernel/type_errors.cmx pretyping/pretype_errors.cmi 
 pretyping/pretyping.cmo: pretyping/cases.cmi pretyping/classops.cmi \
     pretyping/coercion.cmi kernel/environ.cmi pretyping/evarconv.cmi \
     pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \
@@ -840,17 +854,19 @@ toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
     library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
     toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx 
 toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \
-    kernel/constant.cmi library/declare.cmi kernel/evd.cmi kernel/generic.cmi \
-    library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    library/lib.cmi library/libobject.cmi kernel/names.cmi lib/pp.cmi \
-    pretyping/recordops.cmi kernel/reduction.cmi kernel/term.cmi lib/util.cmi \
-    toplevel/discharge.cmi 
+    kernel/constant.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
+    kernel/generic.cmi library/global.cmi kernel/inductive.cmi \
+    kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \
+    kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/recordops.cmi \
+    kernel/reduction.cmi kernel/sign.cmi library/summary.cmi kernel/term.cmi \
+    kernel/typeops.cmi lib/util.cmi toplevel/discharge.cmi 
 toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \
-    kernel/constant.cmx library/declare.cmx kernel/evd.cmx kernel/generic.cmx \
-    library/global.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    library/lib.cmx library/libobject.cmx kernel/names.cmx lib/pp.cmx \
-    pretyping/recordops.cmx kernel/reduction.cmx kernel/term.cmx lib/util.cmx \
-    toplevel/discharge.cmi 
+    kernel/constant.cmx library/declare.cmx kernel/environ.cmx kernel/evd.cmx \
+    kernel/generic.cmx library/global.cmx kernel/inductive.cmx \
+    kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \
+    kernel/names.cmx lib/options.cmx lib/pp.cmx pretyping/recordops.cmx \
+    kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \
+    kernel/typeops.cmx lib/util.cmx toplevel/discharge.cmi 
 toplevel/errors.cmo: parsing/ast.cmi toplevel/himsg.cmi kernel/inductive.cmi \
     parsing/lexer.cmi lib/options.cmi lib/pp.cmi kernel/type_errors.cmi \
     lib/util.cmi toplevel/errors.cmi 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 89174d1bf6..02db98b986 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -31,6 +31,7 @@ type type_error =
   | CantFindCaseType of constr
   | OccurCheck of int * constr
   | NotClean of int * constr
+  | VarNotFound of identifier
   (* Pattern-matching errors *)
   | BadConstructor of constructor_path * inductive_path
   | WrongNumargConstructor of constructor_path * int
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index aaf278c271..1c0df5a31e 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -33,6 +33,7 @@ type type_error =
   | CantFindCaseType of constr
   | OccurCheck of int * constr
   | NotClean of int * constr
+  | VarNotFound of identifier
   (* Pattern-matching errors *)
   | BadConstructor of constructor_path * inductive_path
   | WrongNumargConstructor of constructor_path * int
diff --git a/parsing/ast.ml b/parsing/ast.ml
index fa0246e327..f0fed61983 100755
--- a/parsing/ast.ml
+++ b/parsing/ast.ml
@@ -315,6 +315,12 @@ let alpha_eq_val = function
       & List.for_all2 (fun x y -> alpha_eq (x,y)) al1 al2
   | _ ->  false
 
+let rec occur_var_ast s = function
+  | Node(loc,op,args) -> List.exists (occur_var_ast s) args
+  | Nvar(_,s2) -> s = s2
+  | Slam(_,sopt,body) -> (Some s <> sopt) & occur_var_ast s body
+  | Id _ | Str _ | Num _ | Path _ -> false
+  | Dynamic _ -> (* Hum... what to do here *) false
 
 exception No_match of string
 
diff --git a/parsing/ast.mli b/parsing/ast.mli
index 7a65850f08..4dacd24536 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -88,6 +88,9 @@ val vall_of_astl : entry_env -> Coqast.t list -> patlist
 
 val alpha_eq : Coqast.t * Coqast.t -> bool
 val alpha_eq_val : v * v -> bool
+
+val occur_var_ast : string -> Coqast.t -> bool
+
 val bind_env : env -> string -> v -> env
 val ast_match : env -> pat -> Coqast.t -> env
 val astl_match : env -> patlist -> Coqast.t list -> env
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3739a43c55..dc64fa98b5 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -17,6 +17,7 @@ open Pretyping
 open Evarutil
 open Ast
 open Coqast
+open Pretype_errors
 
 (* when an head ident is not a constructor in pattern *)
 let mssg_hd_is_not_constructor s =
@@ -127,20 +128,12 @@ let ref_from_constr = function
   | VAR id -> RVar id  (* utilisé dans trad pour coe_value (tmp) *)
   | _ -> anomaly "Not a reference"
 
-let error_var_not_found str loc s = 
-  Util.user_err_loc 
-    (loc,str,
-     [< 'sTR "The variable"; 'sPC; 'sTR s;
-	'sPC ; 'sTR "was not found"; 
-	'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >])
-
 let dbize_ref k sigma env loc s =
   let id = ident_of_nvar loc s in
   try 
     match lookup_id id env with
-      | RELNAME(n,_) -> RRel (loc,n),[]
-      | _ -> 
-	  RRef(loc,RVar id), (try implicits_of_var k id with _ -> [])
+      | RELNAME(n,_) -> RRef (loc,RVar id),[]
+      | _ -> RRef(loc,RVar id), (try implicits_of_var k id with _ -> [])
   with Not_found ->
     try 
       let c,il = match k with
@@ -152,7 +145,7 @@ let dbize_ref k sigma env loc s =
       try 
 	(Syntax_def.search_syntactic_definition id, [])
       with Not_found -> 
-	error_var_not_found "dbize_ref" loc s
+	error_var_not_found_loc loc CCI id
 	  
 let mkLambdaC (x,a,b) = ope("LAMBDA",[a;slam(Some (string_of_id x),b)])
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
@@ -209,9 +202,14 @@ let error_fixname_unbound str is_cofix loc name =
        [< 'sTR "The name"; 'sPC ; 'sTR name ; 
 	  'sPC ; 'sTR "is not bound in the corresponding"; 'sPC ;
 	  'sTR ((if is_cofix then "co" else "")^"fixpoint definition") >])
-
+(*
 let rec collapse_env n env = if n=0 then env else
   add_rel (Anonymous,()) (collapse_env (n-1) (snd (uncons_rel_env env)))
+*)
+
+let check_capture s ty = function
+  | Slam _ when occur_var_ast s ty -> error "Capturing variable"
+  | _ -> ()
 
 let dbize k sigma =
   let rec dbrec env = function
@@ -313,6 +311,7 @@ let dbize k sigma =
     | Node(loc,"EQN",rhs::lhs) ->
 	let (idsl,pl) = List.split (List.map (dbize_pattern env) lhs) in
 	let ids = List.flatten idsl in
+	(* Linearity implies the order in ids is irrelevant *)
 	check_linearity loc ids;
 	check_uppercase loc ids;
 	check_number_of_pattern loc n pl;
@@ -324,11 +323,10 @@ let dbize k sigma =
   and iterated_binder oper n ty env = function
     | Slam(loc,ona,body) ->
 	let na = match ona with 
-	  | Some s -> Name (id_of_string s) 
+	  | Some s -> check_capture s ty body; Name (id_of_string s) 
 	  | _ -> Anonymous
-	in 
-	RBinder(loc, oper, na, 
-		dbrec (collapse_env n env) ty, (* To avoid capture *)
+	in
+	RBinder(loc, oper, na, dbrec env ty,
 		(iterated_binder oper n ty (add_rel (na,()) env) body))
     | body -> dbrec env body
 	  
diff --git a/parsing/printer.ml b/parsing/printer.ml
index dc17ae479d..df0daa1301 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -93,6 +93,13 @@ let rec gencompr k gt =
   in 
   gpr gt
 
+let print_if_exception = function
+    Anomaly (s1,s2) ->
+      warning ("Anomaly ("^s1^")");pP s2;
+      [< 'sTR"<PP error: non-printable term>" >]
+  | Failure _ | UserError _ | Not_found ->
+      [< 'sTR"<PP error: non-printable term>" >]
+  | s -> raise s
 
 (* [at_top] means ids of env must be avoided in bound variables *)
 let gentermpr_core at_top k env t =
@@ -105,8 +112,7 @@ let gentermpr_core at_top k env t =
 	Termast.bdize_no_casts at_top uenv t
     in 
     gencompr k ogt
-  with Failure _ | Anomaly _ | UserError _ | Not_found ->
-    [< 'sTR"<PP error: non-printable term>" >]
+  with s -> print_if_exception s
 
 let term0_at_top a = gentermpr_core true CCI a
 let gentermpr a = gentermpr_core false a
@@ -135,17 +141,14 @@ let fprtype = fprtype_env (gLOB nil_sign)
 let genpatternpr k t =
   try 
     gencompr k (Termast.ast_of_pattern t)
-  with Failure _ | Anomaly _ | UserError _ | Not_found ->
-       [< 'sTR"<PP error: non-printable term>" >];;
+  with s -> print_if_exception s
 
 let prpattern = genpatternpr CCI
 
 let genrawtermpr k env t =
-  let uenv = unitize_env env in
-    try 
-      gencompr k (Termast.ast_of_rawconstr uenv t)
-    with Failure _ | Anomaly _ | UserError _ | Not_found ->
-      [< 'sTR"<PP error: non-printable term>" >];;
+  try 
+    gencompr k (Termast.ast_of_rawconstr t)
+  with s -> print_if_exception s
 
 let prrawterm = genrawtermpr CCI (gLOB nil_sign)
 
diff --git a/parsing/termast.ml b/parsing/termast.ml
index 082098a46f..bbc9e368cc 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -32,6 +32,14 @@ let ids_of_ctxt cl =
 
 let ast_of_ident id = nvar (string_of_id id)
 
+let ast_of_name = function 
+  | Name id -> nvar (string_of_id id)
+  | Anonymous -> nvar "_"
+
+let stringopt_of_name = function 
+  | Name id -> Some (string_of_id id)
+  | Anonymous -> None
+
 let ast_of_constructor (((sp,tyi),n),ids) =
   ope("MUTCONSTRUCT",
       (path_section dummy_loc sp)::(num tyi)::(num n)
@@ -684,119 +692,131 @@ variables of a goal.
 
 exception StillDLAM
 
-let rec detype t = 
+let rec detype avoid env t =
   match collapse_appl t with
     (* Not well-formed constructions *)
     | DLAM _ | DLAMV _ -> raise StillDLAM
     (* Well-formed constructions *)
     | regular_constr -> 
-  	(match kind_of_term regular_constr with
-	   | IsRel n -> RRel (dummy_loc,n)
-	   | IsMeta n -> RRef (dummy_loc,RMeta n)
-	   | IsVar id -> RRef (dummy_loc,RVar id)
-	   | IsXtra s -> anomaly "bdize: Xtra should no longer occur in constr"
-	     (*       ope("XTRA",((str s):: pl@(List.map detype cl)))*)
-	   | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
-	   | IsSort (Type _) -> RSort (dummy_loc,RType)
-	   | IsCast (c1,c2) -> RCast(dummy_loc,detype c1,detype c2)
-	   | IsProd (na,ty,c) -> 
-	       RBinder (dummy_loc,BProd,na,detype ty,detype c)
-	   | IsLambda (na,ty,c) -> 
-	       RBinder (dummy_loc,BLambda,na,detype ty,detype c)
-	   | IsAppL (f,args) -> RApp (dummy_loc,detype f,List.map detype args)
-	   | IsConst (sp,cl) -> RRef (dummy_loc,RConst (sp,ids_of_ctxt cl))
-	   | IsEvar (ev,cl) -> RRef (dummy_loc,REVar (ev,ids_of_ctxt cl))
-	   | IsAbst (sp,cl) -> 
-	       anomaly "bdize: Abst should no longer occur in constr"
-	   | IsMutInd (sp,tyi,cl) ->
-	       RRef (dummy_loc,RInd ((sp,tyi),ids_of_ctxt cl))
-	   | IsMutConstruct (sp,tyi,n,cl) -> 
-	       RRef (dummy_loc,RConstruct (((sp,tyi),n),ids_of_ctxt cl))
-	   | IsMutCase (annot,p,c,bl) ->
-	       let synth_type = synthetize_type () in
-	       let tomatch = detype c in
-	       begin match annot with
-		 | None -> (* Pas d'annotation --> affichage avec vieux Case *)
-		     warning "Printing in old Case syntax";
-		     ROldCase (dummy_loc,false,Some (detype p),
-			       tomatch,Array.map detype bl)
-		 | Some indsp ->
-		     let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
-		     let lc = lc_of_lmis lmis in
-		     let lcparams = Array.map get_params lc in
-		     let k = (nb_prod mip.mind_arity.body) - 
-			     mib.mind_nparams in
-		     let pred = 
-		       if synth_type & computable p k & lcparams <> [||] then
-			 None
-		       else 
-			 Some (detype p) 
-		     in
-		     let constructs = 
-		       Array.init
-			 (Array.length mip.mind_consnames)
-			 (fun i -> ((indsp,i+1),[] (* on triche *))) in
-		     let eqnv = array_map3 bdize_eqn constructs lcparams bl in
-		     let eqnl = Array.to_list eqnv in
-		     let tag =
-		       if PrintingLet.active indsp then 
-			 PrintLet 
-		       else if PrintingIf.active indsp then 
-			 PrintIf 
-		       else 
-			 PrintCases
-		     in 
-		     RCases (dummy_loc,tag,pred,[tomatch],eqnl)
-	       end
-	       
-	   | IsFix (nv,n,cl,lfn,vt) ->
-	       let l = 
-		 Array.of_list 
-		   (List.map
-		      (function Name id -> id | Anonymous -> anomaly"detype")
-		      lfn) 
-	       in
-	       RRec(dummy_loc,RFix (nv,n),l,Array.map detype cl,
-		    Array.map detype vt)
-	   | IsCoFix (n,cl,lfn,vt) ->
-	       let l = 
-		 Array.of_list 
-		   (List.map
-		      (function Name id -> id | Anonymous -> anomaly"detype")
-		      lfn) 
-	       in
-	       RRec(dummy_loc,RCofix n,l,Array.map detype cl,
-		    Array.map detype vt))
+    (match kind_of_term regular_constr with
+    | IsRel n ->
+      (try match fst (lookup_rel n env) with
+	 | Name id   -> RRef (dummy_loc, RVar id)
+	 | Anonymous -> anomaly "detype: index to an anonymous variable"
+       with Not_found ->
+	 let s = "[REL "^(string_of_int (n - List.length (get_rels env)))^"]"
+	 in RRef (dummy_loc, RVar (id_of_string s)))
+    | IsMeta n -> RRef (dummy_loc,RMeta n)
+    | IsVar id -> RRef (dummy_loc,RVar id)
+    | IsXtra s -> anomaly "bdize: Xtra should no longer occur in constr"
+	(*       ope("XTRA",((str s):: pl@(List.map detype cl)))*)
+    | IsSort (Prop c) -> RSort (dummy_loc,RProp c)
+    | IsSort (Type _) -> RSort (dummy_loc,RType)
+    | IsCast (c1,c2) ->
+	RCast(dummy_loc,detype avoid env c1,detype avoid env c2)
+    | IsProd (na,ty,c) -> detype_binder BProd avoid env na ty c
+    | IsLambda (na,ty,c) -> detype_binder BLambda avoid env na ty c
+    | IsAppL (f,args) ->
+	RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args)
+    | IsConst (sp,cl) -> RRef (dummy_loc,RConst (sp,ids_of_ctxt cl))
+    | IsEvar (ev,cl) -> RRef (dummy_loc,REVar (ev,ids_of_ctxt cl))
+    | IsAbst (sp,cl) -> 
+	anomaly "bdize: Abst should no longer occur in constr"
+    | IsMutInd (sp,tyi,cl) ->
+	RRef (dummy_loc,RInd ((sp,tyi),ids_of_ctxt cl))
+    | IsMutConstruct (sp,tyi,n,cl) -> 
+	RRef (dummy_loc,RConstruct (((sp,tyi),n),ids_of_ctxt cl))
+    | IsMutCase (annot,p,c,bl) ->
+	let synth_type = synthetize_type () in
+	let tomatch = detype avoid env c in
+	begin match annot with
+	  | None -> (* Pas d'annotation --> affichage avec vieux Case *)
+	      warning "Printing in old Case syntax";
+	      ROldCase (dummy_loc,false,Some (detype avoid env p),
+			tomatch,Array.map (detype avoid env) bl)
+	  | Some indsp ->
+	      let (mib,mip as lmis) = mind_specif_of_mind_light indsp in
+	      let lc = lc_of_lmis lmis in
+	      let lcparams = Array.map get_params lc in
+	      let k = (nb_prod mip.mind_arity.body) - 
+		      mib.mind_nparams in
+	      let pred = 
+		if synth_type & computable p k & lcparams <> [||] then
+		  None
+		else 
+		  Some (detype avoid env p) 
+	      in
+	      let constructs = 
+		Array.init
+		  (Array.length mip.mind_consnames)
+		  (fun i -> ((indsp,i+1),[] (* on triche *))) in
+	      let eqnv =
+		array_map3 (detype_eqn avoid env) constructs lcparams bl in
+	      let eqnl = Array.to_list eqnv in
+	      let tag =
+		if PrintingLet.active indsp then 
+		  PrintLet 
+		else if PrintingIf.active indsp then 
+		  PrintIf 
+		else 
+		  PrintCases
+	      in 
+	      RCases (dummy_loc,tag,pred,[tomatch],eqnl)
+	end
 	
-and bdize_eqn constr_id construct_params branch =
-  let avoid = global_vars_and_consts branch in
-  let make_pat x avoid b =
+    | IsFix (nv,n,cl,lfn,vt) -> detype_fix (RFix (nv,n)) avoid env cl lfn vt
+    | IsCoFix (n,cl,lfn,vt)  -> detype_fix (RCofix n) avoid env cl lfn vt)
+
+and detype_fix fk avoid env cl lfn vt =
+  let lfi = List.map (fun id -> next_name_away id avoid) lfn in
+  let def_avoid = lfi@avoid in
+  let def_env =
+    List.fold_left (fun env id -> add_rel (Name id,()) env) env lfi in
+  RRec(dummy_loc,fk,Array.of_list lfi,Array.map (detype avoid env) cl,
+       Array.map (detype def_avoid def_env) vt)
+
+
+and detype_eqn avoid env constr_id construct_params branch =
+  let make_pat x avoid env b ids =
     if not (force_wildcard ()) or (dependent (Rel 1) b) then
-      let id = next_name_away x avoid in
-      (PatVar (dummy_loc,Name id)),id::avoid,id
+      let id = next_name_away_with_default "x" x avoid in
+      PatVar (dummy_loc,Name id),id::avoid,(add_rel (Name id,()) env),id::ids
     else 
-      PatVar (dummy_loc,Anonymous),avoid,id_of_string "_" 
+      PatVar (dummy_loc,Anonymous),avoid,(add_rel (Anonymous,()) env),ids
   in
-  let rec buildrec idl patlist avoid = function
+  let rec buildrec ids patlist avoid env = function
     | _::l, DOP2(Lambda,_,DLAM(x,b)) -> 
-	let pat,new_avoid,id = make_pat x avoid b in
-        buildrec (id::idl) (pat::patlist) new_avoid (l,b)
-	  
+	let pat,new_avoid,new_env,new_ids = make_pat x avoid env b ids in
+        buildrec new_ids (pat::patlist) new_avoid new_env (l,b)
+
     | l   , DOP2(Cast,b,_) ->    (* Oui, il y a parfois des cast *)
-	buildrec idl patlist avoid (l,b)
+	buildrec ids patlist avoid env (l,b)
 	  
     | x::l, b -> (* eta-expansion : n'arrivera plus lorsque tous les
                    termes seront construits à partir de la syntaxe Cases *)
 	(* nommage de la nouvelle variable *)
 	let new_b = DOPN(AppL,[|lift 1 b; Rel 1|]) in
-        let pat,new_avoid,id = make_pat x avoid new_b in
-	buildrec (id::idl) (pat::patlist) new_avoid (l,new_b)
+        let pat,new_avoid,new_env,new_ids = make_pat x avoid env new_b ids in
+	buildrec new_ids (pat::patlist) new_avoid new_env (l,new_b)
 	  
     | []  , rhs	-> 
-	(idl, [PatCstr(dummy_loc, constr_id, List.rev patlist)], detype rhs)
+	(ids, [PatCstr(dummy_loc, constr_id, List.rev patlist)],
+	 detype avoid env rhs)
   in 
-  buildrec [] [] avoid (construct_params,branch)
+  buildrec [] [] avoid env (construct_params,branch)
+
+and detype_binder bk avoid env na ty c =
+  let na',avoid' = match concrete_name avoid env na c with
+    | (Some id,l') -> (Name id), l'
+    | (None,l')    -> Anonymous, l' in
+  RBinder (dummy_loc,bk,
+	   na',detype [] env ty,
+	   detype avoid' (add_rel (na',()) env) c)
 
+let ast_dependent na aty =
+  match na with
+    | Name id -> occur_var_ast (string_of_id id) aty
+    | Anonymous -> false
 
 let implicit_of_ref = function
   | RConstruct (cstrid,_) -> constructor_implicits_list cstrid
@@ -826,27 +846,19 @@ let ast_of_app impl f args =
     (* On laisse les implicites, à charge du PP de ne pas les imprimer *)
     ope("APPLISTEXPL",f::(Array.to_list al1))
 
-let rec ast_of_raw avoid env = function
+let rec ast_of_raw = function
   | RRef (_,ref) -> ast_of_ref ref
-  | RRel (_,n) ->
-      (try match fst (lookup_rel n env) with
-	 | Name id   -> ast_of_ident id
-	 | Anonymous -> 
-	     anomaly "ast_of_raw: index to an anonymous variable"
-       with Not_found ->
-	 ope("REL",[num (n - List.length (get_rels env))]))
   | RApp (_,f,args) ->
-      let astf = ast_of_raw avoid env  f in
-      let astargs = List.map (ast_of_raw avoid env ) args in
+      let astf = ast_of_raw f in
+      let astargs = List.map ast_of_raw args in
       (match f with 
 	 | RRef (_,ref) -> ast_of_app (implicit_of_ref ref) astf astargs
 	 | _           -> ast_of_app [] astf astargs)
   | RBinder (_,BProd,Anonymous,t,c) ->
       (* Anonymous product are never factorized *)
-      ope("PROD",[ast_of_raw avoid env t;
-		  slam(None,ast_of_raw avoid (add_rel (Anonymous,()) env) c)])
+      ope("PROD",[ast_of_raw t; slam(None,ast_of_raw c)])
   | RBinder (_,bk,na,t,c) ->
-      let (n,a) = factorize_binder 1 avoid env bk na t c in
+      let (n,a) = factorize_binder 1 bk na (ast_of_raw t) c in
       let tag = match bk with
 	  (* LAMBDA et LAMBDALIST se comportent pareil *)
 	| BLambda -> if n=1 then "LAMBDA" else "LAMBDALIST"
@@ -855,56 +867,43 @@ let rec ast_of_raw avoid env = function
 	  (* constructeur ARROW serait-il plus justifié ? *) 
 	| BProd -> if n=1 then "PROD" else "PRODLIST" 
       in
-      ope(tag,[ast_of_raw [] env t;a])
+      ope(tag,[ast_of_raw t;a])
 
   | RCases (_,printinfo,typopt,tml,eqns) ->
-      let pred = ast_of_rawopt avoid env typopt in
+      let pred = ast_of_rawopt typopt in
       let tag = match printinfo with
 	| PrintIf -> "FORCEIF"
 	| PrintLet -> "FORCELET"
 	| PrintCases -> "MULTCASE" 
       in
-      let asttomatch = ope("TOMATCH", List.map (ast_of_raw avoid env) tml) in
-      let asteqns = List.map (ast_of_eqn avoid env) eqns in 
+      let asttomatch = ope("TOMATCH", List.map ast_of_raw tml) in
+      let asteqns = List.map ast_of_eqn eqns in 
       ope(tag,pred::asttomatch::asteqns)
 	
   | ROldCase (_,isrec,typopt,tm,bv) ->
       warning "Old Case syntax";
-      ope("MUTCASE",(ast_of_rawopt avoid env typopt)
-	    ::(ast_of_raw avoid env tm)
-	    ::(Array.to_list (Array.map (ast_of_raw avoid env) bv)))
+      ope("MUTCASE",(ast_of_rawopt typopt)
+	    ::(ast_of_raw tm)
+	    ::(Array.to_list (Array.map ast_of_raw bv)))
   | RRec (_,fk,idv,tyv,bv) ->
-      let lfi = Array.map (fun id -> next_ident_away id avoid) idv in
-      let alfi = Array.map ast_of_ident lfi in
-      let def_avoid = (Array.to_list lfi)@avoid in
-      let def_env =
-	List.fold_left (fun env id -> add_rel (Name id,()) env) env 
-	  (Array.to_list lfi) in
-      (match fk with 
+      let alfi = Array.map ast_of_ident idv in
+      (match fk with
 	 | RFix (nv,n) ->
-             let rec split_lambda binds avoid env = function
-	       | (0, t) -> (binds,ast_of_raw avoid env t)
+             let rec split_lambda binds = function
+	       | (0, t) -> (binds,ast_of_raw t)
 	       | (n, RBinder(_,BLambda,na,t,b)) ->
-		   let ast = ast_of_raw avoid env t in
-		   let id = next_name_away na avoid in
-		   let bind = ope("BINDER",[ast;ast_of_ident id]) in
-		   split_lambda (bind::binds) (id::avoid)
-		     (add_rel (na,()) env) (n-1,b)
-	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" 
-	     in
-	     let rec split_product avoid env = function
-	       | (0, t) -> ast_of_raw avoid env t
-	       | (n, RBinder(_,BProd,na,t,b)) ->
-		   let id = next_name_away na avoid in
-		   split_product (id::avoid) (add_rel (na,()) env) (n-1,b)
-	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" 
-	     in
+		   let bind = ope("BINDER",[ast_of_raw t;ast_of_name na]) in
+		   split_lambda (bind::binds) (n-1,b)
+	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint body" in
+	     let rec split_product = function
+	       | (0, t) -> ast_of_raw t
+	       | (n, RBinder(_,BProd,na,t,b)) -> split_product (n-1,b)
+	       | _ -> anomaly "ast_of_rawconst: ill-formed fixpoint type" in
 	     let listdecl = 
 	       Array.mapi
 		 (fun i fi ->
-		    let (lparams,astdef) =
-		      split_lambda [] avoid def_env (nv.(i)+1,bv.(i)) in
-		    let asttyp = split_product avoid env (nv.(i)+1,tyv.(i)) in
+		    let (lparams,astdef) = split_lambda [] (nv.(i)+1,bv.(i)) in
+		    let asttyp = split_product (nv.(i)+1,tyv.(i)) in
 		    ope("FDECL",
 		       	[fi; ope ("BINDERS",List.rev lparams); 
 			 asttyp; astdef]))
@@ -914,10 +913,8 @@ let rec ast_of_raw avoid env = function
 	 | RCofix n -> 
 	     let listdecl =
                Array.mapi 
-		 (fun i fi -> ope("CFDECL",
-				  [fi;
-				   ast_of_raw avoid env tyv.(i);
-				   ast_of_raw def_avoid def_env bv.(i)]))
+		 (fun i fi ->
+		    ope("CFDECL",[fi; ast_of_raw tyv.(i); ast_of_raw bv.(i)]))
 		 alfi
 	     in 
 	     ope("COFIX", alfi.(n)::(Array.to_list listdecl)))
@@ -928,46 +925,32 @@ let rec ast_of_raw avoid env = function
 	 | RProp Pos -> ope("SET",[])
 	 | RType -> ope("TYPE",[]))
   | RHole _ -> ope("ISEVAR",[])
-  | RCast (_,c,t) ->
-      ope("CAST",[ast_of_raw avoid env c;ast_of_raw avoid env t])
+  | RCast (_,c,t) -> ope("CAST",[ast_of_raw c;ast_of_raw t])
 	
-and ast_of_eqn avoid env (idl,pl,c) =
-  let new_env = 
-    List.fold_left (fun env id -> add_rel (Name id,()) env) env idl in
-  let rhs = ast_of_raw avoid new_env c in
-  ope("EQN", rhs::(List.map ast_of_pattern pl))
+and ast_of_eqn (idl,pl,c) =
+  ope("EQN", (ast_of_raw c)::(List.map ast_of_pattern pl))
 
-and ast_of_rawopt avoid env  = function
+and ast_of_rawopt = function
   | None -> (str "SYNTH")
-  | Some p -> ast_of_raw avoid env  p
-	
-and factorize_binder n avoid env  oper na ty c =
-  let (env2, avoid2,na2) =
-    match weak_concrete_name avoid env na c with
-      | (Some id,l') -> add_rel (Name id,()) env, l', Some (string_of_id id) 
-      | (None,l')    -> add_rel (Anonymous,()) env, l', None
-  in
+  | Some p -> ast_of_raw p
+
+and factorize_binder n oper na aty c =
   let (p,body) = match c with
-      RBinder(_,oper',na',ty',c')
-	when (oper = oper')
-	  & (ast_of_raw avoid env ty) 
-	  = (ast_of_raw avoid (add_rel (na,()) env) ty')
-	    & not (na' = Anonymous & oper = BProd)
-	    -> factorize_binder (n+1) avoid2 env2 oper na' ty' c'
-    | _ -> (n,ast_of_raw avoid2 env2 c)
-  in 
-  (p,slam(na2, body))
-       
-(* A brancher sur le vrai concrete_name *)
-and weak_concrete_name avoid env na c =
-  match na with
-    | Anonymous -> (None,avoid)
-    | Name id -> (Some id,avoid)
+    | RBinder(_,oper',na',ty',c')
+	when (oper = oper') & (aty = ast_of_raw ty')
+	  & not (ast_dependent na aty) (* To avoid na in ty' escapes scope *)
+	  & not (na' = Anonymous & oper = BProd)
+	  -> factorize_binder (n+1) oper na' aty c'
+    | _ -> (n,ast_of_raw c)
+  in
+  (p,slam(stringopt_of_name na, body))
 
+let ast_of_rawconstr = ast_of_raw
+       
 let bdize at_top env t =
   try
     let avoid = if at_top then ids_of_env env else [] in
-    ast_of_raw avoid env (detype t)
+    ast_of_raw (detype avoid env t)
   with StillDLAM -> 
     old_bdize_depcast WithoutCast at_top env t
 
@@ -987,4 +970,4 @@ let rec strong whdfun t =
 
 let bdize_no_casts at_top env t = bdize at_top env (strong strip_outer_cast t) 
 			   
-let ast_of_rawconstr = ast_of_raw []
+
diff --git a/parsing/termast.mli b/parsing/termast.mli
index fd704d48bb..220662ab34 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -13,7 +13,7 @@ val print_implicits : bool ref
 (* Translation of pattern, rawterm and term into syntax trees for printing *)
 
 val ast_of_pattern : pattern -> Coqast.t
-val ast_of_rawconstr : unit assumptions -> rawconstr -> Coqast.t
+val ast_of_rawconstr : rawconstr -> Coqast.t
 val bdize : bool -> unit assumptions -> constr -> Coqast.t
 val bdize_no_casts : bool -> unit assumptions -> constr -> Coqast.t
 
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 * 
diff --git a/syntax/PPCases.v b/syntax/PPCases.v
index 801de0a67d..cbb66e1dc2 100644
--- a/syntax/PPCases.v
+++ b/syntax/PPCases.v
@@ -31,10 +31,8 @@ Syntax constr
       -> [ "| " $eqn ]
 
   | tomatch [(TOMATCH ($LIST $lc))] -> [(NECOMMANDLIST2 ($LIST $lc)):E]
-  ;
+  | pattconstruct [(PATTCONSTRUCT ($LIST $T))] -> [(APPLIST ($LIST $T))]
 
-  level 10:
-    pattconstruct [(PATTCONSTRUCT ($LIST $T))] -> [(APPLIST ($LIST $T))]
   ;
 
   level 8:
@@ -58,7 +56,8 @@ Syntax constr
 
   (* "level" indifférent pour ce qui suit *)
   | let_binder_var [(LETBINDER ($VAR $id))] -> [ $id ]
-  | let_binder_app [(LETBINDER (APPLIST $toforget ($VAR $id) ($LIST $vars)))]
+  | let_binder_app 
+	[(LETBINDER (PATTCONSTRUCT $toforget ($VAR $id) ($LIST $vars)))]
       -> [ "(" $id (LETBINDERTAIL ($LIST $vars)) ")" ]
  
   | let_binder_tail_nil  [(LETBINDERTAIL)] -> [ ]
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a124d1446c..ff96d59a6d 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -201,6 +201,11 @@ let explain_not_clean k ctx ev t =
      'sTR" with a term using variable "; var; 'sPC;
      'sTR"which is not in its scope." >]
 
+let explain_var_not_found k ctx id = 
+  [< 'sTR "The variable"; 'sPC; 'sTR (string_of_id id);
+     'sPC ; 'sTR "was not found"; 
+     'sPC ; 'sTR "in the current"; 'sPC ; 'sTR "environment" >]
+
 (* Pattern-matching errors *)
 let explain_bad_constructor k ctx cstr ind =
   let pi = pr_inductive ind in
@@ -268,6 +273,8 @@ let explain_type_error k ctx = function
       explain_occur_check k ctx n c
   | NotClean (n,c) ->
       explain_not_clean k ctx n c
+  | VarNotFound id ->
+      explain_var_not_found k ctx id
   (* Pattern-matching errors *)
   | BadConstructor (c,ind) ->
       explain_bad_constructor k ctx c ind