summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/command.ml18
-rw-r--r--toplevel/himsg.ml34
-rw-r--r--toplevel/mltop.ml47
-rw-r--r--toplevel/toplevel.ml23
-rw-r--r--toplevel/vernac.ml3
-rw-r--r--toplevel/vernacentries.ml38
-rw-r--r--toplevel/vernacexpr.ml7
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