Deplace dans parsing

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

2 files changed, 0 insertions, 648 deletions

diff --git a/pretyping/astterm.ml b/pretyping/astterm.ml
deleted file mode 100644
index 699a77c497..0000000000
--- a/pretyping/astterm.ml
+++ /dev/null
@@ -1,622 +0,0 @@
-
-(* $Id$ *)
-
-open Std
-open Pp
-open Names
-open CoqAst
-open Ast
-open Vectops
-open Generic
-open Term
-open Environ
-open Termenv
-open Impuniv
-open Himsg
-open Multcase_astterm 
-open Evd
-open More_util
-open Rawterm
-
-(**  Multcases ... **)
-
-let prpattern k p = Printer.gencompr CCI (Termast.ast_of_pat p)
-
-(* when an head ident is not a constructor in pattern *)
-let mssg_hd_is_not_constructor s =
-  [< 'sTR ("The symbol "^s^" should be a constructor") >]
-
-
-(* checking linearity of a list of ids in patterns *)
-let non_linearl_mssg id =
-  [<'sTR "The variable " ; 'sTR(string_of_id id);
-    'sTR " is bound several times in pattern" >] 
-
-let rec has_duplicate = function 
-  | [] -> None
-  | x::l -> if List.mem x l then (Some x) else has_duplicate l
-
-let check_linearity loc ids =
-  match has_duplicate ids with
-    | Some id -> user_err_loc (loc,"dbize_eqn",non_linearl_mssg id)
-    | None -> ()
-
-let mal_formed_mssg () =
-  [<'sTR "malformed macro of multiple case" >]
-
-(* determines if some pattern variable starts with uppercase *)
-let warning_uppercase loc uplid = (* Comment afficher loc ?? *)
-  let vars =
-    prlist_with_sep pr_spc (fun v -> [< 'sTR (string_of_id v) >]) uplid in
-  let (s1,s2) = if List.length uplid = 1 then (" ","s ") else ("s "," ") in
-  wARN [<'sTR ("Warning: the variable"^s1); vars;
-	 'sTR (" start"^s2^" with upper case in pattern"); 'cUT >]
-
-let is_uppercase_var v =
-  match (string_of_id v).[0] with
-    | 'A'..'Z' -> true
-    | _  -> false
-
-let check_uppercase loc ids =
-  let uplid = filter is_uppercase_var ids in
-  if uplid <> [] then warning_uppercase loc uplid
-
-(* check that the number of pattern matches the number of matched args *)
-let mssg_number_of_patterns n pl =
-  [< 'sTR"Expecting ";'iNT n ; 'sTR" pattern(s) but found ";
-    'iNT (List.length pl); 'sTR" in " >]
-
-let check_number_of_pattern loc n l =
-  if n<>(List.length l) then
-    user_err_loc (loc,"check_number_of_pattern",mssg_number_of_patterns n l)
-
-(* absolutize_eqn replaces pattern variables that are global. This
- * means that we are going to remove the pattern abstractions that
- * correspond to constructors.
- * Warning: Names that are global but do not correspond to
- * constructors are considered non-known_global. E.g. if nat appears
- * in a pattern is considered as a variable name.  known_global should
- * be refined in order to consider known_global names only those that
- * correspond to constructors of inductive types.
- *)
-(*
-let is_constructor =  function
-    DOPN(MutConstruct((sp,tyi),i),cl)-> true | _ ->false
-
-let is_known_constructor k env id =
-  let srch =
-    match k with
-	CCI -> Machops.search_reference
-      | FW -> Machops.search_freference
-      | _ -> anomaly "known_global" in
-    try is_constructor (srch env id) 
-    with (Not_found | UserError _) -> 
-      (try  is_constructor (Environ.search_synconst k id) 
-       with Not_found -> false)
-
-
-let rec abs_eqn k env avoid = function
-    (v::ids, Slam(_,ona,t)) ->
-      let id = id_of_string (Ast.id_of_ast v) in
-      if is_known_constructor k env id
-      then abs_eqn k env avoid (ids, subst1 (VAR id) t)
-      else
-	let id' = if is_underscore id then id else next_ident_away id avoid in
-	let (nids,nt) = abs_eqn k env (id'::avoid) (ids,t) in
-	(id'::nids, DLAM(na,nt))
-  | ([],t) -> ([],t)
-  | _ -> assert false
-
-
-let rec absolutize_eqn absrec k env = function
-    DOP1(XTRA("LAMEQN",ids),lam_eqn) ->
-      let gids = ids_of_sign (get_globals env) in
-      let (nids,neqn) =	abs_eqn k env gids (ids, lam_eqn) in
-      let uplid = filter is_uppercase_var nids in
-      let _ = if uplid <> [] then warning_uppercase uplid in
-      DOP1(XTRA("LAMEQN",nids), absrec neqn)
-  | _ -> anomalylabstrm "absolutize_eqn" (mal_formed_mssg())
-
-*)
-(****************************************************************)
-(* Arguments normally implicit in the "Implicit Arguments mode" *)
-(* but explicitely given                                        *)
-(*
-let dest_explicit_arg = function
-    (DOP1(XTRA ("!", [Num(_,j)]), t)) -> (j,t)
-  | _ -> raise Not_found
-
-let is_explicit_arg = function
-    (DOP1(XTRA ("!", [Num(_,j)]), t)) -> true
-  | _ -> false
-
-let explicitize_appl l args = 
- let rec aux n l args acc =
- match (l,args) with 
-  (i::l',a::args') -> 
-   if i=n 
-   then try let j,a' = dest_explicit_arg a in
-            if j > i
-            then aux (n+1) l' args (mkExistential::acc)
-            else if j = i
-                 then aux (n+1) l' args' (a'::acc)
-                 else error "Bad explicitation number"
-        with Not_found -> aux (n+1) l' args (mkExistential::acc)
-   else if is_explicit_arg a then error "Bad explicitation number"
-   else aux (n+1) l args' (a::acc)
- | ([],_) -> (List.rev acc)@args
- | (_,[]) -> (List.rev acc)
-in aux 1 l args []
-
-
-let absolutize k sigma env constr = 
- let rec absrec env constr = match constr with
-    VAR id -> fst (absolutize_var_with_impl k sigma env id)
-  | Rel _ as t -> t
-  | DOP1(XTRA ("!", [Num _]), _) -> error "Bad explicitation number"
-  | DOPN(AppL,cl) -> (* Detect implicit args occurrences *)
-     let cl1 = Array.to_list cl in
-     let f = List.hd cl1 in
-     let args = List.tl cl1 in
-       begin match f with 
-           VAR id ->
-             let (c, impargs) = absolutize_var_with_impl k sigma env id in
-             let newargs = explicitize_appl impargs args in
-               mkAppList c (List.map (absrec env) newargs)
-         | DOPN((Const _ | MutInd _ | MutConstruct _) as op, _) ->
-	     let id = id_of_global op in
-             let (c, impargs) = search_ref_with_impl k env id in
-             let newargs = explicitize_appl impargs args in
-               mkAppList c (List.map (absrec env) newargs)
-         | (DOP1(XTRA ("!",[]), t)) ->
-             mkAppList (absrec env t) (List.map (absrec env) args)
-         | _ -> mkAppL (Array.map (absrec env) cl)
-       end
-
-  (* Pattern branches have a special absolutization *)
-  | DOP1(XTRA("LAMEQN",_),_) as eqn  -> absolutize_eqn (absrec env) k env eqn
-
-  | DOP0 _ as t -> t
-  | DOP1(oper,c) -> DOP1(oper,absrec env c)
-  | DOP2(oper,c1,c2) -> DOP2(oper,absrec env c1,absrec env c2)
-  | DOPN(oper,cl) -> DOPN(oper,Array.map (absrec env) cl)
-  | DOPL(oper,cl) -> DOPL(oper,List.map (absrec env) cl)
-  | DLAM(na,c)    -> DLAM(na,absrec (add_rel (na,()) env) c)
-  | DLAMV(na,cl)  -> DLAMV(na,Array.map (absrec (add_rel (na,()) env)) cl)
-
- in absrec env constr
-
-
-(* Fonctions exportées *)
-let absolutize_cci sigma env constr = absolutize CCI sigma env constr
-let absolutize_fw  sigma env constr = absolutize FW  sigma env constr
-*)
-
-let dbize_sp = function
-    Path(loc,sl,s) ->
-      (try section_path sl s
-       with Invalid_argument _ | Failure _ ->
-         anomaly_loc(loc,"Astterm.dbize_sp",
-                     [< 'sTR"malformed section-path" >]))
-  | ast -> anomaly_loc(Ast.loc ast,"Astterm.dbize_sp",
-                     [< 'sTR"not a section-path" >])
-(*
-let dbize_op loc opn pl cl =
-    match (opn,pl,cl) with
-        ("META",[Num(_,n)], []) -> DOP0(Meta n)
-      | ("XTRA",(Str(_,s))::tlpl,_) when (multcase_kw s) ->
-          DOPN(XTRA(s,tlpl),Array.of_list cl)
-      | ("XTRA",(Str(_,s))::tlpl,[]) -> DOP0(XTRA(s,tlpl))
-      | ("XTRA",(Str(_,s))::tlpl,[c]) -> DOP1(XTRA(s,tlpl),c)
-      | ("XTRA",(Str(_,s))::tlpl,[c1;c2]) -> DOP2(XTRA(s,tlpl),c1,c2)
-      | ("XTRA",(Str(_,s))::tlpl,_) -> DOPN(XTRA(s,tlpl), Array.of_list cl)
-
-      | ("PROP", [Id(_,s)], []) ->
-          (try RSort(Prop (contents_of_str s))
-           with Invalid_argument s -> anomaly_loc (loc,"Astterm.dbize_op",
-                                                   [< 'sTR s >]))
-      | ("TYPE", [], []) -> RSort(Type(dummy_univ))
-
-      | ("IMPLICIT", [], []) -> DOP0(Implicit)
-      | ("CAST", [], [c1;c2]) -> DOP2(Cast,c1,c2)
-
-      | ("CONST", [sp], _) -> DOPN(Const (dbize_sp sp),Array.of_list cl)
-      | ("ABST", [sp], _) ->
-          (try global_abst (dbize_sp sp) (Array.of_list cl)
-           with
-               Failure _ | Invalid_argument _ ->
-                 anomaly_loc(loc,"Astterm.dbize_op",
-                             [< 'sTR"malformed abstraction" >])
-             | Not_found -> user_err_loc(loc,"Astterm.dbize_op",
-                                         [< 'sTR"Unbound abstraction" >]))
-      | ("MUTIND", [sp;Num(_,tyi)], _) ->
-          DOPN(MutInd (dbize_sp sp, tyi),Array.of_list cl)
-            
-      | ("MUTCASE", [], p::c::l) -> mkMutCase None p c l
-
-      | ("MUTCONSTRUCT", [sp;Num(_,tyi);Num(_,n)], _) ->
-          DOPN(MutConstruct ((dbize_sp sp, tyi),n),Array.of_list cl)
-
-      | ("SQUASH",[],[_]) -> user_err_loc
-            (loc,"Astterm.dbize_op",
-             [< 'sTR "Unrecognizable braces expression." >])
-
-      | (op,_,_) -> anomaly_loc
-            (loc,"Astterm.dbize_op",
-             [< 'sTR "Unrecognizable constr operator: "; 'sTR op >])
-
-
-let split_params =
- let rec sprec acc = function
-     (Id _ as p)::l -> sprec (p::acc) l
-   | (Str _ as p)::l -> sprec (p::acc) l
-   | (Num _ as p)::l -> sprec (p::acc) l
-   | (Path _ as p)::l -> sprec (p::acc) l
-   | l -> (List.rev acc,l)
- in sprec []
-
-*)
-
-let is_underscore id = (id = "_")
-
-let name_of_nvar s =
-  if is_underscore s then Anonymous else Name (id_of_string s)
-
-let ident_of_nvar loc s =
-  if is_underscore s then
-    user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >])
-  else (id_of_string s)
-
-let ids_of_ctxt cl =
-  List.map(function (VAR id) -> id |_->anomaly"ids_of_ctxt") (Array.to_list cl)
-
-let maybe_constructor env s =
-  try match Machops.search_reference env (id_of_string s) with 
-      DOPN(MutConstruct (spi,j),cl) -> Some ((spi,j),ids_of_ctxt cl)
-    | _ -> None
-  with Not_found -> None
-
-let dbize_ctxt = 
-  List.map 
-    (function
-       | Nvar (loc,s) -> ident_of_nvar loc s
-       | _ -> anomaly "Bad ast for local ctxt of a global reference")
-
-let dbize_global loc = function
-  | ("CONST", sp::ctxt)  -> RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt))
-  | ("EVAR", sp::ctxt)   -> RRef (loc,EVar (dbize_sp sp,dbize_ctxt ctxt))
-  | ("MUTIND", sp::Num(_,tyi)::ctxt) -> RRef (loc,Ind (dbize_sp sp, tyi,dbize_ctxt ctxt))
-  | ("MUTCONSTRUCT", sp::Num(_,ti)::Num(_,n)::ctxt) ->
-      RRef (loc,Construct (((dbize_sp sp,ti),n),dbize_ctxt ctxt))
-  | ("SYNCONST", [sp]) -> search_synconst_path CCI (dbize_sp sp)
-(* | ("ABST", [sp]) -> RRef (loc,Abst (dbize_sp sp)) *)
-  | _ -> anomaly_loc (loc,"dbize_global",
-		      [< 'sTR "Bad ast for this global a reference">])
-
-let ref_from_constr = function
-  | DOPN (Const sp,ctxt) -> 
-   if is_existential_id (basename sp) 
-   then EVar (sp,ids_of_ctxt ctxt) 
-   else RConst (sp,ids_of_ctxt ctxt)
-  | DOPN (MutConstruct (spi,j),ctxt) -> Construct ((spi,j),ids_of_ctxt ctxt)
-  | DOPN (MutInd (sp,i),ctxt) -> Ind (sp,i,ids_of_ctxt ctxt)
-  | VAR id -> Var id  (* utilisé dans trad pour coe_value (tmp) *)
-  | _ -> anomaly "Not a reference"
-
-let dbize_ref k sigma env loc s =
-  let id = ident_of_nvar loc s in
-  if (is_existential_id id) then
-    match k with
- 	CCI -> 
-	  RRef (loc,ref_from_constr (
-		  Machops.lookup_exist sigma env (evar_of_id k id))),[]
-      | FW  -> error "existentials in fterms not implemented"
-      | OBJ -> anomaly "absolutize_var"
-  else
-  try match lookup_id id env with
-      RELNAME(n,_) -> RRef (loc,RRel n),[]
-    | _ -> RRef(loc,Var id), (try Vartab.implicits_of_var k id with _ -> [])
-  with Not_found ->
-  try let c,il = match k with
-      CCI -> Machops.search_reference1 env id
-    | FW  -> Machops.search_freference1 env id
-    | OBJ -> anomaly "search_ref_cci_fw" in
-    RRef (loc,ref_from_constr c), il
-  with UserError _ ->
-  try (search_synconst k id,[])
-  with Not_found -> error_var_not_found "dbize_ref" loc s
-
-
-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))
-let mkProdC (x,a,b) = ope("PROD",[a;slam(Some (string_of_id x),b)])
-let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
-let destruct_binder = function
-    Node(_,"BINDER",c::idl) ->
-      List.map (fun id -> (id_of_string (nvar_of_ast id),c)) idl
-  | _ -> anomaly "BINDER is expected"
-
-let rec dbize_pattern env = function
-  | Node(_,"AS",[Nvar (loc,s); p]) ->
-      (match name_of_nvar s with
-	  Anonymous -> dbize_pattern env p
-	| Name id   -> 
-	    let (ids,p') = dbize_pattern env p in (id::ids,PatAs (loc,id,p')))
-  | Node(_,"APPLIST", Nvar(loc,s)::pl) ->
-      (match (maybe_constructor env s, pl) with
-	 | Some c, _ ->
-	     let (idsl,pl') = List.split (List.map (dbize_pattern env) pl) in
-	     (List.flatten idsl,PatCstr (loc,c,pl'))
-	 | None, [] ->
-	     (match name_of_nvar s with
-		 Anonymous -> ([], PatVar (loc,Anonymous))
-	       | Name id as name -> ([id], PatVar (loc,name)))
-	 | None, _ ->
-	     user_err_loc (loc,"dbize_pattern",mssg_hd_is_not_constructor s))
-  | _ -> anomaly "dbize: badly-formed ast for Cases pattern"
-
-let rec dbize_fix = function
-  | [] -> ([],[],[],[])
-  | Node(_,"NUMFDECL", [Nvar(_,fi); Num(_,ni); astA; astT])::rest ->
-      let (lf,ln,lA,lt) = dbize_fix rest in
-	((id_of_string fi)::lf, (ni-1)::ln, astA::lA, astT::lt)
-  | Node(_,"FDECL", [Nvar(_,fi); Node(_,"BINDERS",bl); astA; astT])::rest ->
-      let binders = List.flatten (List.map destruct_binder bl) in
-      let ni = List.length binders - 1 in
-      let (lf,ln,lA,lt) = dbize_fix rest in
-        ((id_of_string fi)::lf, ni::ln, (mkProdCit binders astA)::lA,
-	 (mkLambdaCit binders astT)::lt)
-  | _ -> anomaly "FDECL or NUMFDECL is expected"
-
-let rec dbize_cofix = function
-  | [] -> ([],[],[])
-  | Node(_,"CFDECL", [Nvar(_,fi); astA; astT])::rest -> 
-      let (lf,lA,lt) = dbize_cofix rest in
-	((id_of_string fi)::lf, astA::lA, astT::lt)
-  | _ -> anomaly "CFDECL is expected"
-
-let dbize k sigma =
-  let rec dbrec env = function
-    Nvar(loc,s) -> fst (dbize_ref k sigma env loc s)
-
-(*
-   | Slam(_,ona,Node(_,"V$",l)) ->
-       let na =
-         (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
-       in DLAMV(na,Array.of_list (List.map (dbrec (add_rel (na,()) env)) l))
-
-   | Slam(_,ona,t) ->
-       let na =
-         (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
-       in DLAM(na, dbrec (add_rel (na,()) env) t)
-*)
-   | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
-       let (lf,ln,lA,lt) = dbize_fix ldecl in
-       let n =
-	 try (index (ident_of_nvar locid iddef) lf) -1
-         with Failure _ ->
-	   error_fixname_unbound "dbize (FIX)" false locid iddef in
-       let ext_env =
-	 List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in
-       let defl = Array.of_list (List.map (dbrec ext_env) lt) in
-       let arityl = Array.of_list (List.map (dbrec env) lA) in
-	 RRec (loc,RFix (Array.of_list ln,n), Array.of_list lf, arityl, defl)
-
-   | Node(loc,"COFIX", (Nvar(locid,iddef))::ldecl) ->
-       let (lf,lA,lt) = dbize_cofix ldecl in
-       let n =
-         try (index (ident_of_nvar locid iddef) lf) -1
-         with Failure _ ->
-	   error_fixname_unbound "dbize (COFIX)" true locid iddef in
-       let ext_env =
-	 List.fold_left (fun env fid -> add_rel (Name fid,()) env) env lf in
-       let defl = Array.of_list (List.map (dbrec ext_env) lt) in
-       let arityl = Array.of_list (List.map (dbrec env) lA) in
-	 RRec (loc,RCofix n, Array.of_list lf, arityl, defl)
-
-   | Node(loc,("PROD"|"LAMBDA" as k), [c1;Slam(_,ona,c2)]) ->
-       let na = match ona with
-	   Some s -> Name (id_of_string s)
-	 | _ -> Anonymous in
-       let kind = if k="PROD" then BProd else BLambda in
-       RBinder(loc, kind, na, dbrec env c1, dbrec (add_rel (na,()) env) c2)
-   | Node(_,"PRODLIST", [c1;(Slam _ as c2)]) -> iterated_binder BProd c1 env c2
-   | Node(_,"LAMBDALIST", [c1;(Slam _ as c2)]) -> iterated_binder BLambda c1 env c2
-
-   | Node(loc,"APPLISTEXPL", f::args) ->
-       RApp (loc,dbrec env f,List.map (dbrec env) args)
-   | Node(loc,"APPLIST", Nvar(locs,s)::args) ->
-       let (c, impargs) = dbize_ref k sigma env locs s in
-       RApp (loc, c, dbize_args env impargs args)
-   | Node(loc,"APPLIST", f::args) ->	   
-       RApp (loc,dbrec env f,List.map (dbrec env) args)
-
-   | Node(loc,"MULTCASE", p:: Node(_,"TOMATCH",tms):: eqns) ->
-       let po = match p with Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in
-       RCases (loc,po,
-	       List.map (dbrec env) tms,
-	       List.map (dbize_eqn (List.length tms) env) eqns)
-
-   | Node(loc,"CASE",Str(_,isrectag)::p::c::cl) ->
-       let po = match p with Str(_,"SYNTH") -> None | _ -> Some(dbrec env p) in
-       let isrec = match isrectag with
-	 | "REC" -> true | "NOREC" -> false 
-	 | _ -> anomaly "dbize: wrong REC tag in CASE" in
-	 ROldCase (loc,isrec,po,dbrec env c,Array.of_list (List.map (dbrec env) cl))
-
-   | Node(loc,"ISEVAR",[]) -> RHole (Some loc)
-   | Node(loc,"META",[Num(_,n)]) -> RRef (loc,RMeta n)
-
-   | Node(loc,"PROP", []) -> RSort(loc,RProp Null)
-   | Node(loc,"SET", [])  -> RSort(loc,RProp Pos)
-   | Node(loc,"TYPE", []) -> RSort(loc,RType)
-
-   (* This case mainly parses things build from   in a quotation *)
-   | Node(loc,("CONST"|"EVAR"|"MUTIND"|"MUTCONSTRUCT"|"SYNCONST" as key),l) ->
-       dbize_global loc (key,l)
-
-   | Node(loc,opn,tl) -> anomaly "dbize tmp"
-
- | _ -> anomaly "dbize: unexpected ast"
-
-  and dbize_eqn n env = function
-  | Node(loc,"EQN",rhs::lhs) ->
-      let (idsl,pl) = List.split (List.map (dbize_pattern env) lhs) in
-      let ids = List.flatten idsl in
-      check_linearity loc ids;
-      check_uppercase loc ids;
-      check_number_of_pattern loc n pl;
-      let env' =
-	List.fold_left (fun env id -> add_rel (Name id,()) env) env ids in
-	(ids,pl,dbrec env' rhs)
-  | _ -> anomaly "dbize: badly-formed ast for Cases equation"
-
-  and iterated_binder oper ty env = function
-    Slam(loc,ona,body) ->
-      let na =
-        (match ona with Some s -> Name (id_of_string s) | _ -> Anonymous)
-      in RBinder(loc, oper, na, 
-		 dbrec (add_rel (Anonymous,()) env) ty, (* To avoid capture *)
-		 (iterated_binder oper ty (add_rel (na,()) env) body))
-  | body -> dbrec env body
-
-  and dbize_args env l args =
-  let rec aux n l args = match (l,args) with 
-    | (i::l',Node(loc, "EXPL", [Num(_,j);a])::args') ->
-	if i=n & j>=i then
-	  if j=i
-	  then (dbrec env a)::(aux (n+1) l' args')
-	  else (RHole None)::(aux (n+1) l' args)
-	else error "Bad explicitation number"
-    | (i::l',a::args') -> 
-	if i=n
-	then (RHole None)::(aux (n+1) l' args)
-	else (dbrec env a)::(aux (n+1) l' args')
-    | ([],args) -> List.map (dbrec env) args
-    | (_,[]) -> []
-  in aux 1 l args
-
-  in dbrec
-
-
-(*
-let dbize_kind ... =
-  let c =
-    try dbize k sigma env com
-    with e ->
-      wrap_error
- 	(Ast.loc com, "dbize_kind",
-         [< 'sTR"During conversion from explicit-names to" ; 'sPC ;
-           'sTR"debruijn-indices" >], e,
-         [< 'sTR"Perhaps the input is malformed" >]) in
-
-  let c =
-    try absolutize k sigma env c
-    with e -> 
-      wrap_error
- 	(Ast.loc com, "Astterm.dbize_kind",
-         [< 'sTR"During the relocation of global references," >], e,
-         [< 'sTR"Perhaps the input is malformed" >])
-  in c
-
-*)
-
-let dbize_cci sigma env com = dbize CCI sigma env com
-let dbize_fw  sigma env com = dbize FW sigma env com
-
-(* constr_of_com takes an environment of typing assumptions,
- * and translates a command to a constr.
-
-let raw_constr_of_com sigma env com =
-  let c = dbize_cci sigma (unitize_env env) com in
-    try Sosub.soexecute c
-    with Failure _|UserError _ -> error_sosub_execute CCI com
-
-let raw_fconstr_of_com sigma env com =
-  let c = dbize_fw sigma (unitize_env env) com in
-    try Sosub.soexecute c
-    with Failure _|UserError _ -> error_sosub_execute FW com
-
-let raw_constr_of_compattern sigma env com =
-  let c = dbize_cci sigma (unitize_env env) com in
-    try Sosub.try_soexecute c
-    with Failure _|UserError _ -> error_sosub_execute CCI com
- *)
-
-let raw_constr_of_com sigma env com = dbize_cci sigma (unitize_env env) com
-let raw_fconstr_of_com sigma env com = dbize_fw sigma (unitize_env env) com
-let raw_constr_of_compattern sigma env com = 
-  dbize_cci sigma (unitize_env env) com
-
-
-(* Globalization of AST quotations (mainly used in command quotations
-   to get statically bound idents in grammar or pretty-printing rules) *)
-
-let ast_adjust_consts sigma = (* locations are kept *)
- let rec dbrec env = function
-    Nvar(loc,s) as ast ->
-      (let id = id_of_string s in
-      if (Ast.isMeta s) or (is_existential_id id) then ast
-      else if List.mem id (ids_of_env env) then ast
-      else 
-      try match Machops.search_reference env id with
-	| DOPN (Const sp,_) -> 
-	    if is_existential_id (basename sp) 
-	    then Node(loc,"EVAR",[path_section loc sp])
-	    else Node(loc,"CONST",[path_section loc sp])
-	| DOPN (MutConstruct ((sp,i),j),_) ->
-	    Node (loc,"MUTCONSTRUCT",[path_section loc sp;num i;num j])
-	| DOPN (MutInd (sp,i),_) ->
-	    Node (loc,"MUTIND",[path_section loc sp;num i])
-	| _ -> anomaly "Not a reference"
-      with UserError _ | Not_found ->
-      try let _ = search_synconst CCI id in Node(loc,"SYNCONST",[Nvar(loc,s)])
-      with Not_found -> warning ("Could not globalize "^s); ast)
-
-   | Slam(loc,None,t) -> Slam(loc,None,dbrec (add_rel (Anonymous,()) env) t)
-
-   | Slam(loc,Some na,t) ->
-       let env' = add_rel (Name (id_of_string na),()) env in
-         Slam(loc,Some na,dbrec env' t)
-   | Node(loc,opn,tl) -> Node(loc,opn,List.map (dbrec env) tl)
-   | x -> x
- in dbrec
-
-
-
-let globalize_command ast =
-  let (sigma,sign) = Termenv.initial_sigma_sign() in
-    ast_adjust_consts sigma (gLOB sign) ast
-
-
-
-(* Avoid globalizing in non command ast for tactics *)
-let rec glob_ast sigma env = function 
-  | Node(loc,"COMMAND",[c]) ->
-      Node(loc,"COMMAND",[ast_adjust_consts sigma env c])
-  | Node(loc,"COMMANDLIST",l) -> 
-      Node(loc,"COMMANDLIST", List.map (ast_adjust_consts sigma env) l)
-  | Slam(loc,None,t) ->
-      Slam(loc,None,glob_ast sigma (add_rel (Anonymous,()) env) t)
-  | Slam(loc,Some na,t) ->
-      let env' = add_rel (Name (id_of_string na),()) env in
-        Slam(loc,Some na, glob_ast sigma env' t)
-  | Node(loc,opn,tl) -> Node(loc,opn,List.map (glob_ast sigma env) tl)
-  | x -> x
-
-
-let globalize_ast ast =
-  let (sigma,sign) = Termenv.initial_sigma_sign() in
-    glob_ast sigma (gLOB sign) ast
-
-
-(* Installation of the AST quotations. "command" is used by default. *)
-
-open Pcoq
-
-let _ = 
-  define_quotation true "command" 
-    (map_entry globalize_command Command.command);
-  define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic);
-  define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac)
-
diff --git a/pretyping/astterm.mli b/pretyping/astterm.mli
deleted file mode 100755
index dbda7c9586..0000000000
--- a/pretyping/astterm.mli
+++ /dev/null
@@ -1,26 +0,0 @@
-
-(* $Id$ *)
-
-(*i*)
-open Names
-open Term
-open Evd
-(*i*)
-
-val dbize_op : CoqAst.loc -> string -> CoqAst.t list -> constr list -> constr
-val dbize    : unit assumptions -> CoqAst.t -> constr
-
-val absolutize_cci : 'c evar_map -> unit assumptions -> constr -> constr
-val dbize_cci      : 'c evar_map -> unit assumptions -> CoqAst.t -> constr
-val absolutize_fw  : 'c evar_map -> unit assumptions -> constr -> constr
-val dbize_fw       : 'c evar_map -> unit assumptions -> CoqAst.t -> constr
-
-val raw_constr_of_com :
-  'c evar_map -> 'a assumptions -> CoqAst.t -> constr
-val raw_fconstr_of_com :
-  'c evar_map -> 'a assumptions -> CoqAst.t -> constr
-val raw_constr_of_compattern :
-  'c evar_map -> 'a assumptions -> CoqAst.t -> constr
-
-val globalize_command : CoqAst.t -> CoqAst.t
-val globalize_ast     : CoqAst.t -> CoqAst.t