Imported Upstream version 8.1+dfsgupstream/8.1+dfsg

7 files changed, 75 insertions, 55 deletions

diff --git a/toplevel/command.ml b/toplevel/command.ml
index d751f70c..9ef782ff 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: command.ml 9310 2006-10-28 19:35:09Z herbelin $ *)
+(* $Id: command.ml 9617 2007-02-07 18:59:26Z herbelin $ *)
 
 open Pp
 open Util
@@ -216,12 +216,19 @@ let declare_one_elimination ind =
   let env = Global.env () in
   let sigma = Evd.empty in
   let elim_scheme = Indrec.build_indrec env sigma ind in
-  let npars = mib.mind_nparams_rec in
+  let npars = 
+    (* if a constructor of [ind] contains a recursive call, the scheme
+       is generalized only wrt recursively uniform parameters *)
+    if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs) 
+    then 
+      mib.mind_nparams_rec
+    else 
+      mib.mind_nparams in
   let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme 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 *)
+    (* in case the inductive has a type elimination, generates only one
+       induction scheme, the other ones share the same code with the
+       apropriate type *)
   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
@@ -588,6 +595,7 @@ let interp_recursive fixkind l boxed =
   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;
+  List.iter (check_evars env Evd.empty isevars) fixtypes;
   check_mutuality env kind (List.combine fixnames fixdefs);
 
   (* Build the fix declaration block *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index b8e9eeda..dc2cc8cd 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: himsg.ml 9217 2006-10-05 17:31:23Z notin $ *)
+(* $Id: himsg.ml 9528 2007-01-24 09:43:03Z herbelin $ *)
 
 open Pp
 open Util
@@ -96,22 +96,24 @@ let explain_elim_arity ctx ind sorts c pj okinds =
           "strong elimination on non-small inductive types leads to paradoxes."
 	| WrongArity ->
 	  "wrong arity" in
-	(hov 0 
-           (fnl () ++ str "Elimination of an inductive object of sort " ++
-            pki ++ brk(1,0) ++
-            str "is not allowed on a predicate in sort " ++ pkp  ++fnl () ++
-            str "because" ++ spc () ++ str explanation))
+      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
+      hov 0 
+	(str "the return type has sort" ++ spc() ++ ppt ++ spc() ++ 
+	 str "while it" ++ spc() ++ str "should be " ++ ppar ++ str ".") ++ 
+      fnl() ++ 
+      hov 0
+	(str "Elimination of an inductive object of sort " ++
+	 pki ++ brk(1,0) ++
+         str "is not allowed on a predicate in sort " ++ pkp ++ fnl() ++
+         str "because" ++ spc() ++ str explanation ++ str ".")
   | None -> 
-      mt ()
+      str "ill-formed elimination predicate."
   in
   hov 0 (
-  str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++
-  str "in the inductive type " ++ spc() ++ quote pi ++ 
-  (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
+    str "Incorrect elimination of" ++ spc() ++ pc ++ spc () ++
+    str "in the inductive type" ++ spc() ++ quote pi ++ str":") ++ 
+  fnl () ++ msg
 
 let explain_case_not_inductive ctx cj =
   let ctx = make_all_name_different ctx in
@@ -219,8 +221,8 @@ let explain_unexpected_type ctx actual_type expected_type =
 let explain_not_product ctx c =
   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
+  str"while it is expected to be" ++ 
+  if is_Type c then str " a sort" else (brk(1,1) ++ pr)
 
 (* TODO: use the names *)
 (* (co)fixpoints *)
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index a3b7fc14..4e6058be 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: mltop.ml4 6692 2005-02-06 13:03:51Z herbelin $ *)
+(* $Id: mltop.ml4 9397 2006-11-21 21:50:54Z herbelin $ *)
 
 open Util
 open Pp
@@ -42,9 +42,8 @@ open Vernacinterp
 
 (* This path is where we look for .cmo *)
 let coq_mlpath_copy = ref ["."]
-let keep_copy_mlpath s = 
-  let dir = glob s in
-  coq_mlpath_copy := dir :: !coq_mlpath_copy
+let keep_copy_mlpath path = 
+  coq_mlpath_copy := path :: !coq_mlpath_copy
 
 (* If there is a toplevel under Coq *)
 type toplevel = { 
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 439e9254..39106bbf 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: toplevel.ml 9252 2006-10-20 14:22:41Z herbelin $ *)
+(* $Id: toplevel.ml 9432 2006-12-12 09:07:36Z courtieu $ *)
 
 open Pp
 open Util
@@ -52,12 +52,9 @@ let resynch_buffer ibuf =
    (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_startstring() = Printer.emacs_str "" "<prompt>"
 
-let emacs_prompt_endstring() = 
-  if !Options.print_emacs_safechar then "</prompt>"
-  else String.make 1 (Char.chr 249)
+let emacs_prompt_endstring() = Printer.emacs_str (String.make 1 (Char.chr 249)) "</prompt>"
 
 (* Read a char in an input channel, displaying a prompt at every
    beginning of line. *)
@@ -223,16 +220,20 @@ 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()) *)
+  if !Options.print_emacs then statnum ^ " |" ^ pendingprompt ^ "| " ^ proof_info ^ " < "
+  else ""
+
 
 (* 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() = 
-    Printer.emacs_str (emacs_prompt_startstring()) 
+    emacs_prompt_startstring() 
     ^ make_prompt() 
-    ^ Printer.emacs_str (make_emacs_prompt())
+    ^ make_emacs_prompt()
+    ^ emacs_prompt_endstring()
   in
   { prompt = pr;
     str = "";
@@ -244,9 +245,9 @@ let top_buffer =
 let set_prompt prompt =
   top_buffer.prompt
   <- (fun () -> 
-    Printer.emacs_str (emacs_prompt_startstring())
+    emacs_prompt_startstring()
     ^ prompt ()
-    ^ Printer.emacs_str (emacs_prompt_endstring()))
+    ^ 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 710b814d..0bcf55a8 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: vernac.ml 9133 2006-09-12 14:52:07Z notin $ *)
+(* $Id: vernac.ml 9397 2006-11-21 21:50:54Z herbelin $ *)
 
 (* Parsing of vernacular. *)
 
@@ -119,6 +119,7 @@ let pr_new_syntax loc ocom =
 let rec vernac_com interpfun (loc,com) =
   let rec interp = function
     | VernacLoad (verbosely, fname) ->
+	let fname = expand_path_macros fname in
         (* translator state *)
         let ch = !chan_translate in
         let cs = Lexer.com_state() in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 35d202d9..248e0106 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 9304 2006-10-28 09:58:16Z herbelin $ i*)
+(*i $Id: vernacentries.ml 9481 2007-01-11 19:17:56Z herbelin $ i*)
 
 (* Concrete syntax of the mathematical vernacular MV V2.6 *)
 
@@ -284,8 +284,8 @@ let vernac_bind_scope sc cll =
 
 let vernac_open_close_scope = Notation.open_close_scope
 
-let vernac_arguments_scope qid scl =
-  Notation.declare_arguments_scope (global qid) scl
+let vernac_arguments_scope local qid scl =
+  Notation.declare_arguments_scope local (global qid) scl
 
 let vernac_infix = Metasyntax.add_infix
 
@@ -597,28 +597,34 @@ let vernac_proof_instr instr =
 (* Auxiliary file management *)
 
 let vernac_require_from export spec filename =
-  Library.require_library_from_file None filename export
+  Library.require_library_from_file None
+    (System.expand_path_macros filename)
+    export
 
 let vernac_add_loadpath isrec pdir ldiropt =
+  let pdir = System.expand_path_macros pdir in
   let alias = match ldiropt with
     | None -> Nameops.default_root_prefix
     | Some ldir -> ldir in
   (if isrec then Mltop.add_rec_path else Mltop.add_path) pdir alias
 
-let vernac_remove_loadpath = Library.remove_load_path
+let vernac_remove_loadpath path =
+  Library.remove_load_path (System.expand_path_macros path)
 
   (* Coq syntax for ML or system commands *)
 
-let vernac_add_ml_path isrec s =
-  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir) (System.glob s)
+let vernac_add_ml_path isrec path =
+  (if isrec then Mltop.add_rec_ml_dir else Mltop.add_ml_dir)
+    (System.expand_path_macros path)
 
-let vernac_declare_ml_module l = Mltop.declare_ml_modules l
+let vernac_declare_ml_module l =
+  Mltop.declare_ml_modules (List.map System.expand_path_macros l)
 
 let vernac_chdir = function
   | None -> message (Sys.getcwd())
-  | Some s ->
+  | Some path ->
       begin
-	try Sys.chdir (System.glob s)
+	try Sys.chdir (System.expand_path_macros path)
 	with Sys_error str -> warning ("Cd failed: " ^ str)
       end;
       if_verbose message (Sys.getcwd())
@@ -658,9 +664,11 @@ let vernac_hints = Auto.add_hints
 
 let vernac_syntactic_definition = Command.syntax_definition 
 
-let vernac_declare_implicits locqid = function
-  | Some imps -> Impargs.declare_manual_implicits (Nametab.global locqid) imps
-  | None -> Impargs.declare_implicits (Nametab.global locqid)
+let vernac_declare_implicits local locqid = function
+  | Some imps ->
+      Impargs.declare_manual_implicits local (Nametab.global locqid) imps
+  | None -> 
+      Impargs.declare_implicits local (Nametab.global locqid)
 
 let vernac_reserve idl c =
   let t = Constrintern.interp_type Evd.empty (Global.env()) c in
@@ -1114,7 +1122,7 @@ let interp c = match c with
   | 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
+  | VernacArgumentsScope (lcl,qid,scl) -> vernac_arguments_scope lcl qid scl
   | VernacInfix (local,mv,qid,sc) -> vernac_infix local mv qid sc
   | VernacNotation (local,c,infpl,sc) -> vernac_notation local c infpl sc
 
@@ -1184,7 +1192,7 @@ let interp c = match c with
   | VernacDeclareTacticDefinition (x,l) -> vernac_declare_tactic_definition x l
   | VernacHints (local,dbnames,hints) -> vernac_hints local dbnames hints
   | VernacSyntacticDefinition (id,c,l,b) ->vernac_syntactic_definition id c l b
-  | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits qid l
+  | VernacDeclareImplicits (local,qid,l) ->vernac_declare_implicits local qid l
   | VernacReserve (idl,c) -> vernac_reserve idl c
   | VernacSetOpacity (opaq, qidl) -> List.iter (vernac_set_opacity opaq) qidl
   | VernacSetOption (key,v) -> vernac_set_option key v
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9d514622..4c671787 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 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id: vernacexpr.ml 9481 2007-01-11 19:17:56Z herbelin $ i*)
 
 open Util
 open Names
@@ -180,7 +180,7 @@ type vernac_expr =
   | 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
+  | VernacArgumentsScope of locality_flag * lreference * scope_name option list
   | VernacInfix of locality_flag * (lstring * syntax_modifier list) *
       lreference * scope_name option
   | VernacNotation of
@@ -258,7 +258,8 @@ type vernac_expr =
   | VernacHints of locality_flag * lstring list * hints
   | VernacSyntacticDefinition of identifier * constr_expr * locality_flag *
       onlyparsing_flag
-  | VernacDeclareImplicits of lreference * explicitation list option
+  | VernacDeclareImplicits of locality_flag * lreference *
+      explicitation list option
   | VernacReserve of lident list * constr_expr
   | VernacSetOpacity of opacity_flag * lreference list
   | VernacUnsetOption of Goptions.option_name