diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 18 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 34 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 7 | ||||
| -rw-r--r-- | toplevel/toplevel.ml | 23 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 3 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 38 | ||||
| -rw-r--r-- | toplevel/vernacexpr.ml | 7 |
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 |