Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

42 files changed, 1388 insertions, 2205 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 21098a57..ab9c4c63 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,14 +6,14 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cerrors.ml,v 1.12.2.2 2004/07/16 20:48:17 herbelin Exp $ *)
+(* $Id: cerrors.ml 8003 2006-02-07 22:11:50Z herbelin $ *)
 
 open Pp
 open Util
-open Ast
 open Indtypes
 open Type_errors
 open Pretype_errors
+open Indrec
 open Lexer
 
 let print_loc loc =
@@ -47,8 +47,6 @@ let rec explain_exn_default = function
       hov 0 (str "Out of memory")
   | Stack_overflow -> 
       hov 0 (str "Stack overflow")
-  | Ast.No_match s -> 
-      hov 0 (str "Anomaly: Ast matching error: " ++ str s ++ report ())
   | Anomaly (s,pps) -> 
       hov 1 (str "Anomaly: " ++ where s ++ pps ++ report ())
   | Match_failure(filename,pos1,pos2) ->
@@ -76,9 +74,13 @@ let rec explain_exn_default = function
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_pretype_error ctx te)
   | InductiveError e -> 
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_inductive_error e)
+  | RecursionSchemeError e -> 
+      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_recursion_scheme_error e)
   | Cases.PatternMatchingError (env,e) -> 
       hov 0
 	(str "Error:" ++ spc () ++ Himsg.explain_pattern_matching_error env e)
+  | Tacred.ReductionTacticError e -> 
+      hov 0 (str "Error:" ++ spc () ++ Himsg.explain_reduction_tactic_error e)
   | Logic.RefinerError e -> 
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_refiner_error e)
   | Nametab.GlobalizationError q ->
@@ -90,8 +92,7 @@ let rec explain_exn_default = function
       hov 0 (str "Error:" ++ spc () ++
 	       str "No constant of this name:" ++ spc () ++ Libnames.pr_qualid q)
   | Refiner.FailError (i,s) ->
-      let s = if s="" then "" else " \""^s^"\"" in
-      hov 0 (str "Error: Tactic failure" ++ str s ++
+      hov 0 (str "Error: Tactic failure" ++ s ++
              if i=0 then mt () else str " (level " ++ int i ++ str").")
   | Stdpp.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 09d79cec..1236ecf5 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: cerrors.mli,v 1.2.6.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: cerrors.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/class.ml b/toplevel/class.ml
index f5493929..5f385934 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: class.ml,v 1.44.2.3 2004/11/26 18:06:54 herbelin Exp $ *)
+(* $Id: class.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
 
 open Util
 open Pp
@@ -92,42 +92,16 @@ let explain_coercion_error g = function
 
 (* Verifications pour l'ajout d'une classe *)
 
-let rec arity_sort (ctx,a) = match kind_of_term a with
-  | Sort (Prop _ | Type _) -> List.length ctx
-  | _ -> raise Not_found
-
 let check_reference_arity ref =
-  let t = Global.type_of_global ref in
-  try arity_sort (Reductionops.splay_prod (Global.env()) Evd.empty t)
-  with Not_found -> raise (CoercionError (NotAClass ref))
+  if not (Reductionops.is_arity (Global.env()) Evd.empty (Global.type_of_global ref)) then
+    raise (CoercionError (NotAClass ref))
 
 let check_arity = function
-  | CL_FUN | CL_SORT -> 0
+  | CL_FUN | CL_SORT -> ()
   | CL_CONST sp -> check_reference_arity (ConstRef sp)
   | CL_SECVAR sp -> check_reference_arity (VarRef sp)
   | CL_IND sp  -> check_reference_arity (IndRef sp)
 
-(* try_add_class : cl_typ -> strength option -> bool -> unit *)
-
-let strength_of_cl = function 
-  | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
-  | CL_SECVAR sp -> variable_strength sp
-  | _ -> Global
-
-let try_add_class cl streopt fail_if_exists =
-  if not (class_exists cl) then
-    let p = check_arity cl in
-    let stre' = strength_of_cl cl in 
-    let stre = match streopt with
-      | Some stre -> strength_min (stre,stre')
-      | None -> stre'
-    in
-    declare_class (cl,stre,p)
-  else
-    if fail_if_exists then errorlabstrm "try_add_new_class" 
-      (pr_class cl ++ str " is already a class")
-
-
 (* Coercions *)
 
 (* check that the computed target is the provided one *)
@@ -148,18 +122,18 @@ let uniform_cond nargs lt =
 let id_of_cl  = function
   | CL_FUN -> id_of_string "FUNCLASS"
   | CL_SORT -> id_of_string "SORTCLASS"
-  | CL_CONST kn -> id_of_label (label kn)
+  | CL_CONST kn -> id_of_label (con_label kn)
   | CL_IND ind ->
       let (_,mip) = Global.lookup_inductive ind in
       mip.mind_typename
   | CL_SECVAR id -> id
 
-let class_of_ref = function
+let class_of_global = function
   | ConstRef sp -> CL_CONST sp
   | IndRef sp -> CL_IND sp
   | VarRef id -> CL_SECVAR id
   | ConstructRef _ as c -> 
-      errorlabstrm "class_of_ref"
+      errorlabstrm "class_of_global"
 	(str "Constructors, such as " ++ Printer.pr_global c ++ 
 	   str " cannot be used as class")
 
@@ -204,14 +178,19 @@ let get_target t ind =
 let prods_of t = 
   let rec aux acc d = match kind_of_term d with
     | Prod (_,c1,c2) -> aux (c1::acc) c2
-    | Cast (c,_) -> aux acc c
+    | Cast (c,_,_) -> aux acc c
     | _ -> (d,acc)
   in 
   aux [] t
 
+let strength_of_cl = function 
+  | CL_CONST kn -> constant_strength (sp_of_global (ConstRef kn))
+  | CL_SECVAR sp -> variable_strength sp
+  | _ -> Global
+
 let get_strength stre ref cls clt =
-  let stres = (snd (class_info cls)).cl_strength in
-  let stret = (snd (class_info clt)).cl_strength in
+  let stres = strength_of_cl cls in
+  let stret = strength_of_cl clt in
   let stref = strength_of_global ref in
 (* 01/00: Supprimé la prise en compte de la force des variables locales. Sens ?
   let streunif = stre_unif_cond (s_vardep,f_vardep) in
@@ -265,10 +244,11 @@ let build_id_coercion idf_opt source =
   in
   let constr_entry = (* Cast is necessary to express [val_f] is identity *)
     DefinitionEntry
-      { const_entry_body = mkCast (val_f, typ_f);
+      { const_entry_body = mkCast (val_f, DEFAULTcast, typ_f);
 	const_entry_type = Some typ_f;
-        const_entry_opaque = false } in
-  let (_,kn) = declare_constant idf (constr_entry,Decl_kinds.IsDefinition) in
+        const_entry_opaque = false;
+	const_entry_boxed = Options.boxed_definitions()} in
+  let kn = declare_constant idf (constr_entry,IsDefinition IdentityCoercion) in
   ConstRef kn
 
 let check_source = function
@@ -288,11 +268,9 @@ lorque source est None alors target est None aussi.
 
 let add_new_coercion_core coef stre source target isid =
   check_source source;
-  let env = Global.env () in
-  let v = constr_of_reference coef in
-  let vj = Retyping.get_judgment_of env Evd.empty v in
+  let t = Global.type_of_global coef in
   if coercion_exists coef then raise (CoercionError AlreadyExists);
-  let tg,lp = prods_of (vj.uj_type) in
+  let tg,lp = prods_of t in
   let llp = List.length lp in
   if llp = 0 then raise (CoercionError NotAFunction);
   let (cls,lvs,ind) =
@@ -311,10 +289,10 @@ let add_new_coercion_core coef stre source target isid =
       raise (CoercionError NoTarget)
   in
   check_target clt target;
-  try_add_class cls None false;
-  try_add_class clt None false;
+  check_arity cls;
+  check_arity clt;
   let stre' = get_strength stre coef cls clt in
-  declare_coercion coef vj stre' isid cls clt (List.length lvs)
+  declare_coercion coef stre' isid cls clt (List.length lvs)
 
 let try_add_new_coercion_core ref b c d e =
   try add_new_coercion_core ref b c d e
@@ -345,114 +323,5 @@ let add_coercion_hook stre ref =
     ^ " is now a coercion")
 
 let add_subclass_hook stre ref =
-  let cl = class_of_ref ref in
+  let cl = class_of_global ref in
   try_add_new_coercion_subclass cl stre
-
-(* try_add_new_class : global_reference -> strength -> unit *)
-
-let class_of_global = function
-  | VarRef sp -> CL_SECVAR sp
-  | ConstRef sp -> CL_CONST sp
-  | IndRef sp -> CL_IND sp
-  | ConstructRef _ as ref -> raise (CoercionError (NotAClass ref))
-
-let try_add_new_class ref stre =
-  try try_add_class (class_of_global ref) (Some stre) true
-  with CoercionError e ->
-    errorlabstrm "try_add_new_class" (explain_coercion_error ref e)
-
-(* fonctions pour le discharge: encore un peu sale mais ça s'améliore *)
-
-type coercion_entry = 
-    global_reference * strength * bool * cl_typ * cl_typ * int
-
-let add_new_coercion (ref,stre,isid,cls,clt,n) =
-  (* Un peu lourd, tout cela pour trouver l'instance *)
-  let env = Global.env () in
-  let v = constr_of_reference ref in
-  let vj = Retyping.get_judgment_of env Evd.empty v in
-  declare_coercion ref vj stre isid cls clt n
-
-let count_extra_abstractions hyps ids_to_discard =
-  let _,n =
-    List.fold_left
-      (fun (hyps,n as sofar) id -> 
-	 match hyps with
-	   | (hyp,None,_)::rest when id = hyp ->(rest, n+1)
-	   | _ -> sofar)
-      (hyps,0) ids_to_discard
-  in n
-
-let defined_in_sec kn olddir = 
-  let _,dir,_ = repr_kn kn in
-    dir = olddir
-
-(* This moves the global path one step below *)
-let process_global olddir = function
-  | VarRef _ ->
-      anomaly "process_global only processes global surviving the section"
-  | ConstRef kn as x ->
-      if defined_in_sec kn olddir then
-        let newkn = Lib.make_kn (id_of_label (label kn)) in
-        ConstRef newkn
-      else x
-  | IndRef (kn,i) as x -> 
-      if defined_in_sec kn olddir then
-        let newkn = Lib.make_kn (id_of_label (label kn)) in
-        IndRef (newkn,i)
-      else x
-  | ConstructRef ((kn,i),j) as x -> 
-      if defined_in_sec kn olddir then
-        let newkn = Lib.make_kn (id_of_label (label kn)) in
-        ConstructRef ((newkn,i),j)
-      else x
-
-let process_class olddir ids_to_discard x =
-  let (cl,{cl_strength=stre; cl_param=p}) = x in
-(*  let env = Global.env () in*)
-  match cl with 
-    | CL_SECVAR _ -> x
-    | CL_CONST kn -> 
-       if defined_in_sec kn olddir then
-         let newkn = Lib.make_kn (id_of_label (label kn)) in
-	 let hyps = (Global.lookup_constant kn).const_hyps in
-	 let n = count_extra_abstractions hyps ids_to_discard in
-           (CL_CONST newkn,{cl_strength=stre;cl_param=p+n})
-       else 
-	 x
-    | CL_IND (kn,i) ->
-	if defined_in_sec kn olddir then
-          let newkn = Lib.make_kn (id_of_label (label kn)) in
-	  let hyps = (Global.lookup_mind kn).mind_hyps in
-	  let n = count_extra_abstractions hyps ids_to_discard in
-          (CL_IND (newkn,i),{cl_strength=stre;cl_param=p+n})
-        else 
-	  x
-    | _ -> anomaly "process_class" 
-
-let process_cl sec_sp cl =
-  match cl with
-    | CL_SECVAR id -> cl
-    | CL_CONST kn ->
-	if defined_in_sec kn sec_sp then
-          let newkn = Lib.make_kn (id_of_label (label kn)) in
-          CL_CONST newkn
-        else 
-	  cl
-    | CL_IND (kn,i) ->
-	if defined_in_sec kn sec_sp then
-          let newkn = Lib.make_kn (id_of_label (label kn)) in
-          CL_IND (newkn,i)
-        else 
-	  cl
-    | _ -> cl
-
-let process_coercion olddir ids_to_discard (coe,coeinfo,cls,clt) =
-  let hyps = context_of_global_reference coe in
-  let nargs = count_extra_abstractions hyps ids_to_discard in
-  (process_global olddir coe,
-   coercion_strength coeinfo,
-   coercion_identity coeinfo,
-   process_cl olddir cls,
-   process_cl olddir clt,
-   nargs + coercion_params coeinfo)
diff --git a/toplevel/class.mli b/toplevel/class.mli
index b0350985..7717d754 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: class.mli,v 1.17.6.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: class.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -50,19 +50,4 @@ val add_coercion_hook : Tacexpr.declaration_hook
 
 val add_subclass_hook : Tacexpr.declaration_hook
 
-(* [try_add_new_class ref] declares [ref] as a new class; usually,
-   this is done implicitely by [try_add_new_coercion]'s functions *)
-val try_add_new_class : global_reference -> strength -> unit
-
-(*s This is used for the discharge *)
-type coercion_entry
-
-val add_new_coercion : coercion_entry -> unit
-
-val process_class :
-  dir_path -> identifier list -> 
-    (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ)
-val process_coercion :
-  dir_path -> identifier list -> coercion -> coercion_entry
-
-val class_of_ref : global_reference -> cl_typ
+val class_of_global : global_reference -> cl_typ
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 10d6a620..7ff1b1b5 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml,v 1.116.2.4 2005/11/29 21:40:53 letouzey Exp $ *)
+(* $Id: command.ml 8689 2006-04-07 20:20:16Z herbelin $ *)
 
 open Pp
 open Util
@@ -18,7 +18,7 @@ open Entries
 open Inductive
 open Environ
 open Reduction
-open Tacred
+open Redexpr
 open Declare
 open Nametab
 open Names
@@ -37,31 +37,45 @@ open Indtypes
 open Vernacexpr
 open Decl_kinds
 open Pretyping
-open Symbols
+open Notation
 
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
 let mkProdCit = List.fold_right (fun (x,a) b -> mkProdC(x,a,b))
 
-let rec abstract_rawconstr c = function
+let rec abstract_constr_expr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_rawconstr c bl)
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,abstract_constr_expr c bl)
   | LocalRawAssum (idl,t)::bl ->
       List.fold_right (fun x b -> mkLambdaC([x],t,b)) idl
-        (abstract_rawconstr c bl)
+        (abstract_constr_expr c bl)
 
-let rec generalize_rawconstr c = function
+let rec generalize_constr_expr c = function
   | [] -> c
-  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_rawconstr c bl)
+  | LocalRawDef (x,b)::bl -> mkLetInC(x,b,generalize_constr_expr c bl)
   | LocalRawAssum (idl,t)::bl ->
       List.fold_right (fun x b -> mkProdC([x],t,b)) idl
-        (generalize_rawconstr c bl)
+        (generalize_constr_expr c bl)
+
+let rec length_of_raw_binders = function
+  | [] -> 0
+  | LocalRawDef _::bl -> 1 + length_of_raw_binders bl
+  | LocalRawAssum (idl,_)::bl -> List.length idl + length_of_raw_binders bl
+
+let rec under_binders env f n c =
+  if n = 0 then f env Evd.empty c else
+    match kind_of_term c with
+      | Lambda (x,t,c) ->
+	  mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
+      | LetIn (x,b,t,c) ->
+	  mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
+      | _ -> assert false
 
 let rec destSubCast c = match kind_of_term c with
   | Lambda (x,t,c) -> 
       let (b,u) = destSubCast c in mkLambda (x,t,b), mkProd (x,t,u)
   | LetIn (x,b,t,c) ->
       let (d,u) = destSubCast c in mkLetIn (x,b,t,d), mkLetIn (x,b,t,u)
-  | Cast (b,u) -> (b,u)
+  | Cast (b,_, u) -> (b,u)
   | _ -> assert false
 
 let rec adjust_conclusion a cs = function
@@ -84,63 +98,51 @@ let rec adjust_conclusion a cs = function
 let definition_message id =
   if_verbose message ((string_of_id id) ^ " is defined")
 
-let constant_entry_of_com (bl,com,comtypopt,opacity) =
+let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
   let sigma = Evd.empty in
   let env = Global.env() in
   match comtypopt with
       None -> 
-	let b = abstract_rawconstr com bl in
-	let j = judgment_of_rawconstr sigma env b in
+	let b = abstract_constr_expr com bl in
+	let j = interp_constr_judgment sigma env b in
 	{ const_entry_body = j.uj_val;
-	  const_entry_type = Some (Evarutil.refresh_universes j.uj_type);
-          const_entry_opaque = opacity }
+	  const_entry_type = Some (refresh_universes j.uj_type);
+          const_entry_opaque = opacity;
+	  const_entry_boxed = boxed }
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
-	let b = abstract_rawconstr (mkCastC (com,comtyp)) bl in
+	let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in
 	let (body,typ) = destSubCast (interp_constr sigma env b) in
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
-          const_entry_opaque = opacity }
-
-let rec length_of_raw_binders = function
-  | [] -> 0
-  | LocalRawDef _::bl -> 1 + length_of_raw_binders bl
-  | LocalRawAssum (idl,_)::bl -> List.length idl + length_of_raw_binders bl
-
-let rec under_binders env f n c =
-  if n = 0 then f env Evd.empty c else
-    match kind_of_term c with
-      | Lambda (x,t,c) ->
-        mkLambda (x,t,under_binders (push_rel (x,None,t) env) f (n-1) c)
-      | LetIn (x,b,t,c) ->
-        mkLetIn (x,b,t,under_binders (push_rel (x,Some b,t) env) f (n-1) c)
-      | _ -> assert false
+          const_entry_opaque = opacity;
+	  const_entry_boxed = boxed }
 
 let red_constant_entry bl ce = function
   | None -> ce
   | Some red ->
       let body = ce.const_entry_body in
       { ce with const_entry_body = 
-      under_binders (Global.env()) (reduction_of_redexp red)
-        (length_of_raw_binders bl)
-        body }
+	under_binders (Global.env()) (fst (reduction_of_red_expr red))
+	  (length_of_raw_binders bl)
+	  body }
 
 let declare_global_definition ident ce local =
-  let (_,kn) = declare_constant ident (DefinitionEntry ce,IsDefinition) in
-  if local = Local then
+  let kn = declare_constant ident (DefinitionEntry ce,IsDefinition Definition) in
+  if local = Local && Options.is_verbose() then
     msg_warning (pr_id ident ++ str" is declared as a global definition");
   definition_message ident;
   ConstRef kn
 
-let declare_definition ident (local,_) bl red_option c typopt hook =
-  let ce = constant_entry_of_com (bl,c,typopt,false) in
+let declare_definition ident (local,boxed,dok) bl red_option c typopt hook =
+  let ce = constant_entry_of_com (bl,c,typopt,false,boxed) in
   let ce' = red_constant_entry bl ce red_option in
   let r = match local with
     | Local when Lib.sections_are_opened () ->
         let c =
           SectionLocalDef(ce'.const_entry_body,ce'.const_entry_type,false) in
-        let _ = declare_variable ident (Lib.cwd(), c, IsDefinition) in
+        let _ = declare_variable ident (Lib.cwd(),c,IsDefinition Definition) in
         definition_message ident;
         if Pfedit.refining () then 
           msgerrnl (str"Warning: Local definition " ++ pr_id ident ++ 
@@ -152,7 +154,6 @@ let declare_definition ident (local,_) bl red_option c typopt hook =
 
 let syntax_definition ident c local onlyparse =
   let c = snd (interp_aconstr [] [] c) in
-  let onlyparse = !Options.v7_only or onlyparse in
   Syntax_def.declare_syntactic_definition local ident onlyparse c
 
 (* 2| Variable/Hypothesis/Parameter/Axiom declarations *)
@@ -163,7 +164,7 @@ let assumption_message id =
 let declare_one_assumption is_coe (local,kind) c (_,ident) =
   let r = match local with
     | Local when Lib.sections_are_opened () ->
-        let r = 
+        let _ = 
           declare_variable ident 
             (Lib.cwd(), SectionLocalAssum c, IsAssumption kind) in
         assumption_message ident;
@@ -172,7 +173,7 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
           str" is not visible from current goals");
         VarRef ident
     | (Global|Local) ->
-        let (_,kn) =
+        let kn =
           declare_constant ident (ParameterEntry c, IsAssumption kind) in
         assumption_message ident;
         if local=Local & Options.is_verbose () then
@@ -182,9 +183,13 @@ let declare_one_assumption is_coe (local,kind) c (_,ident) =
   if is_coe then Class.try_add_new_coercion r local
 
 let declare_assumption idl is_coe k bl c =
-  let c = generalize_rawconstr c bl in
-  let c = interp_type Evd.empty (Global.env()) c in
-  List.iter (declare_one_assumption is_coe k c) idl
+  if not (Pfedit.refining ()) then 
+    let c = generalize_constr_expr c bl in
+    let c = interp_type Evd.empty (Global.env()) c in
+      List.iter (declare_one_assumption is_coe k c) idl
+  else
+    errorlabstrm "Command.Assumption"
+	(str "Cannot declare an assumption while in proof editing mode.")
 
 (* 3a| Elimination schemes for mutual inductive definitions *)
 
@@ -203,16 +208,17 @@ let declare_one_elimination ind =
       (DefinitionEntry
         { const_entry_body = c;
           const_entry_type = t;
-          const_entry_opaque = false }, 
-       Decl_kinds.IsDefinition) in
+          const_entry_opaque = false;
+	  const_entry_boxed = Options.boxed_definitions() }, 
+       Decl_kinds.IsDefinition Definition) in
     definition_message id;
     kn
   in
   let env = Global.env () in
   let sigma = Evd.empty in
   let elim_scheme = Indrec.build_indrec env sigma ind in
-  let npars = mip.mind_nparams in
-  let make_elim s = Indrec.instanciate_indrec_scheme s npars elim_scheme in
+  let npars = mib.mind_nparams_rec in
+  let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in
   let kelim = mip.mind_kelim in
   (* in case the inductive has a type elimination, generates only one
      induction scheme, the other ones share the same code with the
@@ -220,10 +226,10 @@ let declare_one_elimination ind =
   if List.mem InType kelim then
     let elim = make_elim (new_sort_in_family InType) in
     let cte = declare (mindstr^(Indrec.elimination_suffix InType)) elim None in
-    let c = mkConst (snd cte) and t = constant_type (Global.env()) (snd cte) in
+    let c = mkConst cte and t = constant_type (Global.env()) cte in
     List.iter (fun (sort,suff) -> 
       let (t',c') = 
-	Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort)
+	Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort)
 	  npars c t in
       let _ = declare (mindstr^suff) c' (Some t') in ())
       non_type_eliminations
@@ -270,27 +276,9 @@ let interp_mutual lparams lnamearconstrs finite =
       [] lnamearconstrs in
   if not (list_distinct allnames) then
     error "Two inductive objects have the same name";
-  let nparams = local_binders_length lparams
-  and sigma = Evd.empty 
-  and env0 = Global.env() in
-  let env_params, params =
-    List.fold_left
-      (fun (env, params) d -> match d with
-	| LocalRawAssum ([_,na],(CHole _ as t)) ->
-	    let t = interp_binder sigma env na t in
-	    let d = (na,None,t) in
-	    (push_rel d env, d::params)
-	| LocalRawAssum (nal,t) ->
-	    let t = interp_type sigma env t in
-	    let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
-	    let ctx = List.rev ctx in
-	    (push_rel_context ctx env, ctx@params)
-	| LocalRawDef ((_,na),c) ->
-	    let c = judgment_of_rawconstr sigma env c in
-	    let d = (na, Some c.uj_val, c.uj_type) in
-	    (push_rel d env,d::params))
-      (env0,[]) lparams
-  in
+  let sigma = Evd.empty and env0 = Global.env() in
+  let env_params, params = interp_context sigma env0 lparams in
+
   (* Builds the params of the inductive entry *)
   let params' =
     List.map (fun (na,b,t) ->
@@ -304,8 +292,6 @@ let interp_mutual lparams lnamearconstrs finite =
   let paramassums = 
     List.fold_right (fun d l -> match d with
 	(id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in
-  let indnames =
-    List.map (fun (id,_,_,_)-> id) lnamearconstrs @ paramassums in
   let nparamassums = List.length paramassums in
   let (ind_env,ind_impls,arityl) =
     List.fold_left
@@ -316,7 +302,7 @@ let interp_mutual lparams lnamearconstrs finite =
 	 let argsc = compute_arguments_scope fullarity in
 	 let ind_impls' = 
 	   if Impargs.is_implicit_args() then
-	     let impl = Impargs.compute_implicits false env_params fullarity in
+	     let impl = Impargs.compute_implicits env_params fullarity in
 	     let paramimpl,_ = list_chop nparamassums impl in
 	     let l = List.fold_right
 	       (fun imp l -> if Impargs.is_status_implicit imp then
@@ -337,8 +323,9 @@ let interp_mutual lparams lnamearconstrs finite =
   let fs = States.freeze() in
   (* Declare the notations for the inductive types pushed in local context*)
   try
-  List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
-    Metasyntax.add_notation_interpretation df ind_impls c None) notations;
+  List.iter (fun (df,c,scope) ->
+    silently (Metasyntax.add_notation_interpretation df ind_impls c) scope)
+    notations;
   let ind_env_params = push_rel_context params ind_env in
 
   let mispecvec = 
@@ -358,21 +345,20 @@ let interp_mutual lparams lnamearconstrs finite =
          (* Interpret the constructor types *)
          let constrs =
 	   List.map 
-	     (interp_type_with_implicits sigma ind_env_params
-	       (paramassums,ind_impls))
+	     (interp_type sigma ind_env_params ~impls:(paramassums,ind_impls))
 	     bodies
 	 in
 
          (* Build the inductive entry *)
-	 { mind_entry_params = params';
-	   mind_entry_typename = name;
+	 { mind_entry_typename = name;
 	   mind_entry_arity = ar;
 	   mind_entry_consnames = constrnames;
 	   mind_entry_lc = constrs })
       (List.rev arityl) lnamearconstrs
   in
   States.unfreeze fs;
-  notations, { mind_entry_record = false; 
+  notations, { mind_entry_params = params';
+	       mind_entry_record = false; 
 	       mind_entry_finite = finite; 
 	       mind_entry_inds = mispecvec }
   with e -> States.unfreeze fs; raise e
@@ -388,6 +374,7 @@ let declare_mutual_with_eliminations isrecord mie =
 (* Very syntactical equality *)
 let eq_la d1 d2 = match d1,d2 with
   | LocalRawAssum (nal,ast), LocalRawAssum (nal',ast') ->
+      (List.length nal = List.length nal') &&
       List.for_all2 (fun (_,na) (_,na') -> na = na') nal nal'
       & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false)
   | LocalRawDef ((_,id),ast), LocalRawDef ((_,id'),ast') ->
@@ -422,7 +409,7 @@ let extract_coe_la_lc = function
 let build_mutual lind finite =
   let ((coes:identifier list),lparams,lnamearconstructs) = extract_coe_la_lc lind in
   let notations,mie = interp_mutual lparams lnamearconstructs finite in
-  let kn = declare_mutual_with_eliminations false mie in
+  let _ = declare_mutual_with_eliminations false mie in
   (* Declare the notations now bound to the inductive types *)
   List.iter (fun (df,c,scope) ->
     Metasyntax.add_notation_interpretation df [] c scope) notations;
@@ -465,7 +452,8 @@ let collect_non_rec env =
   in 
   searchrec [] 
 
-let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
+let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
+                                                                   boxed =
   let lrecnames = List.map (fun ((f,_,_,_,_),_) -> f) lnameargsardef 
   and sigma = Evd.empty
   and env0 = Global.env()
@@ -474,11 +462,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
   let (rec_sign,rec_impls,arityl) = 
     List.fold_left 
       (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> 
-        let arityc = generalize_rawconstr arityc bl in
+        let arityc = generalize_constr_expr arityc bl in
         let arity = interp_type sigma env0 arityc in
 	let impl = 
 	  if Impargs.is_implicit_args()
-	  then Impargs.compute_implicits false env0 arity
+	  then Impargs.compute_implicits env0 arity
 	  else [] in
 	let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
         (Environ.push_named (recname,None,arity) env, impls', arity::arl))
@@ -494,13 +482,15 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
     let fs = States.freeze() in
     let def = 
       try
-	List.iter (fun (df,c,scope) -> (* No scope for tmp notation *)
-	 Metasyntax.add_notation_interpretation df rec_impls c None) notations;
+	List.iter (fun (df,c,scope) ->
+	 silently
+	  (Metasyntax.add_notation_interpretation df rec_impls c) scope)
+	  notations;
 	List.map2
 	  (fun ((_,_,bl,_,def),_) arity ->
-            let def = abstract_rawconstr def bl in
-            interp_casted_constr_with_implicits 
-	      sigma rec_sign rec_impls def arity)
+            let def = abstract_constr_expr def bl in
+            interp_casted_constr sigma rec_sign ~impls:([],rec_impls)
+              def arity)
           lnameargsardef arityl
       with e ->
 	States.unfreeze fs; raise e in
@@ -514,11 +504,12 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
   let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
   let rec declare i fi =
     let ce = 
-      { const_entry_body = mkFix ((nvrec,i),recdecls);
+      { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *)
         const_entry_type = Some arrec.(i);
-        const_entry_opaque = false } in
-    let (_,kn) = declare_constant fi (DefinitionEntry ce, IsDefinition) in
-    (ConstRef kn)
+        const_entry_opaque = false;
+        const_entry_boxed = boxed} in
+    let kn = declare_constant fi (DefinitionEntry ce,IsDefinition Fixpoint)
+    in (ConstRef kn)
   in 
   (* declare the recursive definitions *)
   let lrefrec = Array.mapi declare namerec in
@@ -530,8 +521,11 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
       (fun subst (f,def,t) ->
 	 let ce = { const_entry_body = replace_vars subst def;
 		    const_entry_type = Some t;
-                    const_entry_opaque = false } in
-	 let _ = declare_constant f (DefinitionEntry ce, IsDefinition) in
+                    const_entry_opaque = false;
+		    const_entry_boxed = boxed } in
+	 let _ =
+	   declare_constant f (DefinitionEntry ce,IsDefinition Definition)
+	 in
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst (Array.to_list namerec))
@@ -540,7 +534,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)  =
   List.iter (fun (df,c,scope) ->
     Metasyntax.add_notation_interpretation df [] c scope) notations
 
-let build_corecursive lnameardef = 
+let build_corecursive lnameardef boxed = 
   let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef
   and sigma = Evd.empty
   and env0 = Global.env() in
@@ -549,11 +543,10 @@ let build_corecursive lnameardef =
     try 
       List.fold_left 
         (fun (env,arl) (recname,bl,arityc,_) -> 
-           let arityc = generalize_rawconstr arityc bl in
-           let arj = type_judgment_of_rawconstr Evd.empty env0 arityc in
-	   let arity = arj.utj_val in
+           let arityc = generalize_constr_expr arityc bl in
+           let arity = interp_type Evd.empty env0 arityc in
            let _ = declare_variable recname
-	     (Lib.cwd(),SectionLocalAssum arj.utj_val,IsAssumption Definitional) in
+	     (Lib.cwd(),SectionLocalAssum arity,IsAssumption Definitional) in
            (Environ.push_named (recname,None,arity) env, (arity::arl)))
         (env0,[]) lnameardef
     with e -> 
@@ -562,10 +555,10 @@ let build_corecursive lnameardef =
   let recdef =
     try 
       List.map (fun (_,bl,arityc,def) ->
-        let arityc = generalize_rawconstr arityc bl in
-        let def = abstract_rawconstr def bl in
+        let arityc = generalize_constr_expr arityc bl in
+        let def = abstract_constr_expr def bl in
 	let arity = interp_constr sigma rec_sign arityc in
-                  interp_casted_constr sigma rec_sign def arity)
+        interp_casted_constr sigma rec_sign def arity)
         lnameardef
     with e -> 
       States.unfreeze fs; raise e 
@@ -580,10 +573,11 @@ let build_corecursive lnameardef =
     let ce = 
       { const_entry_body = mkCoFix (i, recdecls);
         const_entry_type = Some (arrec.(i));
-        const_entry_opaque = false } 
+        const_entry_opaque = false;
+        const_entry_boxed = boxed } 
     in
-    let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
-    (ConstRef kn)
+    let kn = declare_constant fi (DefinitionEntry ce,IsDefinition CoFixpoint)
+    in (ConstRef kn)
   in 
   let lrefrec = Array.mapi declare namerec in
   if_verbose ppnl (corecursive_message lrefrec);
@@ -593,8 +587,10 @@ let build_corecursive lnameardef =
       (fun subst (f,def,t) ->
 	 let ce = { const_entry_body = replace_vars subst def;
 		    const_entry_type = Some t;
-                    const_entry_opaque = false } in
-	 let _ = declare_constant f (DefinitionEntry ce,IsDefinition) in
+                    const_entry_opaque = false;
+		    const_entry_boxed = boxed } in
+	 let _ = 
+	   declare_constant f (DefinitionEntry ce,IsDefinition Definition) in
       	 warning ((string_of_id f)^" is non-recursively defined");
       	 (var_subst f) :: subst)
       (List.map var_subst (Array.to_list namerec))
@@ -616,11 +612,12 @@ let build_scheme lnamedepindsort =
   let listdecl = Indrec.build_mutual_indrec env0 sigma lrecspec in 
   let rec declare decl fi lrecref =
     let decltype = Retyping.get_type_of env0 Evd.empty decl in
-    let decltype = Evarutil.refresh_universes decltype in
+    let decltype = refresh_universes decltype in
     let ce = { const_entry_body = decl;
                const_entry_type = Some decltype;
-               const_entry_opaque = false } in
-    let _,kn = declare_constant fi (DefinitionEntry ce, IsDefinition) in
+               const_entry_opaque = false;
+	       const_entry_boxed = Options.boxed_definitions() } in
+    let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in
     ConstRef kn :: lrecref
   in 
   let lrecref = List.fold_right2 declare listdecl lrecnames [] in
@@ -643,29 +640,30 @@ let start_proof_com sopt kind (bl,t) hook =
  	  (Pfedit.get_all_proof_names ())
   in
   let env = Global.env () in
-  let c = interp_type Evd.empty env (generalize_rawconstr t bl) in
+  let c = interp_type Evd.empty env (generalize_constr_expr t bl) in
   let _ = Typeops.infer_type env c in
   start_proof id kind c hook
 
-let save id const kind hook =
+let save id const (locality,kind) hook =
   let {const_entry_body = pft;
        const_entry_type = tpo;
        const_entry_opaque = opacity } = const in
-  let l,r = match kind with
-    | IsLocal when Lib.sections_are_opened () ->
+  let l,r = match locality with
+    | Local when Lib.sections_are_opened () ->
+        let k = logical_kind_of_goal_kind kind in
 	let c = SectionLocalDef (pft, tpo, opacity) in
-	let _ = declare_variable id (Lib.cwd(), c, IsDefinition) in
+	let _ = declare_variable id (Lib.cwd(), c, k) in
 	(Local, VarRef id)
-    | IsLocal ->
-        let k = IsDefinition in
-        let _,kn = declare_constant id (DefinitionEntry const, k) in
+    | Local ->
+        let k = logical_kind_of_goal_kind kind in
+        let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn)
-    | IsGlobal k ->
-        let k = theorem_kind_of_goal_kind k in
-        let _,kn = declare_constant id (DefinitionEntry const, k) in
+    | Global ->
+        let k = logical_kind_of_goal_kind kind in
+        let kn = declare_constant id (DefinitionEntry const, k) in
 	(Global, ConstRef kn) in
-  hook l r;
   Pfedit.delete_current_proof ();
+  hook l r;
   definition_message id
 
 let save_named opacity =
@@ -691,7 +689,7 @@ let save_anonymous_with_strength kind opacity save_ident =
   let const = { const with const_entry_opaque = opacity } in
   check_anonymity id save_ident;
   (* we consider that non opaque behaves as local for discharge *)
-  save save_ident const (IsGlobal (Proof kind)) hook
+  save save_ident const (Global, Proof kind) hook
 
 let admit () =
   let (id,k,typ,hook) = Pfedit.current_proof_statement () in
@@ -699,9 +697,10 @@ let admit () =
   if k <> IsGlobal (Proof Conjecture) then
     error "Only statements declared as conjecture can be admitted";
 *)
-  let (_,kn) = declare_constant id (ParameterEntry typ, IsConjecture) in
-  hook Global (ConstRef kn);
+  let kn =
+    declare_constant id (ParameterEntry typ, IsAssumption Conjectural) in
   Pfedit.delete_current_proof ();
+  hook Global (ConstRef kn);
   assumption_message id
 
 let get_current_context () =
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 7997288c..c93f69be 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: command.mli,v 1.38.2.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: command.mli 7682 2005-12-21 15:06:11Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -22,6 +22,7 @@ open Vernacexpr
 open Rawterm
 open Topconstr
 open Decl_kinds
+open Redexpr
 (*i*)
 
 (*s Declaration functions. The following functions take ASTs,
@@ -30,7 +31,7 @@ open Decl_kinds
    defined object *)
 
 val declare_definition : identifier -> definition_kind ->
-  local_binder list -> Tacred.red_expr option -> constr_expr ->
+  local_binder list -> red_expr option -> constr_expr ->
     constr_expr option -> declaration_hook -> unit
 
 val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
@@ -43,13 +44,13 @@ val build_mutual : inductive_expr list -> bool -> unit
 val declare_mutual_with_eliminations :
   bool -> Entries.mutual_inductive_entry -> mutual_inductive
 
-val build_recursive : (fixpoint_expr * decl_notation) list -> unit
+val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit
 
-val build_corecursive : cofixpoint_expr list -> unit
+val build_corecursive : cofixpoint_expr list -> bool -> unit
 
 val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
 
-val generalize_rawconstr : constr_expr -> local_binder list -> constr_expr
+val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
 
 val start_proof : identifier -> goal_kind -> constr ->
   declaration_hook -> unit
@@ -83,3 +84,5 @@ val admit : unit -> unit
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
+
+
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 4ba8f6c2..44b2e231 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqinit.ml,v 1.30.2.4 2006/01/11 23:18:06 barras Exp $ *)
+(* $Id: coqinit.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
 
 open Pp
 open System
@@ -73,23 +73,19 @@ let init_load_path () =
   (* developper specific directories to open *)
   let dev = if Coq_config.local then [ "dev" ] else [] in
   let coqlib =
-    if !Options.boot then Coq_config.coqtop
-      (* variable COQLIB overrides the default library *)
-    else getenv_else "COQLIB" Coq_config.coqlib in
-  let coqlib = canonical_path_name coqlib in
+    (* variable COQLIB overrides the default library *)
+    getenv_else "COQLIB"
+      (if Coq_config.local || !Options.boot then Coq_config.coqtop
+       else Coq_config.coqlib) in
   (* first user-contrib *)
   let user_contrib = coqlib/"user-contrib" in
   if Sys.file_exists user_contrib then 
-    Mltop.add_path user_contrib Nameops.default_root_prefix;
+    Mltop.add_rec_path user_contrib Nameops.default_root_prefix;
   (* then standard library *)
-  let vdirs = 
-    if !Options.v7 then [ "theories7"; "contrib7" ]
-    else [ "theories"; "contrib" ] in
-  let dirs = 
-    (if !Options.v7 then "states7" else "states") :: dev @ vdirs in
+  let vdirs = [ "theories"; "contrib" ] in
+  let dirs = "states" :: dev @ vdirs in
   List.iter (fun s -> coq_add_rec_path (coqlib/s)) dirs;
   let camlp4 = getenv_else "CAMLP4LIB" Coq_config.camlp4lib in
-  let camlp4 = canonical_path_name camlp4 in
   add_ml_include camlp4;
   (* then current directory *)
   Mltop.add_path "." Nameops.default_root_prefix;
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index e029d8ac..d7856170 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqinit.mli,v 1.7.16.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: coqinit.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Initialization. *)
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index af787460..c3f79e0a 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqtop.ml,v 1.72.2.5 2005/11/23 14:46:09 barras Exp $ *)
+(* $Id: coqtop.ml 7740 2005-12-26 20:07:21Z herbelin $ *)
 
 open Pp
 open Util
@@ -29,9 +29,8 @@ let get_version_date () =
   with _ -> Coq_config.date
 
 let print_header () =
-  Printf.printf "Welcome to Coq %s%s (%s)\n"
+  Printf.printf "Welcome to Coq %s (%s)\n" 
     Coq_config.version 
-    (if !Options.v7 then " (V7 syntax)" else "")
     (get_version_date ());
   flush stdout
 
@@ -50,8 +49,10 @@ let engage () =
   
 let set_batch_mode () = batch_mode := true
 
-let toplevel_name = ref (make_dirpath [id_of_string "Top"])
-let set_toplevel_name dir = toplevel_name := dir
+let toplevel_default_name = make_dirpath [id_of_string "Top"]
+let toplevel_name = ref (Some toplevel_default_name)
+let set_toplevel_name dir = toplevel_name := Some dir
+let unset_toplevel_name () = toplevel_name := None
 
 let remove_top_ml () = Mltop.remove ()
 
@@ -91,12 +92,13 @@ let load_vernacular () =
 let load_vernacular_obj = ref ([] : string list)
 let add_vernac_obj s = load_vernacular_obj := s :: !load_vernacular_obj
 let load_vernac_obj () = 
-  List.iter Library.read_library_from_file (List.rev !load_vernacular_obj)
+  List.iter (fun f -> Library.require_library_from_file None f None)
+    (List.rev !load_vernacular_obj)
 
 let require_list = ref ([] : string list)
 let add_require s = require_list := s :: !require_list
 let require () =
-  List.iter (fun s -> Library.require_library_from_file None None s false)
+  List.iter (fun s -> Library.require_library_from_file None s (Some false))
     (List.rev !require_list)
 
 let compile_list = ref ([] : (bool * string) list)
@@ -128,7 +130,6 @@ let re_exec is_ide =
   let s = !re_exec_version in
   let is_native = (Mltop.get()) = Mltop.Native in
   let prog = Sys.argv.(0) in
-  let coq = Filename.basename prog in
   if (is_native && s = "byte") || ((not is_native) && s = "opt")
   then begin
     let s = if s = "" then if is_native then "opt" else "byte" else s in
@@ -142,6 +143,17 @@ let re_exec is_ide =
     Unix.handle_unix_error (Unix.execvp newprog) Sys.argv
   end
 
+(*s options for the virtual machine *)
+
+let boxed_val = ref false
+let boxed_def = ref false
+let use_vm = ref false
+
+let set_vm_opt () =
+  Vm.set_transp_values (not !boxed_val);
+  Options.set_boxed_definitions !boxed_def;
+  Vconv.set_use_vm !use_vm
+
 (*s Parsing of the command line.
     We no longer use [Arg.parse], in order to use share [Usage.print_usage]
     between coqtop and coqc. *)
@@ -162,7 +174,7 @@ let parse_args is_ide =
     | [] -> ()
 
     | "-impredicative-set" :: rem -> 
-        set_engagement Environ.ImpredicativeSet; parse rem
+        set_engagement Declarations.ImpredicativeSet; parse rem
 
     | ("-I"|"-include") :: d :: rem -> set_default_include d; parse rem
     | ("-I"|"-include") :: []       -> usage ()
@@ -173,6 +185,7 @@ let parse_args is_ide =
     | "-top" :: d :: rem -> set_toplevel_name (dirpath_of_string d); parse rem
     | "-top" :: [] -> usage ()
 
+    | "-notop" :: rem -> unset_toplevel_name (); parse rem
     | "-q" :: rem -> no_load_rc (); parse rem
 
     | "-opt" :: rem -> set_opt(); parse rem
@@ -228,6 +241,7 @@ let parse_args is_ide =
 
     | "-debug" :: rem -> set_debug (); parse rem
 
+    | "-vm" :: rem -> use_vm := true; parse rem
     | "-emacs" :: rem -> Options.print_emacs := true; parse rem
 	  
     | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
@@ -253,12 +267,10 @@ let parse_args is_ide =
     | "-xml" :: rem -> Options.xml_export := true; parse rem
 
     (* Scanned in Options! *)
-    | "-v7" :: rem -> (* Options.v7 := true; *) parse rem
-    | "-v8" :: rem -> (* Options.v7 := false; *) parse rem
+    | "-v7" :: rem -> error "This version of Coq does not support v7 syntax"
+    | "-v8" :: rem -> parse rem
 
-    (* Translator options *)
-    | "-strict-implicit" :: rem -> 
-	Options.translate_strict_impargs := false; parse rem
+    | "-no-hash-consing" :: rem -> Options.hash_cons_proofs := false; parse rem
 
     | s :: rem -> 
 	if is_ide then begin
@@ -294,9 +306,10 @@ let init is_ide =
       if_verbose print_header ();
       init_load_path ();
       inputstate ();
+      set_vm_opt ();
       engage ();
-      if not !batch_mode && Global.env_is_empty() then
-        Declaremods.start_library !toplevel_name;
+      if (not !batch_mode|| !compile_list=[]) && Global.env_is_empty() then
+        option_iter Declaremods.start_library !toplevel_name;
       init_library_roots ();
       load_vernac_obj ();
       require ();
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index ef8b4b37..b5a1106c 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: coqtop.mli,v 1.5.4.1 2004/07/16 19:31:47 herbelin Exp $ i*)
+(*i $Id: coqtop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* The Coq main module. The following function [start] will parse the
    command line, print the banner, initialize the load path, load the input 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 281ff1b6..6c543079 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -6,325 +6,83 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: discharge.ml,v 1.81.2.2 2005/11/29 21:40:53 letouzey Exp $ *)
+(* $Id: discharge.ml 7493 2005-11-02 22:12:16Z mohring $ *)
 
-open Pp
-open Util
 open Names
-open Nameops
+open Util
 open Sign
 open Term
-open Declarations
 open Entries
-open Inductive
-open Instantiate
-open Reduction
+open Declarations
 open Cooking
-open Typeops
-open Libnames
-open Libobject
-open Lib
-open Nametab
-open Declare
-open Impargs
-open Classops
-open Class
-open Recordops
-open Library
-open Indtypes
-open Nametab
-open Decl_kinds
 
-let recalc_sp dir sp =
-  let (_,spid) = repr_path sp in Libnames.make_path dir spid
+(********************************)
+(* Discharging mutual inductive *)
 
-let recalc_kn dir kn = 
-  let (mp,_,l) = Names.repr_kn kn in
-    Names.make_kn mp dir l
+let detype_param = function
+  | (Name id,None,p) -> id, Entries.LocalAssum p
+  | (Name id,Some p,_) -> id, Entries.LocalDef p
+  | (Anonymous,_,_) -> anomaly"Unnamed inductive local variable"
 
-let rec find_var id = function
-  | [] -> false
-  | (x,b,_)::l -> if x = id then b=None else find_var id l
+(* Replace
 
-let build_abstract_list sec_sp hyps ids_to_discard =
-  let l1,l2 =
-   List.split
-    (List.fold_left
-      (fun vars id ->
-        if find_var id hyps then (mkVar id, Libnames.make_path sec_sp id)::vars
-        else vars)
-      [] ids_to_discard) in
-  Array.of_list l1, l2
+     Var(y1)..Var(yq):C1..Cq |- Ij:Bj
+     Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
 
-(* Discharge of inductives is done here (while discharge of constants 
-   is done by the kernel for efficiency). *)
+   by
 
-let abstract_inductive sec_sp ids_to_abs hyps inds =
-  let abstract_one_assum id t inds =
-    let ntyp = List.length inds in 
-    let new_refs =
-      list_tabulate (fun k -> applist(mkRel (k+2),[mkRel 1])) ntyp in
-    let inds' =
-      List.map
-      	(function (np,tname,arity,cnames,lc) -> 
-	   let arity' = mkNamedProd id t arity in
-	   let lc' =
-	     List.map (fun b -> mkNamedProd id t (substl new_refs b)) lc
-	   in
-           (np,tname,arity',cnames,lc'))
-      	inds
-    in 
-    inds' in
-  let abstract_one_def id c inds =
-    List.map
-      (function (np,tname,arity,cnames,lc) -> 
-	 let arity' = replace_vars [id, c] arity in
-	 let lc' = List.map (replace_vars [id, c]) lc in
-         (np,tname,arity',cnames,lc'))
-      inds in
-  let abstract_once ((hyps,inds,vars) as sofar) id =
-    match hyps with
-      | (hyp,None,t as d)::rest when id = hyp ->
-	  let inds' = abstract_one_assum hyp t inds in 
-	  (rest, inds', (mkVar id, Libnames.make_path sec_sp id)::vars)
-      | (hyp,Some b,t as d)::rest when id = hyp ->
-	  let inds' = abstract_one_def hyp b inds in 
-	  (rest, inds', vars)
-      | _ -> sofar in
-  let (_,inds',vars) =
-    List.fold_left abstract_once (hyps,inds,[]) ids_to_abs in
-  let inds'' =
-    List.map 
-      (fun (nparams,a,arity,c,lc) ->
-	 let nparams' = nparams + (List.length vars) in
-	 let params, short_arity = decompose_prod_n_assum nparams' arity in
-	 let shortlc =
-	   List.map (fun c -> snd (decompose_prod_n_assum nparams' c))lc in
-	 let params' =
-	   List.map 
-	     (function
-		| (Name id,None,p) -> id, Entries.LocalAssum p
-		| (Name id,Some p,_) -> id, Entries.LocalDef p
-		| (Anonymous,_,_) -> anomaly"Unnamed inductive local variable")
-	     params in
-	 { mind_entry_params = params';
-	   mind_entry_typename = a;
-	   mind_entry_arity = short_arity;
-	   mind_entry_consnames = c;
-	   mind_entry_lc = shortlc })
-      inds' in
-  let l1,l2 = List.split vars in
-   (inds'', Array.of_list l1, l2)
+     |- Ij: (y1..yq:C1..Cq)Bj
+     I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
+*)
 
-let process_inductive sec_sp osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
-  assert (Array.length mib.mind_packets > 0);
-  let record = mib.mind_record in 
-  let finite = mib.mind_finite in
+let abstract_inductive hyps nparams inds =
+  let ntyp = List.length inds in 
+  let nhyp = named_context_length hyps in
+  let args = instance_from_named_context (List.rev hyps) in
+  let subs = list_tabulate (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) ntyp in
+  let inds' =
+    List.map
+      (function (tname,arity,cnames,lc) -> 
+	let lc' = List.map (substl subs) lc in
+	let lc'' = List.map (fun b -> Termops.it_mkNamedProd_wo_LetIn b hyps) lc' in
+	let arity' = Termops.it_mkNamedProd_wo_LetIn arity hyps in
+        (tname,arity',cnames,lc''))
+      	inds in
+  let nparams' = nparams + Array.length args in
+(* To be sure to be the same as before, should probably be moved to process_inductive *) 
+  let params' = let (_,arity,_,_) = List.hd inds' in 
+		let (params,_) = decompose_prod_n_assum nparams' arity in
+		  List.map detype_param params
+  in
+  let ind'' = 
+  List.map 
+    (fun (a,arity,c,lc) ->
+      let _, short_arity = decompose_prod_n_assum nparams' arity in
+      let shortlc =
+	List.map (fun c -> snd (decompose_prod_n_assum nparams' c)) lc in
+      { mind_entry_typename = a;
+	mind_entry_arity = short_arity;
+	mind_entry_consnames = c;
+	mind_entry_lc = shortlc })
+    inds'
+  in (params',ind'')
+
+
+let process_inductive sechyps modlist mib =
+  let nparams = mib.mind_nparams in
   let inds = 
     array_map_to_list
       (fun mip ->
-	 let nparams = mip.mind_nparams in
-	 let arity = expmod_type modlist mip.mind_user_arity in
-	 let lc = Array.map (expmod_type modlist) mip.mind_user_lc in
-	 (nparams,
-	  mip.mind_typename,
+	 let arity = expmod_constr modlist mip.mind_user_arity in
+	 let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
+	 (mip.mind_typename,
 	  arity,
 	  Array.to_list mip.mind_consnames,
 	  Array.to_list lc))
-      mib.mind_packets
-  in
-  let hyps = mib.mind_hyps in
-  let hyps' =
-    Sign.fold_named_context
-      (fun (x,b,t) sgn ->
-        Sign.add_named_decl
-          (x, option_app (expmod_constr modlist) b,expmod_constr modlist t)
-          sgn)
-      mib.mind_hyps ~init:empty_named_context in
-  let (inds',abs_vars,discharged_hyps ) =
-   abstract_inductive sec_sp ids_to_discard hyps' inds in
-  let lmodif_one_mind i = 
-    let nbc = Array.length mib.mind_packets.(i).mind_consnames in 
-    (((osecsp,i), DO_ABSTRACT ((nsecsp,i),abs_vars)),
-     list_tabulate
-       (function j -> 
-	  let j' = j + 1 in
-	  (((osecsp,i),j'), DO_ABSTRACT (((nsecsp,i),j'),abs_vars)))
-      nbc)
-  in
-  let indmodifs,cstrmodifs =
-    List.split (list_tabulate lmodif_one_mind mib.mind_ntypes) in 
-  ({ mind_entry_record = record;
-     mind_entry_finite = finite;
-     mind_entry_inds = inds' },
-   indmodifs,
-   List.flatten cstrmodifs,
-   discharged_hyps)
-
-(* Discharge messages. *)
-
-let constant_message id =
-  Options.if_verbose ppnl (pr_id id ++ str " is discharged.")
-
-let inductive_message inds =
-  Options.if_verbose 
-    ppnl
-      (hov 0 
-	 (match inds with
-	    | [] -> assert false
-	    | [ind] ->
-		(pr_id ind.mind_entry_typename ++ str " is discharged.")
-	    | l ->
-		(prlist_with_sep pr_coma 
-		     (fun ind -> pr_id ind.mind_entry_typename) l ++
-		   spc () ++ str "are discharged.")))
-
-(* Discharge operations for the various objects of the environment. *)
-
-type opacity = bool
-
-type discharge_operation = 
-  | Variable of identifier * section_variable_entry * local_kind * 
-      implicits_flags * Dischargedhypsmap.discharged_hyps
-  | Constant of identifier * recipe * global_kind * constant * 
-      implicits_flags * Dischargedhypsmap.discharged_hyps
-  | Inductive of mutual_inductive_entry * implicits_flags *
-      Dischargedhypsmap.discharged_hyps
-  | Class of cl_typ * cl_info_typ
-  | Struc of inductive * (unit -> struc_typ)
-  | Objdef of constant
-  | Coercion of coercion_entry
-  | Require of library_reference
-  | Constraints of Univ.constraints
-
-(* Main function to traverse the library segment and compute the various
-   discharge operations. *)
-
-let process_object oldenv olddir full_olddir newdir  
-(* {dir -> newdir} {sec_sp -> full_olddir, olddir} *)
-  (ops,ids_to_discard,(constl,indl,cstrl as work_alist)) ((sp,kn),lobj) =
-  let tag = object_tag lobj in 
-  match tag with
-    | "VARIABLE" ->
-	let ((id,c,t),cst) = get_variable_with_constraints (basename sp) in
-	(* VARIABLE means local (entry Variable/Hypothesis/Local and are *)
-	(* always discharged *)
-	(Constraints cst :: ops, id :: ids_to_discard, work_alist)
-
-    | "CONSTANT" ->
-	(* CONSTANT means never discharge (though visibility may vary) *)
- 	let kind = constant_kind sp in
-	let kn = Nametab.locate_constant (qualid_of_sp sp) in
-	let lab = label kn in
-	let cb = Environ.lookup_constant kn oldenv in
-	let imp = is_implicit_constant kn in
-	let newkn = recalc_kn newdir kn in
-	let abs_vars,discharged_hyps0 =
-         build_abstract_list full_olddir cb.const_hyps ids_to_discard in
-        (* let's add the new discharged hypothesis to those already discharged*)
-        let discharged_hyps =
-         discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in
-        let mods = [ (kn, DO_ABSTRACT(newkn,abs_vars)) ]
-	in
-	let r = { d_from = cb;
-	          d_modlist = work_alist;
-	          d_abstract = ids_to_discard } in
-	let op = Constant (id_of_label lab,r,kind,newkn,imp,discharged_hyps) in
-        (op :: ops, ids_to_discard, (mods@constl, indl, cstrl))
-  
-    | "INDUCTIVE" ->
-	let kn = Nametab.locate_mind (qualid_of_sp sp) in
-	let mib = Environ.lookup_mind kn oldenv in
-	let newkn = recalc_kn newdir kn in
-	let imp = is_implicit_inductive_definition kn in
-(*	let imp = is_implicit_args (* CHANGE *) in*)
-	let (mie,indmods,cstrmods,discharged_hyps0) = 
-	  process_inductive full_olddir kn newkn oldenv (ids_to_discard,work_alist) mib in
-        (* let's add the new discharged hypothesis to those already discharged*)
-        let discharged_hyps =
-         discharged_hyps0 @ Dischargedhypsmap.get_discharged_hyps sp in
-	((Inductive(mie,imp,discharged_hyps)) :: ops, ids_to_discard,
-	 (constl,indmods@indl,cstrmods@cstrl))
-
-    | "CLASS" -> 
-	let ((cl,clinfo) as x) = outClass lobj in
-	if clinfo.cl_strength = Local then 
-	  (ops,ids_to_discard,work_alist)
-	else
-	  let (y1,y2) = process_class olddir ids_to_discard x in
-          ((Class (y1,y2))::ops, ids_to_discard, work_alist)
-	  
-    | "COERCION" -> 
-	let (_,coeinfo,_,_ as x) = outCoercion lobj in
-	if coercion_strength coeinfo = Local then
-	  (ops,ids_to_discard,work_alist)
-        else
-	  let y = process_coercion olddir ids_to_discard x in
-          ((Coercion y)::ops, ids_to_discard, work_alist)
-                    
-    | "STRUCTURE" ->
-	let ((kn,i),info) = outStruc lobj in
-	let newkn = recalc_kn newdir kn in
-	let strobj () =
-	  let mib = Environ.lookup_mind newkn (Global.env ()) in
-	  { s_CONST = info.s_CONST;
-	    s_PARAM = mib.mind_packets.(0).mind_nparams;
-	    s_PROJ = List.map (option_app (fun kn -> recalc_kn newdir kn)) info.s_PROJ } in
-	((Struc ((newkn,i),strobj))::ops, ids_to_discard, work_alist)
-
-    | "OBJDEF1" -> 
-	let kn = outObjDef1 lobj in
-	let new_kn = recalc_kn newdir kn in
-        ((Objdef new_kn)::ops, ids_to_discard, work_alist)
-
-    | "REQUIRE" -> 
-	let c = out_require lobj in
-	((Require c)::ops, ids_to_discard, work_alist)
-
-    | _ -> (ops,ids_to_discard,work_alist)
-
-let process_item oldenv olddir full_olddir newdir acc = function
-  | (sp,Leaf lobj) -> 
-      process_object oldenv olddir full_olddir newdir  acc (sp,lobj)
-  | (_,_) -> acc
-
-let process_operation = function
-  | Variable (id,expmod_a,stre,imp,discharged_hyps) ->
-      (* Warning:parentheses needed to get a side-effect from with_implicits *)
-      with_implicits imp (redeclare_variable id discharged_hyps)
-        (Lib.cwd(),expmod_a,stre)
-  | Constant (id,r,stre,kn,imp,discharged_hyps) ->
-      with_implicits imp (redeclare_constant id discharged_hyps) (r,stre);
-      constant_message id
-  | Inductive (mie,imp,discharged_hyps) ->
-      let _ = with_implicits imp (redeclare_inductive discharged_hyps) mie in
-      inductive_message mie.mind_entry_inds
-  | Class (y1,y2) ->
-      Lib.add_anonymous_leaf (inClass (y1,y2))
-  | Struc (newsp,strobj) ->
-      Lib.add_anonymous_leaf (inStruc (newsp,strobj ()))
-  | Objdef newsp ->
-      begin try Recordobj.objdef_declare (ConstRef newsp) with _ -> () end
-  | Coercion y -> add_new_coercion y
-  | Require y -> reload_library y
-  | Constraints y -> Global.add_constraints y
-
-let catch_not_found f x =
-  try f x
-  with Not_found ->
-    error ("Something is missing; perhaps a reference to a"^
-    " module required inside the section")
-
-let close_section _ s = 
-  let oldenv = Global.env() in
-  let prefix,decls,fs = close_section false s in
-  let full_olddir, (_,olddir) = prefix in
-  let newdir = fst (split_dirpath olddir) in
-  let (ops,ids,_) = 
-    List.fold_left 
-      (process_item oldenv olddir full_olddir newdir) ([],[],([],[],[])) decls 
-  in
-  let ids = last_section_hyps olddir in
-  Summary.section_unfreeze_summaries fs;
-  catch_not_found (List.iter process_operation) (List.rev ops);
-  Nametab.push_dir (Until 1) full_olddir (DirClosedSection full_olddir)
+      mib.mind_packets in
+  let sechyps' = map_named_context (expmod_constr modlist) sechyps in
+  let (params',inds') = abstract_inductive sechyps' nparams inds in
+  { mind_entry_record = mib.mind_record;
+    mind_entry_finite = mib.mind_finite;
+    mind_entry_params = params';
+    mind_entry_inds = inds' }
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index c80b93ce..dcf88f31 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -6,13 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: discharge.mli,v 1.6.16.1 2004/07/16 19:31:48 herbelin Exp $ i*)
+(*i $Id: discharge.mli 6748 2005-02-18 22:17:50Z herbelin $ i*)
 
-open Names
+open Sign
+open Cooking
+open Declarations
+open Entries
 
-(* This module implements the discharge mechanism. It provides a function to
-   close the last opened section. That function calls [Lib.close_section] and
-   then re-introduce all the discharged versions of the objects that were
-   defined in the section. *)
-
-val close_section : bool -> identifier -> unit
+val process_inductive : 
+  named_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/fhimsg.ml b/toplevel/fhimsg.ml
index b5185cd3..4ef5d5fd 100644
--- a/toplevel/fhimsg.ml
+++ b/toplevel/fhimsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: fhimsg.ml,v 1.19.2.1 2004/07/16 19:31:48 herbelin Exp $ *)
+(* $Id: fhimsg.ml 7837 2006-01-11 09:47:32Z herbelin $ *)
 
 open Pp
 open Util
@@ -231,7 +231,7 @@ let explain_ill_formed_rec_body k ctx err names i vdefs =
   | RecCallInCasePred c ->
       (str "Not allowed recursive call in the type of cases in")
   | NotGuardedForm c ->
-      str "Sub-expression " ++ prterm_env ctx c ++ spc() ++
+      str "Sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++
       str "not in guarded form (should be a constructor, Cases or CoFix)"
 in
   let pvd = P.pr_term k ctx vdefs.(i) in
@@ -278,14 +278,7 @@ let explain_ml_case k ctx mes c ct br brt =
   hov 0 (str "In ML case expression on " ++ pc ++ ws 1 ++ cut () ++
            str "of type" ++  ws 1 ++ pct ++ ws 1 ++ cut () ++ 
            str "which is an inductive predicate." ++ fnl () ++ expln)
-(*
-let explain_cant_find_case_type loc k ctx c =
-  let pe = P.pr_term k ctx c in
-  Ast.user_err_loc
-    (loc,"pretype",
-     hov 3 (str "Cannot infer type of whole Case expression on" ++ 
-	     ws 1 ++ pe))
-*)
+
 let explain_type_error k ctx = function
   | UnboundRel n -> 
       explain_unbound_rel k ctx n
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index 10175e2a..1ab786d1 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: fhimsg.mli,v 1.8.16.1 2004/07/16 19:31:48 herbelin Exp $ i*)
+(*i $Id: fhimsg.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index beb80d03..3fe51b5a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml,v 1.86.2.4 2004/12/03 18:45:53 herbelin Exp $ *)
+(* $Id: himsg.ml 8005 2006-02-07 22:50:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -21,18 +21,20 @@ open Sign
 open Environ
 open Pretype_errors
 open Type_errors
+open Indrec
 open Reduction
 open Cases
 open Logic
 open Printer
-open Ast
 open Rawterm
+open Evd
 
-let quote s = if !Options.v7 then s else h 0 (str "\"" ++ s ++ str "\"")
+let quote s = h 0 (str "\"" ++ s ++ str "\"")
 
-let prterm c = quote (prterm c)
-let prterm_env e c = quote (prterm_env e c)
-let prjudge_env e c = let v,t = prjudge_env e c in (quote v,quote t)
+let pr_lconstr c = quote (pr_lconstr c)
+let pr_lconstr_env e c = quote (pr_lconstr_env e c)
+let pr_lconstr_env_at_top e c = quote (pr_lconstr_env_at_top e c)
+let pr_ljudge_env e c = let v,t = pr_ljudge_env e c in (quote v,quote t)
 
 let nth i =
   let many = match i mod 10 with 1 -> "st" | 2 -> "nd" | _ -> "th" in
@@ -56,20 +58,20 @@ let explain_unbound_var ctx v =
 
 let explain_not_type ctx j =
   let pe = pr_ne_context_of (str"In environment") ctx in
-  let pc,pt = prjudge_env ctx j in
+  let pc,pt = pr_ljudge_env ctx j in
   pe ++ str "the term" ++ brk(1,1) ++ pc ++ spc () ++
   str"has type" ++ spc () ++ pt ++ spc () ++ 
   str"which should be Set, Prop or Type."
 
 let explain_bad_assumption ctx j =
   let pe = pr_ne_context_of (str"In environment") ctx in
-  let pc,pt = prjudge_env ctx j in
+  let pc,pt = pr_ljudge_env ctx j in
   pe ++ str "cannot declare a variable or hypothesis over the term" ++
   brk(1,1) ++ pc ++ spc () ++ str"of type" ++ spc () ++ pt ++ spc () ++
   str "because this term is not a type."
 
 let explain_reference_variables c =
-  let pc = prterm c in
+  let pc = pr_lconstr c in
   str "the constant" ++ spc () ++ pc ++ spc () ++ 
   str "refers to variables which are not in the context"
 
@@ -82,12 +84,11 @@ let rec pr_disjunction pr = function
 let explain_elim_arity ctx ind aritylst c pj okinds = 
   let ctx = make_all_name_different ctx in
   let pi = pr_inductive ctx ind in
-  let pc = prterm_env ctx c in
-  let ppt = prterm_env ctx pj.uj_type in
+  let pc = pr_lconstr_env ctx c in
   let msg = match okinds with
   | Some(kp,ki,explanation) ->
-      let pki = prterm_env ctx ki in
-      let pkp = prterm_env ctx kp in
+      let pki = pr_lconstr_env ctx ki in
+      let pkp = pr_lconstr_env ctx kp in
       let explanation =	match explanation with
 	| NonInformativeToInformative ->
           "proofs can be eliminated only to build proofs"
@@ -106,29 +107,19 @@ let explain_elim_arity ctx ind aritylst c pj okinds =
   hov 0 (
   str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++
   str "in the inductive type " ++ spc() ++ quote pi ++ 
-  (if !Options.v7 then 
-    let pp = prterm_env ctx pj.uj_val in
-    let ppar = pr_disjunction (prterm_env ctx) aritylst in
-    let ppt = prterm_env ctx pj.uj_type in
-    fnl () ++
-    str "The elimination predicate"  ++ brk(1,1) ++ pp ++ spc () ++
-    str "has arity" ++ brk(1,1) ++ ppt ++ fnl () ++
-    str "It should be " ++ brk(1,1)  ++ ppar
-  else
-    let sorts = List.map (fun x -> mkSort (new_sort_in_family x))
+  (let sorts = List.map (fun x -> mkSort (new_sort_in_family x))
       (list_uniquize (List.map (fun ar ->
       family_of_sort (destSort (snd (decompose_prod_assum ar)))) aritylst)) in
-    let ppar = pr_disjunction (prterm_env ctx) sorts in
-    let ppt = prterm_env ctx (snd (decompose_prod_assum pj.uj_type)) in
+    let ppar = pr_disjunction (pr_lconstr_env ctx) sorts in
+    let ppt = pr_lconstr_env ctx (snd (decompose_prod_assum pj.uj_type)) in
     str "," ++ spc() ++ str "the return type has sort" ++ spc() ++ ppt ++ 
     spc () ++ str "while it should be " ++ ppar))
   ++ fnl () ++ msg
-    
-    
+
 let explain_case_not_inductive ctx cj =
   let ctx = make_all_name_different ctx in
-  let pc = prterm_env ctx cj.uj_val in
-  let pct = prterm_env ctx cj.uj_type in
+  let pc = pr_lconstr_env ctx cj.uj_val in
+  let pct = pr_lconstr_env ctx cj.uj_type in
     match kind_of_term cj.uj_type with
       | Evar _ -> 
 	  str "Cannot infer a type for this expression"
@@ -139,26 +130,30 @@ let explain_case_not_inductive ctx cj =
 
 let explain_number_branches ctx cj expn =
   let ctx = make_all_name_different ctx in
-  let pc = prterm_env ctx cj.uj_val in
-  let pct = prterm_env ctx cj.uj_type in
+  let pc = pr_lconstr_env ctx cj.uj_val in
+  let pct = pr_lconstr_env ctx cj.uj_type in
   str "Matching on term" ++ brk(1,1) ++ pc ++ spc ()  ++
   str "of type" ++ brk(1,1) ++ pct ++ spc () ++
   str "expects " ++  int expn ++ str " branches"
 
+let ordinal n =
+  let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+  string_of_int n ^ s
+
 let explain_ill_formed_branch ctx c i actty expty =
   let ctx = make_all_name_different ctx in
-  let pc = prterm_env ctx c in
-  let pa = prterm_env ctx actty in
-  let pe = prterm_env ctx expty in
+  let pc = pr_lconstr_env ctx c in
+  let pa = pr_lconstr_env ctx actty in
+  let pe = pr_lconstr_env ctx expty in
   str "In pattern-matching on term" ++ brk(1,1) ++ pc ++
-  spc () ++ str "the branch "  ++ int (i+1) ++
-  str " has type" ++ brk(1,1) ++ pa  ++ spc () ++ 
+  spc () ++ str "the " ++ str (ordinal (i+1)) ++ str " branch has type" ++
+  brk(1,1) ++ pa ++ spc () ++ 
   str "which should be" ++ brk(1,1) ++ pe
 
 let explain_generalization ctx (name,var) j =
   let pe = pr_ne_context_of (str "In environment") ctx in
-  let pv = prtype_env ctx var in
-  let (pc,pt) = prjudge_env (push_rel_assum (name,var) ctx) j in
+  let pv = pr_ltype_env ctx var in
+  let (pc,pt) = pr_ljudge_env (push_rel_assum (name,var) ctx) j in
   str"Illegal generalization: " ++ pe ++
   str"Cannot generalize" ++ brk(1,1) ++ pv ++ spc () ++
   str"over" ++ brk(1,1) ++ pc ++ str"," ++ spc () ++ 
@@ -167,17 +162,18 @@ let explain_generalization ctx (name,var) j =
 
 let explain_actual_type ctx j pt =
   let pe = pr_ne_context_of (str "In environment") ctx in
-  let (pc,pct) = prjudge_env ctx j in
-  let pt = prterm_env ctx pt in
+  let (pc,pct) = pr_ljudge_env ctx j in
+  let pt = pr_lconstr_env ctx pt in
   pe ++
   str "The term" ++ brk(1,1) ++ pc ++ spc ()  ++
   str "has type"  ++ brk(1,1) ++ pct ++ brk(1,1) ++ 
   str "while it is expected to have type" ++ brk(1,1) ++ pt
 
 let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
+  let ctx = make_all_name_different ctx in
   let randl = Array.to_list randl in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
-  let pr,prt = prjudge_env ctx rator in
+  let pr,prt = pr_ljudge_env ctx rator in
   let term_string1,term_string2 =
     if List.length randl > 1 then
       str "terms", (str"The "++nth n++str" term")
@@ -185,7 +181,7 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
       str "term", str "This term" in
   let appl = prlist_with_sep pr_fnl 
 	       (fun c ->
-		  let pc,pct = prjudge_env ctx c in
+		  let pc,pct = pr_ljudge_env ctx c in
 		  hov 2 (pc ++ spc () ++ str": "  ++ pct)) randl
   in
   str"Illegal application (Type Error): " ++ (* pe ++ *) fnl () ++
@@ -193,19 +189,20 @@ let explain_cant_apply_bad_type ctx (n,exptyp,actualtyp) rator randl =
   str"of type" ++ brk(1,1) ++ prt ++ spc ()  ++
   str"cannot be applied to the " ++ term_string1 ++ fnl () ++ 
   str" " ++ v 0 appl ++ fnl () ++ term_string2 ++ str" has type" ++
-  brk(1,1) ++ prterm_env ctx actualtyp ++ spc () ++
-  str"which should be coercible to" ++ brk(1,1) ++ prterm_env ctx exptyp
+  brk(1,1) ++ pr_lconstr_env ctx actualtyp ++ spc () ++
+  str"which should be coercible to" ++ brk(1,1) ++ pr_lconstr_env ctx exptyp
 
 let explain_cant_apply_not_functional ctx rator randl =
+  let ctx = make_all_name_different ctx in
   let randl = Array.to_list randl in
 (*  let pe = pr_ne_context_of (str"in environment") ctx in*)
-  let pr = prterm_env ctx rator.uj_val in
-  let prt = prterm_env ctx rator.uj_type in
+  let pr = pr_lconstr_env ctx rator.uj_val in
+  let prt = pr_lconstr_env ctx rator.uj_type in
   let term_string = if List.length randl > 1 then "terms" else "term" in
   let appl = prlist_with_sep pr_fnl 
 	       (fun c ->
-		  let pc = prterm_env ctx c.uj_val in
-		  let pct = prterm_env ctx c.uj_type in
+		  let pc = pr_lconstr_env ctx c.uj_val in
+		  let pct = pr_lconstr_env ctx c.uj_type in
 		  hov 2 (pc ++ spc () ++ str": "  ++ pct)) randl
   in
   str"Illegal application (Non-functional construction): " ++ 
@@ -216,14 +213,14 @@ let explain_cant_apply_not_functional ctx rator randl =
   str" " ++ v 0 appl
 
 let explain_unexpected_type ctx actual_type expected_type =
-  let pract = prterm_env ctx actual_type in
-  let prexp = prterm_env ctx expected_type in
+  let pract = pr_lconstr_env ctx actual_type in
+  let prexp = pr_lconstr_env ctx expected_type in
   str"This type is" ++ spc () ++ pract ++ spc () ++ 
   str "but is expected to be" ++
   spc () ++ prexp
 
 let explain_not_product ctx c =
-  let pr = prterm_env ctx c in
+  let pr = pr_lconstr_env ctx c in
   str"The type of this term is a product," ++ spc () ++
   str"but it is casted with type" ++
   brk(1,1) ++ pr
@@ -241,8 +238,9 @@ let explain_ill_formed_rec_body ctx err names i =
   (* Fixpoint guard errors *)
   | NotEnoughAbstractionInFixBody ->
       str "Not enough abstractions in the definition"
-  | RecursionNotOnInductiveType ->
-      str "Recursive definition on a non inductive type"
+  | RecursionNotOnInductiveType c ->
+      str "Recursive definition on" ++ spc() ++ pr_lconstr_env ctx c ++ spc() ++
+      str "which should be an inductive type"
   | RecursionOnIllegalTerm(j,arg,le,lt) ->
       let called =
         match names.(j) with
@@ -262,7 +260,7 @@ let explain_ill_formed_rec_body ctx err names i =
               prlist_with_sep pr_spc (pr_db ctx) lt in
       str "Recursive call to " ++ called ++ spc() ++
       str "has principal argument equal to" ++ spc() ++
-      prterm_env ctx arg ++ fnl() ++ str "instead of " ++ vars
+      pr_lconstr_env ctx arg ++ fnl() ++ str "instead of " ++ vars
 
   | NotEnoughArgumentsForFixCall j ->
       let called =
@@ -273,31 +271,31 @@ let explain_ill_formed_rec_body ctx err names i =
 
   (* CoFixpoint guard errors *)
   | CodomainNotInductiveType c ->
-      str "the codomain is" ++ spc () ++ prterm_env ctx c ++ spc () ++
+      str "the codomain is" ++ spc () ++ pr_lconstr_env ctx c ++ spc () ++
       str "which should be a coinductive type"
   | NestedRecursiveOccurrences ->
       str "nested recursive occurrences"
   | UnguardedRecursiveCall c ->
-      str "unguarded recursive call in" ++ spc() ++ prterm_env ctx c
+      str "unguarded recursive call in" ++ spc() ++ pr_lconstr_env ctx c
   | RecCallInTypeOfAbstraction c ->
       str "recursive call forbidden in the domain of an abstraction:" ++
-      spc() ++ prterm_env ctx c
+      spc() ++ pr_lconstr_env ctx c
   | RecCallInNonRecArgOfConstructor c ->
       str "recursive call on a non-recursive argument of constructor" ++
-      spc() ++ prterm_env ctx c
+      spc() ++ pr_lconstr_env ctx c
   | RecCallInTypeOfDef c ->
       str "recursive call forbidden in the type of a recursive definition" ++
-      spc() ++ prterm_env ctx c
+      spc() ++ pr_lconstr_env ctx c
   | RecCallInCaseFun c ->
-      str "recursive call in a branch of" ++ spc() ++ prterm_env ctx c
+      str "recursive call in a branch of" ++ spc() ++ pr_lconstr_env ctx c
   | RecCallInCaseArg c -> 
       str "recursive call in the argument of cases in" ++ spc() ++
-      prterm_env ctx c
+      pr_lconstr_env ctx c
   | RecCallInCasePred c ->
       str "recursive call in the type of cases in" ++  spc() ++
-      prterm_env ctx c
+      pr_lconstr_env ctx c
   | NotGuardedForm c ->
-      str "sub-expression " ++ prterm_env ctx c ++ spc() ++
+      str "sub-expression " ++ pr_lconstr_env ctx c ++ spc() ++
       str "not in guarded form" ++ spc()++
       str"(should be a constructor, an abstraction, a match, a cofix or a recursive call)"
   in
@@ -307,8 +305,8 @@ let explain_ill_formed_rec_body ctx err names i =
 
 let explain_ill_typed_rec_body ctx i names vdefj vargs =
   let ctx = make_all_name_different ctx in
-  let pvd,pvdt = prjudge_env ctx (vdefj.(i)) in
-  let pv = prterm_env ctx vargs.(i) in
+  let pvd,pvdt = pr_ljudge_env ctx (vdefj.(i)) in
+  let pv = pr_lconstr_env ctx vargs.(i) in
   str"The "  ++
   (if Array.length vdefj = 1 then mt () else int (i+1) ++ str "-th") ++
   str"recursive definition"  ++ spc () ++ pvd ++ spc () ++
@@ -317,19 +315,19 @@ let explain_ill_typed_rec_body ctx i names vdefj vargs =
 (*
 let explain_not_inductive ctx c =
   let ctx = make_all_name_different ctx in
-  let pc = prterm_env ctx c in
+  let pc = pr_lconstr_env ctx c in
   str"The term" ++ brk(1,1) ++ pc ++ spc () ++
   str "is not an inductive definition"
 *)
 let explain_cant_find_case_type ctx c =
   let ctx = make_all_name_different ctx in
-  let pe = prterm_env ctx c in
+  let pe = pr_lconstr_env ctx c in
   hov 3 (str "Cannot infer type of pattern-matching on" ++ ws 1 ++ pe)
 
 let explain_occur_check ctx ev rhs =
   let ctx = make_all_name_different ctx in
   let id = Evd.string_of_existential ev in
-  let pt = prterm_env ctx rhs in
+  let pt = pr_lconstr_env ctx rhs in
   str"Occur check failed: tried to define " ++ str id ++
   str" with term" ++ brk(1,1) ++ pt
 
@@ -342,14 +340,10 @@ let explain_hole_kind env = function
   | BinderType Anonymous ->
       str "a type for this anonymous binder"
   | ImplicitArg (c,(n,ido)) ->
-      if !Options.v7 then
-	str "the " ++ pr_ord n ++
-	str " implicit argument of " ++ Nametab.pr_global_env Idset.empty c
-      else
-	let id = out_some ido in
-	str "an instance for the implicit parameter " ++
-	pr_id id ++ spc () ++ str "of" ++
-	spc () ++ Nametab.pr_global_env Idset.empty c
+      let id = out_some ido in
+      str "an instance for the implicit parameter " ++
+      pr_id id ++ spc () ++ str "of" ++
+      spc () ++ Nametab.pr_global_env Idset.empty c
   | InternalHole ->
       str "a term for an internal placeholder"
   | TomatchTypeParameter (tyi,n) ->
@@ -361,7 +355,7 @@ let explain_not_clean ctx ev t k =
   let ctx = make_all_name_different ctx in
   let c = mkRel (Intset.choose (free_rels t)) in
   let id = Evd.string_of_existential ev in
-  let var = prterm_env ctx c in
+  let var = pr_lconstr_env ctx c in
   str"Tried to define " ++ explain_hole_kind ctx k ++
   str" (" ++ str id ++ str ")" ++ spc() ++
   str"with a term using variable " ++ var ++ spc () ++
@@ -377,18 +371,36 @@ let explain_var_not_found ctx id =
   spc ()  ++ str "in the current" ++ spc ()  ++ str "environment"
 
 let explain_wrong_case_info ctx ind ci =
-  let ctx = make_all_name_different ctx in
-  let pi = prterm (mkInd ind) in
+  let pi = pr_lconstr (mkInd ind) in
   if ci.ci_ind = ind then
     str"Pattern-matching expression on an object of inductive" ++ spc () ++ pi ++
     spc () ++ str"has invalid information"
   else
-    let pc = prterm (mkInd ci.ci_ind) in
+    let pc = pr_lconstr (mkInd ci.ci_ind) in
     str"A term of inductive type" ++ spc () ++ pi ++ spc () ++
     str"was given to a pattern-matching expression on the inductive type" ++
     spc () ++ pc
        
 
+let explain_cannot_unify m n =
+  let pm = pr_lconstr m in 
+  let pn = pr_lconstr n in
+  str"Impossible to unify" ++ brk(1,1)  ++ pm ++ spc ()  ++
+  str"with" ++ brk(1,1)  ++ pn
+
+let explain_refiner_cannot_generalize ty =
+  str "Cannot find a well-typed generalisation of the goal with type : " ++ 
+  pr_lconstr ty
+
+let explain_no_occurrence_found c =
+  str "Found no subterm matching " ++ pr_lconstr c ++ str " in the current goal"
+
+let explain_cannot_unify_binding_type m n =
+  let pm = pr_lconstr m in 
+  let pn = pr_lconstr n in
+  str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ 
+  str "which should be unifiable with" ++ brk(1,1) ++ pn
+
 let explain_type_error ctx err =
   let ctx = make_all_name_different ctx in
   match err with
@@ -445,93 +457,74 @@ let explain_pretype_error ctx err =
       explain_unexpected_type ctx actual expected
   | NotProduct c ->
       explain_not_product ctx c
+  | CannotUnify (m,n) -> explain_cannot_unify m n
+  | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
+  | NoOccurrenceFound c -> explain_no_occurrence_found c
+  | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n
 
 (* Refiner errors *)
 
 let explain_refiner_bad_type arg ty conclty =
   str"refiner was given an argument" ++ brk(1,1) ++ 
-  prterm arg ++ spc () ++
-  str"of type" ++ brk(1,1) ++ prterm ty ++ spc () ++
-  str"instead of" ++ brk(1,1) ++ prterm conclty
+  pr_lconstr arg ++ spc () ++
+  str"of type" ++ brk(1,1) ++ pr_lconstr ty ++ spc () ++
+  str"instead of" ++ brk(1,1) ++ pr_lconstr conclty
 
 let explain_refiner_occur_meta t =
-  str"cannot refine with term" ++ brk(1,1) ++ prterm t ++
+  str"cannot refine with term" ++ brk(1,1) ++ pr_lconstr t ++
   spc () ++ str"because there are metavariables, and it is" ++
   spc () ++ str"neither an application nor a Case"
 
 let explain_refiner_occur_meta_goal t =
-  str"generated subgoal" ++ brk(1,1) ++ prterm t ++
+  str"generated subgoal" ++ brk(1,1) ++ pr_lconstr t ++
   spc () ++ str"has metavariables in it"
 
-let explain_refiner_cannot_applt t harg =
+let explain_refiner_cannot_apply t harg =
   str"in refiner, a term of type " ++ brk(1,1) ++
-  prterm t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
-  prterm harg
-
-let explain_cannot_unify m n =
-  let pm = prterm m in 
-  let pn = prterm n in
-  str"Impossible to unify" ++ brk(1,1)  ++ pm ++ spc ()  ++
-  str"with" ++ brk(1,1)  ++ pn
-
-let explain_cannot_unify_binding_type m n =
-  let pm = prterm m in 
-  let pn = prterm n in
-  str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++ 
-  str "which should be unifiable with" ++ brk(1,1) ++ pn
-
-let explain_refiner_cannot_generalize ty =
-  str "Cannot find a well-typed generalisation of the goal with type : " ++ 
-  prterm ty
+  pr_lconstr t ++ spc () ++ str"could not be applied to" ++ brk(1,1) ++
+  pr_lconstr harg
 
 let explain_refiner_not_well_typed c =
-  str"The term "  ++ prterm c  ++ str" is not well-typed"
+  str"The term "  ++ pr_lconstr c  ++ str" is not well-typed"
 
 let explain_intro_needs_product () =
   str "Introduction tactics needs products"
 
 let explain_does_not_occur_in c hyp =
-  str "The term" ++ spc () ++ prterm c ++ spc () ++ str "does not occur in" ++ 
+  str "The term" ++ spc () ++ pr_lconstr c ++ spc () ++ str "does not occur in" ++ 
   spc () ++ pr_id hyp
 
 let explain_non_linear_proof c =
-  str "cannot refine with term" ++ brk(1,1) ++ prterm c ++
+  str "cannot refine with term" ++ brk(1,1) ++ pr_lconstr c ++
   spc () ++ str"because a metavariable has several occurrences"
 
-let explain_no_occurrence_found c =
-  str "Found no subterm matching " ++ prterm c ++ str " in the current goal"
-
 let explain_refiner_error = function
   | BadType (arg,ty,conclty) -> explain_refiner_bad_type arg ty conclty
   | OccurMeta t -> explain_refiner_occur_meta t
   | OccurMetaGoal t -> explain_refiner_occur_meta_goal t
-  | CannotApply (t,harg) -> explain_refiner_cannot_applt t harg
-  | CannotUnify (m,n) -> explain_cannot_unify m n
-  | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n
-  | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
+  | CannotApply (t,harg) -> explain_refiner_cannot_apply t harg
   | NotWellTyped c -> explain_refiner_not_well_typed c
   | IntroNeedsProduct -> explain_intro_needs_product ()
   | DoesNotOccurIn (c,hyp) -> explain_does_not_occur_in c hyp
   | NonLinearProof c -> explain_non_linear_proof c
-  | NoOccurrenceFound c -> explain_no_occurrence_found c
 
 (* Inductive errors *)
 
 let error_non_strictly_positive env c v  =
-  let pc = prterm_env env c in
-  let pv = prterm_env env v in
+  let pc = pr_lconstr_env env c in
+  let pv = pr_lconstr_env env v in
   str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
   brk(1,1) ++ pc
 
 let error_ill_formed_inductive env c v =
-  let pc = prterm_env env c in
-  let pv = prterm_env env v in
+  let pc = pr_lconstr_env env c in
+  let pv = pr_lconstr_env env v in
   str "Not enough arguments applied to the " ++ pv ++
   str " in" ++ brk(1,1) ++ pc
 
 let error_ill_formed_constructor env c v =
-  let pc = prterm_env env c in
-  let pv = prterm_env env v in
+  let pc = pr_lconstr_env env c in
+  let pv = pr_lconstr_env env v in
   str "The conclusion of" ++ brk(1,1) ++ pc ++ brk(1,1) ++ 
   str "is not valid;" ++ brk(1,1) ++ str "it must be built from " ++ pv
 
@@ -544,9 +537,9 @@ let str_of_nth n =
      | _ -> "th")
 
 let error_bad_ind_parameters env c n v1 v2  =
-  let pc = prterm_env_at_top env c in
-  let pv1 = prterm_env env v1 in
-  let pv2 = prterm_env env v2 in
+  let pc = pr_lconstr_env_at_top env c in
+  let pv1 = pr_lconstr_env env v1 in
+  let pv2 = pr_lconstr_env env v2 in
   str ("The "^(str_of_nth n)^" argument of ") ++ pv2 ++ brk(1,1) ++
   str "must be " ++ pv1 ++ str " in" ++ brk(1,1) ++ pc
 
@@ -583,10 +576,11 @@ let error_bad_induction dep indid kind =
   str "is not allowed"
 
 let error_not_mutual_in_scheme () =
- str "Induction schemes is concerned only with mutually inductive types"
+ str "Induction schemes are concerned only with distinct mutually inductive types"
+
+(* Inductive constructions errors *)
 
 let explain_inductive_error = function
-  (* These are errors related to inductive constructions *)
   | NonPos (env,c,v) -> error_non_strictly_positive env c v
   | NotEnoughArgs (env,c,v) -> error_ill_formed_inductive env c v
   | NotConstructor (env,c,v) -> error_ill_formed_constructor env c v
@@ -596,7 +590,10 @@ let explain_inductive_error = function
   | SameNamesOverlap idl -> error_same_names_overlap idl
   | NotAnArity id -> error_not_an_arity id
   | BadEntry -> error_bad_entry ()
-  (* These are errors related to recursors *)
+
+(* Recursion schemes errors *)
+
+let explain_recursion_scheme_error = function
   | NotAllowedCaseAnalysis (dep,k,i) ->
       error_not_allowed_case_analysis dep k i
   | BadInduction (dep,indid,kind) -> error_bad_induction dep indid kind
@@ -606,7 +603,7 @@ let explain_inductive_error = function
 
 let explain_bad_pattern ctx cstr ty = 
   let ctx = make_all_name_different ctx in
-  let pt = prterm_env ctx ty in
+  let pt = pr_lconstr_env ctx ty in
   let pc = pr_constructor ctx cstr in
   str "Found the constructor " ++ pc ++ brk(1,1) ++ 
   str "while matching a term of type " ++ pt ++ brk(1,1) ++ 
@@ -620,31 +617,38 @@ let explain_bad_constructor ctx cstr ind =
   str "while a constructor of "  ++ pi ++ brk(1,1)  ++
   str "is expected"
 
-let explain_wrong_numarg_of_constructor ctx cstr n =
-  let pc = pr_constructor ctx cstr in
-  str "The constructor " ++ pc ++ str " expects "  ++
-  (if n = 0 then str "no argument." else if n = 1 then str "1 argument."
-   else (int n  ++ str " arguments."))
+let decline_string n s =
+  if n = 0 then "no "^s
+  else if n = 1 then "1 "^s
+  else (string_of_int n^" "^s^"s")
+
+let explain_wrong_numarg_constructor ctx cstr n =
+  str "The constructor " ++ pr_constructor ctx cstr ++ 
+  str " expects "  ++ str (decline_string n "argument")
+
+let explain_wrong_numarg_inductive ctx ind n =
+  str "The inductive type " ++ pr_inductive ctx ind ++ 
+  str " expects "  ++ str (decline_string n "argument")
 
 let explain_wrong_predicate_arity ctx pred nondep_arity dep_arity=
   let ctx = make_all_name_different ctx in
-  let pp = prterm_env ctx pred in
+  let pp = pr_lconstr_env ctx pred in
   str "The elimination predicate " ++ spc () ++ pp ++ fnl () ++
   str "should be of arity"  ++ spc () ++
-  prterm_env ctx nondep_arity  ++ spc () ++ 
+  pr_lconstr_env ctx nondep_arity  ++ spc () ++ 
   str "(for non dependent case) or"  ++
-  spc () ++ prterm_env ctx dep_arity  ++ spc () ++ str "(for dependent case)."
+  spc () ++ pr_lconstr_env ctx dep_arity  ++ spc () ++ str "(for dependent case)."
 
 let explain_needs_inversion ctx x t =
   let ctx = make_all_name_different ctx in
-  let px = prterm_env ctx x in
-  let pt = prterm_env ctx t in
+  let px = pr_lconstr_env ctx x in
+  let pt = pr_lconstr_env ctx t in
   str "Sorry, I need inversion to compile pattern matching of term " ++
   px  ++ str " of type: " ++ pt
 
 let explain_unused_clause env pats =
-  let s = if List.length pats > 1 then "s" else "" in
 (* Without localisation
+  let s = if List.length pats > 1 then "s" else "" in
   (str ("Unused clause with pattern"^s) ++ spc () ++
     hov 0 (prlist_with_sep pr_spc pr_cases_pattern pats) ++ str ")")
 *)
@@ -659,7 +663,7 @@ let explain_cannot_infer_predicate ctx typs =
   let ctx = make_all_name_different ctx in
   let pr_branch (cstr,typ) =
     let cstr,_ = decompose_app cstr in
-    str "For " ++ prterm_env ctx cstr ++ str " : " ++ prterm_env ctx typ
+    str "For " ++ pr_lconstr_env ctx cstr ++ str " : " ++ pr_lconstr_env ctx typ
   in
   str "Unable to unify the types found in the branches:" ++
   spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))
@@ -670,7 +674,9 @@ let explain_pattern_matching_error env = function
   | BadConstructor (c,ind) ->
       explain_bad_constructor env c ind
   | WrongNumargConstructor (c,n) ->
-      explain_wrong_numarg_of_constructor env c n
+      explain_wrong_numarg_constructor env c n
+  | WrongNumargInductive (c,n) ->
+      explain_wrong_numarg_inductive env c n
   | WrongPredicateArity (pred,n,dep) ->
       explain_wrong_predicate_arity env pred n dep
   | NeedsInversion (x,t) ->
@@ -681,3 +687,9 @@ let explain_pattern_matching_error env = function
       explain_non_exhaustive env tms
   | CannotInferPredicate typs ->
       explain_cannot_infer_predicate env typs
+
+let explain_reduction_tactic_error = function
+  | Tacred.InvalidAbstraction (env,c,(env',e)) ->
+      str "The abstracted term" ++ spc() ++ pr_lconstr_env_at_top env c ++ 
+      spc() ++ str "is not well typed." ++ fnl () ++
+      explain_type_error env' e
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 3e7ba575..92fcafb7 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: himsg.mli,v 1.13.14.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: himsg.mli 8003 2006-02-07 22:11:50Z herbelin $ i*)
 
 (*i*)
 open Pp
@@ -15,6 +15,7 @@ open Indtypes
 open Environ
 open Type_errors
 open Pretype_errors
+open Indrec
 open Cases
 open Logic
 (*i*)
@@ -27,7 +28,12 @@ val explain_pretype_error : env -> pretype_error -> std_ppcmds
 
 val explain_inductive_error : inductive_error -> std_ppcmds
 
+val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds
+
 val explain_refiner_error : refiner_error -> std_ppcmds
 
 val explain_pattern_matching_error :
   env -> pattern_matching_error -> std_ppcmds
+
+val explain_reduction_tactic_error :
+  Tacred.reduction_tactic_error -> std_ppcmds
diff --git a/toplevel/line_oriented_parser.ml b/toplevel/line_oriented_parser.ml
index 81221196..77f5198a 100644
--- a/toplevel/line_oriented_parser.ml
+++ b/toplevel/line_oriented_parser.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: line_oriented_parser.ml,v 1.2.16.1 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: line_oriented_parser.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 let line_oriented_channel_to_option stop_string input_channel =
   let count = ref 0 in
diff --git a/toplevel/line_oriented_parser.mli b/toplevel/line_oriented_parser.mli
index 13af0e06..f37472c0 100644
--- a/toplevel/line_oriented_parser.mli
+++ b/toplevel/line_oriented_parser.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: line_oriented_parser.mli,v 1.3.16.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: line_oriented_parser.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 val line_oriented_channel_to_option: string -> in_channel -> int -> char option
 
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 4c554209..92ce6e36 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,120 +6,27 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: metasyntax.ml,v 1.105.2.12 2006/01/04 20:31:16 herbelin Exp $ *)
+(* $Id: metasyntax.ml 7822 2006-01-08 17:14:56Z herbelin $ *)
 
 open Pp
 open Util
 open Names
 open Topconstr
-open Coqast
-open Ast
 open Ppextend
 open Extend
-open Esyntax
 open Libobject
-open Library
 open Summary
 open Constrintern
 open Vernacexpr
 open Pcoq
 open Rawterm
 open Libnames
-
-let interp_global_rawconstr_with_vars vars c =
-  interp_rawconstr_gen false Evd.empty (Global.env()) false (vars,[]) c
-
-(**********************************************************************)
-(* Parsing via ast (used in Zsyntax) *)
-
-(* This updates default parsers for Grammar actions and Syntax *)
-(* patterns by inserting globalization *)
-(* Done here to get parsing/g_*.ml4 non dependent from kernel *)
-let constr_to_ast a =
-  Termast.ast_of_rawconstr (interp_rawconstr Evd.empty (Global.env()) a)
-
-(* This installs default quotations parsers to escape the ast parser *)
-(* "constr" is used by default in quotations found in the ast parser *) 
-let constr_parser_with_glob = Pcoq.map_entry constr_to_ast Constr.constr
-
-let _ = define_ast_quotation true "constr" constr_parser_with_glob
+open Lexer
+open Egrammar
+open Notation
 
 (**********************************************************************)
-(* Globalisation for constr_expr *)
-
-let globalize_ref vars ref =
-  match Constrintern.interp_reference (vars,[]) ref with
-  | RRef (loc,VarRef a) -> Ident (loc,a)
-  | RRef (loc,a) -> Qualid (loc,qualid_of_sp (Nametab.sp_of_global a))
-  | RVar (loc,x) -> Ident (loc,x)
-  | _ -> anomaly "globalize_ref: not a reference"
-
-let globalize_ref_term vars ref =
-  match Constrintern.interp_reference (vars,[]) ref with
-  | RRef (loc,VarRef a) -> CRef (Ident (loc,a))
-  | RRef (loc,a) -> CRef (Qualid (loc,qualid_of_sp (Nametab.sp_of_global a)))
-  | RVar (loc,x) -> CRef (Ident (loc,x))
-  | c -> Constrextern.extern_rawconstr Idset.empty c 
-
-let rec globalize_constr_expr vars = function
-  | CRef ref -> globalize_ref_term vars ref
-  | CAppExpl (_,(p,ref),l) ->
-      let f = 
-	map_constr_expr_with_binders globalize_constr_expr
-	  (fun x e -> e) vars
-      in
-      CAppExpl (dummy_loc,(p,globalize_ref vars ref), List.map f l)
-  | c ->
-      map_constr_expr_with_binders globalize_constr_expr (fun id e -> id::e)
-        vars c
-
-let without_translation f x =
-  let old = Options.do_translate () in
-  let oldv7 = !Options.v7 in
-  Options.make_translate false;
-  try let r = f x in Options.make_translate old; Options.v7:=oldv7; r
-  with e -> Options.make_translate old; Options.v7:=oldv7; raise e
-
-let _ = set_constr_globalizer
-  (fun vars e -> for_grammar (without_translation (globalize_constr_expr vars)) e)
-
-(**********************************************************************)
-(** For old ast printer *)
-
-(* Pretty-printer state summary *)
-let _ = 
-  declare_summary "syntax"
-    { freeze_function = Esyntax.freeze;
-      unfreeze_function = Esyntax.unfreeze;
-      init_function = Esyntax.init;
-      survive_module = false;
-      survive_section = false }
-
-(* Pretty-printing objects = syntax_entry *)
-let cache_syntax (_,ppobj) = Esyntax.add_ppobject ppobj
-
-let subst_syntax (_,subst,ppobj) = 
-  Extend.subst_syntax_command Ast.subst_astpat subst ppobj
-
-let (inPPSyntax,outPPSyntax) =
-  declare_object {(default_object "PPSYNTAX") with
-       open_function = (fun i o -> if i=1 then cache_syntax o);
-       cache_function = cache_syntax;
-       subst_function = subst_syntax;
-       classify_function = (fun (_,o) -> Substitute o);       
-       export_function = (fun x -> Some x) }
-
-(* Syntax extension functions (registered in the environnement) *)
-
-(* Checking the pretty-printing rules against free meta-variables.
- * Note that object are checked before they are added in the environment.
- * Syntax objects in compiled modules are not re-checked. *)
-
-let add_syntax_obj whatfor sel =
-(*  if not !Options.v7_only then*)
-  Lib.add_anonymous_leaf (inPPSyntax (interp_syntax_entry whatfor sel))
-
-(* Tokens *)
+(* Tokens                                                             *)
 
 let cache_token (_,s) = Pcoq.lexer.Token.using ("", s)
 
@@ -134,69 +41,40 @@ let (inToken, outToken) =
 let add_token_obj s = Lib.add_anonymous_leaf (inToken s)
 
 (**********************************************************************)
-(* Grammars (especially Tactic Notation) *)
+(* Tactic Notation                                                    *)
 
 let make_terminal_status = function
   | VTerm s -> Some s
   | VNonTerm _ -> None
 
-let qualified_nterm current_univ = function
-  | NtQual (univ, en) -> (univ, en)
-  | NtShort en -> (current_univ, en)
-
-let rec make_tags = function
-  | VTerm s :: l -> make_tags l
+let rec make_tags lev = function
+  | VTerm s :: l -> make_tags lev l
   | VNonTerm (loc, nt, po) :: l ->
-      let (u,nt) = qualified_nterm "tactic" nt in
-      let (etyp, _) = Egrammar.interp_entry_name u nt in
-      etyp :: make_tags l
+      let (etyp, _) = Egrammar.interp_entry_name lev "tactic" nt in
+      etyp :: make_tags lev l
   | [] -> []
 
-let declare_pprule = function
-  (* Pretty-printing rules only for Grammar (Tactic Notation) *)
-  | Egrammar.TacticGrammar (_,pp) ->
-      let f (s,t,p) =
-        Pptactic.declare_extra_tactic_pprule true s (t,p);
-        Pptactic.declare_extra_tactic_pprule false s (t,p) in
-      List.iter f pp
-  | _ -> ()
+let cache_tactic_notation (_,(pa,pp)) =
+  Egrammar.extend_grammar (Egrammar.TacticGrammar pa);
+  Pptactic.declare_extra_tactic_pprule pp
 
-let cache_grammar (_,a) =
-  Egrammar.extend_grammar a;
-  declare_pprule a
+let subst_tactic_parule subst (key,n,p,(d,tac)) =
+  (key,n,p,(d,Tacinterp.subst_tactic subst tac))
 
-let subst_grammar (_,subst,a) =
-  Egrammar.subst_all_grammar_command subst a
+let subst_tactic_notation (_,subst,(pa,pp)) =
+  (subst_tactic_parule subst pa,pp)
 
-let (inGrammar, outGrammar) =
-  declare_object {(default_object "GRAMMAR") with
-       open_function = (fun i o -> if i=1 then cache_grammar o);
-       cache_function = cache_grammar;
-       subst_function = subst_grammar;
+let (inTacticGrammar, outTacticGrammar) =
+  declare_object {(default_object "TacticGrammar") with
+       open_function = (fun i o -> if i=1 then cache_tactic_notation o);
+       cache_function = cache_tactic_notation;
+       subst_function = subst_tactic_notation;
        classify_function = (fun (_,o) -> Substitute o);
        export_function = (fun x -> Some x)}
 
-(**********************************************************************)
-(* V7 Grammar                                                         *)
-
-open Genarg
-
-let check_entry_type (u,n) =
-  if u = "tactic" or u = "vernac" then error "tactic and vernac not supported";
-  match entry_type (get_univ u) n with
-    | None -> Pcoq.create_entry_if_new (get_univ u) n ConstrArgType
-    | Some (ConstrArgType | IdentArgType | RefArgType) -> ()
-    | _ -> error "Cannot arbitrarily extend non constr/ident/ref entries"
-
-let add_grammar_obj univ entryl =
-  let u = create_univ_if_new univ in
-  let g = interp_grammar_command univ check_entry_type entryl in
-  Lib.add_anonymous_leaf (inGrammar (Egrammar.Grammar g))
-
-(**********************************************************************)
-(* V8 Grammar *)
-
-(* Tactic notations *)
+let cons_production_parameter l = function
+  | VTerm _ -> l
+  | VNonTerm (_,_,ido) -> option_cons ido l
 
 let rec tactic_notation_key = function
   | VTerm id :: _ -> id
@@ -207,41 +85,49 @@ let rec next_key_away key t =
   if Pptactic.exists_extra_tactic_pprule key t then next_key_away (key^"'") t
   else key
 
-let locate_tactic_body dir (s,(s',prods as x),e) =
-  let tags = make_tags prods in
-  let s = if s="" then next_key_away (tactic_notation_key prods) tags else s in
-  (s,x,(dir,e)),(s,tags,(s',List.map make_terminal_status prods))
-
-let add_tactic_grammar g =
-  let dir = Lib.cwd () in
-  let pa,pp = List.split (List.map (locate_tactic_body dir) g) in
-  Lib.add_anonymous_leaf (inGrammar (Egrammar.TacticGrammar (pa,pp)))
-
-(* Printing grammar entries *)
+let add_tactic_notation (n,prods,e) =
+  let tags = make_tags n prods in
+  let key = next_key_away (tactic_notation_key prods) tags in
+  let pprule = (key,tags,(n,List.map make_terminal_status prods)) in
+  let ids = List.fold_left cons_production_parameter [] prods in
+  let tac = Tacinterp.glob_tactic_env ids (Global.env()) e in
+  let parule = (key,n,prods,(Lib.cwd(),tac)) in
+  Lib.add_anonymous_leaf (inTacticGrammar (parule,pprule))
 
-let print_grammar univ entry =
-  if !Options.v7 then
-    let u = get_univ univ in
-    let typ = explicitize_entry (fst u) entry in
-    let te,_,_ = get_constr_entry false typ in
-    Gram.Entry.print te
-  else
-    match entry with
-      | "constr" | "operconstr" | "binder_constr" ->
-	  msgnl (str "Entry constr is");
-	  Gram.Entry.print Pcoq.Constr.constr;
-	  msgnl (str "and lconstr is");
-	  Gram.Entry.print Pcoq.Constr.lconstr;
-	  msgnl (str "where binder_constr is");
-	  Gram.Entry.print Pcoq.Constr.binder_constr;
-	  msgnl (str "and operconstr is");
-	  Gram.Entry.print Pcoq.Constr.operconstr;
-      | "pattern" ->
-	  Gram.Entry.print Pcoq.Constr.pattern
-      | "tactic" -> 
-	  Gram.Entry.print Pcoq.Tactic.simple_tactic
-      | _ -> error "Unknown or unprintable grammar entry"
+(**********************************************************************)
+(* Printing grammar entries                                           *)
+
+let print_grammar univ = function
+  | "constr" | "operconstr" | "binder_constr" ->
+      msgnl (str "Entry constr is");
+      Gram.Entry.print Pcoq.Constr.constr;
+      msgnl (str "and lconstr is");
+      Gram.Entry.print Pcoq.Constr.lconstr;
+      msgnl (str "where binder_constr is");
+      Gram.Entry.print Pcoq.Constr.binder_constr;
+      msgnl (str "and operconstr is");
+      Gram.Entry.print Pcoq.Constr.operconstr;
+  | "pattern" ->
+      Gram.Entry.print Pcoq.Constr.pattern
+  | "tactic" -> 
+      msgnl (str "Entry tactic_expr is");
+      Gram.Entry.print Pcoq.Tactic.tactic_expr;
+      msgnl (str "Entry simple_tactic is");
+      Gram.Entry.print Pcoq.Tactic.simple_tactic;
+  | "vernac" -> 
+      msgnl (str "Entry vernac is");
+      Gram.Entry.print Pcoq.Vernac_.vernac;
+      msgnl (str "Entry command is");
+      Gram.Entry.print Pcoq.Vernac_.command;
+      msgnl (str "Entry syntax is");
+      Gram.Entry.print Pcoq.Vernac_.syntax;
+      msgnl (str "Entry gallina is");
+      Gram.Entry.print Pcoq.Vernac_.gallina;
+      msgnl (str "Entry gallina_ext is");
+      Gram.Entry.print Pcoq.Vernac_.gallina_ext;
+  | _ -> error "Unknown or unprintable grammar entry"
 
+(**********************************************************************)
 (* Parse a format (every terminal starting with a letter or a single
    quote (except a single quote alone) must be quoted) *)
 
@@ -342,12 +228,12 @@ let parse_format (loc,str) =
     Stdpp.raise_with_loc loc e
 
 (***********************)
-(* Analysing notations *)
-
-open Symbols
+(* Analyzing notations *)
 
 type symbol_token = WhiteSpace of int | String of string
 
+(* Decompose the notation string into tokens *)
+
 let split_notation_string str =
   let push_token beg i l =
     if beg = i then l else
@@ -376,6 +262,43 @@ let split_notation_string str =
   in
   loop 0 0
 
+(* Interpret notations with a recursive component *)
+
+let rec find_pattern xl = function
+  | Break n as x :: l, Break n' :: l' when n=n' -> 
+      find_pattern (x::xl) (l,l')
+  | Terminal s as x :: l, Terminal s' :: l' when s = s' -> 
+      find_pattern (x::xl) (l,l')
+  | [NonTerminal x], NonTerminal x' :: l' ->
+      (x,x',xl),l'
+  | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
+      error ("The token "^s^" occurs on one side of \"..\" but not on the other side")
+  | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
+      error ("A break occurs on one side of \"..\" but not on the other side")
+  | ((SProdList _ | NonTerminal _) :: _ | []), _ -> 
+      error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\"")
+
+let rec interp_list_parser hd = function
+  | [] -> [], List.rev hd
+  | NonTerminal id :: tl when id = ldots_var ->
+      let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
+      let yl,tl'' = interp_list_parser [] tl' in
+      (* We remember the second copy of each recursive part variable to *)
+      (* remove it afterwards *)
+      y::yl, SProdList (x,sl) :: tl''
+  | (Terminal _ | Break _) as s :: tl ->
+      if hd = [] then 
+        let yl,tl' = interp_list_parser [] tl in
+        yl, s :: tl'
+      else
+        interp_list_parser (s::hd) tl
+  | NonTerminal _ as x :: tl ->
+      let yl,tl' = interp_list_parser [x] tl in
+      yl, List.rev_append hd tl'
+  | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
+
+(* Find non-terminal tokens of notation *)
+
 let unquote_notation_token s =
   let n = String.length s in
   if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
@@ -410,38 +333,12 @@ let rec raw_analyse_notation_tokens = function
       let (vars,l) = raw_analyse_notation_tokens sl in
       (vars, Break n :: l)
 
-let rec find_pattern xl = function
-  | Break n as x :: l, Break n' :: l' when n=n' -> 
-      find_pattern (x::xl) (l,l')
-  | Terminal s as x :: l, Terminal s' :: l' when s = s' -> 
-      find_pattern (x::xl) (l,l')
-  | [NonTerminal x], NonTerminal x' :: l' ->
-      (x,x',xl),l'
-  | [NonTerminal _], Terminal s :: _ | Terminal s :: _, _ ->
-      error ("The token "^s^" occurs on one side of \"..\" but not on the other side")
-  | [NonTerminal _], Break s :: _ | Break s :: _, _ ->
-      error ("A break occurs on one side of \"..\" but not on the other side")
-  | ((SProdList _ | NonTerminal _) :: _ | []), _ -> 
-      error ("The special symbol \"..\" must occur in a configuration of the form\n\"x symbs .. symbs y\"")
-
-let rec interp_list_parser hd = function
-  | [] -> [], List.rev hd
-  | NonTerminal id :: tl when id = ldots_var ->
-      let ((x,y,sl),tl') = find_pattern [] (hd,tl) in
-      let yl,tl'' = interp_list_parser [] tl' in
-      (* We remember the second copy of each recursive part variable to *)
-      (* remove it afterwards *)
-      y::yl, SProdList (x,sl) :: tl''
-  | (Terminal _ | Break _) as s :: tl ->
-      if hd = [] then 
-        let yl,tl' = interp_list_parser [] tl in
-        yl, s :: tl'
-      else
-        interp_list_parser (s::hd) tl
-  | NonTerminal _ as x :: tl ->
-      let yl,tl' = interp_list_parser [x] tl in
-      yl, List.rev_append hd tl'
-  | SProdList _ :: _ -> anomaly "Unexpected SProdList in interp_list_parser"
+let is_numeral symbs = 
+  match List.filter (function Break _ -> false | _ -> true) symbs with
+  | ([Terminal "-"; Terminal x] | [Terminal x]) ->
+      (try let _ = Bigint.of_string x in true with _ -> false)
+  | _ ->
+      false
 
 let analyse_notation_tokens l =
   let vars,l = raw_analyse_notation_tokens l in
@@ -450,7 +347,8 @@ let analyse_notation_tokens l =
 
 let remove_vars = List.fold_right List.remove_assoc
  
-(* Build the syntax and grammar rules *)
+(**********************************************************************)
+(* Build pretty-printing rules                                        *)
 
 type printing_precedence = int * parenRelation
 type parsing_precedence = int option
@@ -460,15 +358,10 @@ let prec_assoc = function
   | Gramext.LeftA -> (E,L)
   | Gramext.NonA -> (L,L)
 
-(* For old ast printer *)
-let meta_pattern m = Pmeta(m,Tany)
-
-type white_status = Juxtapose | Separate of int | NextIsTerminal
-
 let precedence_of_entry_type from = function
   | ETConstr (NumLevel n,BorderProd (_,None)) -> n, Prec n
-  | ETConstr (NumLevel n,BorderProd (left,Some a)) ->
-      n, let (lp,rp) = prec_assoc a in if left then lp else rp
+  | ETConstr (NumLevel n,BorderProd (b,Some a)) ->
+      n, let (lp,rp) = prec_assoc a in if b=Left then lp else rp
   | ETConstr (NumLevel n,InternalProd) -> n, Prec n
   | ETConstr (NextLevel,_) -> from, L
   | ETOther ("constr","annot") -> 10, Prec 10
@@ -506,57 +399,15 @@ let is_operator s =
    s.[0] = '-' or s.[0] = '/' or s.[0] = '<' or s.[0] = '>' or
    s.[0] = '@' or s.[0] = '\\' or s.[0] = '&' or s.[0] = '~')
 
-type previous_prod_status = NoBreak | CanBreak
-
 let rec is_non_terminal = function
   | NonTerminal _ | SProdList _ -> true
   | _ -> false
 
-let add_break n l = UNP_BRK (n,1) :: l
-
-(* For old ast printer *)
-let make_hunks_ast symbols etyps from =
-  let rec make ws = function
-    | NonTerminal m :: prods ->
-	let _,lp = precedence_of_entry_type from (List.assoc m etyps) in
-	let u = PH (meta_pattern (string_of_id m), None, lp) in
-	if prods <> [] && is_non_terminal (List.hd prods) then
-	  u :: add_break 1 (make CanBreak prods)
-	else
-	  u :: make CanBreak prods
-
-    | Terminal s :: prods when List.exists is_non_terminal prods ->
-	let protect =
-	  is_letter s.[0] ||
-	  (is_non_terminal (List.hd prods) &&
-	    (is_letter (s.[String.length s -1])) ||
-	    (is_digit (s.[String.length s -1]))) in
-	if is_comma s || is_right_bracket s then
-	  RO s :: add_break 0 (make NoBreak prods)
-	else if (is_operator s || is_left_bracket s) && ws = CanBreak then
-	  add_break (if protect then 1 else 0)
-	    (RO (if protect then s^" " else s) :: make CanBreak prods)
-	else
-          if protect then
-            (if ws = CanBreak then add_break 1 else (fun x -> x))
-	    (RO (s^" ") :: make CanBreak prods)
-          else
-	    RO s :: make CanBreak prods
-
-    | Terminal s :: prods ->
-	RO s :: make NoBreak prods
-
-    | Break n :: prods ->
-	add_break n (make NoBreak prods)
-
-    | SProdList _ :: _ ->
-        anomaly "Recursive notations not supported in old syntax"
-
-    | [] -> []
+let add_break n l = UnpCut (PpBrk(n,0)) :: l
 
-  in make NoBreak symbols
+(* Heuristics for building default printing rules *)
 
-let add_break n l = UnpCut (PpBrk(n,0)) :: l
+type previous_prod_status = NoBreak | CanBreak
 
 let make_hunks etyps symbols from =
   let vars,typs = List.split etyps in
@@ -621,6 +472,8 @@ let make_hunks etyps symbols from =
 
   in make NoBreak symbols
 
+(* Build default printing rules from explicit format *)
+
 let error_format () = error "The format does not match the notation"
 
 let rec split_format_at_ldots hd = function
@@ -656,12 +509,12 @@ let read_recursive_format sl fmt =
   let slfmt, fmt = get_head fmt in
   slfmt, get_tail (slfmt, fmt)
 
-let hunks_of_format (from,(vars,typs) as vt) symfmt = 
+let hunks_of_format (from,(vars,typs)) symfmt = 
   let rec aux = function
   | symbs, (UnpTerminal s' as u) :: fmt
       when s' = String.make (String.length s') ' ' ->
       let symbs, l = aux (symbs,fmt) in symbs, u :: l
-  | Terminal s :: symbs, (UnpTerminal s' as u) :: fmt
+  | Terminal s :: symbs, (UnpTerminal s') :: fmt
       when s = unquote_notation_token s' ->
       let symbs, l = aux (symbs,fmt) in symbs, UnpTerminal s :: l
   | NonTerminal s :: symbs, UnpTerminal s' :: fmt when s = id_of_string s' ->
@@ -689,36 +542,31 @@ let hunks_of_format (from,(vars,typs) as vt) symfmt =
   | [], l -> l
   | _ -> error_format ()
 
-let string_of_prec (n,p) =
-  (string_of_int n)^(match p with E -> "E" | L -> "L" | _ -> "")
+(**********************************************************************)
+(* Build parsing rules                                                *)
 
 let assoc_of_type n (_,typ) = precedence_of_entry_type n typ
 
-let string_of_assoc = function
-  | Some(Gramext.RightA) -> "RIGHTA"
-  | Some(Gramext.LeftA) | None -> "LEFTA"
-  | Some(Gramext.NonA) -> "NONA"
-
 let is_not_small_constr = function
     ETConstr _ -> true
   | ETOther("constr","binder_constr") -> true
   | _ -> false
 
-let rec define_keywords = function
+let rec define_keywords_aux = function
     NonTerm(_,Some(_,e)) as n1 :: Term("IDENT",k) :: l
-     when not !Options.v7 && is_not_small_constr e ->
+      when is_not_small_constr e ->
       prerr_endline ("Defining '"^k^"' as keyword");
       Lexer.add_token("",k);
-      n1 :: Term("",k) :: define_keywords l
-  | n :: l -> n :: define_keywords l
+      n1 :: Term("",k) :: define_keywords_aux l
+  | n :: l -> n :: define_keywords_aux l
   | [] -> []
 
 let define_keywords = function
-    Term("IDENT",k)::l when not !Options.v7 ->
+    Term("IDENT",k)::l ->
       prerr_endline ("Defining '"^k^"' as keyword");
       Lexer.add_token("",k);
-      Term("",k) :: define_keywords l
-  | l -> define_keywords l
+      Term("",k) :: define_keywords_aux l
+  | l -> define_keywords_aux l
 
 let make_production etyps symbols =
   let prod =
@@ -728,12 +576,12 @@ let make_production etyps symbols =
 	    let typ = List.assoc m etyps in
 	    NonTerm (typ, Some (m,typ)) :: l
         | Terminal s ->
-	    Term (Extend.terminal s) :: l
+	    Term (terminal s) :: l
         | Break _ ->
             l
         | SProdList (x,sl) ->
             let sl = List.flatten
-              (List.map (function Terminal s -> [Extend.terminal s] 
+              (List.map (function Terminal s -> [terminal s] 
                 | Break _ -> []
                 | _ -> anomaly "Found a non terminal token in recursive notation separator") sl) in
 	    let y = match List.assoc x etyps with
@@ -766,44 +614,8 @@ let recompute_assoc typs =
     | _, Some Gramext.RightA -> Some Gramext.RightA
     | _ -> None
 
-let make_grammar_rule n typs symbols ntn perm =
-  let assoc = recompute_assoc typs in
-  let prod = make_production typs symbols in
-  (n,assoc,ntn,prod, perm)
-
-(* For old ast printer *)
-let metas_of sl =
-  List.fold_right
-    (fun it metatl -> match it with
-      | NonTerminal m -> m::metatl
-      | _ -> metatl)
-    sl []
-
-(* For old ast printer *)
-let make_pattern symbols ast =
-  let env = List.map (fun m -> (string_of_id m,ETast)) (metas_of symbols) in
-  fst (to_pat env ast)
-
-(* For old ast printer *)
-let make_syntax_rule n name symbols typs ast ntn sc =
-  [{syn_id = name;
-    syn_prec = n;
-    syn_astpat = make_pattern symbols ast;
-    syn_hunks =
-      [UNP_SYMBOLIC(sc,ntn,UNP_BOX (PpHOVB 1,make_hunks_ast symbols typs n))]}]
-
-let make_pp_rule (n,typs,symbols,fmt) =
-  match fmt with
-    | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
-    | Some fmt -> 
-	[UnpBox (PpHOVB 0, 
-	 hunks_of_format (n,List.split typs) (symbols,parse_format fmt))]
-
 (**************************************************************************)
-(* Syntax extenstion: common parsing/printing rules and no interpretation *)
-
-(* v7 and translator : prec is for v7 (None if V8Notation), prec8 is for v8 *)
-(* v8 : prec is for v8, prec8 is the same *)
+(* Registration of syntax extensions (parsing/printing, no interpretation)*)
 
 let pr_arg_level from = function
   | (n,L) when n=from -> str "at next level"
@@ -813,66 +625,38 @@ let pr_arg_level from = function
   | (n,_) -> str "Unknown level"
 
 let pr_level ntn (from,args) =
-  let lopen = ntn.[0] = '_' and ropen = ntn.[String.length ntn - 1] = '_' in
-(*
-  let ppassoc, args = match args with
-    | [] -> mt (), []
-    | (nl,lpr)::l when nl=from & fst (list_last l)=from ->
-	let (_,rpr),l = list_sep_last l in
-	match lpr, snd (list_last l) with
-	  | L,E -> Gramext.RightA, l
-	  | E,L -> Gramext.LeftA, l
-	  | L,L -> Gramext.NoneA, l
-	  | _ -> args
-*)
   str "at level " ++ int from ++ spc () ++ str "with arguments" ++ spc() ++
   prlist_with_sep pr_coma (pr_arg_level from) args
 
-(* In v8: prec = Some prec8 is for both parsing and printing *)
-(* In v7 and translator: 
-     prec is for parsing (None if V8Notation), 
-     prec8 for v8 printing (v7 printing is via ast) *)
-let cache_syntax_extension (_,(_,((prec,prec8),ntn,gr,se))) =
+let error_incompatible_level ntn oldprec prec =
+  errorlabstrm ""
+    (str ("Notation "^ntn^" is already defined") ++ spc() ++ 
+    pr_level ntn oldprec ++ 
+    spc() ++ str "while it is now required to be" ++ spc() ++ 
+    pr_level ntn prec)
+
+let cache_one_syntax_extension (prec,ntn,gr,pp) =
   try 
-    let oldprec, oldprec8 = Symbols.level_of_notation ntn in
-    if prec8 <> oldprec8 & (Options.do_translate () or not !Options.v7) then
-      errorlabstrm ""
-	(str ((if Options.do_translate () then "For new syntax, notation "
-	else "Notation ")
-	^ntn^" is already defined") ++ spc() ++ pr_level ntn oldprec8 ++ 
-	spc() ++ str "while it is now required to be" ++ spc() ++ 
-	pr_level ntn prec8)
-    else
-      (* Inconsistent v8 notations but not while translating; forget... *)
-      ();
-    (* V8 notations are consistent (from both translator or v8) *)
-    if prec <> None & !Options.v7 then begin
-      (* Update the V7 parsing rule *)
-      if oldprec <> None & out_some oldprec <> out_some prec then
-	(* None of them is V8Notation and they are different: warn *)
-	Options.if_verbose
-	  warning ("Notation "^ntn^
-	  " was already assigned a different level or sublevels");
-      if oldprec = None or out_some oldprec <> out_some prec then
-        Egrammar.extend_grammar (Egrammar.Notation (out_some prec,out_some gr))
-    end
+    let oldprec = Notation.level_of_notation ntn in
+    if prec <> oldprec then error_incompatible_level ntn oldprec prec
   with Not_found ->
     (* Reserve the notation level *)
-    Symbols.declare_notation_level ntn (prec,prec8);
+    Notation.declare_notation_level ntn prec;
     (* Declare the parsing rule *)
-    option_iter (fun gr -> 
-      Egrammar.extend_grammar (Egrammar.Notation (out_some prec,gr))) gr;
+    Egrammar.extend_grammar (Egrammar.Notation (prec,gr));
     (* Declare the printing rule *)
-    Symbols.declare_notation_printing_rule ntn (se,fst prec8)
+    Notation.declare_notation_printing_rule ntn (pp,fst prec)
+
+let cache_syntax_extension (_,(_,sy_rules)) =
+  List.iter cache_one_syntax_extension sy_rules
 
-let subst_notation_grammar subst x = x
+let subst_parsing_rule subst x = x
 
 let subst_printing_rule subst x = x
 
-let subst_syntax_extension (_,subst,(local,(prec,ntn,gr,se))) =
-  (local,(prec,ntn,
-   option_app (subst_notation_grammar subst) gr,
-   subst_printing_rule subst se))
+let subst_syntax_extension (_,subst,(local,sy)) =
+  (local, List.map (fun (prec,ntn,gr,pp) ->
+     (prec,ntn, subst_parsing_rule subst gr, subst_printing_rule subst pp)) sy)
 
 let classify_syntax_definition (_,(local,_ as o)) =
   if local then Dispose else Substitute o
@@ -888,6 +672,11 @@ let (inSyntaxExtension, outSyntaxExtension) =
        classify_function = classify_syntax_definition;
        export_function = export_syntax_definition}
 
+(**************************************************************************)
+(* Precedences                                                            *)
+
+(* Interpreting user-provided modifiers *)
+
 let interp_modifiers modl =
   let onlyparsing = ref false in
   let rec interp assoc level etyps format = function
@@ -896,23 +685,22 @@ let interp_modifiers modl =
     | SetEntryType (s,typ) :: l ->
 	let id = id_of_string s in
 	if List.mem_assoc id etyps then
-	  error (s^" is already assigned to an entry or constr level")
-	else interp assoc level ((id,typ)::etyps) format l
+	  error (s^" is already assigned to an entry or constr level");
+	interp assoc level ((id,typ)::etyps) format l
     | SetItemLevel ([],n) :: l ->
 	interp assoc level etyps format l
     | SetItemLevel (s::idl,n) :: l ->
 	let id = id_of_string s in
 	if List.mem_assoc id etyps then
-	  error (s^" is already assigned to an entry or constr level")
-	else
-	  let typ = ETConstr (n,()) in
-	  interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l)
+	  error (s^" is already assigned to an entry or constr level");
+	let typ = ETConstr (n,()) in
+	interp assoc level ((id,typ)::etyps) format (SetItemLevel (idl,n)::l)
     | SetLevel n :: l ->
-	if level <> None then error "A level is given more than once"
-	else interp assoc (Some n) etyps format l
+	if level <> None then error "A level is given more than once";
+	interp assoc (Some n) etyps format l
     | SetAssoc a :: l ->
-	if assoc <> None then error "An associativity is given more than once"
-	else interp (Some a) level etyps format l
+	if assoc <> None then error "An associativity is given more than once";
+	interp (Some a) level etyps format l
     | SetOnlyParsing :: l ->
 	onlyparsing := true;
 	interp assoc level etyps format l
@@ -921,21 +709,15 @@ let interp_modifiers modl =
 	interp assoc level etyps (Some s) l
   in interp None None [] None modl
 
-let merge_modifiers a n l =
-  (match a with None -> [] | Some a -> [SetAssoc a]) @
-  (match n with None -> [] | Some n -> [SetLevel n]) @ l
-
-let interp_infix_modifiers modl =
-  let (assoc,level,t,b,fmt) = interp_modifiers modl in
+let check_infix_modifiers modifiers =
+  let (assoc,level,t,b,fmt) = interp_modifiers modifiers in
   if t <> [] then
-    error "explicit entry level or type unexpected in infix notation";
-  (assoc,level,b,fmt)
+    error "explicit entry level or type unexpected in infix notation"
+
+let no_syntax_modifiers modifiers = 
+  modifiers = [] or modifiers = [SetOnlyParsing]
 
-(* 2nd list of types has priority *)
-let rec merge_entry_types etyps' = function
-  | [] -> etyps'
-  | (x,_ as e)::etyps ->
-      e :: merge_entry_types (List.remove_assoc x etyps') etyps
+(* Compute precedences from modifiers (or find default ones) *)
 
 let set_entry_type etyps (x,typ) =
   let typ = try 
@@ -948,7 +730,7 @@ let set_entry_type etyps (x,typ) =
     with Not_found -> ETConstr typ
   in (x,typ)
 
-let check_rule_reversibility l = 
+let check_rule_productivity l = 
   if List.for_all (function NonTerminal _ -> true | _ -> false) l then
     error "A notation must include at least one symbol"
 
@@ -956,17 +738,6 @@ let is_not_printable = function
   | AVar _ -> warning "This notation won't be used for printing as it is bound to a \nsingle variable"; true
   | _ -> false
 
-let find_precedence_v7 lev etyps symbols =
-  (match symbols with
-    | NonTerminal x :: _ ->
-	(try match List.assoc x etyps with
-	  | ETConstr _ ->
-	      error "The level of the leftmost non-terminal cannot be changed"
-	  | _ -> ()
-	with Not_found -> ())
-    | _ -> ());
-  if lev = None then 1 else out_some lev
-
 let find_precedence lev etyps symbols =
   match symbols with
   | NonTerminal x :: _ ->
@@ -1000,7 +771,7 @@ let find_precedence lev etyps symbols =
       out_some lev
 
 let check_curly_brackets_notation_exists () =
-  try let _ = Symbols.level_of_notation "{ _ }" in ()
+  try let _ = Notation.level_of_notation "{ _ }" in ()
   with Not_found -> 
     error "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved"
@@ -1028,95 +799,59 @@ let remove_curly_brackets l =
   | x :: l -> x :: aux false l
   in aux true l
 
-let compute_syntax_data forv7 (df,modifiers) =
+let compute_syntax_data (df,modifiers) =
   let (assoc,n,etyps,onlyparse,fmt) = interp_modifiers modifiers in
   (* Notation defaults to NONA *)
   let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
   let toks = split_notation_string df in
   let (recvars,vars,symbols) = analyse_notation_tokens toks in
   let ntn_for_interp = make_notation_key symbols in
-  let symbols = remove_curly_brackets symbols in
-  let notation = make_notation_key symbols in
-  check_rule_reversibility symbols;
-  let n =
-    if !Options.v7 then find_precedence_v7 n etyps symbols
-    else find_precedence n etyps symbols in
-  let innerlevel = NumLevel (if forv7 then 10 else 200) in
+  let symbols' = remove_curly_brackets symbols in
+  let need_squash = (symbols <> symbols') in
+  let ntn_for_grammar = make_notation_key symbols' in
+  check_rule_productivity symbols';
+  let n = find_precedence n etyps symbols' in
+  let innerlevel = NumLevel 200 in
   let typs =
     find_symbols
-      (NumLevel n,BorderProd(true,assoc))
+      (NumLevel n,BorderProd(Left,assoc))
       (innerlevel,InternalProd)
-      (NumLevel n,BorderProd(false,assoc))
-      symbols in
+      (NumLevel n,BorderProd(Right,assoc))
+      symbols' in
   (* To globalize... *)
   let typs = List.map (set_entry_type etyps) typs in
-  let ppdata = (n,typs,symbols,fmt) in
   let prec = (n,List.map (assoc_of_type n) typs) in
-  ((onlyparse,recvars,vars,
-    ntn_for_interp,notation),prec,ppdata,(Lib.library_dp(),df))
-
-(* Uninterpreted (reserved) notations *)
-let add_syntax_extension local mv mv8 =
-  (* from v7: 
-       if mv8 <> None: tells the translator how to print in v8
-       if mv <> None: tells how to parse and, how to print in v7
-       mv = None = mv8 does not occur   
-     from v8 (mv8 is always None and mv is always Some)
-       mv tells how to parse and print in v8
-  *)
-  let data8 = option_app (compute_syntax_data false) mv8 in
-  let data = option_app (compute_syntax_data !Options.v7) mv in
-  let prec,gram_rule = match data with
-  | None -> None, None (* Case of V8Notation from v7 *)
-  | Some ((_,_,_,_,notation),prec,(n,typs,symbols,_),_) -> 
-      Some prec, Some (make_grammar_rule n typs symbols notation None) in
-  match data, data8 with
-  | None, None -> (* Nothing to do: V8Notation while not translating *) () 
-  | _, Some d | Some d, None ->
-    let ((_,_,_,_,ntn),ppprec,ppdata,_) = d in (* tells how to print *)
-    let ntn' = match data with Some ((_,_,_,_,ntn),_,_,_) -> ntn | _ -> ntn in
-    let pp_rule = make_pp_rule ppdata in
-    Lib.add_anonymous_leaf
-      (inSyntaxExtension (local,((prec,ppprec),ntn',gram_rule,pp_rule)))
+  let sy_data = (ntn_for_grammar,prec,need_squash,(n,typs,symbols',fmt)) in
+  let df' = (Lib.library_dp(),df) in
+  let i_data = (onlyparse,recvars,vars,(ntn_for_interp,df')) in
+  (i_data,sy_data)
 
 (**********************************************************************)
-(* Distfix, Infix, Symbols *)
-
-(* A notation comes with a grammar rule, a pretty-printing rule, an
-   identifiying pattern called notation and an associated scope *)
-let load_notation _ (_,(_,_,ntn,scope,pat,onlyparse,_,_)) =
-  option_iter Symbols.declare_scope scope
-
-let open_notation i (_,(_,oldse,ntn,scope,pat,onlyparse,pp8only,df)) =
-  if i=1 then begin
-    let b,oldpp8only = Symbols.exists_notation_in_scope scope ntn pat in
-    (* Declare the old printer rule and its interpretation *)
-    if (not b or oldpp8only) & oldse <> None then
-      Esyntax.add_ppobject {sc_univ="constr";sc_entries=out_some oldse};
+(* Registration of notations interpretation                            *)
+
+let load_notation _ (_,(_,scope,pat,onlyparse,_)) =
+  option_iter Notation.declare_scope scope
+
+let open_notation i (_,(_,scope,pat,onlyparse,(ntn,df))) =
+  if i=1 & not (Notation.exists_notation_in_scope scope ntn pat) then begin
     (* Declare the interpretation *)
-    if not b then
-      Symbols.declare_notation_interpretation ntn scope pat df pp8only;
-    if oldpp8only & not pp8only then
-      Options.silently 
-	(Symbols.declare_notation_interpretation ntn scope pat df) pp8only;
-    if not b & not onlyparse then
-      Symbols.declare_uninterpretation (NotationRule (scope,ntn)) pat
+    Notation.declare_notation_interpretation ntn scope pat df;
+    (* Declare the uninterpretation *)
+    if not onlyparse then
+      Notation.declare_uninterpretation (NotationRule (scope,ntn)) pat
   end
 
 let cache_notation o =
   load_notation 1 o;
   open_notation 1 o
 
-let subst_notation (_,subst,(lc,oldse,ntn,scope,(metas,pat),b,b',df)) =
-  (lc,option_app
-    (list_smartmap (Extend.subst_syntax_entry Ast.subst_astpat subst)) oldse,
-   ntn,scope,
-   (metas,subst_aconstr subst pat), b, b', df)
+let subst_notation (_,subst,(lc,scope,(metas,pat),b,ndf)) =
+  (lc,scope,(metas,subst_aconstr subst (List.map fst metas) pat),b,ndf)
 
-let classify_notation (_,(local,_,_,_,_,_,_,_ as o)) =
+let classify_notation (_,(local,_,_,_,_ as o)) =
   if local then Dispose else Substitute o
 
-let export_notation (local,_,_,_,_,_,_,_ as o) =
+let export_notation (local,_,_,_,_ as o) =
   if local then None else Some o
 
 let (inNotation, outNotation) =
@@ -1128,37 +863,8 @@ let (inNotation, outNotation) =
        classify_function = classify_notation;
        export_function = export_notation}
 
-(* For old ast printer *)
-let rec reify_meta_ast vars = function
-  | Smetalam (loc,s,body) -> Smetalam (loc,s,reify_meta_ast vars body)
-(*  | Node(loc,"META",[Num (_,n)]) -> Nmeta (loc,create_meta n)*)
-  | Node(loc,"ISEVAR",[]) -> Nmeta (loc,"$_")
-  | Node(loc,op,args) -> Node (loc,op, List.map (reify_meta_ast vars) args)
-  | Slam(loc,Some id,body) when List.mem id vars ->
-      Smetalam (loc,string_of_id id,reify_meta_ast vars body)
-  | Slam(loc,na,body) -> Slam(loc,na,reify_meta_ast vars body)
-  | Nvar (loc,id) when List.mem id vars -> Nmeta (loc,string_of_id id)
-  | Nmeta _ | Id _ | Nvar _ | Str _ | Num _ | Path _ as a -> a
-  | Dynamic _ as a -> (* Hum... what to do here *) a
-
-(* For old ast syntax *)
-let make_old_pp_rule n symbols typs r ntn scope vars =
-  let ast = Termast.ast_of_rawconstr r in
-  let ast = reify_meta_ast vars ast in
-  let scope_name = match scope with Some s -> s | None -> "core_scope" in
-  let rule_name = ntn^"_"^scope_name^"_notation" in
-  make_syntax_rule n rule_name symbols typs ast ntn scope
-
-(* maps positions in v8-notation into positions in v7-notation (used
-   for parsing).
-   For instance  Notation "x < y < z" := .. V8only "y < z < x"
-   yields [1; 2; 0] (y is the second arg in v7; z is 3rd; x is fst) *)
-let mk_permut vars7 vars8 =
-  if vars7=vars8 then None else
-    Some
-      (List.fold_right
-        (fun v8 subs -> list_index v8 vars7 - 1 :: subs)
-        vars8 [])
+(**********************************************************************)
+(* Recovering existing syntax                                         *)
 
 let contract_notation ntn =
   if ntn = "{ _ }" then ntn else
@@ -1173,304 +879,120 @@ let contract_notation ntn =
     else ntn in
   aux ntn 0
 
-let add_notation_in_scope local df c mods omodv8 scope =
-  let ((onlyparse,recs,vars,intnot,notation),prec,(n,typs,symbols,_ as ppdata),df')=
-    compute_syntax_data !Options.v7 (df,mods) in
-  (* Declare the parsing and printing rules if not already done *)
-    (* For both v7 and translate: parsing is as described for v7 in v7 file *)
-    (* For v8: parsing is as described in v8 file *)
-    (* For v7: printing is by the old printer - see below *)
-    (* For translate: printing is as described for v8 in v7 file *)
-    (* For v8: printing is as described in v8 file *)
-    (* In short: parsing does not depend on omodv8 *)
-    (* Printing depends on mv8 if defined, otherwise of mods (scaled by 10) *)
-    (* if in v7, or of mods without scaling if in v8 *)
-  let intnot,ntn,pprecvars,ppvars,ppprec,pp_rule =
-    match omodv8 with
-    | Some mv8 ->
-        let (_,recs8,vars8,intnot8,ntn8),p,d,_ = compute_syntax_data false mv8 in
-        intnot8,ntn8,recs8,vars8,p,make_pp_rule d
-    | None when not !Options.v7 -> 
-        intnot,notation,recs,vars,prec,make_pp_rule ppdata
-    | None ->
-	(* means the rule already exists: recover it *)
-        (* occurs only with V8only flag alone *)
-	try 
-          let ntn = contract_notation notation in
-	  let _, oldprec8 = Symbols.level_of_notation ntn in
-	  let rule,_ = Symbols.find_notation_printing_rule ntn in
-	  notation,ntn,recs,vars,oldprec8,rule
-	with Not_found -> error "No known parsing rule for this notation in V8"
-  in
-  let permut = mk_permut vars ppvars in
-  let gram_rule = make_grammar_rule n typs symbols ntn permut in
-  Lib.add_anonymous_leaf
-    (inSyntaxExtension
-      (local,((Some prec,ppprec),ntn,Some gram_rule,pp_rule)));
-
-  (* Declare interpretation *)
-  let (acvars,ac) = interp_aconstr [] ppvars c in
-  let a = (remove_vars pprecvars acvars,ac) (* For recursive parts *) in
-  let old_pp_rule =
-    (* Used only by v7; disable if contains a recursive pattern *)
-    if onlyparse or pprecvars <> [] or not (!Options.v7) then None
-    else
-      let r = interp_global_rawconstr_with_vars vars c in
-      Some (make_old_pp_rule n symbols typs r intnot scope vars) in
-  let onlyparse = onlyparse or !Options.v7_only or is_not_printable ac in
-  Lib.add_anonymous_leaf
-    (inNotation(local,old_pp_rule,intnot,scope,a,onlyparse,false,df'))
-
-let level_rule (n,p) = if p = E then n else max (n-1) 0
+exception NoSyntaxRule
 
-let recover_syntax ntn = 
+let recover_syntax ntn =
   try 
-    match Symbols.level_of_notation ntn with
-      | (Some prec,_ as pprec) -> 
-	  let rule,_ = Symbols.find_notation_printing_rule ntn in
-	  let gr = Egrammar.recover_notation_grammar ntn prec in
-	  Some (pprec,ntn,Some gr,rule)
-      | None,_ -> None
-  with Not_found -> None
+    let prec = Notation.level_of_notation ntn in
+    let pprule,_ = Notation.find_notation_printing_rule ntn in
+    let gr = Egrammar.recover_notation_grammar ntn prec in
+    (prec,ntn,gr,pprule)
+  with Not_found ->
+    raise NoSyntaxRule
+
+let recover_squash_syntax () = recover_syntax "{ _ }"
 
 let recover_notation_syntax rawntn =
   let ntn = contract_notation rawntn in
-  match recover_syntax ntn with
-    | None -> None
-    | Some gr -> Some (gr,if ntn=rawntn then None else recover_syntax "{ _ }")
-
-let set_data_for_v7_pp recs a vars =
-  if not !Options.v7 then None else
-    if recs=[] then Some (a,vars)
-    else (warning "No recursive notation in v7 syntax";None)
-
-let build_old_pp_rule notation scope symbs (r,vars) =
-  let prec = 
-    try
-      let a,_ = Symbols.level_of_notation (contract_notation notation) in
-      if a = None then raise Not_found else out_some a
-    with Not_found ->
-      error "Parsing rule for this notation has to be previously declared" in
-  let typs = List.map2 
-    (fun id n -> 
-      id,ETConstr (NumLevel (level_rule n),InternalProd)) vars (snd prec) in
-  make_old_pp_rule (fst prec) symbs typs r notation scope vars
-
-let add_notation_interpretation_core local symbs for_old df a scope onlyparse 
-  onlypp gram_data =
-  let notation = make_notation_key symbs in
-  let old_pp_rule = 
-    if !Options.v7 then 
-      option_app (build_old_pp_rule notation scope symbs) for_old
-    else None in
-  option_iter
-    (fun (x,y) ->
-      Lib.add_anonymous_leaf (inSyntaxExtension (local,x));
-      option_iter
-	(fun z -> Lib.add_anonymous_leaf (inSyntaxExtension (local,z))) y)
-    gram_data;
-  Lib.add_anonymous_leaf
-    (inNotation(local,old_pp_rule,notation,scope,a,onlyparse,onlypp,
-     (Lib.library_dp(),df)))
+  let sy_rule = recover_syntax ntn in
+  let need_squash = ntn<>rawntn in
+  if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
 
-let add_notation_interpretation df names c sc =
+(**********************************************************************)
+(* Main entry point for building parsing and printing rules           *)
+ 
+let make_pa_rule (n,typs,symbols,_) ntn =
+  let assoc = recompute_assoc typs in
+  let prod = make_production typs symbols in
+  (n,assoc,ntn,prod)
+
+let make_pp_rule (n,typs,symbols,fmt) =
+  match fmt with
+  | None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
+  | Some fmt -> hunks_of_format (n,List.split typs) (symbols,parse_format fmt)
+
+let make_syntax_rules (ntn,prec,need_squash,sy_data) =
+  let pa_rule = make_pa_rule sy_data ntn in
+  let pp_rule = make_pp_rule sy_data in
+  let sy_rule = (prec,ntn,pa_rule,pp_rule) in
+  (* By construction, the rule for "{ _ }" is declared, but we need to
+     redeclare it because the file where it is declared needs not be open
+     when the current file opens (especially in presence of -nois) *)
+  if need_squash then [sy_rule; recover_squash_syntax ()] else [sy_rule]
+
+(**********************************************************************)
+(* Main functions about notations                                     *)
+
+let add_notation_in_scope local df c mods scope =
+  let (i_data,sy_data) = compute_syntax_data (df,mods) in
+  (* Declare the parsing and printing rules *)
+  let sy_rules = make_syntax_rules sy_data in
+  Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules));
+  (* Declare interpretation *)
+  let (onlyparse,recvars,vars,df') = i_data in
+  let (acvars,ac) = interp_aconstr [] vars c in
+  let a = (remove_vars recvars acvars,ac) (* For recursive parts *) in
+  let onlyparse = onlyparse or is_not_printable ac in
+  Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df'))
+
+let add_notation_interpretation_core local df names c scope onlyparse =
   let (recs,vars,symbs) = analyse_notation_tokens (split_notation_string df) in
-  let gram_data = recover_notation_syntax (make_notation_key symbs) in
-  if gram_data = None then
-    error "Parsing rule for this notation has to be previously declared";
+  (* Redeclare pa/pp rules *)
+  if not (is_numeral symbs) then begin
+    let sy_rules = recover_notation_syntax (make_notation_key symbs) in
+    Lib.add_anonymous_leaf (inSyntaxExtension (local,sy_rules))
+  end;
+  (* Declare interpretation *)
+  let df' = (make_notation_key symbs,(Lib.library_dp(),df)) in
   let (acvars,ac) = interp_aconstr names vars c in
   let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
-  let a_for_old = interp_rawconstr_with_implicits Evd.empty (Global.env()) vars names c in
-  let for_oldpp = set_data_for_v7_pp recs a_for_old vars in
-  let onlyparse = is_not_printable ac in
-  add_notation_interpretation_core false symbs for_oldpp df a sc onlyparse 
-    false gram_data
-
-let add_notation_in_scope_v8only local df c mv8 scope =
-  let (_,recs,vars,intnot,notation),prec,ppdata,df' = compute_syntax_data false (df,mv8) in
-  let pp_rule = make_pp_rule ppdata in
-  Lib.add_anonymous_leaf
-    (inSyntaxExtension(local,((None,prec),notation,None,pp_rule)));
-  (* Declare the interpretation *)
-  let (acvars,ac) = interp_aconstr [] vars c in
-  let a = (remove_vars recs acvars,ac) (* For recursive parts *) in
-  let onlyparse = is_not_printable ac in
-  Lib.add_anonymous_leaf
-    (inNotation(local,None,intnot,scope,a,onlyparse,true,df'))
+  let onlyparse = onlyparse or is_not_printable ac in
+  Lib.add_anonymous_leaf (inNotation(local,scope,a,onlyparse,df'))
 
-let add_notation_v8only local c (df,modifiers) sc =
-  let toks = split_notation_string df in
-  match toks with 
-    | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
-	(* This is a ident to be declared as a rule *)
-        add_notation_in_scope_v8only local df c (SetLevel 0::modifiers) sc
-    | _ ->
-	let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers	in
-	match lev with
-	  | None->
-	      if modifiers <> [] & modifiers <> [SetOnlyParsing] then
-		error "Parsing rule for this notation includes no level"
-	      else
-	        (* Declare only interpretation *)
-		let (recs,vars,symbs) = analyse_notation_tokens toks in
-                let (acvars,ac) = interp_aconstr [] vars c in
-		let onlyparse = modifiers = [SetOnlyParsing] 
-                  or is_not_printable ac in
-                let a = (remove_vars recs acvars,ac) in
-		add_notation_interpretation_core local symbs None df a sc 
-		  onlyparse true None
-	  | Some n ->
-	    (* Declare both syntax and interpretation *)
-	      let mods =
-		if List.for_all (function SetAssoc _ -> false | _ -> true)
-		  modifiers 
-		then SetAssoc Gramext.NonA :: modifiers else modifiers in
-	      add_notation_in_scope_v8only local df c mods sc
-
-let is_quoted_ident x =
-  let x' = unquote_notation_token x in
-  x <> x' & try Lexer.check_ident x'; true with _ -> false
-
-(* v7: dfmod=None; mv8=Some: add only v8 printing rule *)
-(*     dfmod=Some: add v7 parsing rule; mv8=Some: add v8 printing rule *)
-(*     dfmod=Some; mv8=None: same v7-parsing and v8-printing rules *)
-(* v8: dfmod=Some; mv8=None: same v8 parsing and printing rules *)
-let add_notation local c dfmod mv8 sc =
-  match dfmod with
-  | None -> add_notation_v8only local c (out_some mv8) sc
-  | Some (df,modifiers) ->
-  let toks = split_notation_string df in
-  match toks with 
-    | [String x] when (modifiers = [] or modifiers = [SetOnlyParsing]) ->
-	(* This is a ident to be declared as a rule *)
-        add_notation_in_scope local df c (SetLevel 0::modifiers) mv8 sc
-    | _ ->
-	let (assoc,lev,typs,onlyparse,fmt) = interp_modifiers modifiers	in
-	match lev with
-	  | None->
-	      if modifiers <> [] & modifiers <> [SetOnlyParsing] then
-		error "Parsing rule for this notation includes no level"
-	      else
-	        (* Declare only interpretation *)
-		let (recs,vars,symbs) = analyse_notation_tokens toks in
-                let gram_data =
-		  recover_notation_syntax (make_notation_key symbs) in
-		if gram_data <> None then
-                  let (acvars,ac) = interp_aconstr [] vars c in
-                  let a = (remove_vars recs acvars,ac) in
-		  let onlyparse = modifiers = [SetOnlyParsing] 
-                    or is_not_printable ac in
-		  let a_for_old = interp_global_rawconstr_with_vars vars c in
-                  let for_old = set_data_for_v7_pp recs a_for_old vars in
-		  add_notation_interpretation_core local symbs for_old df a
-		    sc onlyparse false gram_data
-                else
-                  add_notation_in_scope local df c modifiers mv8 sc
-	  | Some n ->
-	    (* Declare both syntax and interpretation *)
-	    let assoc = match assoc with None -> Some Gramext.NonA | a -> a in
-            add_notation_in_scope local df c modifiers mv8 sc
-
-(* TODO add boxes information in the expression *)
+(* Notations without interpretation (Reserved Notation) *)
+
+let add_syntax_extension local mv =
+  let (_,sy_data) = compute_syntax_data mv in
+  let sy_rules = make_syntax_rules sy_data in
+  Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
+
+(* Notations with only interpretation *)
+
+let add_notation_interpretation df names c sc =
+  try add_notation_interpretation_core false df names c sc false
+  with NoSyntaxRule ->
+    error "Parsing rule for this notation has to be previously declared"
+
+(* Main entry point *)
+
+let add_notation local c (df,modifiers) sc =
+  if no_syntax_modifiers modifiers then
+    (* No syntax data: try to rely on a previously declared rule *)
+    let onlyparse = modifiers=[SetOnlyParsing] in
+    try add_notation_interpretation_core local df [] c sc onlyparse
+    with NoSyntaxRule ->
+      (* Try to determine a default syntax rule *)
+      add_notation_in_scope local df c modifiers sc
+  else
+    (* Declare both syntax and interpretation *)
+    add_notation_in_scope local df c modifiers sc
+
+(* Infix notations *)
 
 let inject_var x = CRef (Ident (dummy_loc, id_of_string x))
 
-let rec rename x vars n = function
-  | [] ->
-      (vars,[])
-  | String "_"::l ->
-      let (vars,l) = rename x vars (n+1) l in
-      let xn = x^(string_of_int n) in
-      ((inject_var xn)::vars,xn::l)
-  | String y::l ->
-      let (vars,l) = rename x vars n l in (vars,(quote_notation_token y)::l)
-  | WhiteSpace _::l ->
-      rename x vars n l
-
-let translate_distfix assoc df r = 
-  let (vars,l) = rename "x" [] 1 (split_notation_string df) in
-  let df = String.concat " " l in
-  let a = mkAppC (mkRefC r, vars) in
-  let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
-  (assoc,df,a)
-
-let add_distfix local assoc n df r sc =
-  (* "x" cannot clash since r is globalized (included section vars) *)
-  let (vars,l) = rename "x" [] 1 (split_notation_string df) in
-  let df = String.concat " " l in
-  let a = mkAppC (mkRefC r, vars) in
-  let assoc = match assoc with None -> Gramext.LeftA | Some a -> a in
-  add_notation_in_scope local df a [SetAssoc assoc;SetLevel n] None sc
-
-let make_infix_data n assoc modl mv8 =
-  (* Infix defaults to LEFTA in V7 (cf doc) *)
-  let mv = match n with None when !Options.v7 -> SetLevel 1 :: modl | _ -> modl in
-  let mv = match assoc with None when !Options.v7 -> SetAssoc Gramext.LeftA :: mv | _ -> mv in
-  let mv8 = match mv8 with
-      None -> None
-    | Some(s8,mv8) ->
-	if List.for_all (function SetLevel _ -> false | _ -> true) mv8 then
-	  error "Needs a level"
-	else Some (("x "^quote_notation_token s8^" y"),mv8) in
-  mv,mv8
-
-let add_infix local (inf,modl) pr mv8 sc =
-  if inf="" (* Code for V8Infix only *) then
-    let (p8,mv8) = out_some mv8 in
-    let (a8,n8,onlyparse,fmt) = interp_infix_modifiers mv8 in
-    let metas = [inject_var "x"; inject_var "y"] in
-    let a = mkAppC (mkRefC pr,metas) in
-    let df = "x "^(quote_notation_token p8)^" y" in
-    let toks = split_notation_string df in
-    if a8=None & n8=None & fmt=None then
-      (* Declare only interpretation *)
-      let (recs,vars,symbs) = analyse_notation_tokens toks in
-      let (acvars,ac) = interp_aconstr [] vars a in
-      let a' = (remove_vars recs acvars,ac) in
-      let a_for_old = interp_global_rawconstr_with_vars vars a in
-      add_notation_interpretation_core local symbs None df a' sc 
-	onlyparse true None
-    else
-      if n8 = None then error "Needs a level" else
-      let mv8 = match a8 with None -> SetAssoc Gramext.NonA :: mv8 |_ -> mv8 in
-      add_notation_in_scope_v8only local df a mv8 sc
-  else begin
-  let (assoc,n,onlyparse,fmt) = interp_infix_modifiers modl in
+let add_infix local (inf,modifiers) pr sc =
+  check_infix_modifiers modifiers;
   (* check the precedence *)
-  if !Options.v7 & (n<> None & (out_some n < 1 or out_some n > 10)) then
-    errorlabstrm "Metasyntax.infix_grammar_entry"
-      (str"Precedence must be between 1 and 10.");
-  (*
-  if (assoc<>None) & (n<6 or n>9) then
-    errorlabstrm "Vernacentries.infix_grammar_entry"
-      (str"Associativity Precedence must be 6,7,8 or 9.");
-  *)
   let metas = [inject_var "x"; inject_var "y"] in
-  let a = mkAppC (mkRefC pr,metas) in
+  let c = mkAppC (mkRefC pr,metas) in
   let df = "x "^(quote_notation_token inf)^" y" in
-  let toks = split_notation_string df in
-  if not !Options.v7 & n=None & assoc=None then
-    (* En v8, une notation sans information de parsing signifie *)
-    (* de ne déclarer que l'interprétation *)
-    (* Declare only interpretation *)
-    let (recs,vars,symbs) = analyse_notation_tokens toks in
-    let gram_data = recover_notation_syntax (make_notation_key symbs) in
-    if gram_data <> None then 
-      let (acvars,ac) = interp_aconstr [] vars a in
-      let a' = (remove_vars recs acvars,ac) in
-      let a_for_old = interp_global_rawconstr_with_vars vars a in
-      let for_old = set_data_for_v7_pp recs a_for_old vars in
-      add_notation_interpretation_core local symbs for_old df a' sc 
-        onlyparse false gram_data
-    else
-      let mv,mv8 = make_infix_data n assoc modl mv8 in
-      add_notation_in_scope local df a mv mv8 sc
-  else
-    let mv,mv8 = make_infix_data n assoc modl mv8 in
-    add_notation_in_scope local df a mv mv8 sc
-  end
+  add_notation local c (df,modifiers) sc
+
+(**********************************************************************)
+(* Miscellaneous                                                      *)
 
-let standardise_locatable_notation ntn =
+let standardize_locatable_notation ntn =
   let unquote = function
     | String s -> [unquote_notation_token s]
     | _ -> [] in
@@ -1480,17 +1002,19 @@ let standardise_locatable_notation ntn =
   else
     unquote_notation_token ntn
 
-(* Delimiters and classes bound to scopes *)
+(**********************************************************************)
+(* Delimiters and classes bound to scopes                             *)
+
 type scope_command = ScopeDelim of string | ScopeClasses of Classops.cl_typ
 
 let load_scope_command _ (_,(scope,dlm)) =
-  Symbols.declare_scope scope
+  Notation.declare_scope scope
 
 let open_scope_command i (_,(scope,o)) =
   if i=1 then
     match o with
-    | ScopeDelim dlm -> Symbols.declare_delimiters scope dlm
-    | ScopeClasses cl -> Symbols.declare_class_scope scope cl
+    | ScopeDelim dlm -> Notation.declare_delimiters scope dlm
+    | ScopeClasses cl -> Notation.declare_class_scope scope cl
 
 let cache_scope_command o =
   load_scope_command 1 o;
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index be90cd7a..71522567 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: metasyntax.mli,v 1.26.2.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: metasyntax.mli 7732 2005-12-26 13:51:24Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -15,49 +15,44 @@ open Ppextend
 open Extend
 open Tacexpr
 open Vernacexpr
-open Symbols
+open Notation
 open Topconstr
 (*i*)
 
-(* Adding grammar and pretty-printing objects in the environment *)
+val add_token_obj : string -> unit
 
-val add_syntax_obj : string -> raw_syntax_entry list -> unit
+(* Adding a tactic notation in the environment *)
 
-val add_grammar_obj : string -> raw_grammar_entry list -> unit
-val add_token_obj : string -> unit
-val add_tactic_grammar :
-  (string * (string * grammar_production list) * raw_tactic_expr) list -> unit
+val add_tactic_notation : 
+  int * grammar_production list * raw_tactic_expr -> unit
+
+(* Adding a (constr) notation in the environment*)
 
 val add_infix : locality_flag -> (string * syntax_modifier list) ->
-  reference -> (string * syntax_modifier list) option ->
-    scope_name option -> unit
-val add_distfix : locality_flag ->
-  grammar_associativity -> precedence -> string -> reference
-    -> scope_name option -> unit
-val translate_distfix : grammar_associativity -> string -> reference ->
-  Gramext.g_assoc * string * constr_expr
+  reference -> scope_name option -> unit
+
+val add_notation : locality_flag -> constr_expr ->
+  (string * syntax_modifier list) -> scope_name option -> unit
+
+(* Declaring delimiter keys and default scopes *)
 
 val add_delimiters : scope_name -> string -> unit
 val add_class_scope : scope_name -> Classops.cl_typ -> unit
 
-val add_notation : locality_flag -> constr_expr
-  -> (string * syntax_modifier list) option
-  -> (string * syntax_modifier list) option
-      -> scope_name option -> unit
+(* Add only the interpretation of a notation that already has pa/pp rules *)
 
-val add_notation_interpretation : string -> Constrintern.implicits_env
-  -> constr_expr -> scope_name option -> unit
+val add_notation_interpretation : string -> Constrintern.implicits_env ->
+  constr_expr -> scope_name option -> unit
 
-val add_syntax_extension : locality_flag
-  -> (string * syntax_modifier list) option
-  -> (string * syntax_modifier list) option -> unit
+(* Add only the parsing/printing rule of a notation *)
 
-val print_grammar : string -> string -> unit
+val add_syntax_extension : 
+  locality_flag -> (string * syntax_modifier list) -> unit
 
-val merge_modifiers : Gramext.g_assoc option -> int option -> 
-  syntax_modifier list -> syntax_modifier list
+(* Print the Camlp4 state of a grammar *)
+
+val print_grammar : string -> string -> unit
 
-val interp_infix_modifiers : syntax_modifier list ->
-  Gramext.g_assoc option * precedence option * bool * string located option
+(* Removes quotes in a notation *)
 
-val standardise_locatable_notation : string -> string
+val standardize_locatable_notation : string -> string
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index dcf3e307..490765a4 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: minicoq.ml,v 1.28.14.1 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: minicoq.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index 4da23d42..a3b7fc14 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mltop.ml4,v 1.29.2.3 2004/07/17 13:00:15 herbelin Exp $ *)
+(* $Id: mltop.ml4 6692 2005-02-06 13:03:51Z herbelin $ *)
 
 open Util
 open Pp
@@ -109,7 +109,7 @@ let dir_ml_load s =
 	    [Filename.dirname gname]
 	with | Dynlink.Error a ->
           errorlabstrm "Mltop.load_object" [< str (Dynlink.error_message a) >]
-      else () 
+      else ()
     | Native ->
 	errorlabstrm "Mltop.no_load_object"
           [< str"Loading of ML object file forbidden in a native Coq" >]
@@ -137,7 +137,7 @@ let add_path ~unix_path:dir ~coq_root:coq_dirpath =
   if exists_dir dir then
     begin
       add_ml_dir dir;
-      Library.add_load_path_entry (dir,coq_dirpath)
+      Library.add_load_path (dir,coq_dirpath)
     end
   else
     msg_warning [< str ("Cannot open " ^ dir) >]
@@ -160,7 +160,7 @@ let add_rec_path ~unix_path:dir ~coq_root:coq_dirpath =
     let dirs = map_succeed convert_dirs dirs in
     begin
       List.iter (fun lpe -> add_ml_dir (fst lpe)) dirs;
-      List.iter Library.add_load_path_entry dirs
+      List.iter Library.add_load_path dirs
     end
   else
     msg_warning [< str ("Cannot open " ^ dir) >]
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 6ba8cd76..b869f70b 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: mltop.mli,v 1.8.14.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: mltop.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* If there is a toplevel under Coq, it is described by the following 
    record. *)
diff --git a/toplevel/protectedtoplevel.ml b/toplevel/protectedtoplevel.ml
index c748a12d..a9ff3326 100644
--- a/toplevel/protectedtoplevel.ml
+++ b/toplevel/protectedtoplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: protectedtoplevel.ml,v 1.9.10.1 2004/07/16 19:31:49 herbelin Exp $ *)
+(* $Id: protectedtoplevel.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
 
 open Pp
 open Line_oriented_parser
diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli
index b31afbf6..1d4ba9fc 100644
--- a/toplevel/protectedtoplevel.mli
+++ b/toplevel/protectedtoplevel.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: protectedtoplevel.mli,v 1.5.16.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: protectedtoplevel.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3a10c7e5..b24e85da 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: record.ml,v 1.52.2.2 2005/11/29 21:40:53 letouzey Exp $ *)
+(* $Id: record.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
 
 open Pp
 open Util
@@ -20,7 +20,6 @@ open Declarations
 open Entries
 open Declare
 open Nametab
-open Coqast
 open Constrintern
 open Command
 open Inductive
@@ -37,31 +36,14 @@ let interp_decl sigma env = function
   | Vernacexpr.DefExpr((_,id),c,t) ->
       let c = match t with
 	| None -> c
-	| Some t -> mkCastC (c,t)
+	| Some t -> mkCastC (c,DEFAULTcast,t)
       in
-      let j = judgment_of_rawconstr Evd.empty env c in
+      let j = interp_constr_judgment Evd.empty env c in
       (id,Some j.uj_val, j.uj_type)
 
 let typecheck_params_and_fields ps fs =
   let env0 = Global.env () in
-  let env1,newps =
-    List.fold_left
-      (fun (env,newps) d -> match d with
-	| LocalRawAssum ([_,na],(CHole _ as t)) ->
-	    let t = interp_binder Evd.empty env na t in
-	    let d = (na,None,t) in
-	    (push_rel d env, d::newps)
-	| LocalRawAssum (nal,t) ->
-	    let t = interp_type Evd.empty env t in
-	    let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in
-	    let ctx = List.rev ctx in
-	    (push_rel_context ctx env, ctx@newps)
-	| LocalRawDef ((_,na),c) ->
-	    let c = judgment_of_rawconstr Evd.empty env c in
-	    let d = (na, Some c.uj_val, c.uj_type) in
-	    (push_rel d env, d::newps))
-      (env0,[]) ps
-  in
+  let env1,newps = interp_context Evd.empty env0 ps in
   let env2,newfs =
     List.fold_left
       (fun (env,newfs) d ->
@@ -146,19 +128,20 @@ let subst_projection fid l c =
 let declare_projections indsp coers fields =
   let env = Global.env() in
   let (mib,mip) = Global.lookup_inductive indsp in
-  let paramdecls = mip.mind_params_ctxt in
+  let paramdecls = mib.mind_params_ctxt in
   let r = mkInd indsp in
   let rp = applist (r, extended_rel_list 0 paramdecls) in
   let paramargs = extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = Termops.named_hd (Global.env()) r Anonymous in
   let lifted_fields = lift_rel_context 1 fields in
-  let (_,sp_projs,_) =
+  let (_,kinds,sp_projs,_) =
     List.fold_left2
-      (fun (nfi,sp_projs,subst) coe (fi,optci,ti) ->
-	match fi with
-	| Anonymous ->
-	    (nfi-1, None::sp_projs,NoProjection fi::subst)
-	| Name fid ->
+      (fun (nfi,kinds,sp_projs,subst) coe (fi,optci,ti) ->
+	let (sp_projs,subst) =
+	  match fi with
+	  | Anonymous ->
+	      (None::sp_projs,NoProjection fi::subst)
+	  | Name fid ->
             try
               let ccl = subst_projection fid subst ti in
 	      let body = match optci with
@@ -176,32 +159,34 @@ let declare_projections indsp coers fields =
 	        it_mkLambda_or_LetIn (mkLambda (x,rp,body)) paramdecls in
               let projtyp =
                 it_mkProd_or_LetIn (mkProd (x,rp,ccl)) paramdecls in
-	      let (sp,kn) =
+	      let kn =
 	        try
 		  let cie = {
 		    const_entry_body = proj;
                     const_entry_type = Some projtyp;
-                    const_entry_opaque = false } in
-		  let k = (DefinitionEntry cie,IsDefinition) in
-		  let sp = declare_internal_constant fid k in
+                    const_entry_opaque = false;
+		    const_entry_boxed = Options.boxed_definitions() } in
+		  let k = (DefinitionEntry cie,IsDefinition StructureComponent) in
+		  let kn = declare_internal_constant fid k in
 		  Options.if_verbose message (string_of_id fid ^" is defined");
-		  sp
+		  kn
                 with Type_errors.TypeError (ctx,te) ->
                   raise (NotDefinable (BadTypedProj (fid,ctx,te))) in
 	      let refi = ConstRef kn in
 	      let constr_fi = mkConst kn in
 	      if coe then begin
-	        let cl = Class.class_of_ref (IndRef indsp) in
+	        let cl = Class.class_of_global (IndRef indsp) in
 	        Class.try_add_new_coercion_with_source refi Global cl
 	      end;
 	      let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
 	      let constr_fip = applist (constr_fi,proj_args) in
-	      (nfi-1, (Some kn)::sp_projs, Projection constr_fip::subst)
+	      (Some kn::sp_projs, Projection constr_fip::subst)
             with NotDefinable why ->
 	      warning_or_error coe indsp why;
-	      (nfi-1, None::sp_projs,NoProjection fi::subst))
-      (List.length fields,[],[]) coers (List.rev fields)
-  in sp_projs
+	      (None::sp_projs,NoProjection fi::subst) in
+      (nfi-1,(optci=None)::kinds,sp_projs,subst))
+      (List.length fields,[],[],[]) coers (List.rev fields)
+  in (kinds,sp_projs)
 
 (* [fs] corresponds to fields and [ps] to parameters; [coers] is a boolean 
    list telling if the corresponding fields must me declared as coercion *)
@@ -220,18 +205,18 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let ind = applist (mkRel (1+List.length params+List.length fields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let mie_ind =
-    { mind_entry_params = List.map degenerate_decl params;
-      mind_entry_typename = idstruc;
+    { mind_entry_typename = idstruc;
       mind_entry_arity = mkSort s;
       mind_entry_consnames = [idbuild];
       mind_entry_lc = [type_constructor] } in
   let mie =
-    { mind_entry_record = true;
+    { mind_entry_params = List.map degenerate_decl params;
+      mind_entry_record = true;
       mind_entry_finite = true;
       mind_entry_inds = [mie_ind] } in
   let sp = declare_mutual_with_eliminations true mie in
   let rsp = (sp,0) in (* This is ind path of idstruc *)
-  let sp_projs = declare_projections rsp coers fields in
+  let kinds,sp_projs = declare_projections rsp coers fields in
   let build = ConstructRef (rsp,1) in (* This is construct path of idbuild *)
   if is_coe then Class.try_add_new_coercion build Global;
-  Recordops.add_new_struc (rsp,idbuild,nparams,List.rev sp_projs)
+  Recordops.declare_structure(rsp,idbuild,nparams,List.rev kinds,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 8eff2ed5..66282c20 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: record.mli,v 1.16.2.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: record.mli 6743 2005-02-18 22:14:08Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -21,7 +21,7 @@ open Topconstr
    [coers]; it returns the absolute names of projections *)
 
 val declare_projections :
-  inductive -> bool list -> rel_context -> constant option list
+  inductive -> bool list -> rel_context -> bool list * constant option list
 
 val definition_structure :
   lident with_coercion * local_binder list *
diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
deleted file mode 100755
index d2a1e36e..00000000
--- a/toplevel/recordobj.ml
+++ /dev/null
@@ -1,77 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(* $Id: recordobj.ml,v 1.12.2.1 2004/07/16 19:31:49 herbelin Exp $ *)
-
-open Util
-open Pp
-open Names
-open Libnames
-open Nameops
-open Term
-open Instantiate
-open Lib
-open Declare
-open Recordops
-open Classops
-open Nametab
-
-(*****  object definition ******)
- 
-let typ_lams_of t = 
-  let rec aux acc c = match kind_of_term c with
-    | Lambda (x,c1,c2) -> aux (c1::acc) c2
-    | Cast (c,_) -> aux acc c
-    | t -> acc,t
-  in aux [] t
-
-let objdef_err ref =
-  errorlabstrm "object_declare"
-    (pr_id (id_of_global ref) ++
-       str" is not a structure object")
-
-let objdef_declare ref =
-  let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
-  let env = Global.env () in
-  let v = constr_of_reference ref in
-  let vc = match Environ.constant_opt_value env sp with
-    | Some vc -> vc
-    | None -> objdef_err ref in
-  let lt,t = decompose_lam vc in
-  let lt = List.rev (List.map snd lt) in
-  let f,args = match kind_of_term t with
-    | App (f,args) -> f,args 
-    | _ -> objdef_err ref in
-  let { s_PARAM = p; s_PROJ = lpj } = 
-    try (find_structure
-	   (match kind_of_term f with
-              | Construct (indsp,1) -> indsp
-	      | _ -> objdef_err ref))
-    with Not_found -> objdef_err ref in
-  let params, projs =
-    try list_chop p (Array.to_list args)
-    with _ -> objdef_err ref in
-  let lps = 
-    try List.combine lpj projs 
-    with _ -> objdef_err ref in
-  let comp =
-    List.fold_left
-      (fun l (spopt,t) -> (* comp=components *)
-	 match spopt with
-	   | None -> l
-           | Some proji_sp ->
-	       let c, args = decompose_app t in
-	       try (ConstRef proji_sp, reference_of_constr c, args) :: l
-               with Not_found -> l)
-      [] lps in
-  add_anonymous_leaf (inObjDef1 sp);
-  List.iter
-    (fun (refi,c,argj) -> add_new_objdef ((refi,c),v,lt,params,argj))
-    comp
-
-let add_object_hook _ = objdef_declare
diff --git a/toplevel/searchisos.mli b/toplevel/searchisos.mli
index f1ad7d5a..184725b2 100644
--- a/toplevel/searchisos.mli
+++ b/toplevel/searchisos.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: searchisos.mli,v 1.3.16.1 2004/07/16 19:31:49 herbelin Exp $ i*)
+(*i $Id: searchisos.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 val search_in_lib : bool ref
 val type_search : Term.constr -> unit
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 7fa80bcb..a5c2564c 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml,v 1.22.2.2 2004/07/16 20:48:17 herbelin Exp $ *)
+(* $Id: toplevel.ml 6947 2005-04-20 16:18:41Z coq $ *)
 
 open Pp
 open Util
@@ -182,11 +182,44 @@ let make_prompt () =
   with _ -> 
     "Coq < "
 
+(*let build_pending_list l = 
+  let pl = ref ">" in
+  let l' = ref l in
+  let res = 
+    while List.length !l' > 1 do 
+      pl := !pl ^ "|" Names.string_of_id x;
+      l':=List.tl !l'
+    done in
+  let last = try List.hd !l' with _ ->   in
+  "<"^l'
+*)    
+
+(* the coq prompt added to the default one when in emacs mode
+   The prompt contains the current state label [n] (for global
+   backtracking) and the current proof state [p] (for proof
+   backtracking) plus the list of open (nested) proofs (for proof
+   aborting when backtracking). It looks like:
+   
+   "n |lem1|lem2|lem3| p < "
+*)
+let make_emacs_prompt() =
+  let statnum = string_of_int (Lib.current_command_label ()) in
+  let endchar = String.make 1 (Char.chr 249) in
+  let dpth = Pfedit.current_proof_depth() in
+  let pending = Pfedit.get_all_proof_names() in
+  let pendingprompt = 
+    List.fold_left 
+      (fun acc x -> acc ^ (if acc <> "" then "|" else "") ^ Names.string_of_id x)
+      "" pending in
+  let proof_info = if dpth >= 0 then string_of_int dpth else "0" in
+  statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ endchar
+
 (* A buffer to store the current command read on stdin. It is
  * initialized when a vernac command is immediately followed by "\n",
  * or after a Drop. *)
 let top_buffer =
-  let pr() = (make_prompt())^(emacs_str (String.make 1 (Char.chr 249)))
+  let pr() = 
+    make_prompt() ^ Printer.emacs_str (make_emacs_prompt())
   in
   { prompt = pr;
     str = "";
@@ -197,7 +230,7 @@ let top_buffer =
 
 let set_prompt prompt =
   top_buffer.prompt
-  <- (fun () -> (prompt ()) ^ (emacs_str (String.make 1 (Char.chr 249))))
+  <- (fun () -> (prompt ())^(Printer.emacs_str (String.make 1 (Char.chr 249))))
 
 (* Removes and prints the location of the error. The following exceptions
    need not be located. *)
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index 1b6b48d4..f4d2e28a 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: toplevel.mli,v 1.6.10.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: toplevel.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index b00cfffc..354aff0b 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: usage.ml,v 1.15.2.2 2004/09/03 14:35:26 herbelin Exp $ *)
+(* $Id: usage.ml 6053 2004-09-03 14:33:35Z herbelin $ *)
 
 let version () =
   Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 16929d68..97814fd2 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: usage.mli,v 1.5.16.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: usage.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*s Prints the version number on the standard output and exits (with 0). *)
 
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index a5716619..64d77b74 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml,v 1.59.2.3 2004/07/16 20:48:17 herbelin Exp $ *)
+(* $Id: vernac.ml 7744 2005-12-27 09:16:06Z herbelin $ *)
 
 (* Parsing of vernacular. *)
 
@@ -15,10 +15,9 @@ open Lexer
 open Util
 open Options
 open System
-open Coqast
 open Vernacexpr
 open Vernacinterp
-open Ppvernacnew
+open Ppvernac
 
 (* The functions in this module may raise (unexplainable!) exceptions.
    Use the module Coqtoplevel, which catches these exceptions
@@ -57,7 +56,7 @@ let real_error = function
    the file we parse seems a bit risky to me.  B.B.  *)
 
 let open_file_twice_if verbosely fname =
-  let _,longfname = find_file_in_path (Library.get_load_path ()) fname in
+  let _,longfname = find_file_in_path (Library.get_load_paths ()) fname in
   let in_chan = open_in longfname in
   let verb_ch = if verbosely then Some (open_in longfname) else None in
   let po = Pcoq.Gram.parsable (Stream.of_channel in_chan) in
@@ -95,62 +94,18 @@ let parse_phrase (po, verbch) =
 
 let just_parsing = ref false
 let chan_translate = ref stdout
-let last_char = ref '\000'
 
-(* postprocessor to avoid lexical icompatibilities between V7 and V8.
-   Ex: auto.(* comment *)  or  simpl.auto
- *)
 let set_formatter_translator() =
   let ch = !chan_translate in
-  let out s b e =
-    let n = e-b in
-    if n > 0 then begin
-      (match !last_char with
-          '.' -> 
-            (match s.[b] with
-                '('|'a'..'z'|'A'..'Z' -> output ch " " 0 1 
-              | _ -> ())
-        | _ -> ());
-      last_char := s.[e-1]
-    end;
-    output ch s b e
-  in
+  let out s b e = output ch s b e in
   Format.set_formatter_output_functions out (fun () -> flush ch);
   Format.set_max_boxes max_int
 
-let pre_printing = function
-  | VernacSolve (i,tac,deftac) when Options.do_translate () ->
-      (try
-        let (_,env) = Pfedit.get_goal_context i in
-        let t = Options.with_option Options.translate_syntax
-	  (Tacinterp.glob_tactic_env [] env) tac in
-        let pfts = Pfedit.get_pftreestate () in
-        let gls = fst (Refiner.frontier (Tacmach.proof_of_pftreestate pfts)) in
-        Some (env,t,Pfedit.focus(),List.length gls)
-      with UserError _|Stdpp.Exc_located _ -> None)
-  | _ -> None
-
-let post_printing loc (env,t,f,n) = function
-  | VernacSolve (i,_,deftac) ->
-      let loc = unloc loc in
-      set_formatter_translator();
-      let pp = Ppvernacnew.pr_vernac_solve (i,env,t,deftac) ++ sep_end () in
-      (if !translate_file then begin
-	msg (hov 0 (comment (fst loc) ++ pp ++ comment (snd loc - 1)));
-      end
-      else
-	msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ pp)));
-      Format.set_formatter_out_channel stdout
-  | _ -> ()
-
 let pr_new_syntax loc ocom =
   let loc = unloc loc in
   if !translate_file then set_formatter_translator();
   let fs = States.freeze () in
   let com = match ocom with
-    | Some (VernacV7only _) ->
-        Options.v7_only := true;
-        mt()
     | Some VernacNop -> mt()
     | Some com -> pr_vernac com
     | None -> mt() in
@@ -159,8 +114,6 @@ let pr_new_syntax loc ocom =
   else
     msgnl (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
   States.unfreeze fs;
-  Constrintern.set_temporary_implicits_in [];
-  Constrextern.set_temporary_implicits_out [];
   Format.set_formatter_out_channel stdout
 
 let rec vernac_com interpfun (loc,com) =
@@ -174,7 +127,7 @@ let rec vernac_com interpfun (loc,com) =
         (* coqdoc state *)
         let cds = Constrintern.coqdoc_freeze() in
         if !Options.translate_file then begin
-          let _,f = find_file_in_path (Library.get_load_path ())
+          let _,f = find_file_in_path (Library.get_load_paths ())
             (make_suffix fname ".v") in
           chan_translate := open_out (f^"8");
           Pp.comments := []
@@ -203,39 +156,14 @@ let rec vernac_com interpfun (loc,com) =
         msgnl (str"Finished transaction in " ++
                  System.fmt_time_difference tstart tend)
 
-    (* To be interpreted in v7 or translator input only *)
-    | VernacV7only v ->
-        Options.v7_only := true;
-        if !Options.v7 || Options.do_translate() then interp v;
-        Options.v7_only := false
-
-    (* To be interpreted in translator output only *)
-    | VernacV8only v -> 
-        if not !Options.v7 && not (do_translate()) then
-          interp v
-
     | v -> if not !just_parsing then interpfun v
 
   in 
   try
-    Options.v7_only := false;
-    if do_translate () then
-      match pre_printing com with
-          None ->
-            pr_new_syntax loc (Some com);
-            interp com
-        | Some state ->
-            (try
-              interp com;
-              post_printing loc state com
-            with e ->
-              post_printing loc state com;
-              raise e)
-    else
-      interp com
+    if do_translate () then pr_new_syntax loc (Some com);
+    interp com
   with e -> 
     Format.set_formatter_out_channel stdout;
-    Options.v7_only := false;
     raise (DuringCommandInterp (loc, e))
 
 and vernac interpfun input =
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index d8f4b247..4f95376f 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernac.mli,v 1.10.2.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: vernac.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (* Parsing of vernacular. *)
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 1c6ad9a6..7394bd8f 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.ml,v 1.195.2.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: vernacentries.ml 8700 2006-04-11 23:14:15Z courtieu $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -23,6 +23,7 @@ open Proof_trees
 open Constrintern
 open Prettyp
 open Printer
+open Tactic_printer
 open Tacinterp
 open Command
 open Goptions
@@ -32,6 +33,7 @@ open Vernacexpr
 open Decl_kinds
 open Topconstr
 open Pretyping
+open Redexpr
 
 (* Pcoq hooks *)
 
@@ -55,14 +57,13 @@ let set_pcoq_hook f = pcoq := Some f
 let cl_of_qualid = function
   | FunClass -> Classops.CL_FUN
   | SortClass -> Classops.CL_SORT
-  | RefClass r -> Class.class_of_ref (Nametab.global r)
+  | RefClass r -> Class.class_of_global (Nametab.global r)
 
 (*******************)
 (* "Show" commands *)
 
 let show_proof () =
   let pts = get_pftreestate () in
-  let pf = proof_of_pftreestate pts in
   let cursor = cursor_of_pftreestate pts in
   let evc = evc_of_pftreestate pts in
   let (pfterm,meta_types) = extract_open_pftreestate pts in
@@ -70,41 +71,41 @@ let show_proof () =
     prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++
     str"Subgoals" ++ fnl () ++
     prlist (fun (mv,ty) -> Nameops.pr_meta mv ++ str" -> " ++ 
-      prtype ty ++ fnl ())
+      pr_ltype ty ++ fnl ())
       meta_types
-    ++ str"Proof: " ++ prterm (Evarutil.nf_evar evc pfterm))
+    ++ str"Proof: " ++ pr_lconstr (Evarutil.nf_evar evc pfterm))
 
 let show_node () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and cursor = cursor_of_pftreestate pts in
   msgnl (prlist_with_sep pr_spc pr_int (List.rev cursor) ++ fnl () ++
-         prgl (goal_of_proof pf) ++ fnl () ++
+         pr_goal (goal_of_proof pf) ++ fnl () ++
          (match pf.Proof_type.ref with
             | None -> (str"BY <rule>")
             | Some(r,spfl) ->
-		(str"BY " ++ Refiner.pr_rule r ++ fnl () ++
+		(str"BY " ++ pr_rule r ++ fnl () ++
 		 str"  " ++
-		   hov 0 (prlist_with_sep pr_fnl prgl
+		   hov 0 (prlist_with_sep pr_fnl pr_goal
 			    (List.map goal_of_proof spfl)))))
     
 let show_script () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  msgnl (Refiner.print_treescript true evc (Global.named_context()) pf)
+  msgnl (print_treescript true evc (Global.named_context()) pf)
 
 let show_top_evars () =
   let pfts = get_pftreestate () in 
   let gls = top_goal_of_pftreestate pfts in 
   let sigma = project gls in 
-  msg (pr_evars_int 1 (Evd.non_instantiated sigma))
+  msg (pr_evars_int 1 (Evarutil.non_instantiated sigma))
 
 let show_prooftree () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  msg (Refiner.print_proof evc (Global.named_context()) pf)
+  msg (print_proof evc (Global.named_context()) pf)
 
 let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
 
@@ -112,7 +113,7 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
 
 let fresh_id_of_name avoid gl = function
     Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl
-  | Name id   -> id
+  | Name id   -> Tactics.fresh_id avoid id gl
 
 let rec do_renum avoid gl = function
     [] -> mt ()
@@ -121,27 +122,83 @@ let rec do_renum avoid gl = function
       let id = fresh_id_of_name avoid gl n in
       pr_id id ++ spc () ++ do_renum (id :: avoid) gl l
 
+(* Transforms a product term (x1:T1)..(xn:Tn)T into the pair
+   ([(xn,Tn);...;(x1,T1)],T), where T is not a product nor a letin *)
+let decompose_prod_letins = 
+  let rec prodec_rec l c = match kind_of_term c with
+    | Prod (x,t,c) -> prodec_rec ((x,t)::l) c
+    | LetIn (x,b,t,c) -> prodec_rec ((x,t)::l) c
+    | Cast (c,_,_)   -> prodec_rec l c
+    | _              -> l,c
+  in 
+  prodec_rec []
+
 let show_intro all =
   let pf = get_pftreestate() in
   let gl = nth_goal_of_pftreestate 1 pf in
-  let l,_= decompose_prod (strip_outer_cast (pf_concl gl)) in
+  let l,_= decompose_prod_letins (strip_outer_cast (pf_concl gl)) in
   let nl = List.rev_map fst l in
-  if all then
-    msgnl (do_renum [] gl nl)
-  else
-    try 
-      let n = List.hd nl in
-      msgnl (pr_id (fresh_id_of_name [] gl n))
-    with Failure "hd" -> message "" 
+  if all then msgnl (hov 0 (do_renum [] gl nl))
+  else try 
+    let n = List.hd nl in
+    msgnl (pr_id (fresh_id_of_name [] gl n))
+  with Failure "hd" -> message "" 
+
+
+let id_of_name = function 
+  | Names.Anonymous -> id_of_string "x" 
+  | Names.Name x -> x
+
+
+(* Building of match expression *)
+(* From ide/coq.ml *)
+let make_cases s = 
+  let qualified_name = Libnames.qualid_of_string s in
+  let glob_ref = Nametab.locate qualified_name in
+  match glob_ref with
+    | Libnames.IndRef i -> 
+	let {Declarations.mind_nparams = np}
+	    , {Declarations.mind_consnames = carr ; Declarations.mind_nf_lc = tarr } 
+	      = Global.lookup_inductive i in
+	Util.array_fold_right2 
+	  (fun n t l ->  
+	     let (al,_) = Term.decompose_prod t in
+	     let al,_ = Util.list_chop (List.length al - np) al in
+	     let rec rename avoid = function 
+	       | [] -> []
+	       | (n,_)::l -> 
+		   let n' = Termops.next_global_ident_away true (id_of_name n) avoid in
+		   string_of_id n' :: rename (n'::avoid) l in
+	     let al' = rename [] (List.rev al) in
+	     (string_of_id n :: al') :: l)
+	  carr tarr []
+    | _ -> raise Not_found
+
+
+let show_match id = 
+  try
+    let s = string_of_id (snd id) in
+    let patterns = make_cases s in
+    let cases = 
+      List.fold_left 
+	(fun acc x -> 
+	  match x with
+	    | [] -> assert false
+	    | [x] -> "| "^ x  ^ " => \n" ^ acc
+	    | x::l -> 
+		"| (" ^ List.fold_left (fun acc s ->  acc ^ " " ^ s) x l ^ ")" 
+		^ " => \n" ^ acc)
+	"end" patterns in
+    msg (str ("match # with\n" ^ cases))
+  with Not_found -> error "Unknown inductive type"
 
-(********************)
 (* "Print" commands *)
 
 let print_path_entry (s,l) =
   (str s ++ str " " ++ tbrk (0,2) ++ str (string_of_dirpath l))
 
 let print_loadpath () =
-  let l = Library.get_full_load_path () in
+  let l = Library.get_full_load_paths () in
   msgnl (Pp.t (str "Physical path:                                 " ++
 		 tab () ++ str "Logical Path:" ++ fnl () ++ 
 		 prlist_with_sep pr_fnl print_path_entry l))
@@ -190,8 +247,7 @@ let dump_universes s =
 
 let locate_file f =
   try
-    let _,file =
-      System.where_in_path (Library.get_load_path()) f in
+    let _,file = System.where_in_path (Library.get_load_paths ()) f in
     msgnl (str file)
   with Not_found -> 
     msgnl (hov 0 (str"Can't find file" ++ spc () ++ str f ++ spc () ++
@@ -219,13 +275,22 @@ let print_located_library r =
   try msg_found_library (Library.locate_qualified_library qid)
   with e -> msg_notfound_library loc qid e
 
+let print_located_module r = 
+  let (loc,qid) = qualid_of_reference r in
+  let msg =
+    try 
+      let dir = Nametab.full_name_module qid in
+      str "Module " ++ pr_dirpath dir
+    with Not_found ->
+      (if fst (repr_qualid qid) = empty_dirpath then
+	str "No module is referred to by basename "
+      else 
+	str "No module is referred to by name ") ++ pr_qualid qid
+  in msgnl msg  
+
 (**********)
 (* Syntax *)
 
-let vernac_syntax = Metasyntax.add_syntax_obj
-
-let vernac_grammar = Metasyntax.add_grammar_obj
-
 let vernac_syntax_extension = Metasyntax.add_syntax_extension
 
 let vernac_delimiters = Metasyntax.add_delimiters
@@ -233,15 +298,13 @@ let vernac_delimiters = Metasyntax.add_delimiters
 let vernac_bind_scope sc cll = 
   List.iter (fun cl -> Metasyntax.add_class_scope sc (cl_of_qualid cl)) cll
 
-let vernac_open_close_scope = Symbols.open_close_scope
+let vernac_open_close_scope = Notation.open_close_scope
 
 let vernac_arguments_scope qid scl =
-  Symbols.declare_arguments_scope (global qid) scl
+  Notation.declare_arguments_scope (global qid) scl
 
 let vernac_infix = Metasyntax.add_infix
 
-let vernac_distfix = Metasyntax.add_distfix
-
 let vernac_notation = Metasyntax.add_notation
 
 (***********)
@@ -252,7 +315,7 @@ let start_proof_and_print idopt k t hook =
   print_subgoals ();
   if !pcoq <> None then (out_some !pcoq).start_proof ()
 
-let vernac_definition (local,_ as k) id def hook =
+let vernac_definition (local,_,_ as k) id def hook =
   match def with
   | ProveBody (bl,t) ->   (* local binders, typ *)
       if Lib.is_modtype () then
@@ -260,8 +323,7 @@ let vernac_definition (local,_ as k) id def hook =
 	  (str "Proof editing mode not supported in module types")
       else
 	let hook _ _ = () in
-        let kind = if local=Local then IsLocal else IsGlobal DefinitionBody in
-	  start_proof_and_print (Some id) kind (bl,t) hook
+	start_proof_and_print (Some id) (local,DefinitionBody Definition) (bl,t) hook
   | DefineBody (bl,red_option,c,typ_opt) ->
       let red_option = match red_option with
         | None -> None
@@ -278,7 +340,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
   if Lib.is_modtype () then
     errorlabstrm "Vernacentries.StartProof"
       (str "Proof editing mode not supported in module types");
-  start_proof_and_print sopt (IsGlobal (Proof kind)) (bl,t) hook
+  start_proof_and_print sopt (Global, Proof kind) (bl,t) hook
 
 let vernac_end_proof = function
   | Admitted -> admit ()
@@ -293,9 +355,15 @@ let vernac_end_proof = function
      the theories [??] *)
 
 let vernac_exact_proof c =
-  by (Tactics.exact_proof c); 
-  save_named true
-
+  let pfs = top_of_tree (get_pftreestate()) in
+  let pf = proof_of_pftreestate pfs in
+    if (is_leaf_proof pf) then begin
+      by (Tactics.exact_proof c);
+      save_named true end
+    else
+      errorlabstrm "Vernacentries.ExactProof"
+	(str "Command 'Proof ...' can only be used at the beginning of the proof")
+  	
 let vernac_assumption kind l =
   List.iter (fun (is_coe,(idl,c)) -> declare_assumption idl is_coe kind [] c) l
 
@@ -310,107 +378,70 @@ let vernac_scheme = build_scheme
 (**********************)
 (* Modules            *)
 
-let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o = 
+let vernac_import export refl =
+  let import ref = Library.import_module export (qualid_of_reference ref) in
+  List.iter import refl;
+  Lib.add_frozen_state ()
+
+let vernac_declare_module export id binders_ast mty_ast_o = 
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections";
-
-  if not (Lib.is_modtype ()) then
-    error "Declare Module allowed in module types only";
-
-  let constrain_mty = match mty_ast_o with
-      Some (_,true) -> true
-    | _ -> false
-  in
-
-  match mty_ast_o, constrain_mty, mexpr_ast_o with
-    | _, false, None ->  (* no ident, no/soft type *)
-	Declaremods.start_module Modintern.interp_modtype
-	  id binders_ast mty_ast_o;
-	if_verbose message 
-	  ("Interactive Declaration of Module "^ string_of_id id ^" started")
-	  
-    | Some _, true, None           (* no ident, hard type *)
-    | _, false, Some (CMEident _) ->  (* ident, no/soft type *)
-	Declaremods.declare_module 
-	  Modintern.interp_modtype Modintern.interp_modexpr
-	  id binders_ast mty_ast_o mexpr_ast_o;
-	if_verbose message 
-	  ("Module "^ string_of_id id ^" is declared")
-
-    | _, true, Some (CMEident _) -> (* ident, hard type *)
-	error "You cannot declare an equality and a type in module declaration"
-
-    | _, _, Some _ ->    (* not ident *)
-	error "Only simple modules allowed in module declarations"
-
-    | None,true,None -> assert false  (* 1st None ==> false *)
-
-let vernac_define_module id binders_ast mty_ast_o mexpr_ast_o = 
+  let binders_ast = List.map
+   (fun (export,idl,ty) ->
+     if export <> None then
+      error ("Arguments of a functor declaration cannot be exported. " ^
+       "Remove the \"Export\" and \"Import\" keywords from every functor " ^
+       "argument.")
+     else (idl,ty)) binders_ast in
+  Declaremods.declare_module 
+    Modintern.interp_modtype Modintern.interp_modexpr
+     id binders_ast (Some mty_ast_o) None;
+  if_verbose message ("Module "^ string_of_id id ^" is declared");
+  option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+
+let vernac_define_module export id binders_ast mty_ast_o mexpr_ast_o = 
   (* We check the state of the system (in section, in module type)
      and what module information is supplied *)
   if Lib.sections_are_opened () then
     error "Modules and Module Types are not allowed inside sections";
- 
-  if Lib.is_modtype () then
-    error "Module definitions not allowed in module types. Use Declare Module instead";
-
   match mexpr_ast_o with
     | None ->
-	Declaremods.start_module Modintern.interp_modtype
+       let binders_ast,argsexport =
+        List.fold_right
+         (fun (export,idl,ty) (args,argsexport) ->
+           (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+             ([],[]) in
+	Declaremods.start_module Modintern.interp_modtype export
 	  id binders_ast mty_ast_o;
 	if_verbose message 
-	  ("Interactive Module "^ string_of_id id ^" started")
-	  
+	  ("Interactive Module "^ string_of_id id ^" started") ;
+        List.iter
+         (fun (export,id) ->
+           option_iter
+            (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+         ) argsexport
     | Some _ ->
+       let binders_ast = List.map
+        (fun (export,idl,ty) ->
+          if export <> None then
+           error ("Arguments of a functor definition can be imported only if" ^
+                  " the definition is interactive. Remove the \"Export\" and " ^
+                  "\"Import\" keywords from every functor argument.")
+          else (idl,ty)) binders_ast in
 	Declaremods.declare_module 
 	  Modintern.interp_modtype Modintern.interp_modexpr
 	  id binders_ast mty_ast_o mexpr_ast_o;
 	if_verbose message 
-	  ("Module "^ string_of_id id ^" is defined")
-
-(* let vernac_declare_module id binders_ast mty_ast_o mexpr_ast_o =  *)
-(*   (\* We check the state of the system (in section, in module type) *)
-(*      and what module information is supplied *\) *)
-(*   if Lib.sections_are_opened () then *)
-(*     error "Modules and Module Types are not allowed inside sections"; *)
- 
-(*   let constrain_mty = match mty_ast_o with *)
-(*       Some (_,true) -> true *)
-(*     | _ -> false *)
-(*   in *)
-
-(*   match Lib.is_modtype (), mty_ast_o, constrain_mty, mexpr_ast_o with *)
-(*     | _, None, _, None  *)
-(*     | true, Some _, false, None *)
-(*     | false, _, _, None -> *)
-(* 	Declaremods.start_module Modintern.interp_modtype *)
-(* 	  id binders_ast mty_ast_o; *)
-(* 	if_verbose message  *)
-(* 	  ("Interactive Module "^ string_of_id id ^" started") *)
-	  
-(*     | true, Some _, true, None *)
-(*     | true, _, false, Some (CMEident _) *)
-(*     | false, _, _, Some _ -> *)
-(* 	Declaremods.declare_module  *)
-(* 	  Modintern.interp_modtype Modintern.interp_modexpr *)
-(* 	  id binders_ast mty_ast_o mexpr_ast_o; *)
-(* 	if_verbose message  *)
-(* 	  ("Module "^ string_of_id id ^" is defined") *)
-
-(*     | true, _, _, _ -> *)
-(* 	error "Module definition not allowed in a Module Type" *)
-
-let vernac_end_module id =
-  Declaremods.end_module id;
-  if_verbose message 
-    (if Lib.is_modtype () then 
-       "Module "^ string_of_id id ^" is declared"
-     else
-       "Module "^ string_of_id id ^" is defined")
+	  ("Module "^ string_of_id id ^" is defined");
+        option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)])
+         export
 
-  
+let vernac_end_module export id =
+  Declaremods.end_module id;
+  if_verbose message ("Module "^ string_of_id id ^" is defined") ;
+  option_iter (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
 
 
 let vernac_declare_module_type id binders_ast mty_ast_o =
@@ -419,11 +450,28 @@ let vernac_declare_module_type id binders_ast mty_ast_o =
   
   match mty_ast_o with
     | None ->
+       let binders_ast,argsexport =
+        List.fold_right
+         (fun (export,idl,ty) (args,argsexport) ->
+           (idl,ty)::args, List.map (fun (_,i) -> export,i) idl) binders_ast
+             ([],[]) in
 	Declaremods.start_modtype Modintern.interp_modtype id binders_ast;
 	if_verbose message 
-	  ("Interactive Module Type "^ string_of_id id ^" started")
+	  ("Interactive Module Type "^ string_of_id id ^" started");
+        List.iter
+         (fun (export,id) ->
+           option_iter
+            (fun export -> vernac_import export [Ident (dummy_loc,id)]) export
+         ) argsexport
 	  
     | Some base_mty ->
+       let binders_ast = List.map
+        (fun (export,idl,ty) ->
+          if export <> None then
+           error ("Arguments of a functor definition can be imported only if" ^
+                  " the definition is interactive. Remove the \"Export\" " ^
+                  "and \"Import\" keywords from every functor argument.")
+          else (idl,ty)) binders_ast in
 	Declaremods.declare_modtype Modintern.interp_modtype 
 	  id binders_ast base_mty;
 	if_verbose message 
@@ -455,86 +503,26 @@ let vernac_record struc binders sort nameopt cfs =
 
   (* Sections *)
 
-let vernac_begin_section id = let _ = Lib.open_section id in ()
-
-let vernac_end_section id =
-  Discharge.close_section (is_verbose ()) id
-
+let vernac_begin_section = Lib.open_section
+let vernac_end_section = Lib.close_section
 
 let vernac_end_segment id =
   check_no_pending_proofs ();
-  try
-    match Lib.what_is_opened () with
-      | _,Lib.OpenedModule _ -> vernac_end_module id
-      | _,Lib.OpenedModtype _ -> vernac_end_modtype id
-      | _,Lib.OpenedSection _ -> vernac_end_section id
-      | _ -> anomaly "No more opened things"
-  with
-      Not_found -> error "There is nothing to end."
-
-let is_obsolete_module (_,qid) =
-  match repr_qualid qid with
-  | dir, id when dir = empty_dirpath ->
-      (match string_of_id id with
-	| ("Refine" | "Inv" | "Equality" | "EAuto" | "AutoRewrite"
-	  | "EqDecide" | "Xml" |  "Extraction" | "Tauto" | "Setoid_replace"
-          | "Elimdep" 
-	  | "DatatypesSyntax" | "LogicSyntax" | "Logic_TypeSyntax"
-	  | "SpecifSyntax" | "PeanoSyntax" | "TypeSyntax" | "PolyListSyntax")
-	  -> true
-	| _ -> false)
-  | _ -> false
-
-let test_renamed_module (_,qid) =
-  match repr_qualid qid with
-  | dir, id when dir = empty_dirpath ->
-      (match string_of_id id with
-	| "List" -> warning "List has been renamed into MonoList"
-        | "PolyList" -> warning "PolyList has been renamed into List and old List into MonoList"
-        | _ -> ())
-  | _ -> ()
-
+  let o = 
+    try Lib.what_is_opened ()
+    with Not_found -> error "There is nothing to end." in
+  match o with
+    | _,Lib.OpenedModule (export,_,_) -> vernac_end_module export id
+    | _,Lib.OpenedModtype _ -> vernac_end_modtype id
+    | _,Lib.OpenedSection _ -> vernac_end_section id
+    | _ -> anomaly "No more opened things"
+      
 let vernac_require import _ qidl =
   let qidl = List.map qualid_of_reference qidl in
-  try
-    match import with
-      | None -> List.iter Library.read_library qidl
-      | Some b -> Library.require_library None qidl b
-  with e ->
-  (* Compatibility message *)
-    let qidl' = List.filter is_obsolete_module qidl in
-    if qidl' = qidl then
-      List.iter
-	(fun (_,qid) ->
-	  warning ("Module "^(string_of_qualid qid)^
-	  " is now built-in and shouldn't be required")) qidl
-    else
-      (if not !Options.v7 then List.iter test_renamed_module qidl;
-       raise e)
-      
-let vernac_import export refl =
-  let import_one ref = 
-    let qid = qualid_of_reference ref in
-      Library.import_library export qid
-  in
-    List.iter import_one refl;
-    Lib.add_frozen_state ()
-
-(*  else
-    let import (loc,qid) = 
-      try
-	let mp = Nametab.locate_module qid in
-	  Declaremods.import_module mp
-      with Not_found ->
-	user_err_loc
-        (loc,"vernac_import",
-	 str ((string_of_qualid qid)^" is not a module"))
-    in
-      List.iter import qidl;
-*)
+  Library.require_library qidl import
 
 let vernac_canonical locqid =
-  Recordobj.objdef_declare (Nametab.global locqid)
+  Recordops.declare_canonical_structure (Nametab.global locqid)
 
 let locate_reference ref =
   let (loc,qid) = qualid_of_reference ref in
@@ -591,18 +579,14 @@ let vernac_solve_existential = instantiate_nth_evar_com
 let vernac_set_end_tac tac =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode";
-  if tac <> (Tacexpr.TacId "") then set_end_tac (Tacinterp.interp tac)
-(* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
- 
-   
+  if tac <> (Tacexpr.TacId []) then set_end_tac (Tacinterp.interp tac) else ()
+      (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
+	
 (*****************************)
 (* Auxiliary file management *)
 
 let vernac_require_from export spec filename =
-  match export with
-      Some exp ->
-        Library.require_library_from_file spec None filename exp
-    | None -> Library.read_library_from_file filename
+  Library.require_library_from_file None filename export
 
 let vernac_add_loadpath isrec pdir ldiropt =
   let alias = match ldiropt with
@@ -610,7 +594,7 @@ let vernac_add_loadpath isrec pdir ldiropt =
     | Some ldir -> ldir in
   (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias
 
-let vernac_remove_loadpath = Library.remove_path
+let vernac_remove_loadpath = Library.remove_load_path
 
   (* Coq syntax for ML or system commands *)
 
@@ -651,7 +635,9 @@ let vernac_reset_initial () = abort_refine Lib.reset_initial ()
 
 let vernac_back n = Lib.back n
 
+let vernac_backto n = Lib.reset_label n
 
+(* see also [vernac_backtrack] which combines undoing and resetting *)
 (************)
 (* Commands *)
 
@@ -667,7 +653,7 @@ let vernac_declare_implicits locqid = function
 
 let vernac_reserve idl c =
   let t = Constrintern.interp_type Evd.empty (Global.env()) c in
-  let t = Detyping.detype (false,Global.env()) [] [] t in
+  let t = Detyping.detype false [] [] t in
   List.iter (fun id -> Reserve.declare_reserved_type id t) idl
 
 let make_silent_if_not_pcoq b =
@@ -691,13 +677,11 @@ let _ =
       optread  = Impargs.is_implicit_args;
       optwrite = Impargs.make_implicit_args }
 
-let impargs = if !Options.v7 then "Implicits" else "Implicit"
-
 let _ =
   declare_bool_option 
-    { optsync  = false; (* synchronisation is in Impargs *)
+    { optsync  = true;
       optname  = "strict implicit arguments";
-      optkey   = (SecondaryTable ("Strict",impargs));
+      optkey   = (SecondaryTable ("Strict","Implicit"));
       optread  = Impargs.is_strict_implicit_args;
       optwrite = Impargs.make_strict_implicit_args }
 
@@ -705,7 +689,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "contextual implicit arguments";
-      optkey   = (SecondaryTable ("Contextual",impargs));
+      optkey   = (SecondaryTable ("Contextual","Implicit"));
       optread  = Impargs.is_contextual_implicit_args;
       optwrite = Impargs.make_contextual_implicit_args }
 
@@ -721,7 +705,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "implicit arguments printing";
-      optkey   = (SecondaryTable ("Printing",impargs));
+      optkey   = (SecondaryTable ("Printing","Implicit"));
       optread  = (fun () -> !Constrextern.print_implicits);
       optwrite = (fun b ->  Constrextern.print_implicits := b) }
 
@@ -737,7 +721,7 @@ let _ =
   declare_bool_option 
     { optsync  = true;
       optname  = "notations printing";
-      optkey   = (SecondaryTable ("Printing",if !Options.v7 then "Symbols" else "Notations"));
+      optkey   = (SecondaryTable ("Printing","Notations"));
       optread  = (fun () -> not !Constrextern.print_no_symbol);
       optwrite = (fun b ->  Constrextern.print_no_symbol := not b) }
 
@@ -750,6 +734,30 @@ let _ =
       optwrite = (fun b -> Options.raw_print := b) }
 
 let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "use of virtual machine inside the kernel";
+      optkey   = (SecondaryTable ("Virtual","Machine"));
+      optread  = (fun () -> Vconv.use_vm ());
+      optwrite = (fun b -> Vconv.set_use_vm b) }
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "use of boxed definitions";
+      optkey   = (SecondaryTable ("Boxed","Definitions"));
+      optread  = Options.boxed_definitions;
+      optwrite = (fun b -> Options.set_boxed_definitions b) } 
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "use of boxed values";
+      optkey   = (SecondaryTable ("Boxed","Values"));
+      optread  = (fun _ -> not (Vm.transp_values ()));
+      optwrite = (fun b -> Vm.set_transp_values (not b)) } 
+
+let _ =
   declare_int_option
     { optsync=false;
       optkey=PrimaryTable("Undo");
@@ -784,11 +792,11 @@ let _ =
 let vernac_set_opacity opaq locqid =
   match Nametab.global locqid with
     | ConstRef sp ->
-	if opaq then Tacred.set_opaque_const sp
-	else Tacred.set_transparent_const sp
+	if opaq then set_opaque_const sp
+	else set_transparent_const sp
     | VarRef id ->
-	if opaq then Tacred.set_opaque_var id
-	else Tacred.set_transparent_var id
+	if opaq then set_opaque_var id
+	else set_transparent_var id
     | _ -> error "cannot set an inductive type or a constructor as transparent"
 
 let vernac_set_option key = function
@@ -843,7 +851,7 @@ let vernac_check_may_eval redexp glopt rc =
 	if !pcoq <> None then (out_some !pcoq).print_check j
 	else msg (print_judgment env j)
     | Some r ->
-	let redfun = Tacred.reduction_of_redexp (interp_redexp env evmap r) in
+	let redfun = fst (reduction_of_red_expr (interp_redexp env evmap r)) in
 	if !pcoq <> None
 	then (out_some !pcoq).print_eval (redfun env evmap) env rc j
 	else msg (print_eval redfun env j)
@@ -859,7 +867,6 @@ let vernac_global_check c =
 
 let vernac_print = function
   | PrintTables -> print_tables ()
-  | PrintLocalContext -> msg (print_local_context ())
   | PrintFullContext -> msg (print_full_context_typ ())
   | PrintSectionContext qid -> msg (print_sec_context_typ qid)
   | PrintInspect n -> msg (inspect n)
@@ -876,21 +883,25 @@ let vernac_print = function
   | PrintOpaqueName qid -> msg (print_opaque_name qid)
   | PrintGraph -> ppnl (Prettyp.print_graph())
   | PrintClasses -> ppnl (Prettyp.print_classes())
+  | PrintLtac qid -> ppnl (Tacinterp.print_ltac (snd (qualid_of_reference qid)))
   | PrintCoercions -> ppnl (Prettyp.print_coercions())
   | PrintCoercionPaths (cls,clt) ->
       ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
+  | PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ())
   | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ()))
   | PrintUniverses (Some s) -> dump_universes s
   | PrintHint qid -> Auto.print_hint_ref (Nametab.global qid)
   | PrintHintGoal -> Auto.print_applicable_hint ()
   | PrintHintDbName s -> Auto.print_hint_db_by_name s
+  | PrintRewriteHintDbName s -> Autorewrite.print_rewrite_hintdb s
   | PrintHintDb -> Auto.print_searchtable ()
+  | PrintSetoids -> Setoid_replace.print_setoids()
   | PrintScopes ->
-      pp (Symbols.pr_scopes (Constrextern.without_symbols pr_rawterm))
+      pp (Notation.pr_scopes (Constrextern.without_symbols pr_lrawconstr))
   | PrintScope s ->
-      pp (Symbols.pr_scope (Constrextern.without_symbols pr_rawterm) s)
+      pp (Notation.pr_scope (Constrextern.without_symbols pr_lrawconstr) s)
   | PrintVisibility s ->
-      pp (Symbols.pr_visibility (Constrextern.without_symbols pr_rawterm) s)
+      pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s)
   | PrintAbout qid -> msgnl (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
 
@@ -929,10 +940,11 @@ let vernac_search s r =
 let vernac_locate = function
   | LocateTerm qid -> msgnl (print_located_qualid qid)
   | LocateLibrary qid -> print_located_library qid
+  | LocateModule qid -> print_located_module qid
   | LocateFile f -> locate_file f
   | LocateNotation ntn ->
-      ppnl (Symbols.locate_notation (Constrextern.without_symbols pr_rawterm)
-	(Metasyntax.standardise_locatable_notation ntn))
+      ppnl (Notation.locate_notation (Constrextern.without_symbols pr_lrawconstr)
+	(Metasyntax.standardize_locatable_notation ntn))
 
 (********************)
 (* Proof management *)
@@ -942,7 +954,7 @@ let vernac_goal = function
   | Some c ->
       if not (refining()) then begin
         let unnamed_kind = Lemma (* Arbitrary *) in
-        start_proof_com None (IsGlobal (Proof unnamed_kind)) c (fun _ _ ->());
+        start_proof_com None (Global, Proof unnamed_kind) c (fun _ _ ->());
 	print_subgoals ()
       end else 
 	error "repeated Goal not permitted in refining mode"
@@ -979,6 +991,17 @@ let vernac_undo n =
   undo n;
   print_subgoals ()
 
+(* backtrack with [naborts] abort, then undo_todepth to [pnum], then
+   back-to state number [snum]. This allows to backtrack proofs and
+   state with one command (easier for proofgeneral). *)
+let vernac_backtrack snum pnum naborts =
+  for i = 1 to naborts do vernac_abort None done;
+  undo_todepth pnum;
+  vernac_backto snum;
+  (* there may be no proof in progress, even if no abort *)
+  (try print_subgoals () with UserError _ -> ())
+  
+
   (* Est-ce normal que "Focus" ne semble pas se comporter comme "Focus 1" ? *)
 let vernac_focus = function
   | None -> traverse_nth_goal 1; print_subgoals ()
@@ -1005,10 +1028,10 @@ let apply_subproof f occ =
   f evc (Global.named_context()) pf
 
 let explain_proof occ =
-  msg (apply_subproof (Refiner.print_treescript true) occ)
+  msg (apply_subproof (print_treescript true) occ)
 
 let explain_tree occ =
-  msg (apply_subproof Refiner.print_proof occ)
+  msg (apply_subproof print_proof occ)
 
 let vernac_show = function
   | ShowGoal nopt ->
@@ -1028,17 +1051,17 @@ let vernac_show = function
   | ShowProofNames ->
       msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names()))
   | ShowIntros all -> show_intro all
+  | ShowMatch id -> show_match id
   | ExplainProof occ -> explain_proof occ
   | ExplainTree occ -> explain_tree occ
 
 let vernac_check_guard () =
   let pts = get_pftreestate () in
-  let pf = proof_of_pftreestate pts 
-  and cursor = cursor_of_pftreestate pts in
+  let pf = proof_of_pftreestate pts in
   let (pfterm,_) = extract_open_pftreestate pts in
   let message = 
     try 
-      Inductiveops.control_only_guard (Evarutil.evar_env (goal_of_proof pf))
+      Inductiveops.control_only_guard (Evd.evar_env (goal_of_proof pf))
 	pfterm; 
       (str "The condition holds up to here")
     with UserError(_,s) -> 
@@ -1049,100 +1072,19 @@ let vernac_check_guard () =
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
-
-(**************************)
-(* Not supported commands *)
-(***
-let _ =
-  add "ResetSection"
-    (function 
-       | [VARG_IDENTIFIER id] ->
-	   (fun () -> reset_section (string_of_id id))
-       | _ -> bad_vernac_args "ResetSection")
-
-(* Modules *)
-
-let _ =
-  vinterp_add "BeginModule"
-    (function 
-       | [VARG_IDENTIFIER id] ->
-	   let s = string_of_id id in
-	   let lpe,_ = System.find_file_in_path (Library.get_load_path ()) (s^".v") in
-	   let dir = extend_dirpath (Library.find_logical_path lpe) id in
-	   fun () ->
-	     Lib.start_module dir
-       | _ -> bad_vernac_args "BeginModule")
-
-let _ =
-  vinterp_add "WriteModule"
-    (function 
-       | [VARG_IDENTIFIER id] ->
-	   let mid = Lib.end_module id in
-	   fun () -> let m = string_of_id id in Library.save_module_to mid m
-       | [VARG_IDENTIFIER id; VARG_STRING f] ->
-	   let mid = Lib.end_module id in
-	   fun () -> Library.save_module_to mid f
-       | _ -> bad_vernac_args "WriteModule")
-
-let _ =
-  vinterp_add "CLASS"
-    (function 
-       | [VARG_STRING kind; VARG_QUALID qid] -> 
-	   let stre = 
-	     if kind = "LOCAL" then 
-	       make_strength_0()
-             else 
-	       Nametab.NeverDischarge 
-	   in
-	   fun () -> 
-	     let ref = Nametab.global (dummy_loc, qid) in
-	     Class.try_add_new_class ref stre;
-             if_verbose message
-               ((string_of_qualid qid) ^ " is now a class")
-       | _ -> bad_vernac_args "CLASS")
-
-(* Meta-syntax commands *)
-let _ =
-  add "TOKEN"
-    (function
-       | [VARG_STRING s] -> (fun () -> Metasyntax.add_token_obj s)
-       | _ -> bad_vernac_args "TOKEN")
-***)
-
-(* Search commands *)
-
-(***
-let _ =
-  add "Searchisos"
-  (function
-     | [VARG_CONSTR com] -> 
-	 (fun () ->
-	    let env = Global.env() in
-	    let c = constr_of_com Evd.empty env com in
-	    let cc = nf_betaiota env Evd.empty c in
-            Searchisos.type_search cc)
-     | _ -> bad_vernac_args "Searchisos")
-***)
-
 let interp c = match c with
   (* Control (done in vernac) *)
   | (VernacTime _ | VernacVar _ | VernacList _ | VernacLoad _) -> assert false
-  | (VernacV7only _ | VernacV8only _) -> assert false
 
   (* Syntax *)
-  | VernacSyntax (whatfor,sel) -> vernac_syntax whatfor sel
-  | VernacTacticGrammar al -> Metasyntax.add_tactic_grammar al
-  | VernacGrammar (univ,al) -> vernac_grammar univ al
-  | VernacSyntaxExtension (lcl,sl,l8) -> vernac_syntax_extension lcl sl l8
+  | VernacTacticNotation (n,r,e) -> Metasyntax.add_tactic_notation (n,r,e)
+  | VernacSyntaxExtension (lcl,sl) -> vernac_syntax_extension lcl sl
   | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr
   | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl
   | VernacOpenCloseScope sc -> vernac_open_close_scope sc
   | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope qid scl
-  | VernacInfix (local,mv,qid,mv8,sc) -> vernac_infix local mv qid mv8 sc
-  | VernacDistfix (local,assoc,n,inf,qid,sc) -> 
-      vernac_distfix local assoc n inf qid sc
-  | VernacNotation (local,c,infpl,mv8,sc) ->
-      vernac_notation local c infpl mv8 sc
+  | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc
+  | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
 
   (* Gallina *)
   | VernacDefinition (k,(_,id),d,f) -> vernac_definition k id d f
@@ -1152,15 +1094,15 @@ let interp c = match c with
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,l) -> vernac_assumption stre l
   | VernacInductive (finite,l) -> vernac_inductive finite l
-  | VernacFixpoint l -> vernac_fixpoint l
-  | VernacCoFixpoint l -> vernac_cofixpoint l
+  | VernacFixpoint (l,b) -> vernac_fixpoint l b
+  | VernacCoFixpoint (l,b) -> vernac_cofixpoint l b
   | VernacScheme l -> vernac_scheme l
 
   (* Modules *)
-  | VernacDeclareModule ((_,id),bl,mtyo,mexpro) -> 
-      vernac_declare_module id bl mtyo mexpro
-  | VernacDefineModule ((_,id),bl,mtyo,mexpro) -> 
-      vernac_define_module id bl mtyo mexpro
+  | VernacDeclareModule (export,(_,id),bl,mtyo) -> 
+      vernac_declare_module export id bl mtyo
+  | VernacDefineModule (export,(_,id),bl,mtyo,mexpro) -> 
+      vernac_define_module export id bl mtyo mexpro
   | VernacDeclareModuleType ((_,id),bl,mtyo) -> 
       vernac_declare_module_type id bl mtyo
 
@@ -1196,6 +1138,7 @@ let interp c = match c with
   | VernacResetName id -> vernac_reset_name id
   | VernacResetInitial -> vernac_reset_initial ()
   | VernacBack n -> vernac_back n
+  | VernacBackTo n -> vernac_backto n
 
   (* Commands *)
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
@@ -1226,6 +1169,7 @@ let interp c = match c with
   | VernacSuspend -> vernac_suspend ()
   | VernacResume id -> vernac_resume id
   | VernacUndo n -> vernac_undo n
+  | VernacBacktrack (snum,pnum,naborts) -> vernac_backtrack snum pnum naborts
   | VernacFocus n -> vernac_focus n
   | VernacUnfocus -> vernac_unfocus ()
   | VernacGo g -> vernac_go g
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 89e0d708..a2bcd990 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacentries.mli,v 1.16.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
+(*i $Id: vernacentries.mli 6616 2005-01-21 17:18:23Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 382434dc..a00901a4 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacexpr.ml,v 1.55.2.2 2005/01/21 17:14:10 herbelin Exp $ i*)
+(*i $Id: vernacexpr.ml 7936 2006-01-28 18:36:54Z herbelin $ i*)
 
 open Util
 open Names
@@ -34,7 +34,6 @@ type class_rawexpr = FunClass | SortClass | RefClass of reference
   
 type printable =
   | PrintTables
-  | PrintLocalContext
   | PrintFullContext
   | PrintSectionContext of reference
   | PrintInspect of int
@@ -49,13 +48,17 @@ type printable =
   | PrintOpaqueName of reference
   | PrintGraph
   | PrintClasses
+  | PrintLtac of reference
   | PrintCoercions
   | PrintCoercionPaths of class_rawexpr * class_rawexpr
+  | PrintCanonicalConversions
   | PrintUniverses of string option
   | PrintHint of reference
   | PrintHintGoal
   | PrintHintDbName of string
+  | PrintRewriteHintDbName of string
   | PrintHintDb
+  | PrintSetoids
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
@@ -75,6 +78,7 @@ type searchable =
 type locatable =
   | LocateTerm of reference
   | LocateLibrary of reference
+  | LocateModule of reference
   | LocateFile of string
   | LocateNotation of notation
 
@@ -94,6 +98,7 @@ type showable =
   | ShowTree
   | ShowProofNames
   | ShowIntros of bool
+  | ShowMatch of lident
   | ExplainProof of int list
   | ExplainTree of int list
 
@@ -103,11 +108,11 @@ type comment =
   | CommentInt of int
 
 type hints =
-  | HintsResolve of (identifier option * constr_expr) list
-  | HintsImmediate of (identifier option * constr_expr) list
-  | HintsUnfold of (identifier option * reference) list
-  | HintsConstructors of identifier option * reference list
-  | HintsExtern of identifier option * int * constr_expr * raw_tactic_expr
+  | HintsResolve of constr_expr list
+  | HintsImmediate of constr_expr list
+  | HintsUnfold of reference list
+  | HintsConstructors of reference list
+  | HintsExtern of int * constr_expr * raw_tactic_expr
   | HintsDestruct of identifier *
       int * (bool,unit) location * constr_expr * raw_tactic_expr
 
@@ -152,7 +157,11 @@ type local_decl_expr =
   | AssumExpr of lname * constr_expr
   | DefExpr of lname * constr_expr * constr_expr option
 
-type module_binder = lident list * module_type_ast
+type module_binder = bool option * lident list * module_type_ast
+
+type grammar_production =
+  | VTerm of string
+  | VNonTerm of loc * string * Names.identifier option
 
 type proof_end =
   | Admitted
@@ -166,25 +175,17 @@ type vernac_expr =
   | VernacVar of lident
 
   (* Syntax *) 
-  | VernacGrammar of lstring * raw_grammar_entry list
-  | VernacTacticGrammar of
-      (lstring * (lstring * grammar_production list) * raw_tactic_expr) list
-  | VernacSyntax of lstring * raw_syntax_entry list
-  | VernacSyntaxExtension of locality_flag *
-      (lstring * syntax_modifier list) option 
-      * (lstring * syntax_modifier list) option
-  | VernacDistfix of locality_flag *
-      grammar_associativity * precedence * lstring * lreference *
-      scope_name option
+  | VernacTacticNotation of int * grammar_production list * raw_tactic_expr
+  | VernacSyntaxExtension of locality_flag * (lstring * syntax_modifier list)
   | VernacOpenCloseScope of (locality_flag * bool * scope_name)
   | VernacDelimiters of scope_name * lstring
   | VernacBindScope of scope_name * class_rawexpr list
   | VernacArgumentsScope of lreference * scope_name option list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
-      lreference * (lstring * syntax_modifier list) option * scope_name option
+      lreference * scope_name option
   | VernacNotation of
-      locality_flag * constr_expr * (lstring * syntax_modifier list) option *
-      (lstring * syntax_modifier list) option * scope_name option
+      locality_flag * constr_expr * (lstring * syntax_modifier list) *
+      scope_name option
 
   (* Gallina *)
   | VernacDefinition of definition_kind * lident * definition_expr * 
@@ -195,8 +196,8 @@ type vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
   | VernacInductive of inductive_flag * inductive_expr list
-  | VernacFixpoint of (fixpoint_expr * decl_notation) list
-  | VernacCoFixpoint of cofixpoint_expr list
+  | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
+  | VernacCoFixpoint of cofixpoint_expr list * bool
   | VernacScheme of (lident * bool * lreference * sort_expr) list
 
   (* Gallina extensions *)
@@ -214,9 +215,9 @@ type vernac_expr =
       class_rawexpr * class_rawexpr
 
   (* Modules and Module Types *)
-  | VernacDeclareModule of lident * 
-      module_binder list * (module_type_ast * bool) option * module_ast option
-  | VernacDefineModule of lident * 
+  | VernacDeclareModule of bool option * lident * 
+      module_binder list * (module_type_ast * bool)
+  | VernacDefineModule of bool option * lident * 
       module_binder list * (module_type_ast * bool) option * module_ast option
   | VernacDeclareModuleType of lident * 
       module_binder list * module_type_ast option
@@ -241,6 +242,7 @@ type vernac_expr =
   | VernacResetName of lident
   | VernacResetInitial
   | VernacBack of int
+  | VernacBackTo of int
 
   (* Commands *)
   | VernacDeclareTacticDefinition of
@@ -273,6 +275,7 @@ type vernac_expr =
   | VernacSuspend
   | VernacResume of lident option
   | VernacUndo of int
+  | VernacBacktrack of int*int*int
   | VernacFocus of int option
   | VernacUnfocus
   | VernacGo of goable
@@ -283,10 +286,6 @@ type vernac_expr =
   (* Toplevel control *)
   | VernacToplevelControl of exn
 
-  (* For translation from V7 to V8 syntax *)
-  | VernacV8only of vernac_expr
-  | VernacV7only of vernac_expr
-
   (* For extension *)
   | VernacExtend of string * raw_generic_argument list
 
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index c7846d71..98584bac 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernacinterp.ml,v 1.17.8.1 2004/07/16 19:31:50 herbelin Exp $ *)
+(* $Id: vernacinterp.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
 
 open Pp
 open Util
@@ -15,10 +15,7 @@ open Libnames
 open Himsg
 open Proof_type
 open Tacinterp
-open Coqast
 open Vernacexpr
-open Ast
-open Extend
 
 let disable_drop e =
   if e <> Drop then e
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 86b80935..e0c34dc9 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: vernacinterp.mli,v 1.11.10.1 2004/07/16 19:31:50 herbelin Exp $ i*)
+(*i $Id: vernacinterp.mli 5920 2004-07-16 20:01:26Z herbelin $ i*)
 
 (*i*)
 open Tacexpr
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
new file mode 100644
index 00000000..042ee5c8
--- /dev/null
+++ b/toplevel/whelp.ml4
@@ -0,0 +1,209 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id: whelp.ml4 7837 2006-01-11 09:47:32Z herbelin $ *)
+
+open Options
+open Pp
+open Util
+open System
+open Names
+open Term
+open Environ
+open Rawterm
+open Libnames
+open Nametab
+open Termops
+open Detyping
+open Constrintern
+open Dischargedhypsmap
+open Command
+open Pfedit
+open Refiner
+open Tacmach
+
+(* Coq interface to the Whelp query engine developed at 
+   the University of Bologna *)
+
+let make_whelp_request req c =
+  "http://mowgli.cs.unibo.it/forward/58080/apply?xmluri=http%3A%2F%2Fmowgli.cs.unibo.it%3A58081%2Fgetempty&param.profile=firewall&profile=firewall&param.keys=d_c%2CC1%2CHC2%2CL&param.embedkeys=d_c%2CTC1%2CHC2%2CL&param.thkeys=T1%2CT2%2CL%2CE&param.prooftreekeys=HAT%2CG%2CHAO%2CL&param.media-type=text%2Fhtml&param.thmedia-type=&prooftreemedia-type=&param.doctype-public=&param.encoding=&param.thencoding=&param.prooftreeencoding=&advanced=no&keys=S%2CT1%2CT2%2CL%2CRT%2CE&param.expression=" ^ c ^ "&param.action=" ^ req
+
+let b = Buffer.create 16
+
+let url_char c =
+  if 'A' <= c & c <= 'Z' or 'a' <= c & c <= 'z' or 
+     '0' <= c & c <= '9' or c ='.'
+  then Buffer.add_char b c
+  else Buffer.add_string b (Printf.sprintf "%%%2X" (Char.code c))
+
+let url_string s = String.iter url_char s
+
+let rec url_list_with_sep sep f = function
+  | [] -> ()
+  | [a] -> f a
+  | a::l -> f a; url_string sep; url_list_with_sep sep f l 
+
+let url_id id = url_string (string_of_id id)
+
+let uri_of_dirpath dir =
+  url_string "cic:/"; url_list_with_sep "/" url_id (List.rev dir)
+
+let error_whelp_unknown_reference ref =
+  let qid = Nametab.shortest_qualid_of_global Idset.empty ref in
+  error ("Definitions of the current session not supported in Whelp: " ^ string_of_qualid qid)
+
+let uri_of_repr_kn ref (mp,dir,l) = 
+  match mp with
+    | MPfile sl ->
+        uri_of_dirpath (id_of_label l :: repr_dirpath dir @ repr_dirpath sl)
+    | _ ->
+        error_whelp_unknown_reference ref
+
+let url_paren f l = url_char '('; f l; url_char ')'
+let url_bracket f l = url_char '['; f l; url_char ']'
+
+let whelp_of_rawsort = function
+  | RProp Null -> "Prop"
+  | RProp Pos -> "Set"
+  | RType _ -> "Type"
+
+let uri_int n = Buffer.add_string b (string_of_int n)
+
+let uri_of_ind_pointer l =
+  url_string ".ind#xpointer"; url_paren (url_list_with_sep "/" uri_int) l
+
+let uri_of_global ref =
+  match ref with
+  | VarRef id -> error ("Unknown Whelp reference: "^(string_of_id id))
+  | ConstRef cst ->
+      uri_of_repr_kn ref (repr_con cst); url_string ".con"
+  | IndRef (kn,i) -> 
+      uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1]
+  | ConstructRef ((kn,i),j) ->
+      uri_of_repr_kn ref (repr_kn kn); uri_of_ind_pointer [1;i+1;j]
+
+let whelm_special = id_of_string "WHELM_ANON_VAR"
+
+let url_of_name = function
+  | Name id -> url_id id
+  | Anonymous -> url_id whelm_special (* No anon id in Whelp *)
+
+let uri_of_binding f (id,c) = url_id id; url_string "\\Assign "; f c
+
+let uri_params f = function
+  | [] -> ()
+  | l -> url_string "\\subst"; 
+         url_bracket (url_list_with_sep ";" (uri_of_binding f)) l
+
+let get_discharged_hyp_names sp = List.map basename (get_discharged_hyps sp)
+
+let section_parameters = function
+  | RRef (_,(ConstructRef ((induri,_),_) | IndRef (induri,_))) ->
+      get_discharged_hyp_names (sp_of_global (IndRef(induri,0)))
+  | RRef (_,(ConstRef cst as ref)) ->
+      get_discharged_hyp_names (sp_of_global ref)
+  | _ -> []
+
+let merge vl al =
+  let rec aux acc = function
+  | ([],l) | (_,([] as l)) -> List.rev acc, l
+  | (v::vl,a::al) -> aux ((v,a)::acc) (vl,al)
+  in aux [] (vl,al)
+
+let rec uri_of_constr c =
+  match c with
+  | RVar (_,id) -> url_id id
+  | RRef (_,ref) ->  uri_of_global ref
+  | RHole _ | REvar _ -> url_string "?"
+  | RSort (_,s) -> url_string (whelp_of_rawsort s)
+  | _ -> url_paren (fun () -> match c with
+  | RApp (_,f,args) ->
+      let inst,rest = merge (section_parameters f) args in
+      uri_of_constr f; url_char ' '; uri_params uri_of_constr inst; 
+      url_list_with_sep " " uri_of_constr rest
+  | RLambda (_,na,ty,c) ->
+      url_string "\\lambda "; url_of_name na; url_string ":";
+      uri_of_constr ty; url_string "."; uri_of_constr c
+  | RProd (_,Anonymous,ty,c) ->
+      uri_of_constr ty; url_string "\\to "; uri_of_constr c
+  | RProd (_,Name id,ty,c) ->
+      url_string "\\forall "; url_id id; url_string ":";
+      uri_of_constr ty; url_string "."; uri_of_constr c
+  | RLetIn (_,na,b,c) ->
+      url_string "let "; url_of_name na; url_string "\\def ";
+      uri_of_constr b; url_string " in "; uri_of_constr c
+  | RCast (_,c,_,t) ->
+      uri_of_constr c; url_string ":"; uri_of_constr t
+  | RRec _ | RIf _ | RLetTuple _ | RCases _ ->
+      error "Whelp does not support pattern-matching and (co-)fixpoint"
+  | RVar _ | RRef _ | RHole _ | REvar _ | RSort _ ->
+      anomaly "Written w/o parenthesis"
+  | RPatVar _ | RDynamic _ -> 
+      anomaly "Found constructors not supported in constr") ()
+
+let make_string f x = Buffer.reset b; f x; Buffer.contents b
+
+let send_whelp req s =
+  let url = make_whelp_request req s in
+  let command = (fst browser_cmd_fmt) ^ url ^ (snd browser_cmd_fmt) in
+  let _ = run_command (fun x -> x) print_string command in ()
+
+let whelp_constr req c =
+  let c = detype false [whelm_special] [] c in
+  send_whelp req (make_string uri_of_constr c)
+
+let whelp_constr_expr req c =
+  let (sigma,env)= get_current_context () in
+  let _,c = interp_open_constr sigma env c in
+  whelp_constr req c
+
+let whelp_locate s =
+  send_whelp "locate" s
+
+let whelp_elim ind = 
+  send_whelp "elim" (make_string uri_of_global (IndRef ind))
+
+let locate_inductive r =
+  let (loc,qid) = qualid_of_reference r in
+  try match Syntax_def.locate_global qid with
+    | IndRef ind -> ind
+    | _ -> user_err_loc (loc,"",str "Inductive type expected")
+  with Not_found -> error_global_not_found_loc loc qid
+
+let on_goal f =
+  let gls = nth_goal_of_pftreestate 1 (get_pftreestate ()) in
+  f (it_mkNamedProd_or_LetIn (pf_concl gls) (pf_hyps gls))
+
+type whelp_request =
+  | Locate of string
+  | Elim of inductive
+  | Constr of string * constr
+
+let whelp = function
+  | Locate s -> whelp_locate s
+  | Elim ind -> whelp_elim ind
+  | Constr (s,c) -> whelp_constr s c
+
+VERNAC ARGUMENT EXTEND whelp_constr_request
+| [ "Match" ] -> [ "match" ]
+| [ "Instance" ] -> [ "instance" ]
+END
+
+VERNAC COMMAND EXTEND Whelp
+| [ "Whelp" "Locate" string(s) ] -> [ whelp_locate s ] 
+| [ "Whelp" "Locate" preident(s) ] -> [ whelp_locate s ] 
+| [ "Whelp" "Elim" global(r) ] -> [ whelp_elim (locate_inductive r) ] 
+| [ "Whelp" whelp_constr_request(req) constr(c) ] -> [ whelp_constr_expr req c]
+END
+
+VERNAC COMMAND EXTEND WhelpHint
+| [ "Whelp" "Hint" constr(c) ] -> [ whelp_constr_expr "hint" c ] 
+| [ "Whelp" "Hint" ] -> [ on_goal (whelp_constr "hint") ] 
+END
diff --git a/toplevel/recordobj.mli b/toplevel/whelp.mli
index 91550c34..f3f7408a 100755..100644
--- a/toplevel/recordobj.mli
+++ b/toplevel/whelp.mli
@@ -6,7 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: recordobj.mli,v 1.7.6.2 2005/01/21 17:18:33 herbelin Exp $ i*)
+(*i $Id: whelp.mli 7837 2006-01-11 09:47:32Z herbelin $ i*)
 
-val objdef_declare : Libnames.global_reference -> unit
-val add_object_hook : Tacexpr.declaration_hook
+(* Coq interface to the Whelp query engine developed at 
+   the University of Bologna *)
+
+open Names
+open Term
+open Topconstr
+open Environ
+
+type whelp_request =
+  | Locate of string
+  | Elim of inductive
+  | Constr of string * constr
+
+val whelp : whelp_request -> unit