Réforme de l'interprétation des termes :

- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t"
- "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième
  pretty-printer dans ppconstr.ml est basé sur "constr_expr".
- Nouveau répertoire "interp" qui hérite de la partie interprétation qui
  se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml;
  constrextern.ml est l'équivalent de termast.ml pour le nouveau
  printer; topconstr.ml; contient la définition de "constr_expr";
  modintern.ml remplace astmod.ml)
- Libnames.reference tend à remplacer Libnames.qualid


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

16 files changed, 142 insertions, 193 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 4c6e5bb014..5c129efa90 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -591,10 +591,10 @@ let occur_rawconstr id =
     | RLambda (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RProd (loc,na,ty,c) -> (occur ty) or ((na <> Name id) & (occur c))
     | RLetIn (loc,na,b,c) -> (occur b) or ((na <> Name id) & (occur c))
-    | RCases (loc,prinfo,tyopt,tml,pl) ->
+    | RCases (loc,tyopt,tml,pl) ->
 	(occur_option tyopt) or (List.exists occur tml)
 	or (List.exists occur_pattern pl)
-    | ROldCase (loc,b,tyopt,tm,bv) -> 
+    | ROrderedCase (loc,b,tyopt,tm,bv) -> 
 	(occur_option tyopt) or (occur tm) or (array_exists occur bv)
     | RRec (loc,fk,idl,tyl,bv) ->
 	(array_exists occur tyl) or
@@ -1369,7 +1369,7 @@ and match_current pb ((current,typ as ct),deps) =
 	  let (pred,typ,s) =
 	    find_predicate pb.caseloc pb.env pb.isevars 
 	      pb.pred brtyps cstrs current indt in
-	  let ci = make_case_info pb.env mind None tags in
+	  let ci = make_case_info pb.env mind RegularStyle tags in
 	  let case = mkCase (ci,nf_betaiota pred,current,brvals) in
 	  let inst = List.map mkRel deps in
 	  pattern_status tags,
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 46f9568fa5..238fd470f3 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -204,7 +204,7 @@ let inh_apply_rel_list apploc env isevars argjl (funloc,funj) tycon =
 	      apply_rec (push_rel (na,None,c1) env) (n+1) newresj restjl
           | _ ->
               error_cant_apply_not_functional_loc 
-		(Rawterm.join_loc funloc loc) env sigma resj
+		(join_loc funloc loc) env sigma resj
                 (List.map snd restjl)
   in 
   apply_rec env 1 funj argjl
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 748c72f4cf..53c9453d0b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -19,7 +19,6 @@ open Inductiveops
 open Environ
 open Sign
 open Declare
-open Impargs
 open Rawterm
 open Nameops
 open Termops
@@ -43,23 +42,23 @@ let isomorphic_to_bool lc =
 
 let isomorphic_to_tuple lc = (Array.length lc = 1)
 
-let encode_bool (loc,_ as locqid) =
-  let (_,lc as x) = encode_inductive locqid in
+let encode_bool r =
+  let (_,lc as x) = encode_inductive r in
   if not (isomorphic_to_bool lc) then
-    user_err_loc (loc,"encode_if",
+    user_err_loc (loc_of_reference r,"encode_if",
       str "This type cannot be seen as a boolean type");
   x
 
-let encode_tuple (loc,_ as locqid) =
-  let (_,lc as x) = encode_inductive locqid in
+let encode_tuple r =
+  let (_,lc as x) = encode_inductive r in
   if not (isomorphic_to_tuple lc) then
-    user_err_loc (loc,"encode_tuple",
+    user_err_loc (loc_of_reference r,"encode_tuple",
       str "This type cannot be seen as a tuple type");
   x
 
 module PrintingCasesMake =
   functor (Test : sig 
-     val encode : qualid located -> inductive * int array
+     val encode : reference -> inductive * int array
      val member_message : std_ppcmds -> bool -> std_ppcmds
      val field : string
      val title : string
@@ -249,14 +248,18 @@ let rec detype tenv avoid env t =
 	  array_map3 (detype_eqn tenv avoid env) constructs consnargsl bl in
 	let eqnl = Array.to_list eqnv in
 	let tag =
-	  if PrintingLet.active (indsp,consnargsl) then 
-	    PrintLet 
+	  if PrintingLet.active (indsp,consnargsl) then
+	    LetStyle
 	  else if PrintingIf.active (indsp,consnargsl) then 
-	    PrintIf 
+	    IfStyle
 	  else 
-	    PrintCases
+	    annot.ci_pp_info.style
 	in 
-	RCases (dummy_loc,tag,pred,[tomatch],eqnl)
+	if tag = RegularStyle then
+	  RCases (dummy_loc,pred,[tomatch],eqnl)
+	else
+	  let bl = Array.map (detype tenv avoid env) bl in
+	  ROrderedCase (dummy_loc,LetStyle,pred,tomatch,bl)
 	
     | Fix (nvn,recdef) -> detype_fix tenv avoid env (RFix nvn) recdef
     | CoFix (n,recdef) -> detype_fix tenv avoid env (RCoFix n) recdef
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 772eae76b8..cff9b1acf0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -19,6 +19,7 @@ open Typing
 open Classops
 open Recordops 
 open Evarutil
+open Libnames
 
 type flexible_term = FConst of constant | FRel of int | FVar of identifier 
 type flex_kind_of_term =
@@ -70,8 +71,8 @@ let evar_apprec env isevars stack c =
 
 let check_conv_record (t1,l1) (t2,l2) =
   try
-    let proji = Declare.reference_of_constr t1 in
-    let cstr = Declare.reference_of_constr t2 in
+    let proji = reference_of_constr t1 in
+    let cstr = reference_of_constr t2 in
     let { o_DEF = c; o_TABS = bs; o_TPARAMS = params; o_TCOMPS = us } = 
       objdef_info (proji, cstr) in
     let params1, c1, extra_args1 =
@@ -327,7 +328,7 @@ and conv_record env isevars (c,bs,(params,params1),(us,us2),(ts,ts1),c1) =
   let ks =
     List.fold_left
       (fun ks b ->
-	 let dloc = (Rawterm.dummy_loc,Rawterm.InternalHole) in
+	 let dloc = (dummy_loc,Rawterm.InternalHole) in
 	 (new_isevar isevars env dloc (substl ks b)) :: ks)
       [] bs
   in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6a1fb9edec..9d65430eda 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -220,7 +220,7 @@ let evars_reset_evd evd d = d.evars <- evd
 let add_conv_pb d pb = d.conv_pbs <- pb::d.conv_pbs
 let evar_source ev d =
   try List.assoc ev d.history
-  with Failure _ -> (Rawterm.dummy_loc, Rawterm.InternalHole)
+  with Failure _ -> (dummy_loc, Rawterm.InternalHole)
 
 (* ise_try [f1;...;fn] tries fi() for i=1..n, restoring the evar constraints
  * when fi returns false or an exception. Returns true if one of the fi
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 44398099cc..f508ac886b 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -68,7 +68,7 @@ let mis_make_case_com depopt env sigma (ind,mib,mip) kind =
       let nbprod = k+1 in
       let indf = make_ind_family(ind,extended_rel_list nbprod lnamespar) in
       let lnamesar,_ = get_arity env indf in
-      let ci = make_default_case_info env ind in
+      let ci = make_default_case_info env RegularStyle ind in
       it_mkLambda_or_LetIn_name env'
        	(lambda_create env'
            (build_dependent_inductive env indf,
@@ -288,7 +288,7 @@ let mis_make_indrec env sigma listdepkind (ind,mib,mip) =
 		(lambda_create env
 		   (build_dependent_inductive env
                      (lift_inductive_family nrec indf),
-		    mkCase (make_default_case_info env indi,
+		    mkCase (make_default_case_info env RegularStyle indi,
 			       mkRel (dect+j+1), mkRel 1, branches)))
 		(Termops.lift_rel_context nrec lnames)
 	    in
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index f14f219229..e3a536420b 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -91,9 +91,9 @@ let make_case_info env ind style pats_source =
     ci_npar    = mip.mind_nparams;
     ci_pp_info = print_info }
 
-let make_default_case_info env ind =
+let make_default_case_info env style ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  make_case_info env ind None
+  make_case_info env ind style
     (Array.map (fun _ -> RegularPat) mip.mind_consnames)
 
 (*s Useful functions *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 43adfd889c..4c5c58a9f2 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -82,8 +82,8 @@ val type_case_branches_with_names :
   env -> inductive * constr list -> unsafe_judgment -> constr ->
     types array * types
 val make_case_info :
-  env -> inductive -> case_style option -> pattern_source array -> case_info
-val make_default_case_info : env -> inductive -> case_info
+  env -> inductive -> case_style -> pattern_source array -> case_info
+val make_default_case_info : env -> case_style -> inductive -> case_info
 
 (********************)
 val control_only_guard : env -> types -> unit
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 6d79b9d28d..0afcbdde7e 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -31,7 +31,8 @@ type constr_pattern =
   | PLetIn of name * constr_pattern * constr_pattern
   | PSort of rawsort
   | PMeta of int option
-  | PCase of constr_pattern option * constr_pattern * constr_pattern array
+  | PCase of case_style * constr_pattern option * constr_pattern * 
+      constr_pattern array
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
@@ -41,9 +42,9 @@ let rec occur_meta_pattern = function
   | PLambda (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PProd (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
   | PLetIn (na,t,c)  -> (occur_meta_pattern t) or (occur_meta_pattern c)
-  | PCase(None,c,br)   ->
+  | PCase(_,None,c,br)   ->
       (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
-  | PCase(Some p,c,br) ->
+  | PCase(_,Some p,c,br) ->
       (occur_meta_pattern p) or
       (occur_meta_pattern c) or (array_exists occur_meta_pattern br)
   | PMeta _ | PSoApp _ -> true
@@ -83,12 +84,12 @@ let rec subst_pattern subst pat = match pat with
 	  PLetIn (name,c1',c2')
   | PSort _ 
   | PMeta _ -> pat
-  | PCase (typ, c, branches) -> 
+  | PCase (cs,typ, c, branches) -> 
       let typ' = option_smartmap (subst_pattern subst) typ in 
       let c' = subst_pattern subst c in
       let branches' = array_smartmap (subst_pattern subst) branches in
 	if typ' == typ && c' == c && branches' == branches then pat else
-	  PCase(typ', c', branches') 
+	  PCase(cs,typ', c', branches') 
   | PFix fixpoint ->
       let cstr = mkFix fixpoint in
       let fixpoint' = destFix (subst_mps subst cstr) in
@@ -132,7 +133,7 @@ let rec head_pattern_bound t =
     | PProd (_,_,b)  -> head_pattern_bound b 
     | PLetIn (_,_,b) -> head_pattern_bound b 
     | PApp (c,args)  -> head_pattern_bound c
-    | PCase (p,c,br) -> head_pattern_bound c
+    | PCase (_,p,c,br) -> head_pattern_bound c
     | PRef r         -> label_of_ref r
     | PVar id        -> VarNode id
     | PEvar _ | PRel _ | PMeta _ | PSoApp _  | PSort _ | PFix _
@@ -229,7 +230,7 @@ let matches_core convert pat c =
 
       | PVar v1, Var v2 when v1 = v2 -> sigma
 
-      | PRef ref, _ when Declare.constr_of_reference ref = cT -> sigma
+      | PRef ref, _ when constr_of_reference ref = cT -> sigma
 
       | PRel n1, Rel n2 when n1 = n2 -> sigma
 
@@ -252,11 +253,11 @@ let matches_core convert pat c =
 
       | PRef (ConstRef _ as ref), _ when convert <> None ->
 	  let (env,evars) = out_some convert in
-	  let c = Declare.constr_of_reference ref in
+	  let c = constr_of_reference ref in
 	  if is_conv env evars c cT then sigma
 	  else raise PatternMatchingFailure
 
-      | PCase (_,a1,br1), Case (_,_,a2,br2) ->
+      | PCase (_,_,a1,br1), Case (_,_,a2,br2) ->
 	  (* On ne teste pas le prédicat *)
           if (Array.length br1) = (Array.length br2) then
   	    array_fold_left2 (sorec stk) (sorec stk sigma a1 a2) br1 br2
@@ -386,7 +387,8 @@ let rec pattern_of_constr t =
 	if ctxt = [||] then PEvar n
 	else PApp (PEvar n, Array.map pattern_of_constr ctxt)
     | Case (ci,p,a,br) ->
-	PCase (Some (pattern_of_constr p),pattern_of_constr a,
+	PCase (ci.ci_pp_info.style,
+	       Some (pattern_of_constr p),pattern_of_constr a,
 	       Array.map pattern_of_constr br)
     | Fix f -> PFix f
     | CoFix _ ->
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 943a8d8c3d..4b8c0aa8dd 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -29,7 +29,8 @@ type constr_pattern =
   | PLetIn of name * constr_pattern * constr_pattern
   | PSort of Rawterm.rawsort
   | PMeta of int option
-  | PCase of constr_pattern option * constr_pattern * constr_pattern array
+  | PCase of case_style * constr_pattern option * constr_pattern * 
+      constr_pattern array
   | PFix of fixpoint
   | PCoFix of cofixpoint
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 162e31e731..cb224fac23 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -19,6 +19,7 @@ open Reductionops
 open Environ
 open Type_errors
 open Typeops
+open Libnames
 open Classops
 open List
 open Recordops 
@@ -48,7 +49,7 @@ let transform_rec loc env sigma (pj,c,lf) indt =
   let (mib,mip) = lookup_mind_specif env ind in
   let recargs = mip.mind_recargs in
   let mI = mkInd ind in
-  let ci = make_default_case_info env ind in
+  let ci = make_default_case_info env MatchStyle ind in
   let nconstr = Array.length mip.mind_consnames in
   if Array.length lf <> nconstr then 
     (let cj = {uj_val=c; uj_type=mkAppliedInd indt} in
@@ -185,7 +186,7 @@ let make_dep_of_undep env (IndType (indf,realargs)) pj =
 (* Main pretyping function                                               *)
 
 let pretype_ref isevars env lvar ref = 
-  let c = Declare.constr_of_reference ref in
+  let c = constr_of_reference ref in
   make_judge c (Retyping.get_type_of env Evd.empty c)
 
 let pretype_sort = function
@@ -285,7 +286,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	      | _ ->
 		  let hj = pretype empty_tycon env isevars lvar lmeta c in
 		  error_cant_apply_not_functional_loc 
-		    (Rawterm.join_loc floc argloc) env (evars_of isevars)
+		    (join_loc floc argloc) env (evars_of isevars)
 	      	    resj [hj]
 
       in let resj = apply_rec env 1 fj args in
@@ -331,7 +332,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	uj_type = type_app (subst1 j.uj_val) j'.uj_type }
 
   (* Special Case for let constructions to avoid exponential behavior *)      
-  | ROldCase (loc,false,po,c,[|f|]) ->
+  | ROrderedCase (loc,st,po,c,[|f|]) when st <> MatchStyle ->
       let cj = pretype empty_tycon env isevars lvar lmeta c in
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
@@ -364,7 +365,7 @@ let rec pretype tycon env isevars lvar lmeta = function
 	     check_branches_message loc env isevars cj.uj_val (bty,[|ft|]);
 	     let v =
 	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env mis in
+	       let ci = make_default_case_info env st mis in
 	       mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,[|fv|])
 	     in 
 	     { uj_val = v;  uj_type = rsty }
@@ -422,12 +423,13 @@ let rec pretype tycon env isevars lvar lmeta = function
 	     let ft = fj.uj_type in
 	     let v =
 	       let mis,_ = dest_ind_family indf in
-	       let ci = make_default_case_info env mis in
+	       let ci = make_default_case_info env st mis in
 	       mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,[|fv|] ) 
 	     in
 	     { uj_val = v; uj_type = rsty })
 
-  | ROldCase (loc,isrec,po,c,lf) ->
+  | ROrderedCase (loc,st,po,c,lf) ->
+      let isrec = (st = MatchStyle) in
       let cj = pretype empty_tycon env isevars lvar lmeta c in
       let (IndType (indf,realargs) as indt) = 
 	try find_rectype env (evars_of isevars) cj.uj_type
@@ -498,14 +500,14 @@ let rec pretype tycon env isevars lvar lmeta = function
 	    transform_rec loc env (evars_of isevars)(pj,cj.uj_val,lfv) indt
 	  else
 	    let mis,_ = dest_ind_family indf in
-	    let ci = make_default_case_info env mis in
+	    let ci = make_default_case_info env st mis in
 	    mkCase (ci, (nf_betaiota pj.uj_val), cj.uj_val,
                        Array.map (fun j-> j.uj_val) lfj)
 	in
 	{ uj_val = v;
 	  uj_type = rsty }
 
-  | RCases (loc,prinfo,po,tml,eqns) ->
+  | RCases (loc,po,tml,eqns) ->
       Cases.compile_cases loc
 	((fun vtyc env -> pretype vtyc env isevars lvar lmeta),isevars)
 	tycon env (* loc *) (po,tml,eqns)
@@ -640,3 +642,12 @@ let understand_gen sigma env lvar lmeta ~expected_type:exptyp c =
 let understand_gen_tcc sigma env lvar lmeta exptyp c =
   let metamap, c = ise_infer_gen false sigma env lvar lmeta exptyp c in
   metamap, c.uj_val
+
+let interp_sort = function
+  | RProp c -> Prop c
+  | RType _ -> new_Type_sort ()
+
+let interp_elimination_sort = function
+  | RProp Null -> InProp
+  | RProp Pos  -> InSet
+  | RType _ -> InType
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index e76c6c14fa..dadc8b94c9 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -76,3 +76,7 @@ val pretype_type :
   val_constraint -> env -> evar_defs -> var_map -> meta_map ->
     rawconstr -> unsafe_type_judgment
 (*i*)
+
+val interp_sort : rawsort -> sorts
+
+val interp_elimination_sort : rawsort -> sorts_family
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 43bd6fc5b1..eaba7663a7 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -52,25 +52,18 @@ type hole_kind =
   | InternalHole
   | TomatchTypeParameter of inductive * int
 
-type 'ctxt reference =
-  | RConst of constant * 'ctxt
-  | RInd of inductive * 'ctxt
-  | RConstruct of constructor * 'ctxt
-  | RVar of identifier
-  | REVar of int * 'ctxt
-
 type rawconstr = 
-  | RRef of loc * global_reference
-  | RVar of loc * identifier
+  | RRef of (loc * global_reference)
+  | RVar of (loc * identifier)
   | REvar of loc * existential_key
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
+  | RCases of loc * rawconstr option * rawconstr list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
-  | ROldCase of loc * bool * rawconstr option * rawconstr * 
+  | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
       rawconstr array
   | RRec of loc * fix_kind * identifier array * 
       rawconstr array * rawconstr array
@@ -96,15 +89,55 @@ let map_rawconstr f = function
   | RLambda (loc,na,ty,c) -> RLambda (loc,na,f ty,f c)
   | RProd (loc,na,ty,c) -> RProd (loc,na,f ty,f c)
   | RLetIn (loc,na,b,c) -> RLetIn (loc,na,f b,f c)
-  | RCases (loc,prinfo,tyopt,tml,pl) ->
-      RCases (loc,prinfo,option_app f tyopt,List.map f tml,
+  | RCases (loc,tyopt,tml,pl) ->
+      RCases (loc,option_app f tyopt,List.map f tml,
         List.map (fun (loc,idl,p,c) -> (loc,idl,p,f c)) pl)
-  | ROldCase (loc,b,tyopt,tm,bv) ->
-      ROldCase (loc,b,option_app f tyopt,f tm, Array.map f bv)
+  | ROrderedCase (loc,b,tyopt,tm,bv) ->
+      ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv)
   | RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv)
   | RCast (loc,c,t) -> RCast (loc,f c,f t)
   | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _ | RDynamic _) as x -> x
 
+(*
+let name_app f e = function
+  | Name id -> let (id, e) = f id e in (Name id, e)
+  | Anonymous -> Anonymous, e
+
+let fold_ident g idl e =
+  let (idl,e) =
+    Array.fold_right
+      (fun id (idl,e) -> let id,e = g id e in (id::idl,e)) idl ([],e)
+  in (Array.of_list idl,e)
+
+let map_rawconstr_with_binders_loc loc g f e = function
+  | RVar (_,id) -> RVar (loc,id)
+  | RApp (_,a,args) -> RApp (loc,f e a, List.map (f e) args)
+  | RLambda (_,na,ty,c) ->
+      let na,e = name_app g e na in RLambda (loc,na,f e ty,f e c)
+  | RProd (_,na,ty,c) ->
+      let na,e = name_app g e na in RProd (loc,na,f e ty,f e c)
+  | RLetIn (_,na,b,c) ->
+      let na,e = name_app g e na in RLetIn (loc,na,f e b,f e c)
+  | RCases (_,tyopt,tml,pl) ->
+      (* We don't modify pattern variable since we don't traverse patterns *)
+      let g' id e = snd (g id e) in
+      let h (_,idl,p,c) = (loc,idl,p,f (List.fold_right g' idl e) c) in
+      RCases
+	(loc,option_app (f e) tyopt,List.map (f e) tml, List.map h pl)
+  | ROrderedCase (_,b,tyopt,tm,bv) ->
+      ROrderedCase (loc,b,option_app (f e) tyopt,f e tm,Array.map (f e) bv)
+  | RRec (_,fk,idl,tyl,bv) ->
+      let idl',e' = fold_ident g idl e in
+      RRec (loc,fk,idl',Array.map (f e) tyl,Array.map (f e') bv)
+  | RCast (_,c,t) -> RCast (loc,f e c,f e t)
+  | RSort (_,x) -> RSort (loc,x)
+  | RHole (_,x)  -> RHole (loc,x)
+  | RRef (_,x) -> RRef (loc,x)
+  | REvar (_,x) -> REvar (loc,x)
+  | RMeta (_,x) -> RMeta (loc,x)
+  | RDynamic (_,x) -> RDynamic (loc,x)
+*)
+
 let rec subst_pat subst pat = 
   match pat with
   | PatVar _ -> pat
@@ -114,6 +147,7 @@ let rec subst_pat subst pat =
 	if kn' == kn && cpl' == cpl then pat else
 	  PatCstr (loc,((kn',i),j),cpl',n)
 	
+(*
 let rec subst_raw subst raw = 
   match raw with
   | RRef (loc,ref) -> 
@@ -146,7 +180,7 @@ let rec subst_raw subst raw =
 	if r1' == r1 && r2' == r2 then raw else
 	  RLetIn (loc,n,r1',r2')
 
-  | RCases (loc,cs,ro,rl,branches) -> 
+  | RCases (loc,ro,rl,branches) -> 
       let ro' = option_smartmap (subst_raw subst) ro 
       and rl' = list_smartmap (subst_raw subst) rl
       and branches' = list_smartmap 
@@ -158,14 +192,14 @@ let rec subst_raw subst raw =
 			branches
       in
 	if ro' == ro && rl' == rl && branches' == branches then raw else
-	  RCases (loc,cs,ro',rl',branches')
+	  RCases (loc,ro',rl',branches')
 
-  | ROldCase (loc,b,ro,r,ra) -> 
+  | ROrderedCase (loc,b,ro,r,ra) -> 
       let ro' = option_smartmap (subst_raw subst) ro
       and r' = subst_raw subst r 
       and ra' = array_smartmap (subst_raw subst) ra in
 	if ro' == ro && r' == r && ra' == ra then raw else
-	  ROldCase (loc,b,ro',r',ra')
+	  ROrderedCase (loc,b,ro',r',ra')
 
   | RRec (loc,fix,ida,ra1,ra2) -> 
       let ra1' = array_smartmap (subst_raw subst) ra1
@@ -188,8 +222,7 @@ let rec subst_raw subst raw =
 	  RCast (loc,r1',r2')
 
   | RDynamic _ -> raw
-
-let dummy_loc = (0,0)
+*)
 
 let loc_of_rawconstr = function
   | RRef (loc,_) -> loc
@@ -200,16 +233,14 @@ let loc_of_rawconstr = function
   | RLambda (loc,_,_,_) -> loc
   | RProd (loc,_,_,_) -> loc
   | RLetIn (loc,_,_,_) -> loc
-  | RCases (loc,_,_,_,_) -> loc
-  | ROldCase (loc,_,_,_,_) -> loc
+  | RCases (loc,_,_,_) -> loc
+  | ROrderedCase (loc,_,_,_,_) -> loc
   | RRec (loc,_,_,_,_) -> loc
   | RSort (loc,_) -> loc
   | RHole (loc,_) -> loc
   | RCast (loc,_,_) -> loc
   | RDynamic (loc,_) -> loc
 
-let join_loc (deb1,_) (_,fin2) = (deb1,fin2)
-
 type 'a raw_red_flag = {
   rBeta : bool;
   rIota : bool;
@@ -229,10 +260,10 @@ type ('a,'b) red_expr_gen =
   | Pattern of (int list * 'a) list
   | ExtraRedExpr of string * 'a
 
-type 'a or_metanum = AN of loc * 'a | MetaNum of loc * int
+type 'a or_metanum = AN of 'a | MetaNum of int located
 
 type 'a may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, qualid or_metanum) red_expr_gen * 'a
+  | ConstrEval of ('a, reference or_metanum) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 51ea180286..d1c480ef72 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -9,6 +9,7 @@
 (*i $Id$ i*)
 
 (*i*)
+open Util
 open Names
 open Sign
 open Term
@@ -51,25 +52,18 @@ type hole_kind =
   | InternalHole
   | TomatchTypeParameter of inductive * int
 
-type 'ctxt reference =
-  | RConst of constant * 'ctxt
-  | RInd of inductive * 'ctxt
-  | RConstruct of constructor * 'ctxt
-  | RVar of identifier
-  | REVar of int * 'ctxt
-
 type rawconstr = 
-  | RRef of loc * Libnames.global_reference
-  | RVar of loc * identifier
+  | RRef of (loc * global_reference)
+  | RVar of (loc * identifier)
   | REvar of loc * existential_key
   | RMeta of loc * int
   | RApp of loc * rawconstr * rawconstr list
   | RLambda of loc * name * rawconstr * rawconstr
   | RProd of loc * name * rawconstr * rawconstr
   | RLetIn of loc * name * rawconstr * rawconstr
-  | RCases of loc * Term.case_style * rawconstr option * rawconstr list * 
+  | RCases of loc * rawconstr option * rawconstr list * 
       (loc * identifier list * cases_pattern list * rawconstr) list
-  | ROldCase of loc * bool * rawconstr option * rawconstr * 
+  | ROrderedCase of loc * case_style * rawconstr option * rawconstr * 
       rawconstr array
   | RRec of loc * fix_kind * identifier array * 
       rawconstr array * rawconstr array
@@ -92,11 +86,17 @@ i*)
 
 val map_rawconstr : (rawconstr -> rawconstr) -> rawconstr -> rawconstr
 
-val dummy_loc : loc
+(*
+val map_rawconstr_with_binders_loc : loc -> 
+  (identifier -> 'a -> identifier * 'a) ->
+  ('a -> rawconstr -> rawconstr) -> 'a -> rawconstr -> rawconstr
+*)
+
 val loc_of_rawconstr : rawconstr -> loc
-val join_loc : loc -> loc -> loc
 
+(*
 val subst_raw : Names.substitution -> rawconstr -> rawconstr
+*)
 
 type 'a raw_red_flag = {
   rBeta : bool;
@@ -117,10 +117,10 @@ type ('a,'b) red_expr_gen =
   | Pattern of (int list * 'a) list
   | ExtraRedExpr of string * 'a
 
-type 'a or_metanum = AN of loc * 'a | MetaNum of loc * int
+type 'a or_metanum = AN of 'a | MetaNum of int located
 
 type 'a may_eval =
   | ConstrTerm of 'a
-  | ConstrEval of ('a, qualid or_metanum) red_expr_gen * 'a
+  | ConstrEval of ('a, reference or_metanum) red_expr_gen * 'a
   | ConstrContext of (loc * identifier) * 'a
   | ConstrTypeOf of 'a
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml
deleted file mode 100644
index cb1be3ebb8..0000000000
--- a/pretyping/syntax_def.ml
+++ /dev/null
@@ -1,81 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(* $Id$ *)
-
-open Util
-open Pp
-open Names
-open Libnames
-open Rawterm
-open Libobject
-open Lib
-open Nameops
-
-(* Syntactic definitions. *)
-
-let syntax_table = ref (KNmap.empty : rawconstr KNmap.t)
-
-let _ = Summary.declare_summary
-	  "SYNTAXCONSTANT"
-	  { Summary.freeze_function = (fun () -> !syntax_table);
-	    Summary.unfreeze_function = (fun ft -> syntax_table := ft);
-	    Summary.init_function = (fun () -> syntax_table := KNmap.empty);
-	    Summary.survive_section = false }
-
-let add_syntax_constant kn c =
-  syntax_table := KNmap.add kn c !syntax_table
-
-let cache_syntax_constant ((sp,kn),c) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_syntax_constant"
-      (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant kn c;
-  Nametab.push_syntactic_definition (Nametab.Until 1) sp kn
-
-let load_syntax_constant i ((sp,kn),c) =
-  if Nametab.exists_cci sp then
-    errorlabstrm "cache_syntax_constant"
-      (pr_id (basename sp) ++ str " already exists");
-  add_syntax_constant kn c;
-  Nametab.push_syntactic_definition (Nametab.Until i) sp kn
-
-let open_syntax_constant i ((sp,kn),c) =
-  Nametab.push_syntactic_definition (Nametab.Exactly i) sp kn
-
-let subst_syntax_constant ((sp,kn),subst,c) =
-  subst_raw subst c
-
-let classify_syntax_constant (_,c) = Substitute c
-
-let (in_syntax_constant, out_syntax_constant) =
-  declare_object {(default_object "SYNTAXCONSTANT") with
-    cache_function = cache_syntax_constant;
-    load_function = load_syntax_constant;
-    open_function = open_syntax_constant;
-    subst_function = subst_syntax_constant;
-    classify_function = classify_syntax_constant;
-    export_function = (fun x -> Some x) } 
-
-let declare_syntactic_definition id c =
-  let _ = add_leaf id (in_syntax_constant c) in ()
-
-let rec set_loc loc = function
-  | RRef (_,a)      -> RRef (loc,a)
-  | RVar (_,a)      -> RVar (loc,a)
-  | RApp (_,a,b)    -> RApp (loc,set_loc loc a,List.map (set_loc loc) b)
-  | RSort (_,a)      -> RSort (loc,a) 
-  | RHole (_,a)      -> RHole (loc,a)
-  | RLambda (_,na,ty,c) -> RLambda (loc,na,set_loc loc ty,set_loc loc c)
-  | RProd (_,na,ty,c) -> RProd (loc,na,set_loc loc ty,set_loc loc c)
-  | RLetIn (_,na,b,c) -> RLetIn (loc,na,set_loc loc b,set_loc loc c)
-  | RCast (_,a,b) -> RCast (loc,set_loc loc a,set_loc loc b)
-  | a -> warning "Unrelocatated syntactic definition"; a
-
-let search_syntactic_definition loc kn =
-  set_loc loc (KNmap.find kn !syntax_table)
diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli
deleted file mode 100644
index d9537cd203..0000000000
--- a/pretyping/syntax_def.mli
+++ /dev/null
@@ -1,23 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(*i $Id$ i*)
-
-(*i*)
-open Names
-open Libnames
-open Rawterm
-(*i*)
-
-(* Syntactic definitions. *)
-
-val declare_syntactic_definition : identifier -> rawconstr -> unit
-
-val search_syntactic_definition : loc -> kernel_name -> rawconstr
-
-