summaryrefslogtreecommitdiff
path: root/toplevel/vernacentries.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/vernacentries.ml')
-rw-r--r--toplevel/vernacentries.ml287
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-26 06:01:18 +0000