diff options
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r-- | toplevel/vernacentries.ml | 287 |
1 files changed, 148 insertions, 139 deletions
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index cfa9bddc..b6a1a53f 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -76,9 +76,8 @@ let show_universes () = let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in let ctx = Evd.universe_context_set (Evd.nf_constraints sigma) in - let cstrs = Univ.merge_constraints (Univ.ContextSet.constraints ctx) Univ.empty_universes in msg_notice (Evd.pr_evar_universe_context (Evd.evar_universe_context sigma)); - msg_notice (str"Normalized constraints: " ++ Univ.pr_universes (Evd.pr_evd_level sigma) cstrs) + msg_notice (str"Normalized constraints: " ++ Univ.pr_universe_context_set (Evd.pr_evd_level sigma) ctx) let show_prooftree () = (* Spiwack: proof tree is currently not working *) @@ -102,17 +101,16 @@ let try_print_subgoals () = let show_intro all = let pf = get_pftreestate() in let {Evd.it=gls ; sigma=sigma; } = Proof.V82.subgoals pf in - let gl = {Evd.it=List.hd gls ; sigma = sigma; } in - let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in - if all - then - let lid = Tactics.find_intro_names l gl in - msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) - else - try + if not (List.is_empty gls) then begin + let gl = {Evd.it=List.hd gls ; sigma = sigma; } in + let l,_= decompose_prod_assum (strip_outer_cast (pf_concl gl)) in + if all then + let lid = Tactics.find_intro_names l gl in + msg_notice (hov 0 (prlist_with_sep spc pr_id lid)) + else if not (List.is_empty l) then let n = List.last l in msg_notice (pr_id (List.hd (Tactics.find_intro_names [n] gl))) - with Failure "List.last" -> () + end (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name @@ -351,7 +349,7 @@ let dump_universes_gen g s = try Univ.dump_universes output_constraint g; close (); - msg_info (str ("Universes written to file \""^s^"\".")) + msg_info (str "Universes written to file \"" ++ str s ++ str "\".") with reraise -> let reraise = Errors.push reraise in close (); @@ -366,8 +364,7 @@ let dump_universes sorted s = (* "Locate" commands *) let locate_file f = - let paths = Loadpath.get_paths () in - let _, file = System.find_file_in_path ~warn:false paths f in + let file = Flags.silently Loadpath.locate_file f in str file let msg_found_library = function @@ -379,17 +376,27 @@ let msg_found_library = function msg_info (hov 0 (pr_dirpath fulldir ++ strbrk " is bound to file " ++ str file)) -let err_unmapped_library loc qid = +let err_unmapped_library loc ?from qid = let dir = fst (repr_qualid qid) in + let prefix = match from with + | None -> str "." + | Some from -> + str " and prefix " ++ pr_dirpath from ++ str "." + in user_err_loc (loc,"locate_library", - strbrk "Cannot find a physical path bound to logical path " ++ - pr_dirpath dir ++ str".") + strbrk "Cannot find a physical path bound to logical path matching suffix " ++ + pr_dirpath dir ++ prefix) -let err_notfound_library loc qid = +let err_notfound_library loc ?from qid = + let prefix = match from with + | None -> str "." + | Some from -> + str " with prefix " ++ pr_dirpath from ++ str "." + in user_err_loc (loc,"locate_library", - strbrk "Unable to locate library " ++ pr_qualid qid ++ str".") + strbrk "Unable to locate library " ++ pr_qualid qid ++ prefix) let print_located_library r = let (loc,qid) = qualid_of_reference r in @@ -415,7 +422,9 @@ let vernac_syntax_extension locality local = let local = enforce_module_locality locality local in Metasyntax.add_syntax_extension local -let vernac_delimiters = Metasyntax.add_delimiters +let vernac_delimiters sc = function + | Some lr -> Metasyntax.add_delimiters sc lr + | None -> Metasyntax.remove_delimiters sc let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) @@ -450,7 +459,7 @@ let vernac_definition_hook p = function | SubClass -> Class.add_subclass_hook p | _ -> no_hook -let vernac_definition locality p (local,k) (loc,id as lid) def = +let vernac_definition locality p (local,k) ((loc,id as lid),pl) def = let local = enforce_locality_exp locality local in let hook = vernac_definition_hook p k in let () = match local with @@ -460,26 +469,27 @@ let vernac_definition locality p (local,k) (loc,id as lid) def = (match def with | ProveBody (bl,t) -> (* local binders, typ *) start_proof_and_print (local,p,DefinitionBody Definition) - [Some lid, (bl,t,None)] no_hook + [Some (lid,pl), (bl,t,None)] no_hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with | None -> None | Some r -> let (evc,env)= get_current_context () in Some (snd (interp_redexp env evc r)) in - do_definition id (local,p,k) bl red_option c typ_opt hook) + do_definition id (local,p,k) pl bl red_option c typ_opt hook) -let vernac_start_proof p kind l lettop = +let vernac_start_proof locality p kind l lettop = + let local = enforce_locality_exp locality None in if Dumpglob.dump () then List.iter (fun (id, _) -> match id with - | Some lid -> Dumpglob.dump_definition lid false "prf" + | Some (lid,_) -> Dumpglob.dump_definition lid false "prf" | None -> ()) l; if not(refining ()) then if lettop then errorlabstrm "Vernacentries.StartProof" (str "Let declarations can only be used in proof editing mode."); - start_proof_and_print (Global, p, Proof kind) l no_hook + start_proof_and_print (local, p, Proof kind) l no_hook let qed_display_script = ref true @@ -506,7 +516,7 @@ let vernac_assumption locality poly (local, kind) l nl = let kind = local, poly, kind in List.iter (fun (is_coe,(idl,c)) -> if Dumpglob.dump () then - List.iter (fun lid -> + List.iter (fun (lid, _) -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl) l; let status = do_assumptions kind nl l in @@ -514,11 +524,11 @@ let vernac_assumption locality poly (local, kind) l nl = let vernac_record k poly finite struc binders sort nameopt cfs = let const = match nameopt with - | None -> add_prefix "Build_" (snd (snd struc)) + | None -> add_prefix "Build_" (snd (fst (snd struc))) | Some (_,id as lid) -> Dumpglob.dump_definition lid false "constr"; id in if Dumpglob.dump () then ( - Dumpglob.dump_definition (snd struc) false "rec"; + Dumpglob.dump_definition (fst (snd struc)) false "rec"; List.iter (fun (((_, x), _), _) -> match x with | Vernacexpr.AssumExpr ((loc, Name id), _) -> Dumpglob.dump_definition (loc,id) false "proj" @@ -527,7 +537,7 @@ let vernac_record k poly finite struc binders sort nameopt cfs = let vernac_inductive poly lo finite indl = if Dumpglob.dump () then - List.iter (fun (((coe,lid), _, _, _, cstrs), _) -> + List.iter (fun (((coe,(lid,_)), _, _, _, cstrs), _) -> match cstrs with | Constructors cstrs -> Dumpglob.dump_definition lid false "ind"; @@ -542,12 +552,12 @@ let vernac_inductive poly lo finite indl = Errors.error "The Variant keyword cannot be used to define a record type. Use Record instead." | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> vernac_record (match b with Class true -> Class false | _ -> b) - poly finite id bl c oc fs + poly finite id bl c oc fs | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> let f = let (coe, ((loc, id), ce)) = l in let coe' = if coe then Some true else None in - (((coe', AssumExpr ((loc, Name id), ce)), None), []) + (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) poly finite id bl c None [f] | [ ( id , bl , c , Class true, _), _ ] -> Errors.error "Definitional classes must have a single method" @@ -567,13 +577,13 @@ let vernac_inductive poly lo finite indl = let vernac_fixpoint locality poly local l = let local = enforce_locality_exp locality local in if Dumpglob.dump () then - List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_fixpoint local poly l let vernac_cofixpoint locality poly local l = let local = enforce_locality_exp locality local in if Dumpglob.dump () then - List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; + List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_cofixpoint local poly l let vernac_scheme l = @@ -592,8 +602,19 @@ let vernac_combined_scheme lid l = List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l); Indschemes.do_combined_scheme lid l -let vernac_universe l = do_universe l -let vernac_constraint l = do_constraint l +let vernac_universe loc poly l = + if poly && not (Lib.sections_are_opened ()) then + user_err_loc (loc, "vernac_universe", + str"Polymorphic universes can only be declared inside sections, " ++ + str "use Monomorphic Universe instead"); + do_universe poly l + +let vernac_constraint loc poly l = + if poly && not (Lib.sections_are_opened ()) then + user_err_loc (loc, "vernac_constraint", + str"Polymorphic universe constraints can only be declared" + ++ str " inside sections, use Monomorphic Constraint instead"); + do_constraint poly l (**********************) (* Modules *) @@ -610,16 +631,14 @@ let vernac_declare_module export (loc, id) binders_ast mty_ast = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor declaration cannot be exported. " ^ - "Remove the \"Export\" and \"Import\" keywords from every functor " ^ - "argument.") + error "Arguments of a functor declaration cannot be exported. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast id binders_ast (Enforce mty_ast) [] in Dumpglob.dump_moddef loc mp "mod"; - if_verbose msg_info (str ("Module "^ Id.to_string id ^" is declared")); + if_verbose msg_info (str "Module " ++ pr_id id ++ str " is declared"); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = @@ -641,7 +660,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info - (str ("Interactive Module "^ Id.to_string id ^" started")); + (str "Interactive Module " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -651,9 +670,7 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor definition can be imported only if" ^ - " the definition is interactive. Remove the \"Export\" and " ^ - "\"Import\" keywords from every functor argument.") + error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_module Modintern.interp_module_ast @@ -661,14 +678,14 @@ let vernac_define_module export (loc, id) binders_ast mty_ast_o mexpr_ast_l = in Dumpglob.dump_moddef loc mp "mod"; if_verbose msg_info - (str ("Module "^ Id.to_string id ^" is defined")); + (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident (Loc.ghost,id)]) export let vernac_end_module export (loc,id as lid) = let mp = Declaremods.end_module () in Dumpglob.dump_modref loc mp "mod"; - if_verbose msg_info (str ("Module "^ Id.to_string id ^" is defined")); + if_verbose msg_info (str "Module " ++ pr_id id ++ str " is defined"); Option.iter (fun export -> vernac_import export [Ident lid]) export let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = @@ -690,7 +707,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef loc mp "modtype"; if_verbose msg_info - (str ("Interactive Module Type "^ Id.to_string id ^" started")); + (str "Interactive Module Type " ++ pr_id id ++ str " started"); List.iter (fun (export,id) -> Option.iter @@ -701,9 +718,7 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = let binders_ast = List.map (fun (export,idl,ty) -> if not (Option.is_empty export) then - error ("Arguments of a functor definition can be imported only if" ^ - " the definition is interactive. Remove the \"Export\" " ^ - "and \"Import\" keywords from every functor argument.") + error "Arguments of a functor definition can be imported only if the definition is interactive. Remove the \"Export\" and \"Import\" keywords from every functor argument." else (idl,ty)) binders_ast in let mp = Declaremods.declare_modtype Modintern.interp_module_ast @@ -711,12 +726,12 @@ let vernac_declare_module_type (loc,id) binders_ast mty_sign mty_ast_l = in Dumpglob.dump_moddef loc mp "modtype"; if_verbose msg_info - (str ("Module Type "^ Id.to_string id ^" is defined")) + (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_end_modtype (loc,id) = let mp = Declaremods.end_modtype () in Dumpglob.dump_modref loc mp "modtype"; - if_verbose msg_info (str ("Module Type "^ Id.to_string id ^" is defined")) + if_verbose msg_info (str "Module Type " ++ pr_id id ++ str " is defined") let vernac_include l = Declaremods.declare_include Modintern.interp_module_ast l @@ -765,8 +780,8 @@ let vernac_require from import qidl = let (_, dir, f) = Library.locate_qualified_library ?root ~warn qid in (dir, f) with - | Library.LibUnmappedDir -> err_unmapped_library loc qid - | Library.LibNotFound -> err_notfound_library loc qid + | Library.LibUnmappedDir -> err_unmapped_library loc ?from:root qid + | Library.LibNotFound -> err_notfound_library loc ?from:root qid in let modrefl = List.map locate qidl in if Dumpglob.dump () then @@ -868,20 +883,10 @@ let vernac_set_used_variables e = let vars = Environ.named_context env in List.iter (fun id -> if not (List.exists (fun (id',_,_) -> Id.equal id id') vars) then - error ("Unknown variable: " ^ Id.to_string id)) + errorlabstrm "vernac_set_used_variables" + (str "Unknown variable: " ++ pr_id id)) l; - let closure_l = List.map pi1 (set_used_variables l) in - let closure_l = List.fold_right Id.Set.add closure_l Id.Set.empty in - let vars_of = Environ.global_vars_set in - let aux env entry (all_safe,rest as orig) = - match entry with - | (x,None,_) -> - if Id.Set.mem x all_safe then orig else (all_safe, (Loc.ghost,x)::rest) - | (x,Some bo, ty) -> - let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in - if Id.Set.subset vars all_safe then (Id.Set.add x all_safe, rest) - else (all_safe, (Loc.ghost,x) :: rest) in - let _,to_clear = Environ.fold_named_context aux env ~init:(closure_l,[]) in + let _, to_clear = set_used_variables l in vernac_solve SelectAll None Tacexpr.(TacAtom (Loc.ghost,TacClear(false,to_clear))) false @@ -914,7 +919,7 @@ let vernac_chdir = function | Some path -> begin try Sys.chdir (expand path) - with Sys_error err -> msg_warning (str ("Cd failed: " ^ err)) + with Sys_error err -> msg_warning (str "Cd failed: " ++ str err) end; if_verbose msg_info (str (Sys.getcwd())) @@ -924,10 +929,12 @@ let vernac_chdir = function let vernac_write_state file = Pfedit.delete_all_proofs (); + let file = CUnix.make_suffix file ".coq" in States.extern_state file let vernac_restore_state file = Pfedit.delete_all_proofs (); + let file = Loadpath.locate_file (CUnix.make_suffix file ".coq") in States.intern_state file (************) @@ -1051,15 +1058,16 @@ let vernac_declare_arguments locality r l nargs flags = let inf_names = let ty = Global.type_of_global_unsafe sr in Impargs.compute_implicits_names (Global.env ()) ty in - let string_of_name = function Anonymous -> "_" | Name id -> Id.to_string id in let rec check li ld ls = match li, ld, ls with | [], [], [] -> () | [], Anonymous::ld, (Some _)::ls when extra_scope_flag -> check li ld ls | [], _::_, (Some _)::ls when extra_scope_flag -> error "Extra notation scopes can be set on anonymous arguments only" - | [], x::_, _ -> error ("Extra argument " ^ string_of_name x ^ ".") - | l, [], _ -> error ("The following arguments are not declared: " ^ - (String.concat ", " (List.map string_of_name l)) ^ ".") + | [], x::_, _ -> errorlabstrm "vernac_declare_arguments" + (str "Extra argument " ++ pr_name x ++ str ".") + | l, [], _ -> errorlabstrm "vernac_declare_arguments" + (str "The following arguments are not declared: " ++ + prlist_with_sep pr_comma pr_name l ++ str ".") | _::li, _::ld, _::ls -> check li ld ls | _ -> assert false in let () = match l with @@ -1087,9 +1095,6 @@ let vernac_declare_arguments locality r l nargs flags = let renamed_arg = ref None in let set_renamed a b = if Option.is_empty !renamed_arg && not (Id.equal a b) then renamed_arg := Some(b,a) in - let pr_renamed_arg () = match !renamed_arg with None -> "" - | Some (o,n) -> - "\nArgument "^string_of_id o ^" renamed to "^string_of_id n^"." in let some_renaming_specified = try let names = Arguments_renaming.arguments_names sr in @@ -1103,7 +1108,8 @@ let vernac_declare_arguments locality r l nargs flags = let sr', impl = List.fold_map (fun b -> function | (Anonymous, _,_, true, max), Name id -> assert false | (Name x, _,_, true, _), Anonymous -> - error ("Argument "^Id.to_string x^" cannot be declared implicit.") + errorlabstrm "vernac_declare_arguments" + (str "Argument " ++ pr_id x ++ str " cannot be declared implicit.") | (Name iid, _,_, true, max), Name id -> set_renamed iid id; b || not (Id.equal iid id), Some (ExplByName id, max, false) @@ -1116,8 +1122,12 @@ let vernac_declare_arguments locality r l nargs flags = some_renaming_specified l in if some_renaming_specified then if not (List.mem `Rename flags) then - error ("To rename arguments the \"rename\" flag must be specified." - ^ pr_renamed_arg ()) + errorlabstrm "vernac_declare_arguments" + (str "To rename arguments the \"rename\" flag must be specified." ++ + match !renamed_arg with + | None -> mt () + | Some (o,n) -> + str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".") else Arguments_renaming.rename_arguments (make_section_locality locality) sr names_decl; @@ -1175,8 +1185,9 @@ let default_env () = { let vernac_reserve bl = let sb_decl = (fun (idl,c) -> let env = Global.env() in - let t,ctx = Constrintern.interp_type env Evd.empty c in - let t = Detyping.detype false [] env Evd.empty t in + let sigma = Evd.from_env env in + let t,ctx = Constrintern.interp_type env sigma c in + let t = Detyping.detype false [] env (Evd.from_ctx ctx) t in let t = Notation_ops.notation_constr_of_glob_constr (default_env ()) t in Reserve.declare_reserved_type idl t) in List.iter sb_decl bl @@ -1348,19 +1359,10 @@ let _ = optwrite = Flags.make_universe_polymorphism } let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "use of virtual machine inside the kernel"; - optkey = ["Virtual";"Machine"]; - optread = (fun () -> Vconv.use_vm ()); - optwrite = (fun b -> Vconv.set_use_vm b) } - -let _ = declare_int_option { optsync = true; optdepr = false; - optname = "the level of inling duging functor application"; + optname = "the level of inlining during functor application"; optkey = ["Inline";"Level"]; optread = (fun () -> Some (Flags.get_inline_level ())); optwrite = (fun o -> @@ -1376,15 +1378,6 @@ let _ = optread = (fun () -> !Closure.share); optwrite = (fun b -> Closure.share := b) } -let _ = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "use of boxed values"; - optkey = ["Boxed";"Values"]; - optread = (fun _ -> not (Vm.transp_values ())); - optwrite = (fun b -> Vm.set_transp_values (not b)) } - (* No more undo limit in the new proof engine. The command still exists for compatibility (e.g. with ProofGeneral) *) @@ -1432,6 +1425,15 @@ let _ = optkey = ["Printing";"Universes"]; optread = (fun () -> !Constrextern.print_universes); optwrite = (fun b -> Constrextern.print_universes:=b) } + +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "dumping bytecode after compilation"; + optkey = ["Dump";"Bytecode"]; + optread = Flags.get_dump_bytecode; + optwrite = Flags.set_dump_bytecode } let vernac_debug b = set_debug (if b then Tactic_debug.DebugOn 0 else Tactic_debug.DebugOff) @@ -1478,6 +1480,8 @@ let vernac_set_opacity locality (v,l) = let vernac_set_option locality key = function | StringValue s -> set_string_option_value_gen locality key s + | StringOptValue (Some s) -> set_string_option_value_gen locality key s + | StringOptValue None -> unset_option_value_gen locality key | IntValue n -> set_int_option_value_gen locality key n | BoolValue b -> set_bool_option_value_gen locality key b @@ -1523,7 +1527,7 @@ let vernac_check_may_eval redexp glopt rc = let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in Evarconv.check_problems_are_solved env sigma'; let sigma',nf = Evarutil.nf_evars_and_universes sigma' in - let uctx = Evd.universe_context sigma' in + let pl, uctx = Evd.universe_context sigma' in let env = Environ.push_context uctx (Evarutil.nf_env_evar sigma' env) in let c = nf c in let j = @@ -1538,7 +1542,7 @@ let vernac_check_may_eval redexp glopt rc = let j = { j with Environ.uj_type = Reductionops.nf_betaiota sigma' j.Environ.uj_type } in msg_notice (print_judgment env sigma' j ++ pr_ne_evar_set (fnl () ++ str "where" ++ fnl ()) (mt ()) sigma' l ++ - Printer.pr_universe_ctx uctx) + Printer.pr_universe_ctx sigma uctx) | Some r -> Tacintern.dump_glob_red_expr r; let (sigma',r_interp) = interp_redexp env sigma' r in @@ -1555,7 +1559,7 @@ let vernac_global_check c = let sigma = Evd.from_env env in let c,ctx = interp_constr env sigma c in let senv = Global.safe_env() in - let cstrs = snd (Evd.evar_universe_context_set ctx) in + let cstrs = snd (Evd.evar_universe_context_set Univ.UContext.empty ctx) in let senv = Safe_typing.add_constraints cstrs senv in let j = Safe_typing.typing senv c in let env = Safe_typing.env_of_safe_env senv in @@ -1581,7 +1585,8 @@ let print_about_hyp_globs ref_or_by_not glnumopt = | Some n,AN (Ident (_loc,id)) -> (* goal number given, catch if wong *) (try get_nth_goal n,id with - Failure _ -> Errors.error ("No such goal: "^string_of_int n^".")) + Failure _ -> errorlabstrm "print_about_hyp_globs" + (str "No such goal: " ++ int n ++ str ".")) | _ , _ -> raise NoHyp in let hyps = pf_hyps gl in let (id,bdyopt,typ) = Context.lookup_named id hyps in @@ -1619,9 +1624,13 @@ let vernac_print = function msg_notice (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt)) | PrintCanonicalConversions -> msg_notice (Prettyp.print_canonical_projections ()) | PrintUniverses (b, None) -> - let univ = Global.universes () in - let univ = if b then Univ.sort_universes univ else univ in - msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ) + let univ = Global.universes () in + let univ = if b then Univ.sort_universes univ else univ in + let pr_remaining = + if Global.is_joined_environment () then mt () + else str"There may remain asynchronous universe constraints" + in + msg_notice (Univ.pr_universes Universes.pr_with_global_universes univ ++ pr_remaining) | PrintUniverses (b, Some s) -> dump_universes b s | PrintHint r -> msg_notice (Hints.pr_hint_ref (smart_global r)) | PrintHintGoal -> msg_notice (Hints.pr_applicable_hint ()) @@ -1640,10 +1649,11 @@ let vernac_print = function dump_global qid; msg_notice (print_impargs qid) | PrintAssumptions (o,t,r) -> (* Prints all the axioms and section variables used by a term *) - let cstr = printable_constr_of_global (smart_global r) in + let gr = smart_global r in + let cstr = printable_constr_of_global gr in let st = Conv_oracle.get_transp_state (Environ.oracle (Global.env())) in let nassums = - Assumptions.assumptions st ~add_opaque:o ~add_transparent:t cstr in + Assumptions.assumptions st ~add_opaque:o ~add_transparent:t gr cstr in msg_notice (Printer.pr_assumptionset (Global.env ()) nassums) | PrintStrategy r -> print_strategy r @@ -1674,8 +1684,8 @@ let interp_search_about_item env = (fun _ -> true) s sc in GlobSearchSubPattern (Pattern.PRef ref) with UserError _ -> - error ("Unable to interp \""^s^"\" either as a reference or \ - as an identifier component") + errorlabstrm "interp_search_about_item" + (str "Unable to interp \"" ++ str s ++ str "\" either as a reference or as an identifier component") let vernac_search s gopt r = let r = interp_search_restriction r in @@ -1776,6 +1786,7 @@ let vernac_show = function | OpenSubgoals -> pr_open_subgoals () | NthGoal n -> pr_nth_open_subgoal n | GoalId id -> pr_goal_by_id id + | GoalUid id -> pr_goal_by_uid id in msg_notice info | ShowGoalImplicitly None -> @@ -1817,23 +1828,11 @@ let vernac_load interp fname = match Pcoq.Gram.entry_parse Pcoq.main_entry po with | Some x -> x | None -> raise End_of_input) in - let open_utf8_file_in fname = - let is_bom s = - Int.equal (Char.code s.[0]) 0xEF && - Int.equal (Char.code s.[1]) 0xBB && - Int.equal (Char.code s.[2]) 0xBF - in - let in_chan = open_in fname in - let s = " " in - if input in_chan s 0 3 < 3 || not (is_bom s) then seek_in in_chan 0; - in_chan in let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in let fname = CUnix.make_suffix fname ".v" in let input = - let paths = Loadpath.get_paths () in - let _,longfname = - System.find_file_in_path ~warn:(Flags.is_verbose()) paths fname in + let longfname = Loadpath.locate_file fname in let in_chan = open_utf8_file_in longfname in Pcoq.Gram.parsable (Stream.of_channel in_chan) in try while true do interp (snd (parse_sentence input)) done @@ -1842,14 +1841,16 @@ let vernac_load interp fname = (* "locality" is the prefix "Local" attribute, while the "local" component * is the outdated/deprecated "Local" attribute of some vernacular commands - * still parsed as the obsolete_locality grammar entry for retrocompatibility *) -let interp ?proof locality poly c = + * still parsed as the obsolete_locality grammar entry for retrocompatibility. + * loc is the Loc.t of the vernacular command being interpreted. *) +let interp ?proof ~loc locality poly c = prerr_endline ("interpreting: " ^ Pp.string_of_ppcmds (Ppvernac.pr_vernac c)); match c with (* Done later in this file *) | VernacLoad _ -> assert false | VernacFail _ -> assert false | VernacTime _ -> assert false + | VernacRedirect _ -> assert false | VernacTimeout _ -> assert false | VernacStm _ -> assert false @@ -1872,7 +1873,7 @@ let interp ?proof locality poly c = (* Gallina *) | VernacDefinition (k,lid,d) -> vernac_definition locality poly k lid d - | VernacStartTheoremProof (k,l,top) -> vernac_start_proof poly k l top + | VernacStartTheoremProof (k,l,top) -> vernac_start_proof locality poly k l top | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl @@ -1881,8 +1882,8 @@ let interp ?proof locality poly c = | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l - | VernacUniverse l -> vernac_universe l - | VernacConstraint l -> vernac_constraint l + | VernacUniverse l -> vernac_universe loc poly l + | VernacConstraint l -> vernac_constraint loc poly l (* Modules *) | VernacDeclareModule (export,lid,bl,mtyo) -> @@ -1977,7 +1978,7 @@ let interp ?proof locality poly c = | VernacBacktrack _ -> msg_warning (str "VernacBacktrack not handled by Stm") (* Proof management *) - | VernacGoal t -> vernac_start_proof poly Theorem [None,([],t,None)] false + | VernacGoal t -> vernac_start_proof locality poly Theorem [None,([],t,None)] false | VernacFocus n -> vernac_focus n | VernacUnfocus -> vernac_unfocus () | VernacUnfocused -> vernac_unfocused () @@ -1986,10 +1987,16 @@ let interp ?proof locality poly c = | VernacEndSubproof -> vernac_end_subproof () | VernacShow s -> vernac_show s | VernacCheckGuard -> vernac_check_guard () - | VernacProof (None, None) -> () - | VernacProof (Some tac, None) -> vernac_set_end_tac tac - | VernacProof (None, Some l) -> vernac_set_used_variables l + | VernacProof (None, None) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:no" + | VernacProof (Some tac, None) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:no"; + vernac_set_end_tac tac + | VernacProof (None, Some l) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:no using:yes"; + vernac_set_used_variables l | VernacProof (Some tac, Some l) -> + Aux_file.record_in_aux_at loc "VernacProof" "tac:yes using:yes"; vernac_set_end_tac tac; vernac_set_used_variables l | VernacProofMode mn -> Proof_global.set_proof_mode mn (* Toplevel control *) @@ -2012,7 +2019,7 @@ let check_vernac_supports_locality c l = | VernacOpenCloseScope _ | VernacSyntaxExtension _ | VernacInfix _ | VernacNotation _ | VernacDefinition _ | VernacFixpoint _ | VernacCoFixpoint _ - | VernacAssumption _ + | VernacAssumption _ | VernacStartTheoremProof _ | VernacCoercion _ | VernacIdentityCoercion _ | VernacInstance _ | VernacDeclareInstances _ | VernacDeclareMLModule _ @@ -2039,7 +2046,7 @@ let check_vernac_supports_polymorphism c p = | VernacCoercion _ | VernacIdentityCoercion _ | VernacInstance _ | VernacDeclareInstances _ | VernacHints _ | VernacContext _ - | VernacExtend _ ) -> () + | VernacExtend _ | VernacUniverse _ | VernacConstraint _) -> () | Some _, _ -> Errors.error "This command does not support Polymorphism" let enforce_polymorphism = function @@ -2096,7 +2103,7 @@ let with_fail b f = | e -> let e = Errors.push e in raise (HasFailed (Errors.iprint - (Cerrors.process_vernac_interp_error ~with_header:false e)))) + (Cerrors.process_vernac_interp_error ~allow_uncaught:false ~with_header:false e)))) () with e when Errors.noncritical e -> let (e, _) = Errors.push e in @@ -2104,7 +2111,7 @@ let with_fail b f = | HasNotFailed -> errorlabstrm "Fail" (str "The command has not failed!") | HasFailed msg -> - if is_verbose () || !Flags.ide_slave then msg_info + if is_verbose () || !test_mode || !ide_slave then msg_info (str "The command has indeed failed with message:" ++ fnl () ++ msg) | _ -> assert false end @@ -2128,6 +2135,8 @@ let interp ?(verbosely=true) ?proof (loc,c) = | VernacTimeout (n,v) -> current_timeout := Some n; aux ?locality ?polymorphism isprogcmd v + | VernacRedirect (s, v) -> + Pp.with_output_to_file s (aux_list ?locality ?polymorphism isprogcmd) v; | VernacTime v -> System.with_time !Flags.time (aux_list ?locality ?polymorphism isprogcmd) v; @@ -2139,8 +2148,9 @@ let interp ?(verbosely=true) ?proof (loc,c) = Obligations.set_program_mode isprogcmd; try vernac_timeout begin fun () -> - if verbosely then Flags.verbosely (interp ?proof locality poly) c - else Flags.silently (interp ?proof locality poly) c; + if verbosely + then Flags.verbosely (interp ?proof ~loc locality poly) c + else Flags.silently (interp ?proof ~loc locality poly) c; if orig_program_mode || not !Flags.program_mode || isprogcmd then Flags.program_mode := orig_program_mode end @@ -2162,5 +2172,4 @@ let interp ?(verbosely=true) ?proof (loc,c) = else aux false c let () = Hook.set Stm.interp_hook interp -let () = Hook.set Stm.process_error_hook Cerrors.process_vernac_interp_error let () = Hook.set Stm.with_fail_hook with_fail |