Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

11 files changed, 93 insertions, 65 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7ff1b1b5..56a32f04 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 8689 2006-04-07 20:20:16Z herbelin $ *)
+(* $Id: command.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
 
 open Pp
 open Util
@@ -112,7 +112,7 @@ let constant_entry_of_com (bl,com,comtypopt,opacity,boxed) =
     | Some comtyp ->
 	(* We use a cast to avoid troubles with evars in comtyp *)
 	(* that can only be resolved knowing com *)
-	let b = abstract_constr_expr (mkCastC (com,DEFAULTcast,comtyp)) bl in
+	let b = abstract_constr_expr (mkCastC (com, Rawterm.CastConv DEFAULTcast,comtyp)) bl in
 	let (body,typ) = destSubCast (interp_constr sigma env b) in
 	{ const_entry_body = body;
 	  const_entry_type = Some typ;
@@ -219,7 +219,7 @@ let declare_one_elimination ind =
   let elim_scheme = Indrec.build_indrec env sigma ind 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
+  let kelim = elim_sorts (mib,mip) in
   (* in case the inductive has a type elimination, generates only one
      induction scheme, the other ones share the same code with the
      apropriate type *)
@@ -457,7 +457,9 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
   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) in
+  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 
@@ -502,9 +504,24 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list)
   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 ((Array.map fst nvrec,i),recdecls); (* ignore rec order *)
+      { 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
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index c3f79e0a..6d65ccc2 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: coqtop.ml 7740 2005-12-26 20:07:21Z herbelin $ *)
+(* $Id: coqtop.ml 8932 2006-06-09 09:29:03Z notin $ *)
 
 open Pp
 open Util
@@ -108,14 +108,16 @@ let add_compile verbose s =
   compile_list := (verbose,s) :: !compile_list
 let compile_files () =
   let init_state = States.freeze() in
-  List.iter
-    (fun (v,f) ->
-      States.unfreeze init_state;
-      if Options.do_translate () then
-	with_option translate_file (Vernac.compile v) f
-      else
-	Vernac.compile v f)
-    (List.rev !compile_list)
+  let coqdoc_init_state = Constrintern.coqdoc_freeze () in
+    List.iter
+      (fun (v,f) ->
+	 States.unfreeze init_state;
+	 Constrintern.coqdoc_unfreeze coqdoc_init_state;
+	 if Options.do_translate () then
+	   with_option translate_file (Vernac.compile v) f
+	 else
+	   Vernac.compile v f)
+      (List.rev !compile_list)
 
 let re_exec_version = ref ""
 let set_byte () = re_exec_version := "byte"
@@ -172,7 +174,11 @@ let ide_args = ref []
 let parse_args is_ide =
   let rec parse = function
     | [] -> ()
-
+    | "-with-geoproof" :: s :: rem -> 
+	if s = "yes" then Coq_config.with_geoproof := true
+	else if s = "no" then Coq_config.with_geoproof := false
+	else usage ();
+	parse rem
     | "-impredicative-set" :: rem -> 
         set_engagement Declarations.ImpredicativeSet; parse rem
 
@@ -242,9 +248,9 @@ 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
+    | "-emacs" :: rem -> Options.print_emacs := true; Pp.make_pp_emacs(); parse rem
 	  
-    | "-where" :: _ -> print_endline Coq_config.coqlib; exit 0
+    | "-where" :: _ -> print_endline (getenv_else "COQLIB" Coq_config.coqlib); exit 0
 
     | ("-quiet"|"-silent") :: rem -> Options.make_silent true; parse rem
 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 6c543079..c011ba52 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: discharge.ml 7493 2005-11-02 22:12:16Z mohring $ *)
+(* $Id: discharge.ml 8845 2006-05-23 07:41:58Z 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 mip.mind_user_arity in
+	 let arity = expmod_constr modlist (Termops.refresh_universes (Inductive.type_of_inductive (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 3fe51b5a..73aaef30 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml 8005 2006-02-07 22:50:35Z herbelin $ *)
+(* $Id: himsg.ml 8845 2006-05-23 07:41:58Z herbelin $ *)
 
 open Pp
 open Util
@@ -81,14 +81,14 @@ let rec pr_disjunction pr = function
   | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
   | [] -> assert false
 
-let explain_elim_arity ctx ind aritylst c pj okinds = 
+let explain_elim_arity ctx ind sorts c pj okinds = 
   let ctx = make_all_name_different ctx in
   let pi = pr_inductive ctx ind in
   let pc = pr_lconstr_env ctx c in
   let msg = match okinds with
   | Some(kp,ki,explanation) ->
-      let pki = pr_lconstr_env ctx ki in
-      let pkp = pr_lconstr_env ctx kp in
+      let pki = pr_sort_family ki in
+      let pkp = pr_sort_family kp in
       let explanation =	match explanation with
 	| NonInformativeToInformative ->
           "proofs can be eliminated only to build proofs"
@@ -107,13 +107,10 @@ 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 ++ 
-  (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 (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))
+  (let ppar = pr_disjunction (fun s -> quote (pr_sort_family s)) 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 =
@@ -565,14 +562,14 @@ let error_bad_entry () =
 
 let error_not_allowed_case_analysis dep kind i =
   str (if dep then "Dependent" else "Non Dependent") ++
-  str " case analysis on sort: " ++ print_sort kind ++ fnl () ++
+  str " case analysis on sort: " ++ pr_sort kind ++ fnl () ++
   str "is not allowed for inductive definition: " ++
   pr_inductive (Global.env()) i
 
 let error_bad_induction dep indid kind =
   str (if dep then "Dependent" else "Non dependent") ++
   str " induction for type " ++ pr_id indid ++
-  str " and sort " ++ print_sort kind ++ spc () ++
+  str " and sort " ++ pr_sort kind ++ spc () ++
   str "is not allowed"
 
 let error_not_mutual_in_scheme () =
diff --git a/toplevel/minicoq.ml b/toplevel/minicoq.ml
index 490765a4..a3b51a11 100644
--- a/toplevel/minicoq.ml
+++ b/toplevel/minicoq.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: minicoq.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
+(* $Id: minicoq.ml 8752 2006-04-27 19:37:33Z herbelin $ *)
 
 open Pp
 open Util
@@ -54,7 +54,7 @@ let check c =
 
 let definition id ty c =
   let c = globalize [] c in
-  let ty = option_app (globalize []) ty in
+  let ty = option_map (globalize []) ty in
   let ce = { const_entry_body = c; const_entry_type = ty } in
   let sp = make_path [] id CCI in
   env := add_constant sp ce (locals()) !env;
diff --git a/toplevel/record.ml b/toplevel/record.ml
index b24e85da..9eeeb51e 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: record.ml 7941 2006-01-28 23:07:59Z herbelin $ *)
+(* $Id: record.ml 8875 2006-05-29 19:59:11Z msozeau $ *)
 
 open Pp
 open Util
@@ -36,7 +36,7 @@ let interp_decl sigma env = function
   | Vernacexpr.DefExpr((_,id),c,t) ->
       let c = match t with
 	| None -> c
-	| Some t -> mkCastC (c,DEFAULTcast,t)
+	| Some t -> mkCastC (c, Rawterm.CastConv DEFAULTcast,t)
       in
       let j = interp_constr_judgment Evd.empty env c in
       (id,Some j.uj_val, j.uj_type)
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index a5c2564c..95c1b7d9 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 6947 2005-04-20 16:18:41Z coq $ *)
+(* $Id: toplevel.ml 8748 2006-04-27 16:01:26Z courtieu $ *)
 
 open Pp
 open Util
@@ -47,9 +47,12 @@ let resynch_buffer ibuf =
         ibuf.start <- ibuf.start + ll
     | _ -> ()
 
+
 (* Read a char in an input channel, displaying a prompt at every
    beginning of line. *)
 
+let emacs_prompt_endstring = String.make 1 (Char.chr 249)
+
 let prompt_char ic ibuf count =
   let bol = match ibuf.bols with
     | ll::_ -> ibuf.len == ll
@@ -204,7 +207,6 @@ let make_prompt () =
 *)
 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 = 
@@ -212,7 +214,7 @@ 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 ^ " < " ^ endchar
+  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",
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 354aff0b..782fdc80 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: usage.ml 6053 2004-09-03 14:33:35Z herbelin $ *)
+(* $Id: usage.ml 8932 2006-06-09 09:29:03Z notin $ *)
 
 let version () =
   Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
@@ -54,6 +54,7 @@ let print_usage_channel co command =
   -boot                  boot mode (implies -q and -batch)
   -emacs                 tells Coq it is executed under Emacs
   -dump-glob f           dump globalizations in file f (to be used by coqdoc)
+  -with-geoproof (yes|no) to (de)activate special functions for Geoproof within Coqide (default is yes)
   -impredicative-set     set sort Set impredicative
   -dont-load-proofs      don't load opaque proofs in memory
   -xml                   export XML files either to the hierarchy rooted in
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 64d77b74..afe72f0f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 7744 2005-12-27 09:16:06Z herbelin $ *)
+(* $Id: vernac.ml 8924 2006-06-08 17:49:01Z notin $ *)
 
 (* Parsing of vernacular. *)
 
@@ -126,27 +126,30 @@ let rec vernac_com interpfun (loc,com) =
         (* end translator state *)
         (* coqdoc state *)
         let cds = Constrintern.coqdoc_freeze() in
-        if !Options.translate_file then begin
-          let _,f = find_file_in_path (Library.get_load_paths ())
-            (make_suffix fname ".v") in
-          chan_translate := open_out (f^"8");
-          Pp.comments := []
-        end;
-        begin try
-          read_vernac_file verbosely (make_suffix fname ".v");
-          if !Options.translate_file then close_out !chan_translate;
-          chan_translate := ch;
-          Lexer.restore_com_state cs;
-          Pp.comments := cl;
-          Constrintern.coqdoc_unfreeze cds;
-        with e ->
-          if !Options.translate_file then close_out !chan_translate;
-          chan_translate := ch;
-          Lexer.restore_com_state cs;
-          Pp.comments := cl;
-          Constrintern.coqdoc_unfreeze cds;
-          raise e end;
-
+          if !Options.translate_file then 
+	    begin
+              let _,f = find_file_in_path (Library.get_load_paths ())
+		(make_suffix fname ".v") in
+		chan_translate := open_out (f^"8");
+		Pp.comments := []
+            end;
+          begin 
+	    try
+	      read_vernac_file verbosely (make_suffix fname ".v");
+              if !Options.translate_file then close_out !chan_translate;
+              chan_translate := ch;
+              Lexer.restore_com_state cs;
+              Pp.comments := cl;
+              Constrintern.coqdoc_unfreeze cds
+	    with e -> 
+	      if !Options.translate_file then close_out !chan_translate;
+              chan_translate := ch;
+              Lexer.restore_com_state cs;
+              Pp.comments := cl;
+              Constrintern.coqdoc_unfreeze cds;
+	      raise e
+	  end
+	      
     | VernacList l -> List.iter (fun (_,v) -> interp v) l
 
     | VernacTime v ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7394bd8f..033fb0e6 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 8700 2006-04-11 23:14:15Z courtieu $ i*)
+(*i $Id: vernacentries.ml 8751 2006-04-27 16:17:51Z courtieu $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -345,7 +345,7 @@ let vernac_start_proof kind sopt (bl,t) lettop hook =
 let vernac_end_proof = function
   | Admitted -> admit ()
   | Proved (is_opaque,idopt) ->
-    if_verbose show_script ();
+    if not !Options.print_emacs then if_verbose show_script ();
     match idopt with
     | None -> save_named is_opaque
     | Some ((_,id),None) -> save_anonymous is_opaque id
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index a2bcd990..bcd89490 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 6616 2005-01-21 17:18:23Z herbelin $ i*)
+(*i $Id: vernacentries.mli 8781 2006-05-03 10:15:05Z jforest $ i*)
 
 (*i*)
 open Names
@@ -52,3 +52,5 @@ val set_pcoq_hook : pcoq_hook -> unit
 val abort_refine : ('a -> unit) -> 'a -> unit;;
 
 val interp : Vernacexpr.vernac_expr -> unit
+
+val vernac_reset_name : identifier Util.located -> unit