portage Astterm (partiellement)

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

1 files changed, 322 insertions, 282 deletions

diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index 3ca214a43..a6fa07f66 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -1,38 +1,31 @@
 
 (* $Id$ *)
 
-open Std;;
-open Pp;;
-open Names;;
-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)
+open Pp
+open Util
+open Names
+open Sign
+open Generic
+open Term
+open Environ
+open Evd
+open Impargs
+open Rawterm
+open Pretyping
+open Ast
+open Coqast
 
 (* 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") >]
-;;
+  [< '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" >] 
+  [< 'sTR "The variable " ; 'sTR(string_of_id id);
+     'sTR " is bound several times in pattern" >] 
 
 let rec has_duplicate = function 
-    [] -> None
+  | [] -> None
   | x::l -> if List.mem x l then (Some x) else has_duplicate l
 
 let check_linearity loc ids =
@@ -41,7 +34,7 @@ let check_linearity loc ids =
     | None -> ()
 
 let mal_formed_mssg () =
-  [<'sTR "malformed macro of multiple case" >];;
+  [<'sTR "malformed macro of multiple case" >]
 
 (* determines if some pattern variable starts with uppercase *)
 let warning_uppercase loc uplid = (* Comment afficher loc ?? *)
@@ -57,7 +50,7 @@ let is_uppercase_var v =
  | _  -> false
 
 let check_uppercase loc ids =
-  let uplid = filter is_uppercase_var ids in
+  let uplid = List.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 *)
@@ -92,7 +85,7 @@ let is_known_constructor k 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)) ->
@@ -105,7 +98,7 @@ let rec abs_eqn k env avoid = function
 	(id'::nids, DLAM(na,nt))
   | ([],t) -> ([],t)
   | _ -> assert false
-;;
+
 
 let rec absolutize_eqn absrec k env = function
     DOP1(XTRA("LAMEQN",ids),lam_eqn) ->
@@ -115,7 +108,7 @@ let rec absolutize_eqn absrec k env = function
       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" *)
@@ -146,7 +139,7 @@ let explicitize_appl l args =
  | ([],_) -> (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
@@ -184,7 +177,7 @@ let absolutize k sigma env constr =
   | 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
@@ -192,13 +185,14 @@ let absolutize_fw  sigma env constr = absolutize FW  sigma env constr
 *)
 
 let dbize_sp = function
-    Path(loc,sl,s) ->
-      (try section_path sl s
+  | 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" >]);;
+                     [< 'sTR"not a section-path" >])
 (*
 let dbize_op loc opn pl cl =
     match (opn,pl,cl) with
@@ -243,7 +237,7 @@ let dbize_op loc opn pl cl =
       | (op,_,_) -> anomaly_loc
             (loc,"Astterm.dbize_op",
              [< 'sTR "Unrecognizable constr operator: "; 'sTR op >])
-;;
+
 
 let split_params =
  let rec sprec acc = function
@@ -253,7 +247,7 @@ let split_params =
    | (Path _ as p)::l -> sprec (p::acc) l
    | l -> (List.rev acc,l)
  in sprec []
-;;
+
 *)
 
 let is_underscore id = (id = "_")
@@ -266,13 +260,15 @@ let ident_of_nvar loc s =
     user_err_loc (loc,"ident_of_nvar", [< 'sTR "Unexpected wildcard" >])
   else (id_of_string s)
 
-let ids_of_ctxt = Termast.ids_of_ctxt
+let ids_of_ctxt = array_map_to_list (function VAR id -> id | _ -> assert false)
 
 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
+  try 
+    match Declare.global_reference CCI (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 
@@ -281,65 +277,70 @@ let dbize_ctxt =
        | _ -> 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,REVar (dbize_sp sp,dbize_ctxt ctxt))
-  | ("MUTIND", sp::Num(_,tyi)::ctxt) -> RRef (loc,RInd ((dbize_sp sp, tyi),dbize_ctxt ctxt))
+  | ("CONST", sp::ctxt) -> 
+      RRef (loc,RConst (dbize_sp sp,dbize_ctxt ctxt))
+  | ("EVAR", (Num (_,ev))::ctxt) -> 
+      RRef (loc,REVar (ev,dbize_ctxt ctxt))
+  | ("MUTIND", sp::Num(_,tyi)::ctxt) -> 
+      RRef (loc,RInd ((dbize_sp sp, tyi),dbize_ctxt ctxt))
   | ("MUTCONSTRUCT", sp::Num(_,ti)::Num(_,n)::ctxt) ->
       RRef (loc,RConstruct (((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)) *)
+  (* | ("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 REVar (sp,ids_of_ctxt ctxt) 
-   else RConst (sp,ids_of_ctxt ctxt)
+  | DOPN (Const sp,ctxt) -> RConst (sp,ids_of_ctxt ctxt)
+  | DOPN (Evar ev,ctxt) -> REVar (ev,ids_of_ctxt ctxt) 
   | DOPN (MutConstruct (spi,j),ctxt) -> RConstruct ((spi,j),ids_of_ctxt ctxt)
   | DOPN (MutInd (sp,i),ctxt) -> RInd ((sp,i),ids_of_ctxt ctxt)
   | VAR id -> RVar id  (* utilisé dans trad pour coe_value (tmp) *)
   | _ -> anomaly "Not a reference"
 
+let error_var_not_found str loc s = 
+  Ast.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
-  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,_) -> RRel (loc,n),[]
-    | _ -> RRef(loc,RVar id), (try Vartab.implicits_of_var k id with _ -> [])
+  try 
+    match lookup_id id env with
+      | RELNAME(n,_) -> RRel (loc,n),[]
+      | _ -> 
+	  RRef(loc,RVar id), (try 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)])
+    try 
+      let c,il = match k with
+	| CCI -> Declare.global_reference_imps CCI id
+	| FW  -> Declare.global_reference_imps FW id
+	| OBJ -> anomaly "search_ref_cci_fw" in
+      RRef (loc,ref_from_constr c), il
+    with UserError _ ->
+      try 
+	RRef (loc,ref_from_constr (Declare.out_syntax_constant 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) ->
+  | 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(_,"PATTAS",[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')))
+	 | Anonymous -> dbize_pattern env p
+	 | Name id   -> 
+	     let (ids,p') = dbize_pattern env p in (id::ids,PatAs (loc,id,p')))
   | Node(_,"PATTCONSTRUCT", Nvar(loc,s)::((_::_) as pl)) ->
       (match maybe_constructor env s with
 	 | Some c ->
@@ -349,7 +350,7 @@ let rec dbize_pattern env = function
 	     user_err_loc (loc,"dbize_pattern",mssg_hd_is_not_constructor s))
   | Nvar(loc,s) ->
       (match name_of_nvar s with
-	   Anonymous -> ([], PatVar (loc,Anonymous))
+	 | Anonymous -> ([], PatVar (loc,Anonymous))
 	 | Name id as name -> ([id], PatVar (loc,name)))
   | _ -> anomaly "dbize: badly-formed ast for Cases pattern"
 
@@ -357,27 +358,34 @@ 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)
+      ((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)
+      ((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)
+      ((id_of_string fi)::lf, astA::lA, astT::lt)
   | _ -> anomaly "CFDECL is expected"
 
+let error_fixname_unbound str is_cofix loc name = 
+  user_err_loc 
+    (loc,"dbize (COFIX)",
+       [< '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 dbize k sigma =
   let rec dbrec env = function
-    Nvar(loc,s) -> fst (dbize_ref k sigma env loc s)
-
-(*
+    | 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)
@@ -387,115 +395,133 @@ let dbize k sigma =
        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,PrintCases,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 found operator "^opn^" with "^(string_of_int (List.length tl))^" arguments")
-
- | _ -> anomaly "dbize: unexpected ast"
+   *)
+    | Node(loc,"FIX", (Nvar (locid,iddef))::ldecl) ->
+	let (lf,ln,lA,lt) = dbize_fix ldecl in
+	let n =
+	  try 
+	    (list_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 
+	    (list_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,PrintCases,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 found operator "^opn^" with "^
+		 (string_of_int (List.length tl))^" arguments")
+
+    | _ -> 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
+    | 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"
+    | _ -> 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
-
+    | 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 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 ... =
@@ -516,7 +542,7 @@ let 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
@@ -528,17 +554,17 @@ let dbize_fw  sigma env com = dbize FW sigma env com
 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;;
+    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;;
+    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;;
+    with Failure _|UserError _ -> error_sosub_execute CCI com
  *)
 
 let raw_constr_of_com sigma env com = dbize_cci sigma (unitize_env env) com
@@ -551,42 +577,46 @@ let raw_constr_of_compattern sigma env com =
    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 rec dbrec env = function
+    | Nvar(loc,s) as ast ->
+	(let id = id_of_string s in
+	 if Ast.isMeta s then 
+	   ast
+	 else if List.mem id (ids_of_env env) then 
+	   ast
+	 else 
+	   try 
+	     match Declare.global_reference CCI id with
+	       | DOPN (Const sp,_) -> 
+		   Node(loc,"CONST",[path_section loc sp])
+	       | DOPN (Evar ev,_) ->
+		   Node(loc,"EVAR",[Num(loc,ev)])
+	       | 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 _ = Declare.out_syntax_constant 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
-;;
-
+  let env = Global.unsafe_env () in
+  let sign = get_globals (Environ.context env) in
+  ast_adjust_consts Evd.empty (gLOB sign) ast
 
 (* Avoid globalizing in non command ast for tactics *)
 let rec glob_ast sigma env = function 
@@ -598,21 +628,25 @@ let rec glob_ast sigma env = function
       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)
+      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
-;;
+  let env = Global.unsafe_env () in
+  let sign = get_globals (Environ.context env) in
+  glob_ast Evd.empty (gLOB sign) ast
+
 
 (* Installation of the AST quotations. "command" is used by default. *)
-open Pcoq;;
-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);;
+open Pcoq
+
+let _ = 
+  define_quotation true "command" (map_entry globalize_command Command.command)
+let _ = 
+  define_quotation false "tactic" (map_entry globalize_ast Tactic.tactic)
+let _ = 
+  define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac)
 
 
 (*********************************************************************)
@@ -622,43 +656,46 @@ define_quotation false "vernac" (map_entry globalize_ast Vernac.vernac);;
 
 (* With dB *)
 
-let constr_of_com_env1 is_ass sigma hyps com = 
-  let c = Astterm.raw_constr_of_com sigma hyps com in
-  try ise_resolve1 is_ass sigma hyps c
-  with e -> Stdpp.raise_with_loc (Ast.loc com) e
-
-
-let constr_of_com_env sigma hyps com =
-  constr_of_com_env1 false sigma hyps com
-
-let fconstr_of_com_env1 is_ass  sigma hyps com = 
-  let c = Astterm.raw_fconstr_of_com sigma hyps com in
-    try ise_resolve1 is_ass sigma hyps c
-    with e -> Stdpp.raise_with_loc (Ast.loc com) e
-
+let constr_of_com_env1 is_ass sigma env com = 
+  let c = raw_constr_of_com sigma (context env) com in
+  try 
+    ise_resolve1 is_ass sigma env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
+
+let constr_of_com_env sigma env com =
+  constr_of_com_env1 false sigma env com
+    
+let fconstr_of_com_env1 is_ass sigma env com = 
+  let c = raw_fconstr_of_com sigma (context env) com in
+  try 
+    ise_resolve1 is_ass sigma env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
  
 let fconstr_of_com_env sigma hyps com =
   fconstr_of_com_env1 false sigma hyps com 
-
-
+    
 (* Without dB *)
-let type_of_com sign com =
-  let env = gLOB sign in
-  let c = Astterm.raw_constr_of_com mt_evd env com in
-  try ise_resolve_type true mt_evd [] env c
-  with e -> Stdpp.raise_with_loc (Ast.loc com) e
-
-
-let constr_of_com1 is_ass sigma sign com = 
-  constr_of_com_env1 is_ass sigma (gLOB sign) com
+let type_of_com env com =
+  let sign = context env in
+  let c = raw_constr_of_com Evd.empty sign com in
+  try 
+    ise_resolve_type true Evd.empty [] env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
+
+let constr_of_com1 is_ass sigma env com = 
+  constr_of_com_env1 is_ass sigma env com
+    
+let constr_of_com sigma env com =
+  constr_of_com1 false sigma env com
 
-let constr_of_com sigma sign com =
-  constr_of_com1 false sigma sign com
 let constr_of_com_sort sigma sign com =
   constr_of_com1 true sigma sign com
 
-let fconstr_of_com1 is_ass sigma sign com = 
-  fconstr_of_com_env1 is_ass sigma (gLOB sign) com
+let fconstr_of_com1 is_ass sigma env com = 
+  fconstr_of_com_env1 is_ass sigma env com
 
 let fconstr_of_com sigma sign com  =
   fconstr_of_com1 false sigma sign com
@@ -666,40 +703,43 @@ let fconstr_of_com_sort sigma sign com  =
   fconstr_of_com1 true sigma sign com
 
 (* Note: typ is retyped *)
-let constr_of_com_casted sigma sign com typ = 
-  let env = gLOB sign in
-  let c = Astterm.raw_constr_of_com sigma env com in
+(***
+let constr_of_com_casted sigma env com typ = 
+  let sign = context env in
+  let c = raw_constr_of_com sigma sign com in
   let isevars = ref sigma in
   try
     let j = unsafe_fmachine
 	      (mk_tycon (nf_ise1 sigma typ)) false isevars [] env c in
-    (j_apply (process_evars true !isevars) j)._VAL
-  with e -> Stdpp.raise_with_loc (Ast.loc com) e
-
-
+    (j_apply (process_evars true !isevars) j).uj_val
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
 
 (* Typing with Trad, and re-checking with Mach *)
 let fconstruct_type sigma sign com =
-  let c = constr_of_com1 true sigma sign com
-  in Mach.fexecute_type sigma sign c
+  let c = constr_of_com1 true sigma sign com in 
+  Mach.fexecute_type sigma sign c
 
 let fconstruct sigma sign com =
-  let c = constr_of_com1 false sigma sign com
-  in Mach.fexecute sigma sign c
+  let c = constr_of_com1 false sigma sign com in 
+  Mach.fexecute sigma sign c
 
 let infconstruct_type sigma (sign,fsign) cmd =
-  let c = constr_of_com1 true sigma sign cmd
-  in Mach.infexecute_type sigma (sign,fsign) c
+  let c = constr_of_com1 true sigma sign cmd in 
+  Mach.infexecute_type sigma (sign,fsign) c
 
 let infconstruct sigma (sign,fsign) cmd =
-  let c = constr_of_com1 false sigma sign cmd
-  in Mach.infexecute sigma (sign,fsign) c
+  let c = constr_of_com1 false sigma sign cmd in 
+  Mach.infexecute sigma (sign,fsign) c
 
 (* Type-checks a term with the current universe constraints, the resulting
    constraints are dropped. *)
+
 let univ_sp = make_path ["univ"] (id_of_string "dummy") OBJ
+
 let fconstruct_with_univ sigma sign com =
   let c = constr_of_com sigma sign com in
-  let(_,j) = with_universes (Mach.fexecute sigma sign)
-               (univ_sp, Constraintab.current_constraints(), c)
-  in j
+  let (_,j) = with_universes (Mach.fexecute sigma sign)
+		(univ_sp, Constraintab.current_constraints(), c) in 
+  j
+***)