Imported Upstream version 8.1~gammaupstream/8.1.gamma

12 files changed, 562 insertions, 474 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index ab9c4c63..f6c5c3af 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: cerrors.ml 8003 2006-02-07 22:11:50Z herbelin $ *)
+(* $Id: cerrors.ml 9306 2006-10-28 18:28:19Z herbelin $ *)
 
 open Pp
 open Util
@@ -28,19 +28,21 @@ let guill s = "\""^s^"\""
 let where s =
   if !Options.debug then  (str"in " ++ str s ++ str":" ++ spc ()) else (mt ())
 
+let anomaly_string () = str "Anomaly: "
+
 let report () = (str "." ++ spc () ++ str "Please report.")
 
 (* assumption : explain_sys_exn does NOT end with a 'FNL anymore! *)
 
-let rec explain_exn_default = function
+let rec explain_exn_default_aux anomaly_string report_fn = function
   | Stream.Failure -> 
-      hov 0 (str "Anomaly: uncaught Stream.Failure.")
+      hov 0 (anomaly_string () ++ str "uncaught Stream.Failure.")
   | Stream.Error txt -> 
       hov 0 (str "Syntax error: " ++ str txt)
   | Token.Error txt -> 
       hov 0 (str "Syntax error: " ++ str txt)
   | Sys_error msg -> 
-      hov 0 (str "Anomaly: uncaught exception Sys_error " ++ str (guill msg) ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Sys_error " ++ str (guill msg) ++ report_fn ())
   | UserError(s,pps) -> 
       hov 1 (str "User error: " ++ where s ++ pps)
   | Out_of_memory -> 
@@ -48,26 +50,26 @@ let rec explain_exn_default = function
   | Stack_overflow -> 
       hov 0 (str "Stack overflow")
   | Anomaly (s,pps) -> 
-      hov 1 (str "Anomaly: " ++ where s ++ pps ++ report ())
+      hov 1 (anomaly_string () ++ where s ++ pps ++ report_fn ())
   | Match_failure(filename,pos1,pos2) ->
-      hov 1 (str "Anomaly: Match failure in file " ++ str (guill filename) ++ 
+      hov 1 (anomaly_string () ++ str "Match failure in file " ++ str (guill filename) ++ 
       if Sys.ocaml_version = "3.06" then
 		   (str " from character " ++ int pos1 ++ 
                     str " to " ++ int pos2)
 		 else
 		   (str " at line " ++ int pos1 ++
 		    str " character " ++ int pos2)
-	           ++ report ())
+	           ++ report_fn ())
   | Not_found -> 
-      hov 0 (str "Anomaly: uncaught exception Not_found" ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Not_found" ++ report_fn ())
   | Failure s -> 
-      hov 0 (str "Anomaly: uncaught exception Failure " ++ str (guill s) ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Failure " ++ str (guill s) ++ report_fn ())
   | Invalid_argument s -> 
-      hov 0 (str "Anomaly: uncaught exception Invalid_argument " ++ str (guill s) ++ report ())
+      hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ str (guill s) ++ report_fn ())
   | Sys.Break -> 
-      hov 0 (fnl () ++ str "User Interrupt.")
+      hov 0 (fnl () ++ str "User interrupt.")
   | Univ.UniverseInconsistency -> 
-      hov 0 (str "Error: Universe Inconsistency.")
+      hov 0 (str "Error: Universe inconsistency.")
   | TypeError(ctx,te) -> 
       hov 0 (str "Error:" ++ spc () ++ Himsg.explain_type_error ctx te)
   | PretypeError(ctx,te) ->
@@ -97,7 +99,7 @@ let rec explain_exn_default = function
   | Stdpp.Exc_located (loc,exc) ->
       hov 0 ((if loc = dummy_loc then (mt ())
                else (str"At location " ++ print_loc loc ++ str":" ++ fnl ()))
-               ++ explain_exn_default exc)
+               ++ explain_exn_default_aux anomaly_string report_fn exc)
   | Lexer.Error Illegal_character -> 
       hov 0 (str "Syntax error: Illegal character.")
   | Lexer.Error Unterminated_comment -> 
@@ -109,7 +111,7 @@ let rec explain_exn_default = function
   | Lexer.Error (Bad_token s) -> 
       hov 0 (str "Syntax error: Bad token" ++ spc () ++ str s ++ str ".")
   | Assert_failure (s,b,e) ->
-      hov 0 (str "Anomaly: assert failure" ++ spc () ++
+      hov 0 (anomaly_string () ++ str "assert failure" ++ spc () ++
 	       (if s <> "" then 
 		 if Sys.ocaml_version = "3.06" then
 		   (str ("(file \"" ^ s ^ "\", characters ") ++ 
@@ -120,16 +122,22 @@ let rec explain_exn_default = function
 		    int (e+6) ++ str ")")
 	       else
 		 (mt ())) ++
-	       report ())
+	       report_fn ())
   | reraise ->
-      hov 0 (str "Anomaly: Uncaught exception " ++ 
-	       str (Printexc.to_string reraise) ++ report ())
+      hov 0 (anomaly_string () ++ str "Uncaught exception " ++ 
+	       str (Printexc.to_string reraise) ++ report_fn ())
+
+let explain_exn_default =
+    explain_exn_default_aux (fun () -> str "Anomaly: ") report
 
 let raise_if_debug e =
   if !Options.debug then raise e
 
 let _ = Tactic_debug.explain_logic_error := explain_exn_default
 
+let _ = Tactic_debug.explain_logic_error_no_anomaly :=
+          explain_exn_default_aux (fun () -> mt()) (fun () -> mt())
+
 let explain_exn_function = ref explain_exn_default
 
 let explain_exn e = !explain_exn_function e
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 56a32f04..d751f70c 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: command.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Pp
 open Util
@@ -32,11 +32,15 @@ open Proof_type
 open Tacmach
 open Safe_typing
 open Nametab
+open Impargs
 open Typeops
+open Reductionops
 open Indtypes
 open Vernacexpr
 open Decl_kinds
 open Pretyping
+open Evarutil
+open Evarconv
 open Notation
 
 let mkLambdaCit = List.fold_right (fun (x,a) b -> mkLambdaC(x,a,b))
@@ -56,11 +60,6 @@ let rec generalize_constr_expr c = function
       List.fold_right (fun x b -> mkProdC([x],t,b)) idl
         (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
@@ -78,12 +77,12 @@ let rec destSubCast c = match kind_of_term c with
   | Cast (b,_, u) -> (b,u)
   | _ -> assert false
 
-let rec adjust_conclusion a cs = function
-  | CProdN (loc,bl,c) -> CProdN (loc,bl,adjust_conclusion a cs c)
-  | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,adjust_conclusion a cs c)
+let rec complete_conclusion a cs = function
+  | CProdN (loc,bl,c) -> CProdN (loc,bl,complete_conclusion a cs c)
+  | CLetIn (loc,b,t,c) -> CLetIn (loc,b,t,complete_conclusion a cs c)
   | CHole loc ->
-      let (nar,name,params) = a in
-      if nar <> 0 then
+      let (has_no_args,name,params) = a in
+      if not has_no_args then
 	user_err_loc (loc,"",
 	  str "Cannot infer the non constant arguments of the conclusion of "
 	  ++ pr_id cs);
@@ -106,7 +105,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
 	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 (refresh_universes j.uj_type);
+	  const_entry_type = None;
           const_entry_opaque = opacity;
 	  const_entry_boxed = boxed }
     | Some comtyp ->
@@ -125,7 +124,7 @@ let red_constant_entry bl ce = function
       let body = ce.const_entry_body in
       { ce with const_entry_body = 
 	under_binders (Global.env()) (fst (reduction_of_red_expr red))
-	  (length_of_raw_binders bl)
+	  (local_binders_length bl)
 	  body }
 
 let declare_global_definition ident ce local =
@@ -226,7 +225,8 @@ 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 cte and t = constant_type (Global.env()) cte in
+    let c = mkConst cte in
+    let t = type_of_constant (Global.env()) cte in
     List.iter (fun (sort,suff) -> 
       let (t',c') = 
 	Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort)
@@ -248,371 +248,380 @@ let declare_eliminations sp =
       declare_one_elimination (sp,i)
     done
 
-(* 3b| Mutual Inductive definitions *)
-
-let minductive_message = function 
+(* 3b| Mutual inductive definitions *)
+
+let compute_interning_datas env l nal typl =
+  let mk_interning_data na typ =
+    let idl, impl =
+      if is_implicit_args() then
+	let impl = compute_implicits env typ in
+	let sub_impl,_ = list_chop (List.length l) impl in
+	let sub_impl' = List.filter is_status_implicit sub_impl in
+	(List.map name_of_implicit sub_impl', impl)
+      else 
+	([],[]) in
+    (na, (idl, impl, compute_arguments_scope typ)) in
+  (l, List.map2 mk_interning_data nal typl)
+
+let declare_interning_data (_,impls) (df,c,scope) =
+  silently (Metasyntax.add_notation_interpretation df impls c) scope
+
+let push_named_types env idl tl =
+  List.fold_left2 (fun env id t -> Environ.push_named (id,None,t) env)
+    env idl tl
+
+let push_types env idl tl =
+  List.fold_left2 (fun env id t -> Environ.push_rel (Name id,None,t) env)
+    env idl tl
+
+type inductive_expr = {
+  ind_name : identifier;
+  ind_arity : constr_expr;
+  ind_lc : (identifier * constr_expr) list
+}
+
+let minductive_message = function
   | []  -> error "no inductive definition"
   | [x] -> (pr_id x ++ str " is defined")
   | l   -> hov 0  (prlist_with_sep pr_coma pr_id l ++
 		     spc () ++ str "are defined")
 
-let recursive_message v =
-  match Array.length v with
-    | 0 -> error "no recursive definition"
-    | 1 -> (Printer.pr_global v.(0) ++ str " is recursively defined")
-    | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
-		    spc () ++ str "are recursively defined")
-
-let corecursive_message v =
-  match Array.length v with
-    | 0 -> error "no corecursive definition"
-    | 1 -> (Printer.pr_global v.(0) ++ str " is corecursively defined")
-    | _ -> hov 0 (prvect_with_sep pr_coma Printer.pr_global v ++
-                    spc () ++ str "are corecursively defined")
+let check_all_names_different indl =
+  let get_names ind = ind.ind_name::List.map fst ind.ind_lc in
+  if not (list_distinct (List.flatten (List.map get_names indl))) then
+    error "Two inductive objects have the same name"
+
+let mk_mltype_data isevars env assums arity indname =
+  let is_ml_type = is_sort env (Evd.evars_of !isevars) arity in
+  (is_ml_type,indname,assums)
+
+let prepare_param = function
+  | (na,None,t) -> out_name na, LocalAssum t 
+  | (na,Some b,_) -> out_name na, LocalDef b
+
+let interp_ind_arity isevars env ind =
+  interp_type_evars isevars env ind.ind_arity
+
+let interp_cstrs isevars env impls mldata arity ind =
+  let cnames,ctyps = List.split ind.ind_lc in
+  (* Complete conclusions of constructor types if given in ML-style syntax *)
+  let ctyps' = List.map2 (complete_conclusion mldata) cnames ctyps in
+  (* Interpret the constructor types *)
+  let ctyps'' = List.map (interp_type_evars isevars env ~impls) ctyps' in
+  (cnames, ctyps'')
+
+let interp_mutual paramsl indl notations finite = 
+  check_all_names_different indl;
+  let env0 = Global.env() in
+  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let env_params, ctx_params = interp_context_evars isevars env0 paramsl in
+  let indnames = List.map (fun ind -> ind.ind_name) indl in
 
-let interp_mutual lparams lnamearconstrs finite = 
-  let allnames = 
-    List.fold_left (fun acc (id,_,_,l) -> id::(List.map fst l)@acc)
-      [] lnamearconstrs in
-  if not (list_distinct allnames) then
-    error "Two inductive objects have the same name";
-  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) ->
-		let id = match na with
-		  | Name id -> id
-		  | Anonymous -> anomaly "Unnamed inductive variable" in 
-		match b with
-		  | None -> (id, LocalAssum t)
-		  | Some b -> (id, LocalDef b)) params
-  in
-  let paramassums = 
-    List.fold_right (fun d l -> match d with
-	(id,LocalAssum _) -> id::l | (_,LocalDef _) -> l) params' [] in
-  let nparamassums = List.length paramassums in
-  let (ind_env,ind_impls,arityl) =
-    List.fold_left
-      (fun (env, ind_impls, arl) (recname, _, arityc, _) ->
-         let arity = interp_type sigma env_params arityc in
-	 let fullarity = it_mkProd_or_LetIn arity params in
-	 let env' = Termops.push_rel_assum (Name recname,fullarity) env in
-	 let argsc = compute_arguments_scope fullarity in
-	 let ind_impls' = 
-	   if Impargs.is_implicit_args() then
-	     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
-		 Impargs.name_of_implicit imp::l else l) paramimpl [] in
-	     (recname,(l,impl,argsc))::ind_impls
-	   else
-	     (recname,([],[],argsc))::ind_impls in
-	 (env', ind_impls', (arity::arl)))
-      (env0, [], []) lnamearconstrs
-  in
   (* Names of parameters as arguments of the inductive type (defs removed) *)
-  let lparargs = 
-    List.flatten
-      (List.map (function (id,LocalAssum _) -> [id] | _ -> []) params') in
-  let notations = 
-    List.fold_right (fun (_,ntnopt,_,_) l -> option_cons ntnopt l) 
-      lnamearconstrs [] in
-  let fs = States.freeze() in
-  (* Declare the notations for the inductive types pushed in local context*)
-  try
-  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 = 
-    List.map2
-      (fun ar (name,_,_,lname_constr) ->
-	 let constrnames, bodies = List.split lname_constr in
-         (* Compute the conclusions of constructor types *)
-	 (* for inductive given in ML syntax *)
-	 let nar = 
-	   List.length (fst (Reductionops.splay_arity env_params Evd.empty ar))
-	 in
-	 let bodies =
-	   List.map2 (adjust_conclusion (nar,name,lparargs))
-	     constrnames bodies
-	 in
-
-         (* Interpret the constructor types *)
-         let constrs =
-	   List.map 
-	     (interp_type sigma ind_env_params ~impls:(paramassums,ind_impls))
-	     bodies
-	 in
-
-         (* Build the inductive entry *)
-	 { 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_params = params';
-	       mind_entry_record = false; 
-	       mind_entry_finite = finite; 
-	       mind_entry_inds = mispecvec }
-  with e -> States.unfreeze fs; raise e
+  let assums = List.filter(fun (_,b,_) -> b=None) ctx_params in
+  let params = List.map (fun (na,_,_) -> out_name na) assums in
+
+  (* Interpret the arities *)
+  let arities = List.map (interp_ind_arity isevars env_params) indl in
+  let fullarities = List.map (fun c -> it_mkProd_or_LetIn c ctx_params) arities in
+  let env_ar = push_types env0 indnames fullarities in
+  let env_ar_params = push_rel_context ctx_params env_ar in
+
+  (* Compute interpretation metadatas *)
+  let impls = compute_interning_datas env0 params indnames fullarities in
+  let mldatas = List.map2 (mk_mltype_data isevars env_params params) arities indnames in
+
+  let constructors =
+    States.with_heavy_rollback (fun () -> 
+     (* Temporary declaration of notations and scopes *)
+     List.iter (declare_interning_data impls) notations;
+     (* Interpret the constructor types *)
+     list_map3 (interp_cstrs isevars env_ar_params impls) mldatas arities indl)
+     () in
+
+  (* Instantiate evars and check all are resolved *)
+  let isevars,_ = consider_remaining_unif_problems env_params !isevars in
+  let sigma = Evd.evars_of isevars in
+  let constructors = List.map (fun (idl,cl) -> (idl,List.map (nf_evar sigma) cl)) constructors in
+  let ctx_params = Sign.map_rel_context (nf_evar sigma) ctx_params in
+  let arities = List.map (nf_evar sigma) arities in
+  List.iter (check_evars env_params Evd.empty isevars) arities;
+  Sign.iter_rel_context (check_evars env0 Evd.empty isevars) ctx_params;
+  List.iter (fun (_,ctyps) ->
+    List.iter (check_evars env_ar_params Evd.empty isevars) ctyps)
+    constructors;
+  
+  (* Build the inductive entries *)
+  let entries = list_map3 (fun ind arity (cnames,ctypes) -> {
+    mind_entry_typename = ind.ind_name;
+    mind_entry_arity = arity;
+    mind_entry_consnames = cnames;
+    mind_entry_lc = ctypes
+  }) indl arities constructors in
+
+  (* Build the mutual inductive entry *)
+  { mind_entry_params = List.map prepare_param ctx_params;
+    mind_entry_record = false; 
+    mind_entry_finite = finite; 
+    mind_entry_inds = entries }
+
+let eq_constr_expr c1 c2 =
+  try let _ = Constrextern.check_same_type c1 c2 in true with _ -> false
+
+(* Very syntactical equality *)
+let eq_local_binder d1 d2 = match d1,d2 with
+  | LocalRawAssum (nal1,c1), LocalRawAssum (nal2,c2) ->
+      List.length nal1 = List.length nal2 &&
+      List.for_all2 (fun (_,na1) (_,na2) -> na1 = na2) nal1 nal2 &&
+      eq_constr_expr c1 c2
+  | LocalRawDef ((_,id1),c1), LocalRawDef ((_,id2),c2) ->
+      id1 = id2 && eq_constr_expr c1 c2
+  | _ ->
+      false
+
+let eq_local_binders bl1 bl2 =
+  List.length bl1 = List.length bl2 && List.for_all2 eq_local_binder bl1 bl2
+
+let extract_coercions indl =
+  let mkqid (_,((_,id),_)) = make_short_qualid id in
+  let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
+  List.map mkqid (List.flatten(List.map (fun (_,_,_,lc) -> extract lc) indl))
+
+let extract_params indl =
+  let paramsl = List.map (fun (_,params,_,_) -> params) indl in
+  match paramsl with
+  | [] -> anomaly "empty list of inductive types"
+  | params::paramsl ->
+      if not (List.for_all (eq_local_binders params) paramsl) then error 
+	"Parameters should be syntactically the same for each inductive type";
+      params
+
+let prepare_inductive ntnl indl =
+  let indl =
+    List.map (fun ((_,indname),_,ar,lc) -> { 
+      ind_name = indname;
+      ind_arity = ar;
+      ind_lc = List.map (fun (_,((_,id),t)) -> (id,t)) lc
+    }) indl in
+  List.fold_right option_cons ntnl [], indl
 
 let declare_mutual_with_eliminations isrecord mie =
-  let lrecnames =
-    List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
+  let names = List.map (fun e -> e.mind_entry_typename) mie.mind_entry_inds in
   let (_,kn) = declare_mind isrecord mie in
-  if_verbose ppnl (minductive_message lrecnames);
+  if_verbose ppnl (minductive_message names);
   declare_eliminations kn;
   kn
 
-(* 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') ->
-      id=id' & (try let _ = Constrextern.check_same_type ast ast' in true with _ -> false)
-  | _ -> false
-
-let extract_coe lc =
-  List.fold_right
-    (fun (addcoe,((_,(id:identifier)),t)) (l1,l2) ->
-      ((if addcoe then id::l1 else l1), (id,t)::l2)) lc ([],[])
-
-let extract_coe_la_lc = function
-  | []            -> anomaly "Vernacentries: empty list of inductive types"
-  | ((_,id),ntn,la,ar,lc)::rest ->
-      let rec check = function 
-	| []             -> [],[]
-  	| ((_,id),ntn,la',ar,lc)::rest ->
-            if (List.length la = List.length la') && 
-               (List.for_all2 eq_la la la')
-	    then
-	      let mcoes, mspec = check rest in
-	      let coes, lc' = extract_coe lc in
-	      (coes::mcoes,(id,ntn,ar,lc')::mspec)
-	    else 
-	      error ("Parameters should be syntactically the same "^
-		     "for each inductive type")
-      in
-      let mcoes, mspec = check rest in
-      let coes, lc' = extract_coe lc in
-      (coes,la,(id,ntn,ar,lc'):: mspec)
-
-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 _ = 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;
-  List.iter
-    (fun id -> 
-      Class.try_add_new_coercion (locate (make_short_qualid id)) Global) coes
-
-(* try to find non recursive definitions *)
-
-let list_chop_hd i l = match list_chop i l with
-  | (l1,x::l2) -> (l1,x,l2)
-  | _ -> assert false
+let build_mutual l finite =
+  let indl,ntnl = List.split l in
+  let paramsl = extract_params indl in
+  let coes = extract_coercions indl in
+  let notations,indl = prepare_inductive ntnl indl in
+  let mie = interp_mutual paramsl indl notations finite in
+  (* Declare the mutual inductive block with its eliminations *)
+  ignore (declare_mutual_with_eliminations false mie);
+  (* Declare the possible notations of inductive types *)
+  List.iter (declare_interning_data ([],[])) notations;
+  (* Declare the coercions *)
+  List.iter (fun qid -> Class.try_add_new_coercion (locate qid) Global) coes
+
+(* 3c| Fixpoints and co-fixpoints *)
+
+let recursive_message = function
+  | [] -> anomaly "no recursive definition"
+  | [id] -> pr_id id ++ str " is recursively defined"
+  | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+		    spc () ++ str "are recursively defined")
 
-let collect_non_rec env = 
-  let rec searchrec lnonrec lnamerec ldefrec larrec nrec = 
-    try
-      let i = 
-        list_try_find_i
-          (fun i f ->
-             if List.for_all (fun def -> not (occur_var env f def)) ldefrec
-             then i else failwith "try_find_i")
-          0 lnamerec 
-      in
-      let (lf1,f,lf2) = list_chop_hd i lnamerec in
-      let (ldef1,def,ldef2) = list_chop_hd i ldefrec in
-      let (lar1,ar,lar2) = list_chop_hd i larrec in
-      let newlnv = 
-	try 
-	  match list_chop i nrec with 
-            | (lnv1,_::lnv2) -> (lnv1@lnv2)
-	    | _ -> [] (* nrec=[] for cofixpoints *)
-        with Failure "list_chop" -> []
-      in 
-      searchrec ((f,def,ar)::lnonrec) 
-	(lf1@lf2) (ldef1@ldef2) (lar1@lar2) newlnv
-    with Failure "try_find_i" -> 
-      (List.rev lnonrec,
-       (Array.of_list lnamerec, Array.of_list ldefrec,
-        Array.of_list larrec, Array.of_list nrec))
-  in 
-  searchrec [] 
+let corecursive_message = function
+  | [] -> error "no corecursive definition"
+  | [id] -> pr_id id ++ str " is corecursively defined"
+  | l -> hov 0 (prlist_with_sep pr_coma pr_id l ++
+                    spc () ++ str "are corecursively defined")
 
-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()
-  and nv = Array.of_list (List.map (fun ((_,n,_,_,_),_) -> n) lnameargsardef)
-  and bl = Array.of_list (List.map (fun ((_,_,bl,_,_),_) -> bl) lnameargsardef) 
-  in 
-  (* Build the recursive context and notations for the recursive types *)
-  let (rec_sign,rec_impls,arityl) = 
-    List.fold_left 
-      (fun (env,impls,arl) ((recname,_,bl,arityc,_),_) -> 
-        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 env0 arity
-	  else [] in
-	let impls' =(recname,([],impl,compute_arguments_scope arity))::impls in
-        (Environ.push_named (recname,None,arity) env, impls', arity::arl))
-      (env0,[],[]) lnameargsardef in
-  let arityl = List.rev arityl in
-  let notations = 
-    List.fold_right (fun (_,ntnopt) l -> option_cons ntnopt l) 
-      lnameargsardef [] in
-
-  let recdef =
-
-    (* Declare local notations *)
-    let fs = States.freeze() in
-    let def = 
-      try
-	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_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
-    States.unfreeze fs; def 
-  in
+let recursive_message isfix = 
+  if isfix=Fixpoint then recursive_message else corecursive_message
 
-  let (lnonrec,(namerec,defrec,arrec,nvrec)) = 
-    collect_non_rec env0 lrecnames recdef arityl (Array.to_list nv) in
-  let recvec = 
-    Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
-  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
-  let nvrec = Array.mapi 
-    (fun i (n,_) -> match n with 
-       | Some n -> n 
-       | None -> 
-	   (* Recursive argument was not given by the user : 
-	      We check that there is only one inductive argument *)
-	   let ctx = snd (interp_context sigma env0 bl.(i)) in 
-	   let isIndApp t = isInd (fst (decompose_app (strip_head_cast t))) in 
-	   (* This could be more precise (e.g. do some delta) *)
-	   let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
-	   try (list_unique_index true lb) - 1
-	   with Not_found -> 
-	     error "the recursive argument needs to be specified")
-    nvrec
-  in  
-  let rec declare i fi =
-    let ce = 
-      { const_entry_body = mkFix ((nvrec,i),recdecls); (* ignore rec order *)
-        const_entry_type = Some arrec.(i);
-        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
-  if_verbose ppnl (recursive_message lrefrec);
-  (* The others are declared as normal definitions *)
-  let var_subst id = (id, global_reference id) in
-  let _ = 
-    List.fold_left
-      (fun subst (f,def,t) ->
-	 let ce = { const_entry_body = replace_vars subst def;
-		    const_entry_type = Some t;
-                    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))
-      lnonrec 
-  in
-  List.iter (fun (df,c,scope) ->
-    Metasyntax.add_notation_interpretation df [] c scope) notations
+(* An (unoptimized) function that maps preorders to partial orders...
 
-let build_corecursive lnameardef boxed = 
-  let lrecnames = List.map (fun (f,_,_,_) -> f) lnameardef
-  and sigma = Evd.empty
-  and env0 = Global.env() in
-  let fs = States.freeze() in
-  let (rec_sign,arityl) = 
-    try 
-      List.fold_left 
-        (fun (env,arl) (recname,bl,arityc,_) -> 
-           let arityc = generalize_constr_expr arityc bl in
-           let arity = interp_type Evd.empty env0 arityc in
-           let _ = declare_variable recname
-	     (Lib.cwd(),SectionLocalAssum arity,IsAssumption Definitional) in
-           (Environ.push_named (recname,None,arity) env, (arity::arl)))
-        (env0,[]) lnameardef
-    with e -> 
-      States.unfreeze fs; raise e in 
-  let arityl = List.rev arityl in
-  let recdef =
-    try 
-      List.map (fun (_,bl,arityc,def) ->
-        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)
-        lnameardef
-    with e -> 
-      States.unfreeze fs; raise e 
+   Input:  a list of associations (x,[y1;...;yn]), all yi distincts
+           and different of x, meaning x<=y1, ..., x<=yn
+
+   Output: a list of associations (x,Inr [y1;...;yn]), collecting all
+           distincts yi greater than x, _or_, (x, Inl y) meaning that
+           x is in the same class as y (in which case, x occurs
+           nowhere else in the association map)
+
+   partial_order : ('a * 'a list) list -> ('a * ('a,'a list) union) list
+*)
+
+let rec partial_order = function
+  | [] -> []
+  | (x,xge)::rest ->
+    let rec browse res xge' = function
+    | [] ->
+	let res = List.map (function
+	  | (z, Inr zge) when List.mem x zge -> (z, Inr (list_union zge xge'))
+	  | r -> r) res in
+	(x,Inr xge')::res
+    | y::xge -> 
+      let rec link y = 
+	try match List.assoc y res with
+	| Inl z -> link z
+	| Inr yge -> 
+	  if List.mem x yge then
+	    let res = List.remove_assoc y res in
+	    let res = List.map (function
+	      | (z, Inl t) ->
+		  if t = y then (z, Inl x) else (z, Inl t)
+	      | (z, Inr zge) ->
+		  if List.mem y zge then
+		    (z, Inr (list_add_set x (list_remove y zge)))
+		  else
+		    (z, Inr zge)) res in
+	    browse ((y,Inl x)::res) xge' (list_union xge (list_remove x yge))
+	  else
+	    browse res (list_add_set y (list_union xge' yge)) xge
+	with Not_found -> browse res (list_add_set y xge') xge
+      in link y
+    in browse (partial_order rest) [] xge 
+
+let non_full_mutual_message x xge y yge kind rest =
+  let reason = 
+    if List.mem x yge then 
+      string_of_id y^" depends on "^string_of_id x^" but not conversely"
+    else if List.mem y xge then 
+      string_of_id x^" depends on "^string_of_id y^" but not conversely"
+    else
+      string_of_id y^" and "^string_of_id x^" are not mutually dependent" in
+  let e = if rest <> [] then "e.g.: "^reason else reason in
+  let k = if kind=Fixpoint then "fixpoint" else "cofixpoint" in
+  let w =
+    if kind=Fixpoint then "Well-foundedness check may fail unexpectedly.\n"
+    else "" in
+  "Not a fully mutually defined "^k^"\n("^e^").\n"^w
+
+let check_mutuality env kind fixl =
+  let names = List.map fst fixl in
+  let preorder =
+    List.map (fun (id,def) -> 
+      (id, List.filter (fun id' -> id<>id' & occur_var env id' def) names))
+      fixl in
+  let po = partial_order preorder in
+  match List.filter (function (_,Inr _) -> true | _ -> false) po with
+    | (x,Inr xge)::(y,Inr yge)::rest ->
+	if_verbose warning (non_full_mutual_message x xge y yge kind rest)
+    | _ -> ()
+
+type fixpoint_kind =
+  | IsFixpoint of (int option * recursion_order_expr) list
+  | IsCoFixpoint
+
+type fixpoint_expr = {
+  fix_name : identifier;
+  fix_binders : local_binder list;
+  fix_body : constr_expr;
+  fix_type : constr_expr
+}
+
+let interp_fix_type isevars env fix =
+  interp_type_evars isevars env 
+    (generalize_constr_expr fix.fix_type fix.fix_binders)
+
+let interp_fix_body isevars env impls fix fixtype =
+  interp_casted_constr_evars isevars env ~impls
+    (abstract_constr_expr fix.fix_body fix.fix_binders) fixtype
+
+let declare_fix boxed kind f def t =
+  let ce = {
+    const_entry_body = def;
+    const_entry_type = Some t;
+    const_entry_opaque = false;
+    const_entry_boxed = boxed
+  } in
+  let kn = declare_constant f (DefinitionEntry ce,IsDefinition kind) in
+  ConstRef kn
+
+let prepare_recursive_declaration fixnames fixtypes fixdefs =
+  let defs = List.map (subst_vars (List.rev fixnames)) fixdefs in
+  let names = List.map (fun id -> Name id) fixnames in
+  (Array.of_list names, Array.of_list fixtypes, Array.of_list defs)
+
+let compute_guardness_evidence (n,_) fixl fixtype =
+  match n with 
+  | Some n -> n 
+  | None -> 
+      (* Recursive argument was not given by the user : 
+	 We check that there is only one inductive argument *)
+      let m = local_binders_length fixl.fix_binders in
+      let ctx = fst (Sign.decompose_prod_n_assum m fixtype) in
+      let isIndApp t = isInd (fst (decompose_app (strip_head_cast t))) in 
+      (* This could be more precise (e.g. do some delta) *)
+      let lb = List.rev_map (fun (_,_,t) -> isIndApp t) ctx in
+      try (list_unique_index true lb) - 1
+      with Not_found -> error "the recursive argument needs to be specified"
+
+let interp_recursive fixkind l boxed =
+  let env = Global.env() in
+  let fixl, ntnl = List.split l in
+  let kind = if fixkind <> IsCoFixpoint then Fixpoint else CoFixpoint in
+  let fixnames = List.map (fun fix -> fix.fix_name) fixl in
+
+  (* Interp arities allowing for unresolved types *)
+  let isevars = ref (Evd.create_evar_defs Evd.empty) in
+  let fixtypes = List.map (interp_fix_type isevars env) fixl in
+  let env_rec = push_named_types env fixnames fixtypes in
+
+  (* Get interpretation metadatas *)
+  let impls = compute_interning_datas env [] fixnames fixtypes in
+  let notations = List.fold_right option_cons ntnl [] in
+
+  (* Interp bodies with rollback because temp use of notations/implicit *)
+  let fixdefs = 
+    States.with_heavy_rollback (fun () -> 
+      List.iter (declare_interning_data impls) notations;
+      List.map2 (interp_fix_body isevars env_rec impls) fixl fixtypes)
+      () in
+
+  (* Instantiate evars and check all are resolved *)
+  let isevars,_ = consider_remaining_unif_problems env_rec !isevars in
+  let fixdefs = List.map (nf_evar (Evd.evars_of isevars)) fixdefs in
+  let fixtypes = List.map (nf_evar (Evd.evars_of isevars)) fixtypes in
+  List.iter (check_evars env_rec Evd.empty isevars) fixdefs;
+  check_mutuality env kind (List.combine fixnames fixdefs);
+
+  (* Build the fix declaration block *)
+  let fixdecls = prepare_recursive_declaration fixnames fixtypes fixdefs in
+  let fixdecls = 
+    match fixkind with
+    | IsFixpoint wfl ->
+	let fixwf = list_map3 compute_guardness_evidence wfl fixl fixtypes in
+	list_map_i (fun i _ -> mkFix ((Array.of_list fixwf,i),fixdecls)) 0 l
+    | IsCoFixpoint ->
+	list_map_i (fun i _ -> mkCoFix (i,fixdecls)) 0 l
   in
-  States.unfreeze fs;
-  let (lnonrec,(namerec,defrec,arrec,_)) = 
-    collect_non_rec env0 lrecnames recdef arityl [] in
-  let recvec = 
-    Array.map (subst_vars (List.rev (Array.to_list namerec))) defrec in
-  let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in
-  let rec declare i fi =
-    let ce = 
-      { const_entry_body = mkCoFix (i, recdecls);
-        const_entry_type = Some (arrec.(i));
-        const_entry_opaque = false;
-        const_entry_boxed = boxed } 
-    in
-    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);
-  let var_subst id = (id, global_reference id) in
-  let _ = 
-    List.fold_left
-      (fun subst (f,def,t) ->
-	 let ce = { const_entry_body = replace_vars subst def;
-		    const_entry_type = Some t;
-                    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))
-      lnonrec 
-  in ()
+
+  (* Declare the recursive definitions *)
+  ignore (list_map3 (declare_fix boxed kind) fixnames fixdecls fixtypes);
+  if_verbose ppnl (recursive_message kind fixnames);
+
+  (* Declare notations *)
+  List.iter (declare_interning_data ([],[])) notations
+
+let build_recursive l b =
+  let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
+  let fixl = List.map (fun ((id,_,bl,typ,def),ntn) -> 
+    ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
+    l in
+  interp_recursive (IsFixpoint g) fixl b
+
+let build_corecursive l b =
+  let fixl = List.map (fun ((id,bl,typ,def),ntn) -> 
+    ({fix_name = id; fix_binders = bl; fix_body = def; fix_type = typ},ntn))
+    l in
+  interp_recursive IsCoFixpoint fixl b
+
+(* 3d| Schemes *)
 
 let build_scheme lnamedepindsort = 
   let lrecnames = List.map (fun ((_,f),_,_,_) -> f) lnamedepindsort
@@ -637,8 +646,10 @@ let build_scheme lnamedepindsort =
     let kn = declare_constant fi (DefinitionEntry ce, IsDefinition Scheme) in
     ConstRef kn :: lrecref
   in 
-  let lrecref = List.fold_right2 declare listdecl lrecnames [] in
-  if_verbose ppnl (recursive_message (Array.of_list lrecref))
+  let _ = List.fold_right2 declare listdecl lrecnames [] in
+  if_verbose ppnl (recursive_message Fixpoint lrecnames)
+
+(* 4| Goal declaration *)
 
 let start_proof id kind c hook =
   let sign = Global.named_context () in
diff --git a/toplevel/command.mli b/toplevel/command.mli
index c93f69be..6f9a55c3 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 7682 2005-12-21 15:06:11Z herbelin $ i*)
+(*i $Id: command.mli 9110 2006-09-01 12:30:52Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -39,14 +39,14 @@ val syntax_definition : identifier -> constr_expr -> bool -> bool -> unit
 val declare_assumption : identifier located list ->
   coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> unit
 
-val build_mutual : inductive_expr list -> bool -> unit
+val build_mutual : (inductive_expr * decl_notation) list -> bool -> unit
 
 val declare_mutual_with_eliminations :
   bool -> Entries.mutual_inductive_entry -> mutual_inductive
 
 val build_recursive : (fixpoint_expr * decl_notation) list -> bool -> unit
 
-val build_corecursive : cofixpoint_expr list -> bool -> unit
+val build_corecursive : (cofixpoint_expr * decl_notation) list -> bool -> unit
 
 val build_scheme : (identifier located * bool * reference * rawsort) list -> unit
 
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 6d65ccc2..3374b0ee 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqtop.ml 8932 2006-06-09 09:29:03Z notin $ *)
+(* $Id: coqtop.ml 9191 2006-09-29 15:45:42Z courtieu $ *)
 
 open Pp
 open Util
@@ -21,18 +21,16 @@ open Coqinit
 
 let get_version_date () =
   try
-    let ch = open_in (Coq_config.coqtop^"/make.result") in
-    let l = input_line ch in
-    let i = String.index l ' ' in
-    let j = String.index_from l (i+1) ' ' in
-    "checked out on "^(String.sub l (i+1) (j-i-1))
-  with _ -> Coq_config.date
+    let ch = open_in (Coq_config.coqlib^"/revision") in
+    let ver = input_line ch in
+    let rev = input_line ch in
+      (ver,rev)
+  with _ -> (Coq_config.version,Coq_config.date)
 
 let print_header () =
-  Printf.printf "Welcome to Coq %s (%s)\n" 
-    Coq_config.version 
-    (get_version_date ());
-  flush stdout
+  let (ver,rev) = (get_version_date ()) in
+    Printf.printf "Welcome to Coq %s (%s)\n" ver rev;
+    flush stdout
 
 let memory_stat = ref false
 
@@ -249,6 +247,8 @@ let parse_args is_ide =
 
     | "-vm" :: rem -> use_vm := true; parse rem
     | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem
+    | "-emacs-U" :: rem -> Options.print_emacs := true; 
+	Options.print_emacs_safechar := true; Pp.make_pp_emacs(); parse rem
 	  
     | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index c011ba52..63a6ad07 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: discharge.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: discharge.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
 
 open Names
 open Util
@@ -73,7 +73,7 @@ let process_inductive sechyps modlist mib =
   let inds = 
     array_map_to_list
       (fun mip ->
-	 let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (mib,mip))) in
+	 let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (Global.env()) (mib,mip))) in
 	 let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
 	 (mip.mind_typename,
 	  arity,
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 73aaef30..b8e9eeda 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
+(* $Id: himsg.ml 9217 2006-10-05 17:31:23Z notin $ *)
 
 open Pp
 open Util
@@ -385,6 +385,14 @@ let explain_cannot_unify m n =
   str"Impossible to unify" ++ brk(1,1)  ++ pm ++ spc ()  ++
   str"with" ++ brk(1,1)  ++ pn
 
+let explain_cannot_unify_local env m n subn =
+  let pm = pr_lconstr m in 
+  let pn = pr_lconstr n in
+  let psubn = pr_lconstr_env env subn in
+    str"Impossible to unify" ++ brk(1,1)  ++ pm ++ spc ()  ++
+      str"with" ++ brk(1,1)  ++ pn ++ spc() ++ str"as" ++ brk(1,1) ++ 
+      psubn ++ str" contains local variables"
+
 let explain_refiner_cannot_generalize ty =
   str "Cannot find a well-typed generalisation of the goal with type : " ++ 
   pr_lconstr ty
@@ -455,6 +463,7 @@ let explain_pretype_error ctx err =
   | NotProduct c ->
       explain_not_product ctx c
   | CannotUnify (m,n) -> explain_cannot_unify m n
+  | CannotUnifyLocal (e,m,n,sn) -> explain_cannot_unify_local e m n sn
   | CannotGeneralize ty -> explain_refiner_cannot_generalize ty
   | NoOccurrenceFound c -> explain_no_occurrence_found c
   | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type m n
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 92ce6e36..3dcb1f58 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: metasyntax.ml 7822 2006-01-08 17:14:56Z herbelin $ *)
+(* $Id: metasyntax.ml 9333 2006-11-02 13:59:14Z barras $ *)
 
 open Pp
 open Util
@@ -50,7 +50,7 @@ let make_terminal_status = function
 let rec make_tags lev = function
   | VTerm s :: l -> make_tags lev l
   | VNonTerm (loc, nt, po) :: l ->
-      let (etyp, _) = Egrammar.interp_entry_name lev "tactic" nt in
+      let (etyp, _) = Egrammar.interp_entry_name lev nt in
       etyp :: make_tags lev l
   | [] -> []
 
@@ -112,6 +112,8 @@ let print_grammar univ = function
   | "tactic" -> 
       msgnl (str "Entry tactic_expr is");
       Gram.Entry.print Pcoq.Tactic.tactic_expr;
+      msgnl (str "Entry binder_tactic is");
+      Gram.Entry.print Pcoq.Tactic.binder_tactic;
       msgnl (str "Entry simple_tactic is");
       Gram.Entry.print Pcoq.Tactic.simple_tactic;
   | "vernac" -> 
@@ -399,6 +401,10 @@ 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] = '~')
 
+let is_prod_ident = function
+  | Terminal s when is_letter s.[0] or s.[0] = '_' -> true
+  | _ -> false
+
 let rec is_non_terminal = function
   | NonTerminal _ | SProdList _ -> true
   | _ -> false
@@ -437,10 +443,11 @@ let make_hunks etyps symbols from =
 	  else 
 	    UnpTerminal s :: add_break 1 (make NoBreak prods)
 	else if is_ident_tail s.[String.length s - 1] then
+	  let sep = if is_prod_ident (List.hd prods) then "" else " " in
 	  if ws = CanBreak then
-	    add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods)
+	    add_break 1 (UnpTerminal (s^sep) :: make CanBreak prods)
 	  else
-	    UnpTerminal (s^" ") :: make CanBreak prods
+	    UnpTerminal (s^sep) :: make CanBreak prods
 	else if ws = CanBreak then
 	  add_break 1 (UnpTerminal (s^" ") :: make CanBreak prods)
 	else
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 9eeeb51e..bf0271d9 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: record.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
+(* $Id: record.ml 9082 2006-08-24 17:03:28Z herbelin $ *)
 
 open Pp
 open Util
@@ -192,7 +192,6 @@ let declare_projections indsp coers fields =
    list telling if the corresponding fields must me declared as coercion *)
 let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   let coers,fs = List.split cfs in
-  let nparams = local_binders_length ps in
   let extract_name acc = function
       Vernacexpr.AssumExpr((_,Name id),_) -> id::acc
     | Vernacexpr.DefExpr ((_,Name id),_,_) -> id::acc
@@ -219,4 +218,4 @@ let definition_structure ((is_coe,(_,idstruc)),ps,cfs,idbuild,s) =
   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.declare_structure(rsp,idbuild,nparams,List.rev kinds,List.rev sp_projs)
+  Recordops.declare_structure(rsp,idbuild,List.rev kinds,List.rev sp_projs)
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 95c1b7d9..439e9254 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 8748 2006-04-27 16:01:26Z courtieu $ *)
+(* $Id: toplevel.ml 9252 2006-10-20 14:22:41Z herbelin $ *)
 
 open Pp
 open Util
@@ -48,11 +48,19 @@ let resynch_buffer ibuf =
     | _ -> ()
 
 
-(* Read a char in an input channel, displaying a prompt at every
-   beginning of line. *)
+(* emacs special character for prompt end (fast) detection. Prefer
+   (Char.chr 6) since it does not interfere with utf8. For
+    compatibility we let (Char.chr 249) as default for a while. *)
+
+let emacs_prompt_startstring() = 
+  if !Options.print_emacs_safechar then "<prompt>" else ""
 
-let emacs_prompt_endstring = String.make 1 (Char.chr 249)
+let emacs_prompt_endstring() = 
+  if !Options.print_emacs_safechar then "</prompt>"
+  else String.make 1 (Char.chr 249)
 
+(* Read a char in an input channel, displaying a prompt at every
+   beginning of line. *)
 let prompt_char ic ibuf count =
   let bol = match ibuf.bols with
     | ll::_ -> ibuf.len == ll
@@ -128,6 +136,7 @@ let print_highlight_location ib loc =
                       str sn ++ str dn) in 
 	  (l1 ++ li ++ ln)
   in 
+  let loc = make_loc (bp,ep) in
   (str"Toplevel input, characters " ++ Cerrors.print_loc loc ++ fnl () ++
      highlight_lines ++ fnl ())
 
@@ -214,14 +223,16 @@ let make_emacs_prompt() =
       (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 ^ " < " ^ emacs_prompt_endstring
+  statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < " ^ (emacs_prompt_endstring())
 
 (* 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() ^ Printer.emacs_str (make_emacs_prompt())
+    Printer.emacs_str (emacs_prompt_startstring()) 
+    ^ make_prompt() 
+    ^ Printer.emacs_str (make_emacs_prompt())
   in
   { prompt = pr;
     str = "";
@@ -232,7 +243,10 @@ let top_buffer =
 
 let set_prompt prompt =
   top_buffer.prompt
-  <- (fun () -> (prompt ())^(Printer.emacs_str (String.make 1 (Char.chr 249))))
+  <- (fun () -> 
+    Printer.emacs_str (emacs_prompt_startstring())
+    ^ prompt ()
+    ^ Printer.emacs_str (emacs_prompt_endstring()))
 
 (* Removes and prints the location of the error. The following exceptions
    need not be located. *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index afe72f0f..710b814d 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 8924 2006-06-08 17:49:01Z notin $ *)
+(* $Id: vernac.ml 9133 2006-09-12 14:52:07Z notin $ *)
 
 (* Parsing of vernacular. *)
 
@@ -162,12 +162,12 @@ let rec vernac_com interpfun (loc,com) =
     | v -> if not !just_parsing then interpfun v
 
   in 
-  try
-    if do_translate () then pr_new_syntax loc (Some com);
-    interp com
-  with e -> 
-    Format.set_formatter_out_channel stdout;
-    raise (DuringCommandInterp (loc, e))
+    try
+      if do_translate () then pr_new_syntax loc (Some com);
+      interp com
+    with e -> 
+      Format.set_formatter_out_channel stdout;
+      raise (DuringCommandInterp (loc, e))
 
 and vernac interpfun input =
   vernac_com interpfun (parse_phrase input)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index d384541f..35d202d9 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 9017 2006-07-05 17:27:34Z herbelin $ i*)
+(*i $Id: vernacentries.ml 9304 2006-10-28 09:58:16Z herbelin $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -20,6 +20,7 @@ open Term
 open Pfedit
 open Tacmach
 open Proof_trees
+open Decl_mode
 open Constrintern
 open Prettyp
 open Printer
@@ -93,7 +94,10 @@ let show_script () =
   let pts = get_pftreestate () in
   let pf = proof_of_pftreestate pts
   and evc = evc_of_pftreestate pts in
-  msgnl (print_treescript true evc (Global.named_context()) pf)
+  msgnl (print_treescript true evc pf)
+
+let show_thesis () =
+     msgnl (anomaly "TODO" )
 
 let show_top_evars () =
   let pfts = get_pftreestate () in 
@@ -111,39 +115,19 @@ let print_subgoals () = if_verbose (fun () -> msg (pr_open_subgoals ())) ()
 
   (* Simulate the Intro(s) tactic *)
 
-let fresh_id_of_name avoid gl = function
-    Anonymous -> Tactics.fresh_id avoid (id_of_string "H") gl
-  | Name id   -> Tactics.fresh_id avoid id gl
-
-let rec do_renum avoid gl = function
-    [] -> mt ()
-  | [n] -> pr_id (fresh_id_of_name avoid gl n)
-  | n :: l ->
-      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_letins (strip_outer_cast (pf_concl gl)) in
-  let nl = List.rev_map fst l in
-  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 l,_= Sign.decompose_prod_assum (strip_outer_cast (pf_concl gl)) in
+  if all 
+  then 
+    let lid = Tactics.find_intro_names l gl in 
+    msgnl (hov 0 (prlist_with_sep  spc pr_id lid))
+  else  
+    try  
+      let n = list_last l in
+      msgnl (pr_id (List.hd (Tactics.find_intro_names [n] gl)))
+    with Failure "list_last" -> message ""
 
 let id_of_name = function 
   | Names.Anonymous -> id_of_string "x" 
@@ -508,15 +492,14 @@ let vernac_end_section = Lib.close_section
 
 let vernac_end_segment id =
   check_no_pending_proofs ();
-  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 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
   Library.require_library qidl import
@@ -553,6 +536,7 @@ let vernac_identity_coercion stre id qids qidt =
 let vernac_solve n tcom b =
   if not (refining ()) then
     error "Unknown command of the non proof-editing mode";
+  Decl_mode.check_not_proof_mode "Unknown proof instruction";
   begin
     if b then 
       solve_nth n (Tacinterp.hide_interp tcom (get_end_tac ()))
@@ -563,7 +547,7 @@ let vernac_solve n tcom b =
   if subtree_solved () then begin
     Options.if_verbose msgnl (str "Subgoal proved");
     make_focus 0;
-    reset_top_of_tree ()
+    reset_top_of_script ()
   end;
   print_subgoals();
   if !pcoq <> None then (out_some !pcoq).solve n
@@ -580,8 +564,35 @@ 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) else ()
-      (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
-	
+    (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*)
+
+(***********************)
+(* Proof Language Mode *)
+
+let vernac_decl_proof () = 
+  check_not_proof_mode "Already in Proof Mode";
+  if tree_solved () then 
+    error "Nothing left to prove here."
+  else
+    begin
+      Decl_proof_instr.go_to_proof_mode ();
+      print_subgoals ()
+    end
+
+let vernac_return () = 
+  match get_current_mode () with
+      Mode_tactic ->
+	Decl_proof_instr.return_from_tactic_mode ();
+	print_subgoals ()
+    | Mode_proof -> 
+	error "\"return\" is only used after \"escape\"."
+    | Mode_none -> 
+	error "There is no proof to end." 
+
+let vernac_proof_instr instr = 
+  Decl_proof_instr.proof_instr instr;
+  print_subgoals ()
+
 (*****************************)
 (* Auxiliary file management *)
 
@@ -789,6 +800,14 @@ let _ =
       optread=Pp_control.get_margin;
       optwrite=Pp_control.set_margin }
 
+let _ =
+  declare_bool_option
+    { optsync=true;
+      optkey=SecondaryTable("Printing","Universes");
+      optname="the printing of universes";
+      optread=(fun () -> !Constrextern.print_universes);
+      optwrite=(fun b -> Constrextern.print_universes:=b) }
+
 let vernac_debug b =
   set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff)
 
@@ -1009,18 +1028,21 @@ let vernac_backtrack snum pnum naborts =
   for i = 1 to naborts do vernac_abort None done;
   undo_todepth pnum;
   vernac_backto snum;
+  Pp.flush_all();
   (* 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 ()
-  | Some n -> traverse_nth_goal n; print_subgoals ()
-
+let vernac_focus gln =
+  check_not_proof_mode "No focussing or Unfocussing in Proof Mode.";
+  match gln with 
+    | None -> traverse_nth_goal 1; print_subgoals ()
+    | Some n -> traverse_nth_goal n; print_subgoals ()
+	
   (* Reset the focus to the top of the tree *)
 let vernac_unfocus () =
-  make_focus 0; reset_top_of_tree (); print_subgoals ()
+  check_not_proof_mode "No focussing or Unfocussing in Proof Mode.";
+  make_focus 0; reset_top_of_script (); print_subgoals ()
 
 let vernac_go = function
   | GoTo n -> Pfedit.traverse n;show_node()
@@ -1039,7 +1061,7 @@ let apply_subproof f occ =
   f evc (Global.named_context()) pf
 
 let explain_proof occ =
-  msg (apply_subproof (print_treescript true) occ)
+  msg (apply_subproof (fun evd _ -> print_treescript true evd) occ)
 
 let explain_tree occ =
   msg (apply_subproof print_proof occ)
@@ -1063,9 +1085,11 @@ let vernac_show = function
       msgnl (prlist_with_sep pr_spc pr_id (Pfedit.get_all_proof_names()))
   | ShowIntros all -> show_intro all
   | ShowMatch id -> show_match id
+  | ShowThesis -> show_thesis ()
   | 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 in
@@ -1130,6 +1154,14 @@ let interp c = match c with
   | VernacSolve (n,tac,b) -> vernac_solve n tac b
   | VernacSolveExistential (n,c) -> vernac_solve_existential n c
 
+  (* MMode *)
+
+  | VernacDeclProof -> vernac_decl_proof ()
+  | VernacReturn -> vernac_return ()
+  | VernacProofInstr stp -> vernac_proof_instr stp 
+
+  (* /MMode *)
+
   (* Auxiliary file and library management *)
   | VernacRequireFrom (exp,spec,f) -> vernac_require_from exp spec f
   | VernacAddLoadPath (isrec,s,alias) -> vernac_add_loadpath isrec s alias
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 972d7ed9..9d514622 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 9017 2006-07-05 17:27:34Z herbelin $ i*)
+(*i $Id: vernacexpr.ml 9154 2006-09-20 17:18:18Z corbinea $ i*)
 
 open Util
 open Names
@@ -99,6 +99,7 @@ type showable =
   | ShowProofNames
   | ShowIntros of bool
   | ShowMatch of lident
+  | ShowThesis
   | ExplainProof of int list
   | ExplainTree of int list
 
@@ -146,8 +147,7 @@ type simple_binder = lident list  * constr_expr
 type 'a with_coercion = coercion_flag * 'a
 type constructor_expr = (lident * constr_expr) with_coercion
 type inductive_expr =
-     lident * decl_notation * local_binder list * constr_expr
-    * constructor_expr list
+     lident * local_binder list * constr_expr * constructor_expr list
 type definition_expr =
   | ProveBody of local_binder list * constr_expr
   | DefineBody of local_binder list * raw_red_expr option * constr_expr
@@ -195,9 +195,9 @@ type vernac_expr =
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
   | VernacAssumption of assumption_kind * simple_binder with_coercion list
-  | VernacInductive of inductive_flag * inductive_expr list
+  | VernacInductive of inductive_flag * (inductive_expr * decl_notation) list
   | VernacFixpoint of (fixpoint_expr * decl_notation) list * bool
-  | VernacCoFixpoint of cofixpoint_expr list * bool
+  | VernacCoFixpoint of (cofixpoint_expr * decl_notation) list * bool
   | VernacScheme of (lident * bool * lreference * sort_expr) list
 
   (* Gallina extensions *)
@@ -223,9 +223,17 @@ type vernac_expr =
       module_binder list * module_type_ast option
 
   (* Solving *)
+
   | VernacSolve of int * raw_tactic_expr * bool
   | VernacSolveExistential of int * constr_expr
 
+  (* Proof Mode *)
+
+  | VernacDeclProof
+  | VernacReturn
+  | VernacProofInstr of Decl_expr.raw_proof_instr
+
+
   (* Auxiliary file and library management *)
   | VernacRequireFrom of export_flag option * specif_flag option * lstring
   | VernacAddLoadPath of rec_flag * lstring * dir_path option