aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml12
-rw-r--r--toplevel/auto_ind_decl.mli2
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/coqloop.ml4
-rw-r--r--toplevel/coqtop.ml1
-rw-r--r--toplevel/himsg.ml3
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/metasyntax.ml75
-rw-r--r--toplevel/record.ml4
-rw-r--r--toplevel/search.ml50
-rw-r--r--toplevel/usage.ml2
-rw-r--r--toplevel/vernacentries.ml119
12 files changed, 185 insertions, 91 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 5171473a1..b1811d6a6 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -55,7 +55,7 @@ exception EqUnknown of string
exception UndefinedCst of string
exception InductiveWithProduct
exception InductiveWithSort
-exception ParameterWithoutEquality of constant
+exception ParameterWithoutEquality of global_reference
exception NonSingletonProp of inductive
exception DecidabilityMutualNotSupported
@@ -182,7 +182,13 @@ let build_beq_scheme mode kn =
let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in
match kind_of_term c with
| Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants
- | Var x -> mkVar (id_of_string ("eq_"^(string_of_id x))), Safe_typing.empty_private_constants
+ | Var x ->
+ let eid = id_of_string ("eq_"^(string_of_id x)) in
+ let () =
+ try ignore (Environ.lookup_named eid env)
+ with Not_found -> raise (ParameterWithoutEquality (VarRef x))
+ in
+ mkVar eid, Safe_typing.empty_private_constants
| Cast (x,_,_) -> aux (applist (x,a))
| App _ -> assert false
| Ind ((kn',i as ind'),u) (*FIXME: universes *) ->
@@ -210,7 +216,7 @@ let build_beq_scheme mode kn =
| LetIn _ -> raise (EqUnknown "LetIn")
| Const kn ->
(match Environ.constant_opt_value_in env kn with
- | None -> raise (ParameterWithoutEquality (fst kn))
+ | None -> raise (ParameterWithoutEquality (ConstRef (fst kn)))
| Some c -> aux (applist (c,a)))
| Proj _ -> raise (EqUnknown "Proj")
| Construct _ -> raise (EqUnknown "Construct")
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index b6c66a1e8..fa5c61484 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -21,7 +21,7 @@ exception EqUnknown of string
exception UndefinedCst of string
exception InductiveWithProduct
exception InductiveWithSort
-exception ParameterWithoutEquality of constant
+exception ParameterWithoutEquality of Globnames.global_reference
exception NonSingletonProp of inductive
exception DecidabilityMutualNotSupported
diff --git a/toplevel/command.mli b/toplevel/command.mli
index d35372429..616afb91f 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -22,7 +22,7 @@ open Pfedit
val do_universe : polymorphic -> Id.t Loc.located list -> unit
val do_constraint : polymorphic ->
- (Id.t Loc.located * Univ.constraint_type * Id.t Loc.located) list -> unit
+ (Misctypes.glob_level * Univ.constraint_type * Misctypes.glob_level) list -> unit
(** {6 Hooks for Pcoq} *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index 0d4807e16..69d68bd35 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -348,5 +348,7 @@ let rec loop () =
| any ->
Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++
str (Printexc.to_string any) ++
- fnl() ++ str"Please report.");
+ fnl() ++
+ str"Please report" ++
+ strbrk" at " ++ str Coq_config.wwwbugtracker ++ str ".");
loop ()
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index ee331e37c..47d433d79 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -523,6 +523,7 @@ let parse_args arglist =
|"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ())
|"-outputstate" -> set_outputstate (next ())
|"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0
+ |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ())
|"-require" -> add_require (next ())
|"-top" -> set_toplevel_name (dirpath_of_string (next ()))
|"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ())
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 670d30c6c..66781a8c3 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -303,7 +303,8 @@ let explain_unification_error env sigma p1 p2 = function
else []
| MetaOccurInBody evk ->
[str "instance for " ++ quote (pr_existential_key sigma evk) ++
- strbrk " refers to a metavariable - please report your example"]
+ strbrk " refers to a metavariable - please report your example" ++
+ strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."]
| InstanceNotSameType (evk,env,t,u) ->
let t, u = pr_explicit env sigma t u in
[str "unable to find a well-typed instantiation for " ++
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index e0b861e0a..48521a8e5 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -161,7 +161,7 @@ let try_declare_scheme what f internal names kn =
let msg = match fst e with
| ParameterWithoutEquality cst ->
alarm what internal
- (str "Boolean equality not found for parameter " ++ pr_con cst ++
+ (str "Boolean equality not found for parameter " ++ Printer.pr_global cst ++
str".")
| InductiveWithProduct ->
alarm what internal
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index bbec5b72d..ec45c7ed8 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -682,8 +682,13 @@ type syntax_extension = {
synext_notgram : notation_grammar;
synext_unparsing : unparsing list;
synext_extra : (string * string) list;
+ synext_compat : Flags.compat_version option;
}
+let is_active_compat = function
+| None -> true
+| Some v -> 0 <= Flags.version_compare v !Flags.compat_version
+
type syntax_extension_obj = locality_flag * syntax_extension list
let cache_one_syntax_extension se =
@@ -694,13 +699,15 @@ let cache_one_syntax_extension se =
let oldprec = Notation.level_of_notation ntn in
if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec
with Not_found ->
- (* Reserve the notation level *)
- Notation.declare_notation_level ntn prec;
- (* Declare the parsing rule *)
- if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram;
- (* Declare the notation rule *)
- Notation.declare_notation_rule ntn
- ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram
+ if is_active_compat se.synext_compat then begin
+ (* Reserve the notation level *)
+ Notation.declare_notation_level ntn prec;
+ (* Declare the parsing rule *)
+ if not onlyprint then Egramcoq.extend_constr_grammar prec se.synext_notgram;
+ (* Declare the notation rule *)
+ Notation.declare_notation_rule ntn
+ ~extra:se.synext_extra (se.synext_unparsing, fst prec) se.synext_notgram
+ end
let cache_syntax_extension (_, (_, sy)) =
List.iter cache_one_syntax_extension sy
@@ -734,9 +741,10 @@ let inSyntaxExtension : syntax_extension_obj -> obj =
let interp_modifiers modl =
let onlyparsing = ref false in
let onlyprinting = ref false in
+ let compat = ref None in
let rec interp assoc level etyps format extra = function
| [] ->
- (assoc,level,etyps,!onlyparsing,!onlyprinting,format,extra)
+ (assoc,level,etyps,!onlyparsing,!onlyprinting,!compat,format,extra)
| SetEntryType (s,typ) :: l ->
let id = Id.of_string s in
if Id.List.mem_assoc id etyps then
@@ -758,12 +766,15 @@ let interp_modifiers modl =
| SetAssoc a :: l ->
if not (Option.is_empty assoc) then error"An associativity is given more than once.";
interp (Some a) level etyps format extra l
- | SetOnlyParsing _ :: l ->
+ | SetOnlyParsing :: l ->
onlyparsing := true;
interp assoc level etyps format extra l
| SetOnlyPrinting :: l ->
onlyprinting := true;
interp assoc level etyps format extra l
+ | SetCompatVersion v :: l ->
+ compat := Some v;
+ interp assoc level etyps format extra l
| SetFormat ("text",s) :: l ->
if not (Option.is_empty format) then error "A format is given more than once.";
interp assoc level etyps (Some s) extra l
@@ -772,7 +783,7 @@ let interp_modifiers modl =
in interp None None [] None [] modl
let check_infix_modifiers modifiers =
- let (_, _, t, _, _, _, _) = interp_modifiers modifiers in
+ let (_, _, t, _, _, _, _, _) = interp_modifiers modifiers in
if not (List.is_empty t) then
error "Explicit entry level or type unexpected in infix notation."
@@ -784,20 +795,25 @@ let check_useless_entry_types recvars mainvars etyps =
| _ -> ()
let not_a_syntax_modifier = function
-| SetOnlyParsing _ -> true
+| SetOnlyParsing -> true
| SetOnlyPrinting -> true
+| SetCompatVersion _ -> true
| _ -> false
let no_syntax_modifiers mods = List.for_all not_a_syntax_modifier mods
let is_only_parsing mods =
- let test = function SetOnlyParsing _ -> true | _ -> false in
+ let test = function SetOnlyParsing -> true | _ -> false in
List.exists test mods
let is_only_printing mods =
let test = function SetOnlyPrinting -> true | _ -> false in
List.exists test mods
+let get_compat_version mods =
+ let test = function SetCompatVersion v -> Some v | _ -> None in
+ try Some (List.find_map test mods) with Not_found -> None
+
(* Compute precedences from modifiers (or find default ones) *)
let set_entry_type etyps (x,typ) =
@@ -975,7 +991,7 @@ let remove_curly_brackets l =
in aux true l
let compute_syntax_data df modifiers =
- let (assoc,n,etyps,onlyparse,onlyprint,fmt,extra) = interp_modifiers modifiers in
+ let (assoc,n,etyps,onlyparse,onlyprint,compat,fmt,extra) = interp_modifiers modifiers in
let assoc = match assoc with None -> (* default *) Some NonA | a -> a in
let toks = split_notation_string df in
let (recvars,mainvars,symbols) = analyze_notation_tokens toks in
@@ -1001,12 +1017,12 @@ let compute_syntax_data df modifiers =
let sy_data = (n,sy_typs,symbols',fmt) in
let sy_fulldata = (i_typs,ntn_for_grammar,prec,need_squash,sy_data) in
let df' = ((Lib.library_dp(),Lib.current_dirpath true),df) in
- let i_data = (onlyparse,onlyprint,recvars,mainvars,(ntn_for_interp,df')) in
+ let i_data = (onlyparse,onlyprint,compat,recvars,mainvars,(ntn_for_interp,df')) in
(* Return relevant data for interpretation and for parsing/printing *)
(msgs,i_data,i_typs,sy_fulldata,extra)
let compute_pure_syntax_data df mods =
- let (msgs,(onlyparse,onlyprint,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
+ let (msgs,(onlyparse,onlyprint,_,_,_,_),_,sy_data,extra) = compute_syntax_data df mods in
let msgs =
if onlyparse then
(Feedback.msg_warning ?loc:None,
@@ -1023,6 +1039,7 @@ type notation_obj = {
notobj_interp : interpretation;
notobj_onlyparse : bool;
notobj_onlyprint : bool;
+ notobj_compat : Flags.compat_version option;
notobj_notation : notation * notation_location;
}
@@ -1033,7 +1050,9 @@ let open_notation i (_, nobj) =
let scope = nobj.notobj_scope in
let (ntn, df) = nobj.notobj_notation in
let pat = nobj.notobj_interp in
- if Int.equal i 1 && not (Notation.exists_notation_in_scope scope ntn pat) then begin
+ let fresh = not (Notation.exists_notation_in_scope scope ntn pat) in
+ let active = is_active_compat nobj.notobj_compat in
+ if Int.equal i 1 && fresh && active then begin
(* Declare the interpretation *)
let onlyprint = nobj.notobj_onlyprint in
let () = Notation.declare_notation_interpretation ntn scope pat df ~onlyprint in
@@ -1103,7 +1122,9 @@ let recover_syntax ntn =
synext_notation = ntn;
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
- synext_extra = pp_extra_rules }
+ synext_extra = pp_extra_rules;
+ synext_compat = None;
+ }
with Not_found ->
raise NoSyntaxRule
@@ -1137,7 +1158,7 @@ let make_pp_rule (n,typs,symbols,fmt) =
| None -> [UnpBox (PpHOVB 0, make_hunks typs symbols n)]
| Some fmt -> hunks_of_format (n, List.split typs) (symbols, parse_format fmt)
-let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint =
+let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint compat =
let pa_rule = make_pa_rule i_typs sy_data ntn onlyprint in
let pp_rule = make_pp_rule sy_data in
let sy = {
@@ -1146,6 +1167,7 @@ let make_syntax_rules (i_typs,ntn,prec,need_squash,sy_data) extra onlyprint =
synext_notgram = pa_rule;
synext_unparsing = pp_rule;
synext_extra = extra;
+ synext_compat = compat;
} in
(* By construction, the rule for "{ _ }" is declared, but we need to
redeclare it because the file where it is declared needs not be open
@@ -1162,9 +1184,9 @@ let to_map l =
let add_notation_in_scope local df c mods scope =
let (msgs,i_data,i_typs,sy_data,extra) = compute_syntax_data df mods in
(* Prepare the interpretation *)
- let (onlyparse, onlyprint, recvars,mainvars, df') = i_data in
+ let (onlyparse, onlyprint, compat, recvars,mainvars, df') = i_data in
(* Prepare the parsing and printing rules *)
- let sy_rules = make_syntax_rules sy_data extra onlyprint in
+ let sy_rules = make_syntax_rules sy_data extra onlyprint compat in
let i_vars = make_internalization_vars recvars mainvars i_typs in
let nenv = {
ninterp_var_type = to_map i_vars;
@@ -1182,6 +1204,7 @@ let add_notation_in_scope local df c mods scope =
(** Order is important here! *)
notobj_onlyparse = onlyparse;
notobj_onlyprint = onlyprint;
+ notobj_compat = compat;
notobj_notation = df';
} in
(* Ready to change the global state *)
@@ -1190,7 +1213,7 @@ let add_notation_in_scope local df c mods scope =
Lib.add_anonymous_leaf (inNotation notation);
df'
-let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint =
+let add_notation_interpretation_core local df ?(impls=empty_internalization_env) c scope onlyparse onlyprint compat =
let dfs = split_notation_string df in
let (recvars,mainvars,symbs) = analyze_notation_tokens dfs in
(* Recover types of variables and pa/pp rules; redeclare them if needed *)
@@ -1221,6 +1244,7 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
(** Order is important here! *)
notobj_onlyparse = onlyparse;
notobj_onlyprint = onlyprint;
+ notobj_compat = compat;
notobj_notation = df';
} in
Lib.add_anonymous_leaf (inNotation notation);
@@ -1230,19 +1254,19 @@ let add_notation_interpretation_core local df ?(impls=empty_internalization_env)
let add_syntax_extension local ((loc,df),mods) =
let msgs, sy_data, extra, onlyprint = compute_pure_syntax_data df mods in
- let sy_rules = make_syntax_rules sy_data extra onlyprint in
+ let sy_rules = make_syntax_rules sy_data extra onlyprint None in
Flags.if_verbose (List.iter (fun (f,x) -> f x)) msgs;
Lib.add_anonymous_leaf (inSyntaxExtension(local,sy_rules))
(* Notations with only interpretation *)
let add_notation_interpretation ((loc,df),c,sc) =
- let df' = add_notation_interpretation_core false df c sc false false in
+ let df' = add_notation_interpretation_core false df c sc false false None in
Dumpglob.dump_notation (loc,df') sc true
let set_notation_for_interpretation impls ((_,df),c,sc) =
(try ignore
- (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false) ());
+ (silently (fun () -> add_notation_interpretation_core false df ~impls c sc false false None) ());
with NoSyntaxRule ->
error "Parsing rule for this notation has to be previously declared.");
Option.iter (fun sc -> Notation.open_close_scope (false,true,sc)) sc
@@ -1255,7 +1279,8 @@ let add_notation local c ((loc,df),modifiers) sc =
(* No syntax data: try to rely on a previously declared rule *)
let onlyparse = is_only_parsing modifiers in
let onlyprint = is_only_printing modifiers in
- try add_notation_interpretation_core local df c sc onlyparse onlyprint
+ let compat = get_compat_version modifiers in
+ try add_notation_interpretation_core local df c sc onlyparse onlyprint compat
with NoSyntaxRule ->
(* Try to determine a default syntax rule *)
add_notation_in_scope local df c modifiers sc
diff --git a/toplevel/record.ml b/toplevel/record.ml
index de056fa9b..a8f8c9293 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -523,11 +523,9 @@ let add_inductive_class ind =
| LocalDef _ -> None
| LocalAssum (_, t) -> Some (lazy t)
in
- let args = List.map_filter map ctx in
- let ty = Inductive.type_of_inductive_knowing_parameters
+ let ty = Inductive.type_of_inductive
(push_rel_context ctx (Global.env ()))
((mind,oneind),inst)
- (Array.of_list args)
in
{ cl_impl = IndRef ind;
cl_context = List.map (const None) ctx, ctx;
diff --git a/toplevel/search.ml b/toplevel/search.ml
index d1c108c37..4e1b00533 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -155,8 +155,9 @@ let full_name_of_reference ref =
DirPath.to_string dir ^ "." ^ Id.to_string id
(** Whether a reference is blacklisted *)
-let blacklist_filter ref env typ =
+let blacklist_filter_aux () =
let l = SearchBlacklist.elements () in
+ fun ref env typ ->
let name = full_name_of_reference ref in
let is_not_bl str = not (String.string_contains ~where:name ~what:str) in
List.for_all is_not_bl l
@@ -182,11 +183,11 @@ let search_about_filter query gr env typ = match query with
let search_pattern gopt pat mods =
let ans = ref [] in
+ let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
- let f_module = module_filter mods ref env typ in
- let f_blacklist = blacklist_filter ref env typ in
- let f_pattern () = pattern_filter pat ref env typ in
- f_module && f_pattern () && f_blacklist
+ module_filter mods ref env typ &&
+ pattern_filter pat ref env typ &&
+ blacklist_filter ref env typ
in
let iter ref env typ =
if filter ref env typ then plain_display ans ref env typ
@@ -208,14 +209,12 @@ let search_rewrite gopt pat mods =
let pat1 = rewrite_pat1 pat in
let pat2 = rewrite_pat2 pat in
let ans = ref [] in
+ let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
- let f_module = module_filter mods ref env typ in
- let f_blacklist = blacklist_filter ref env typ in
- let f_pattern () =
- pattern_filter pat1 ref env typ ||
- pattern_filter pat2 ref env typ
- in
- f_module && f_pattern () && f_blacklist
+ module_filter mods ref env typ &&
+ (pattern_filter pat1 ref env typ ||
+ pattern_filter pat2 ref env typ) &&
+ blacklist_filter ref env typ
in
let iter ref env typ =
if filter ref env typ then plain_display ans ref env typ
@@ -227,11 +226,11 @@ let search_rewrite gopt pat mods =
let search_by_head gopt pat mods =
let ans = ref [] in
+ let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
- let f_module = module_filter mods ref env typ in
- let f_blacklist = blacklist_filter ref env typ in
- let f_pattern () = head_filter pat ref env typ in
- f_module && f_pattern () && f_blacklist
+ module_filter mods ref env typ &&
+ head_filter pat ref env typ &&
+ blacklist_filter ref env typ
in
let iter ref env typ =
if filter ref env typ then plain_display ans ref env typ
@@ -243,12 +242,13 @@ let search_by_head gopt pat mods =
let search_about gopt items mods =
let ans = ref [] in
+ let blacklist_filter = blacklist_filter_aux () in
let filter ref env typ =
let eqb b1 b2 = if b1 then b2 else not b2 in
- let f_module = module_filter mods ref env typ in
- let f_about (b, i) = eqb b (search_about_filter i ref env typ) in
- let f_blacklist = blacklist_filter ref env typ in
- f_module && List.for_all f_about items && f_blacklist
+ module_filter mods ref env typ &&
+ List.for_all
+ (fun (b,i) -> eqb b (search_about_filter i ref env typ)) items &&
+ blacklist_filter ref env typ
in
let iter ref env typ =
if filter ref env typ then plain_display ans ref env typ
@@ -287,6 +287,7 @@ let interface_search =
let (name, tpe, subtpe, mods, blacklist) =
extract_flags [] [] [] [] false flags
in
+ let blacklist_filter = blacklist_filter_aux () in
let filter_function ref env constr =
let id = Names.Id.to_string (Nametab.basename_of_global ref) in
let path = Libnames.dirpath (Nametab.path_of_global ref) in
@@ -305,13 +306,11 @@ let interface_search =
let match_module (mdl, flag) =
toggle (Libnames.is_dirpath_prefix_of mdl path) flag
in
- let in_blacklist =
- blacklist || (blacklist_filter ref env constr)
- in
List.for_all match_name name &&
List.for_all match_type tpe &&
List.for_all match_subtype subtpe &&
- List.for_all match_module mods && in_blacklist
+ List.for_all match_module mods &&
+ (blacklist || blacklist_filter ref env constr)
in
let ans = ref [] in
let print_function ref env constr =
@@ -342,3 +341,6 @@ let interface_search =
in
let () = generic_search glnum iter in
!ans
+
+let blacklist_filter ref env typ =
+ blacklist_filter_aux () ref env typ
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 8f77aea44..de41f7b19 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -82,7 +82,7 @@ let print_usage_channel co command =
\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
\n stdout (if unset)\
\n -time display the time taken by each command\
-\n -profile-ltac display the time taken by each (sub)tactic\
+\n -profile-ltac display the time taken by each (sub)tactic\
\n -m, --memory display total heap size at program exit\
\n (use environment variable\
\n OCAML_GC_STATS=\"/tmp/gclog.txt\"\
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index aa1999cf1..3b14f597c 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -449,7 +449,27 @@ let vernac_notation locality local =
(***********)
(* Gallina *)
-let start_proof_and_print k l hook = start_proof_com k l hook
+let start_proof_and_print k l hook =
+ let inference_hook =
+ if Flags.is_program_mode () then
+ let hook env sigma ev =
+ let tac = !Obligations.default_tactic in
+ let evi = Evd.find sigma ev in
+ let env = Evd.evar_filtered_env evi in
+ try
+ let concl = Evarutil.nf_evars_universes sigma evi.Evd.evar_concl in
+ if Evarutil.has_undefined_evars sigma concl then raise Exit;
+ let c, _, ctx =
+ Pfedit.build_by_tactic env (Evd.evar_universe_context sigma)
+ concl (Tacticals.New.tclCOMPLETE tac)
+ in Evd.set_universe_context sigma ctx, c
+ with Logic_monad.TacticFailure e when Logic.catchable_exception e ->
+ error "The statement obligations could not be resolved \
+ automatically, write a statement definition first."
+ in Some hook
+ else None
+ in
+ start_proof_com ?inference_hook k l hook
let no_hook = Lemmas.mk_hook (fun _ _ -> ())
@@ -960,12 +980,18 @@ let warn_arguments_assert =
strbrk "to clear implicit arguments add ': clear implicits'. " ++
strbrk "If you want to clear notation scopes add ': clear scopes'")
+let warn_renaming_nonimplicit =
+ CWarnings.create ~name:"arguments-ignore-rename-nonimpl"
+ ~category:"vernacular"
+ (fun (oldn, newn) ->
+ strbrk "Ignoring rename of "++pr_id oldn++str" into "++pr_id newn++
+ strbrk ". Only implicit arguments can be renamed.")
let vernac_declare_arguments locality r l nargs flags =
let extra_scope_flag = List.mem `ExtraScopes flags in
- let names = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
+ let names = List.map (List.map (fun { name } -> name)) l in
let names, rest = List.hd names, List.tl names in
- let scopes = List.map (List.map (fun (_,_, s, _,_) -> s)) l in
+ let scopes = List.map (List.map (fun { notation_scope = s } -> s)) l in
if List.exists (fun na -> not (List.equal Name.equal na names)) rest then
error "All arguments lists must declare the same names.";
if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names))
@@ -987,9 +1013,11 @@ let vernac_declare_arguments locality r l nargs flags =
| _::li, _::ld, _::ls -> check li ld ls
| _ -> assert false in
let () = match l with
- | [[]] -> ()
+ | [[]] when List.exists ((<>) `Assert) flags ||
+ (* Arguments f /. used to be allowed by mistake *)
+ (Flags.version_less_or_equal Flags.V8_5 && nargs >= 0) -> ()
| _ ->
- List.iter2 (fun l -> check inf_names l) (names :: rest) scopes
+ List.iter2 (check inf_names) (names :: rest) scopes
in
(* we take extra scopes apart, and we check they are consistent *)
let l, scopes =
@@ -1004,13 +1032,15 @@ let vernac_declare_arguments locality r l nargs flags =
| [[]] -> l
| _ ->
let name_anons = function
- | (Anonymous, a,b,c,d), Name id -> Name id, a,b,c,d
+ | { name = Anonymous } as x, Name id -> { x with name = Name id }
| x, _ -> x in
List.map (fun ns -> List.map name_anons (List.combine ns inf_names)) l in
- let names_decl = List.map (List.map (fun (id, _,_,_,_) -> id)) l in
+ let names_decl = List.map (List.map (fun { name } -> name)) l in
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
+ if Option.is_empty !renamed_arg && not (Id.equal a b) then
+ renamed_arg := Some(b,a)
+ in
let some_renaming_specified =
try
let names = Arguments_renaming.arguments_names sr in
@@ -1020,22 +1050,50 @@ let vernac_declare_arguments locality r l nargs flags =
match l with
| [[]] -> false, [[]]
| _ ->
- List.fold_map (fun sr il ->
- let sr', impl = List.fold_map (fun b -> function
- | (Anonymous, _,_, true, max), Name id -> assert false
- | (Name x, _,_, true, _), Anonymous ->
- user_err ~hdr:"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)
- | (Name iid, _,_, _, _), Name id ->
- set_renamed iid id;
- b || not (Id.equal iid id), None
- | _ -> b, None)
- sr (List.combine il inf_names) in
- sr || sr', List.map_filter (fun x -> x) impl)
- some_renaming_specified l in
+ let some_renaming = ref some_renaming_specified in
+ let rec aux il =
+ match il with
+ | [] -> []
+ | il :: ils -> aux_single il inf_names :: aux ils
+ and aux_single impl inf_names =
+ match impl, inf_names with
+ | [], _ -> []
+ | { name = Anonymous;
+ implicit_status = (`Implicit|`MaximallyImplicit)} :: _,
+ Name id :: _ ->
+ assert false
+ | { name = Name x;
+ implicit_status = (`Implicit|`MaximallyImplicit)} :: _,
+ Anonymous :: _ ->
+ user_err ~hdr:"vernac_declare_arguments"
+ (str"Argument "++ pr_id x ++str " cannot be declared implicit.")
+ | { name = Name iid;
+ implicit_status = (`Implicit|`MaximallyImplicit as i)} :: impl,
+ Name id :: inf_names ->
+ let max = i = `MaximallyImplicit in
+ set_renamed iid id;
+ some_renaming := !some_renaming || not (Id.equal iid id);
+ (ExplByName id,max,false) :: aux_single impl inf_names
+ | { name = Name iid } :: impl,
+ Name id :: inf_names when not (Id.equal iid id) ->
+ warn_renaming_nonimplicit (id, iid);
+ aux_single impl inf_names
+ | { name = Name iid } :: impl, Name id :: inf_names
+ when not (Id.equal iid id) ->
+ aux_single impl inf_names
+ | { name = Name iid } :: impl, Name id :: inf_names ->
+ set_renamed iid id;
+ some_renaming := !some_renaming || not (Id.equal iid id);
+ aux_single impl inf_names
+ | _ :: impl, _ :: inf_names ->
+ (* no rename, no implicit status *) aux_single impl inf_names
+ | _ :: _, [] -> assert false (* checked before in check() *)
+ in
+ !some_renaming, aux l in
+ (* We check if renamed arguments do match previously declared imp args,
+ * since the system has this invariant *)
+ let some_implicits_specified =
+ match implicits with [[]] -> false | _ -> true in
if some_renaming_specified then
if not (List.mem `Rename flags) then
user_err ~hdr:"vernac_declare_arguments"
@@ -1043,14 +1101,13 @@ let vernac_declare_arguments locality r l nargs flags =
match !renamed_arg with
| None -> mt ()
| Some (o,n) ->
- str "\nArgument " ++ pr_id o ++ str " renamed to " ++ pr_id n ++ str ".")
+ str "\nArgument " ++ pr_id o ++
+ str " renamed to " ++ pr_id n ++ str ".")
else
Arguments_renaming.rename_arguments
- (make_section_locality locality) sr names_decl;
+ (make_section_locality locality) sr names_decl;
(* All other infos are in the first item of l *)
let l = List.hd l in
- let some_implicits_specified = match implicits with
- | [[]] -> false | _ -> true in
let scopes = List.map (function
| None -> None
| Some (o, k) ->
@@ -1061,7 +1118,7 @@ let vernac_declare_arguments locality r l nargs flags =
let some_scopes_specified = List.exists ((!=) None) scopes in
let rargs =
Util.List.map_filter (function (n, true) -> Some n | _ -> None)
- (Util.List.map_i (fun i (_, b, _,_,_) -> i, b) 0 l) in
+ (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 l) in
if some_scopes_specified || List.mem `ClearScopes flags then
vernac_arguments_scope locality r scopes;
if not some_implicits_specified && List.mem `DefaultImplicits flags then
@@ -1082,7 +1139,9 @@ let vernac_declare_arguments locality r l nargs flags =
| ConstRef _ as c ->
Reductionops.ReductionBehaviour.set
(make_section_locality locality) c (rargs, nargs, flags)
- | _ -> user_err (strbrk "Modifiers of the behavior of the simpl tactic are relevant for constants only.")
+ | _ -> user_err
+ (strbrk "Modifiers of the behavior of the simpl tactic "++
+ strbrk "are relevant for constants only.")
end;
if not (some_renaming_specified ||
some_implicits_specified ||
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 00:00:17 +0000