From 7461f18cbe722610613bdd8c729665ac48395b6e Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Fri, 5 Apr 2019 21:21:53 +0200 Subject: [vernac] [ast] Make location info an attribute of vernaculars. This has been a mess for quite a while, we try to improve it. --- vernac/g_vernac.mlg | 13 +++++-------- vernac/ppvernac.ml | 10 +++++----- vernac/pvernac.ml | 2 +- vernac/pvernac.mli | 4 ++-- vernac/topfmt.ml | 4 ++-- vernac/topfmt.mli | 2 +- vernac/vernacentries.ml | 2 +- vernac/vernacentries.mli | 2 +- vernac/vernacexpr.ml | 11 ++++++----- vernac/vernacprop.ml | 35 ++++++++++++++++++----------------- 10 files changed, 42 insertions(+), 43 deletions(-) (limited to 'vernac') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3f491d1dd4..d97fb523f7 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -77,11 +77,11 @@ let parse_compat_version = let open Flags in function GRAMMAR EXTEND Gram GLOBAL: vernac_control gallina_ext noedit_mode subprf; vernac_control: FIRST - [ [ IDENT "Time"; c = located_vernac -> { VernacTime (false,c) } - | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) } - | IDENT "Timeout"; n = natural; v = located_vernac -> { VernacTimeout(n,v) } - | IDENT "Fail"; v = located_vernac -> { VernacFail v } - | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ] + [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) } + | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) } + | IDENT "Timeout"; n = natural; v = vernac_control -> { CAst.make ~loc @@ VernacTimeout(n,v) } + | IDENT "Fail"; v = vernac_control -> { CAst.make ~loc @@ VernacFail v } + | v = decorated_vernac -> { let (f, v) = v in CAst.make ~loc @@ VernacExpr(f, v) } ] ] ; decorated_vernac: @@ -147,9 +147,6 @@ GRAMMAR EXTEND Gram ] ] ; - located_vernac: - [ [ v = vernac_control -> { CAst.make ~loc v } ] ] - ; END { diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 4e4d431e89..327efcda2b 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1262,15 +1262,15 @@ let pr_vernac_attributes = let rec pr_vernac_control v = let return = tag_vernac v in - match v with + match v.v with | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v' - | VernacTime (_,{v}) -> + | VernacTime (_,v) -> return (keyword "Time" ++ spc() ++ pr_vernac_control v) - | VernacRedirect (s, {v}) -> + | VernacRedirect (s, v) -> return (keyword "Redirect" ++ spc() ++ qs s ++ spc() ++ pr_vernac_control v) - | VernacTimeout(n,{v}) -> + | VernacTimeout(n,v) -> return (keyword "Timeout " ++ int n ++ spc() ++ pr_vernac_control v) - | VernacFail {v} -> + | VernacFail v-> return (keyword "Fail" ++ spc() ++ pr_vernac_control v) let pr_vernac v = diff --git a/vernac/pvernac.ml b/vernac/pvernac.ml index d474ef8637..4d9157089c 100644 --- a/vernac/pvernac.ml +++ b/vernac/pvernac.ml @@ -52,7 +52,7 @@ module Vernac_ = let () = let open Extend in - let act_vernac v loc = Some CAst.(make ~loc v) in + let act_vernac v loc = Some v in let act_eoi _ loc = None in let rule = [ Rule (Next (Stop, Atoken Tok.PEOI), act_eoi); diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 4bf7c9f7bd..41a2e7fd6f 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -26,7 +26,7 @@ module Vernac_ : val rec_definition : (fixpoint_expr * decl_notation list) Entry.t val noedit_mode : vernac_expr Entry.t val command_entry : vernac_expr Entry.t - val main_entry : vernac_control CAst.t option Entry.t + val main_entry : vernac_control option Entry.t val red_expr : raw_red_expr Entry.t val hint_info : Hints.hint_info_expr Entry.t end @@ -40,7 +40,7 @@ module Unsafe : sig end (** The main entry: reads an optional vernac command *) -val main_entry : proof_mode option -> vernac_control CAst.t option Entry.t +val main_entry : proof_mode option -> vernac_control option Entry.t (** Grammar entry for tactics: proof mode(s). By default Coq's grammar has an empty entry (non-terminal) for diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 60b0bdc7e7..fffa51f0b4 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -413,7 +413,7 @@ let with_output_to_file fname func input = (* For coqtop -time, we display the position in the file, and a glimpse of the executed command *) -let pr_cmd_header {CAst.loc;v=com} = +let pr_cmd_header com = let shorten s = if Unicode.utf8_length s > 33 then (Unicode.utf8_sub s 0 30) ^ "..." else s in @@ -423,7 +423,7 @@ let pr_cmd_header {CAst.loc;v=com} = | x -> x ) s in - let (start,stop) = Option.cata Loc.unloc (0,0) loc in + let (start,stop) = Option.cata Loc.unloc (0,0) com.CAst.loc in let safe_pr_vernac x = try Ppvernac.pr_vernac x with e -> str (Printexc.to_string e) in diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index b0e3b3772c..dd6194168a 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -72,4 +72,4 @@ val print_err_exn : exn -> unit redirected to a file [file] *) val with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b -val pr_cmd_header : Vernacexpr.vernac_control CAst.t -> Pp.t +val pr_cmd_header : Vernacexpr.vernac_control -> Pp.t diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3a305c3b61..2e060e97f7 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -2599,7 +2599,7 @@ and vernac_load ?proof ~verbosely ~st fname = CErrors.user_err Pp.(str "Files processed by Load cannot leave open proofs."); pstate -and interp_control ?proof ~st = function +and interp_control ?proof ~st v = match v with | { v=VernacExpr (atts, cmd) } -> interp_expr ?proof ~atts ~st cmd | { v=VernacFail v } -> diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli index 71cc29b6e1..12451370c8 100644 --- a/vernac/vernacentries.mli +++ b/vernac/vernacentries.mli @@ -23,7 +23,7 @@ val vernac_require : val interp : ?verbosely:bool -> ?proof:Proof_global.closed_proof -> - st:Vernacstate.t -> Vernacexpr.vernac_control CAst.t -> Vernacstate.t + st:Vernacstate.t -> Vernacexpr.vernac_control -> Vernacstate.t (** Prepare a "match" template for a given inductive type. For each branch of the match, we list the constructor name diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index d0dae1aa53..99b457effe 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -398,11 +398,12 @@ type nonrec vernac_expr = (* For extension *) | VernacExtend of extend_name * Genarg.raw_generic_argument list -type vernac_control = +type vernac_control_r = | VernacExpr of Attributes.vernac_flags * vernac_expr (* boolean is true when the `-time` batch-mode command line flag was set. the flag is used to print differently in `-time` vs `Time foo` *) - | VernacTime of bool * vernac_control CAst.t - | VernacRedirect of string * vernac_control CAst.t - | VernacTimeout of int * vernac_control CAst.t - | VernacFail of vernac_control CAst.t + | VernacTime of bool * vernac_control + | VernacRedirect of string * vernac_control + | VernacTimeout of int * vernac_control + | VernacFail of vernac_control +and vernac_control = vernac_control_r CAst.t diff --git a/vernac/vernacprop.ml b/vernac/vernacprop.ml index 704c5b2170..b3490c7dc6 100644 --- a/vernac/vernacprop.ml +++ b/vernac/vernacprop.ml @@ -13,19 +13,20 @@ open Vernacexpr -let rec under_control = function +let rec under_control v = v |> CAst.with_val (function | VernacExpr (_, c) -> c - | VernacRedirect (_,{CAst.v=c}) - | VernacTime (_,{CAst.v=c}) - | VernacFail {CAst.v=c} - | VernacTimeout (_,{CAst.v=c}) -> under_control c + | VernacRedirect (_,c) + | VernacTime (_,c) + | VernacFail c + | VernacTimeout (_,c) -> under_control c + ) -let rec has_Fail = function +let rec has_Fail v = v |> CAst.with_val (function | VernacExpr _ -> false - | VernacRedirect (_,{CAst.v=c}) - | VernacTime (_,{CAst.v=c}) - | VernacTimeout (_,{CAst.v=c}) -> has_Fail c - | VernacFail _ -> true + | VernacRedirect (_,c) + | VernacTime (_,c) + | VernacTimeout (_,c) -> has_Fail c + | VernacFail _ -> true) (* Navigation commands are allowed in a coqtop session but not in a .v file *) let is_navigation_vernac_expr = function @@ -38,17 +39,17 @@ let is_navigation_vernac_expr = function let is_navigation_vernac c = is_navigation_vernac_expr (under_control c) -let rec is_deep_navigation_vernac = function - | VernacTime (_,{CAst.v=c}) -> is_deep_navigation_vernac c - | VernacRedirect (_, {CAst.v=c}) - | VernacTimeout (_,{CAst.v=c}) | VernacFail {CAst.v=c} -> is_navigation_vernac c - | VernacExpr _ -> false +let rec is_deep_navigation_vernac v = v |> CAst.with_val (function + | VernacTime (_,c) -> is_deep_navigation_vernac c + | VernacRedirect (_, c) + | VernacTimeout (_, c) | VernacFail c -> is_navigation_vernac c + | VernacExpr _ -> false) (* NB: Reset is now allowed again as asked by A. Chlipala *) -let is_reset = function +let is_reset = CAst.with_val (function | VernacExpr ( _, VernacResetInitial) | VernacExpr (_, VernacResetName _) -> true - | _ -> false + | _ -> false) let is_debug cmd = match under_control cmd with | VernacSetOption (_, ["Ltac";"Debug"], _) -> true -- cgit v1.2.3 From 6ef5a36a69e9116344af7fae4434a487be9c3b0e Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Tue, 23 Apr 2019 17:23:58 -0700 Subject: Update behavior of -emacs to support showing diffs in ProofGeneral (master branch) Adds XML-like tags in output to mark diffs --- vernac/topfmt.ml | 16 ++++++++++++++-- vernac/topfmt.mli | 1 + 2 files changed, 15 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 60b0bdc7e7..7bc3264968 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -196,6 +196,18 @@ let init_tag_map styles = let default_styles () = init_tag_map (default_tag_map ()) +let set_emacs_print_strings () = + let open Terminal in + let diff = "diff." in + List.iter (fun b -> + let (name, attrs) = b in + if diff = (String.sub name 0 (String.length diff)) then + tag_map := CString.Map.add name + { attrs with prefix = Some (Printf.sprintf "<%s>" name); + suffix = Some (Printf.sprintf "" name) } + !tag_map) + (CString.Map.bindings !tag_map) + let parse_color_config str = let styles = Terminal.parse str in init_tag_map styles @@ -264,13 +276,13 @@ let make_printing_functions () = let (tpfx, ttag) = split_tag tag in if tpfx <> end_pfx then let style = get_style ttag in - match style.Terminal.prefix with Some s -> Format.pp_print_string ft s | None -> () in + match style.Terminal.prefix with Some s -> Format.pp_print_as ft 0 s | None -> () in let print_suffix ft tag = let (tpfx, ttag) = split_tag tag in if tpfx <> start_pfx then let style = get_style ttag in - match style.Terminal.suffix with Some s -> Format.pp_print_string ft s | None -> () in + match style.Terminal.suffix with Some s -> Format.pp_print_as ft 0 s | None -> () in print_prefix, print_suffix diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index b0e3b3772c..a1e289cd5a 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -46,6 +46,7 @@ val emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit val default_styles : unit -> unit val parse_color_config : string -> unit val dump_tags : unit -> (string * Terminal.style) list +val set_emacs_print_strings : unit -> unit (** Initialization of interpretation of tags *) val init_terminal_output : color:bool -> unit -- cgit v1.2.3 From 77257819ea4a381067e65fd46e7d7590aa7e2600 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 11 Apr 2019 12:45:07 +0200 Subject: Remove Global.env from goptions by passing from vernacentries Currently this env is only used to error for Printing If/Let on non-2-constructor/non-1-constructor types so we could alternatively remove it and not error / error later when trying to print. Keeping the env and the error as-is should be fine though. --- vernac/vernacentries.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) (limited to 'vernac') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e44d68b87d..fa170e4104 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1732,29 +1732,29 @@ let vernac_set_option ~local export table v = match v with let vernac_add_option key lv = let f = function - | StringRefValue s -> (get_string_table key)#add s - | QualidRefValue locqid -> (get_ref_table key)#add locqid + | StringRefValue s -> (get_string_table key).add (Global.env()) s + | QualidRefValue locqid -> (get_ref_table key).add (Global.env()) locqid in try List.iter f lv with Not_found -> error_undeclared_key key let vernac_remove_option key lv = let f = function - | StringRefValue s -> (get_string_table key)#remove s - | QualidRefValue locqid -> (get_ref_table key)#remove locqid + | StringRefValue s -> (get_string_table key).remove (Global.env()) s + | QualidRefValue locqid -> (get_ref_table key).remove (Global.env()) locqid in try List.iter f lv with Not_found -> error_undeclared_key key let vernac_mem_option key lv = let f = function - | StringRefValue s -> (get_string_table key)#mem s - | QualidRefValue locqid -> (get_ref_table key)#mem locqid + | StringRefValue s -> (get_string_table key).mem (Global.env()) s + | QualidRefValue locqid -> (get_ref_table key).mem (Global.env()) locqid in try List.iter f lv with Not_found -> error_undeclared_key key let vernac_print_option key = - try (get_ref_table key)#print + try (get_ref_table key).print () with Not_found -> - try (get_string_table key)#print + try (get_string_table key).print () with Not_found -> try print_option_value key with Not_found -> error_undeclared_key key -- cgit v1.2.3 From ba5ea9fb6aaa3faace0960adca4d41fc74cb2ac7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 May 2019 08:28:57 +0200 Subject: [comDefinition] Use prepare function from DeclareDef. We also update the plugin tutorial. This was already tried [in the same exact way] in #8811, however the bench time was not convincing then, but now things seem a bit better, likely due to the removal of some extra normalization somewhere. Some more changes from #8811 are still pending. --- vernac/comDefinition.ml | 31 ++++++++++--------------------- 1 file changed, 10 insertions(+), 21 deletions(-) (limited to 'vernac') diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index feaf47df18..12df3215ad 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -12,7 +12,6 @@ open Pp open Util open Entries open Redexpr -open Declare open Constrintern open Pretyping @@ -42,10 +41,9 @@ let check_imps ~impsty ~impsbody = if not b then warn_implicits_in_term () let interp_definition ~program_mode pl bl poly red_option c ctypopt = - let open EConstr in let env = Global.env() in (* Explicitly bound universes and constraints *) - let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in + let evd, udecl = Constrexpr_ops.interp_univ_decl_opt env pl in (* Build the parameters *) let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars ~program_mode env evd bl in (* Build the type *) @@ -66,24 +64,15 @@ let interp_definition ~program_mode pl bl poly red_option c ctypopt = in (* Do the reduction *) let evd, c = red_constant_body red_option env_bl evd c in - (* universe minimization *) - let evd = Evd.minimize_universes evd in - (* Substitute evars and universes, and add parameters. - Note: in program mode some evars may remain. *) - let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in - let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in - let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd ty) ctx) tyopt in - (* Keep only useful universes. *) - let uvars_fold uvars c = - Univ.LSet.union uvars (universes_of_constr evd (of_constr c)) - in - let uvars = List.fold_left uvars_fold Univ.LSet.empty (Option.List.cons tyopt [c]) in - let evd = Evd.restrict_universe_context evd uvars in - (* Check we conform to declared universes *) - let uctx = Evd.check_univ_decl ~poly evd decl in - (* We're done! *) - let ce = definition_entry ?types:tyopt ~univs:uctx c in - (ce, evd, decl, imps) + + (* Declare the definition *) + let c = EConstr.it_mkLambda_or_LetIn c ctx in + let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in + + let evd, ce = DeclareDef.prepare_definition ~allow_evars:program_mode + ~opaque:false ~poly evd udecl ~types:tyopt ~body:c in + + (ce, evd, udecl, imps) let check_definition ~program_mode (ce, evd, _, imps) = let env = Global.env () in -- cgit v1.2.3 From e6383e516036a15bccdbc2b125019a40181c6028 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 7 May 2019 08:07:28 +0000 Subject: [Record] Deforestation --- vernac/record.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/record.ml b/vernac/record.ml index 74e5a03659..d246c161a0 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -699,8 +699,7 @@ let definition_structure udecl kind ~template cum poly finite records = let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = - let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in - let coe = List.map (fun coe -> not (Option.is_empty coe)) coers in + let coe = List.map (fun (((coe, _), _), _) -> not (Option.is_empty coe)) cfs in id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in -- cgit v1.2.3 From a7f678c2209bbe56b18ed3cdf1306fed161d7b07 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Tue, 7 May 2019 08:07:34 +0000 Subject: [Record] Une a record to gather field declaration attributes --- vernac/g_vernac.mlg | 6 ++++-- vernac/ppvernac.ml | 6 +++--- vernac/record.ml | 14 +++++++------- vernac/record.mli | 2 +- vernac/vernacentries.ml | 5 +++-- vernac/vernacexpr.ml | 11 +++++++---- 6 files changed, 25 insertions(+), 19 deletions(-) (limited to 'vernac') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index d97fb523f7..59d2a66259 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -447,8 +447,10 @@ GRAMMAR EXTEND Gram *) (* ... with coercions *) record_field: - [ [ bd = record_binder; pri = OPT [ "|"; n = natural -> { n } ]; - ntn = decl_notation -> { (bd,pri),ntn } ] ] + [ [ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; + rf_notation = decl_notation -> { + let rf_subclass, rf_decl = bd in + rf_decl, { rf_subclass ; rf_priority ; rf_notation } } ] ] ; record_fields: [ [ f = record_field; ";"; fs = record_fields -> { f :: fs } diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 327efcda2b..889dbafabd 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -446,15 +446,15 @@ open Pputils | Some true -> str" :>" | Some false -> str" :>>" - let pr_record_field ((x, pri), ntn) = + let pr_record_field (x, { rf_subclass = oc ; rf_priority = pri ; rf_notation = ntn }) = let env = Global.env () in let sigma = Evd.from_env env in let prx = match x with - | (oc,AssumExpr (id,t)) -> + | AssumExpr (id,t) -> hov 1 (pr_lname id ++ pr_oc oc ++ spc() ++ pr_lconstr_expr env sigma t) - | (oc,DefExpr(id,b,opt)) -> (match opt with + | DefExpr(id,b,opt) -> (match opt with | Some t -> hov 1 (pr_lname id ++ pr_oc oc ++ spc() ++ diff --git a/vernac/record.ml b/vernac/record.ml index d246c161a0..f489707eb3 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -634,7 +634,7 @@ let declare_existing_class g = open Vernacexpr let check_unique_names records = - let extract_name acc (((_, bnd), _), _) = match bnd with + let extract_name acc (rf_decl, _) = match rf_decl with Vernacexpr.AssumExpr({CAst.v=Name id},_) -> id::acc | Vernacexpr.DefExpr ({CAst.v=Name id},_,_) -> id::acc | _ -> acc in @@ -649,15 +649,15 @@ let check_unique_names records = let check_priorities kind records = let isnot_class = match kind with Class false -> false | _ -> true in let has_priority (_, _, _, cfs, _, _) = - List.exists (fun ((_, pri), _) -> not (Option.is_empty pri)) cfs + List.exists (fun (_, { rf_priority }) -> not (Option.is_empty rf_priority)) cfs in if isnot_class && List.exists has_priority records then user_err Pp.(str "Priorities only allowed for type class substructures") let extract_record_data records = let map (is_coe, id, _, cfs, idbuild, s) = - let fs = List.map (fun (((_, f), _), _) -> f) cfs in - id.CAst.v, s, List.map snd cfs, fs + let fs = List.map fst cfs in + id.CAst.v, s, List.map (fun (_, { rf_notation }) -> rf_notation) cfs, fs in let data = List.map map records in let pss = List.map (fun (_, _, ps, _, _, _) -> ps) records in @@ -691,15 +691,15 @@ let definition_structure udecl kind ~template cum poly finite records = | [r], [d] -> r, d | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled") in - let priorities = List.map (fun ((_, id), _) -> {hint_priority = id; hint_pattern = None}) cfs in - let coers = List.map (fun (((coe, _), _), _) -> coe) cfs in + let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in + let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in declare_class def cum ubinders univs id.CAst.v idbuild implpars params arity template implfs fields coers priorities | _ -> let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = - let coe = List.map (fun (((coe, _), _), _) -> not (Option.is_empty coe)) cfs in + let coe = List.map (fun (_, { rf_subclass }) -> not (Option.is_empty rf_subclass)) cfs in id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in diff --git a/vernac/record.mli b/vernac/record.mli index 12a2a765b5..d6e63901cd 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -33,7 +33,7 @@ val definition_structure : (coercion_flag * Names.lident * local_binder_expr list * - (local_decl_expr with_instance with_priority with_notation) list * + (local_decl_expr * record_field_attr) list * Id.t * constr_expr option) list -> GlobRef.t list diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0f6374c506..388f6957cf 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -684,7 +684,7 @@ let vernac_record ~template udecl cum k poly finite records = let () = if Dumpglob.dump () then let () = Dumpglob.dump_definition id false "rec" in - let iter (((_, x), _), _) = match x with + let iter (x, _) = match x with | Vernacexpr.AssumExpr ({loc;v=Name id}, _) -> Dumpglob.dump_definition (make ?loc id) false "proj" | _ -> () @@ -743,7 +743,8 @@ let vernac_inductive ~atts cum lo finite indl = let (id, bl, c, l) = Option.get is_defclass in let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in - let f = (((coe', AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce)), None), []) in + let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), + { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] } in vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 99b457effe..34a9b9394a 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -143,13 +143,16 @@ type decl_notation = lstring * constr_expr * scope_name option type simple_binder = lident list * constr_expr type class_binder = lident * constr_expr list type 'a with_coercion = coercion_flag * 'a -type 'a with_instance = instance_flag * 'a -type 'a with_notation = 'a * decl_notation list -type 'a with_priority = 'a * int option +(* Attributes of a record field declaration *) +type record_field_attr = { + rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *) + rf_priority: int option; (* priority of the instance, if relevant *) + rf_notation: decl_notation list; + } type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = | Constructors of constructor_expr list - | RecordDecl of lident option * local_decl_expr with_instance with_priority with_notation list + | RecordDecl of lident option * (local_decl_expr * record_field_attr) list type inductive_expr = ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind * constructor_list_or_record_decl_expr -- cgit v1.2.3 From 21e5a5d510de59a33f3e6a0f88b8321ac0d7d23d Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Tue, 7 May 2019 12:04:34 -0700 Subject: Show diffs in error messages only if Diffs is enabled --- vernac/himsg.ml | 1 + 1 file changed, 1 insertion(+) (limited to 'vernac') diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 082b22b373..f58eeae6dc 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -150,6 +150,7 @@ let explicit_flags = [print_universes; print_implicits; print_coercions; print_no_symbol] (* and more! *) ] let with_diffs pm pn = + if not (Proof_diffs.show_diffs ()) then pm, pn else try let tokenize_string = Proof_diffs.tokenize_string in Pp_diff.diff_pp ~tokenize_string pm pn -- cgit v1.2.3 From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Tue, 2 Apr 2019 13:22:11 +0200 Subject: [api] Remove 8.10 deprecations. Some of them are significant so presumably it will take a bit of effort to fix overlays. I left out the removal of `nf_enter` for now as MTac2 needs some serious porting in order to avoid it. --- vernac/himsg.ml | 3 --- vernac/himsg.mli | 5 ----- 2 files changed, 8 deletions(-) (limited to 'vernac') diff --git a/vernac/himsg.ml b/vernac/himsg.ml index f58eeae6dc..b2382ce6fc 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -1348,9 +1348,6 @@ let explain_pattern_matching_error env sigma = function | CannotInferPredicate typs -> explain_cannot_infer_predicate env sigma typs -let map_pguard_error = map_pguard_error -let map_ptype_error = map_ptype_error - let explain_reduction_tactic_error = function | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) -> let e = map_ptype_error EConstr.of_constr e in diff --git a/vernac/himsg.mli b/vernac/himsg.mli index d0f42ea16b..d1c1c092e3 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -43,9 +43,4 @@ val explain_module_error : Modops.module_typing_error -> Pp.t val explain_module_internalization_error : Modintern.module_internalization_error -> Pp.t -val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error -[@@ocaml.deprecated "Use [Type_errors.map_pguard_error]."] -val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error -[@@ocaml.deprecated "Use [Type_errors.map_ptype_error]."] - val explain_prim_token_notation_error : string -> env -> Evd.evar_map -> Notation.prim_token_notation_error -> Pp.t -- cgit v1.2.3 From 857082b492760c17bfbc2b2022862c7cd758261e Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 2 May 2019 21:28:47 +0200 Subject: Remove various circumvolutions from reduction behaviors Incidentally, this fixes #10056 --- vernac/vernacentries.ml | 34 ++++++++++++++++++---------------- 1 file changed, 18 insertions(+), 16 deletions(-) (limited to 'vernac') diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 388f6957cf..279d4f0935 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1231,16 +1231,13 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red let clear_implicits_flag = List.mem `ClearImplicits flags in let default_implicits_flag = List.mem `DefaultImplicits flags in let never_unfold_flag = List.mem `ReductionNeverUnfold flags in + let nomatch_flag = List.mem `ReductionDontExposeCase flags in let err_incompat x y = user_err Pp.(str ("Options \""^x^"\" and \""^y^"\" are incompatible.")) in if assert_flag && rename_flag then err_incompat "assert" "rename"; - if Option.has_some nargs_for_red && never_unfold_flag then - err_incompat "simpl never" "/"; - if never_unfold_flag && List.mem `ReductionDontExposeCase flags then - err_incompat "simpl never" "simpl nomatch"; if clear_scopes_flag && extra_scopes_flag then err_incompat "clear scopes" "extra scopes"; if clear_implicits_flag && default_implicits_flag then @@ -1385,19 +1382,24 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red (Util.List.map_i (fun i { recarg_like = b } -> i, b) 0 args) in - let rec narrow = function - | #Reductionops.ReductionBehaviour.flag as x :: tl -> x :: narrow tl - | [] -> [] | _ :: tl -> narrow tl - in - let red_flags = narrow flags in - let red_modifiers_specified = - not (List.is_empty rargs) || Option.has_some nargs_for_red - || not (List.is_empty red_flags) + let red_behavior = + let open Reductionops.ReductionBehaviour in + match never_unfold_flag, nomatch_flag, rargs, nargs_for_red with + | true, false, [], None -> Some NeverUnfold + | true, true, _, _ -> err_incompat "simpl never" "simpl nomatch" + | true, _, _::_, _ -> err_incompat "simpl never" "!" + | true, _, _, Some _ -> err_incompat "simpl never" "/" + | false, false, [], None -> None + | false, false, _, _ -> Some (UnfoldWhen { nargs = nargs_for_red; + recargs = rargs; + }) + | false, true, _, _ -> Some (UnfoldWhenNoMatch { nargs = nargs_for_red; + recargs = rargs; + }) in - if not (List.is_empty rargs) && never_unfold_flag then - err_incompat "simpl never" "!"; + let red_modifiers_specified = Option.has_some red_behavior in (* Actions *) @@ -1424,8 +1426,8 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red match sr with | ConstRef _ as c -> Reductionops.ReductionBehaviour.set - section_local c - (rargs, Option.default ~-1 nargs_for_red, red_flags) + ~local:section_local c (Option.get red_behavior) + | _ -> user_err (strbrk "Modifiers of the behavior of the simpl tactic "++ strbrk "are relevant for constants only.") -- cgit v1.2.3 From 4e760a40f22e2d76a3d246b225d290eb5d15e9e8 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 6 May 2019 14:05:09 +0000 Subject: [Canonical structures] Some projections may not be canonical --- vernac/record.ml | 2 +- vernac/record.mli | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/record.ml b/vernac/record.ml index f489707eb3..9b0fbea148 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -368,7 +368,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f with NotDefinable why -> warning_or_error coe indsp why; (None::sp_projs,i,NoProjection fi::subst) in - (nfi-1,i,(fi, is_local_assum decl)::kinds,sp_projs,subst)) + (nfi - 1, i, Recordops.mk_proj_kind fi (is_local_assum decl) :: kinds, sp_projs, subst)) (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) diff --git a/vernac/record.mli b/vernac/record.mli index d6e63901cd..51ab7487d7 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -22,7 +22,7 @@ val declare_projections : bool list -> Impargs.manual_implicits list -> Constr.rel_context -> - (Name.t * bool) list * Constant.t option list + Recordops.proj_kind list * Constant.t option list val declare_structure_entry : Recordops.struc_tuple -> unit -- cgit v1.2.3 From 6e0467e746e40c10bdc110e8d21e26846219d510 Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Mon, 6 May 2019 15:36:49 +0000 Subject: [Canonical structures] “not_canonical” annotation to field declarations --- vernac/attributes.ml | 3 +++ vernac/attributes.mli | 1 + vernac/g_vernac.mlg | 9 ++++++--- vernac/record.ml | 26 ++++++++++++++++++-------- vernac/record.mli | 7 ++++++- vernac/vernacentries.ml | 2 +- vernac/vernacexpr.ml | 1 + 7 files changed, 36 insertions(+), 13 deletions(-) (limited to 'vernac') diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 9b8c4efb37..31b0b7e49a 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -219,3 +219,6 @@ let only_polymorphism atts = parse polymorphic atts let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty] let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] + +let canonical = + bool_attribute ~name:"Canonical projection" ~on:"canonical" ~off:"not_canonical" diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 3cb4d69ca0..2559941354 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -52,6 +52,7 @@ val program : bool attribute val template : bool option attribute val locality : bool option attribute val deprecation : deprecation option attribute +val canonical : bool option attribute val program_mode_option_name : string list (** For internal use when messing with the global option. *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 59d2a66259..cc74121064 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -43,6 +43,7 @@ let query_command = Entry.create "vernac:query_command" let subprf = Entry.create "vernac:subprf" +let quoted_attributes = Entry.create "vernac:quoted_attributes" let class_rawexpr = Entry.create "vernac:class_rawexpr" let thm_token = Entry.create "vernac:thm_token" let def_body = Entry.create "vernac:def_body" @@ -75,7 +76,7 @@ let parse_compat_version = let open Flags in function } GRAMMAR EXTEND Gram - GLOBAL: vernac_control gallina_ext noedit_mode subprf; + GLOBAL: vernac_control quoted_attributes gallina_ext noedit_mode subprf; vernac_control: FIRST [ [ IDENT "Time"; c = vernac_control -> { CAst.make ~loc @@ VernacTime (false,c) } | IDENT "Redirect"; s = ne_string; c = vernac_control -> { CAst.make ~loc @@ VernacRedirect (s, c) } @@ -447,10 +448,12 @@ GRAMMAR EXTEND Gram *) (* ... with coercions *) record_field: - [ [ bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; + [ [ attr = LIST0 quoted_attributes ; + bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; rf_notation = decl_notation -> { + let rf_canonical = attr |> List.flatten |> parse canonical |> Option.default true in let rf_subclass, rf_decl = bd in - rf_decl, { rf_subclass ; rf_priority ; rf_notation } } ] ] + rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ] ; record_fields: [ [ f = record_field; ";"; fs = record_fields -> { f :: fs } diff --git a/vernac/record.ml b/vernac/record.ml index 9b0fbea148..f737a8c524 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -276,8 +276,13 @@ let instantiate_possibly_recursive_type ind u ntypes paramdecls fields = let subst' = List.init ntypes (fun i -> mkIndU ((ind, ntypes - i - 1), u)) in Termops.substl_rel_context (subst @ subst') fields +type projection_flags = { + pf_subclass: bool; + pf_canonical: bool; +} + (* We build projections *) -let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers fieldimpls fields = +let declare_projections indsp ctx ?(kind=StructureComponent) binder_name flags fieldimpls fields = let env = Global.env() in let (mib,mip) = Global.lookup_inductive indsp in let poly = Declareops.inductive_is_polymorphic mib in @@ -299,7 +304,7 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f in let (_,_,kinds,sp_projs,_) = List.fold_left3 - (fun (nfi,i,kinds,sp_projs,subst) coe decl impls -> + (fun (nfi,i,kinds,sp_projs,subst) flags decl impls -> let fi = RelDecl.get_name decl in let ti = RelDecl.get_type decl in let (sp_projs,i,subst) = @@ -359,17 +364,17 @@ let declare_projections indsp ctx ?(kind=StructureComponent) binder_name coers f in let refi = ConstRef kn in Impargs.maybe_declare_manual_implicits false refi impls; - if coe then begin + if flags.pf_subclass then begin let cl = Class.class_of_global (IndRef indsp) in Class.try_add_new_coercion_with_source refi ~local:false poly ~source:cl end; let i = if is_local_assum decl then i+1 else i in (Some kn::sp_projs, i, Projection term::subst) with NotDefinable why -> - warning_or_error coe indsp why; + warning_or_error flags.pf_subclass indsp why; (None::sp_projs,i,NoProjection fi::subst) in - (nfi - 1, i, Recordops.mk_proj_kind fi (is_local_assum decl) :: kinds, sp_projs, subst)) - (List.length fields,0,[],[],[]) coers (List.rev fields) (List.rev fieldimpls) + (nfi - 1, i, { Recordops.pk_name = fi ; pk_true_proj = is_local_assum decl ; pk_canonical = flags.pf_canonical } :: kinds, sp_projs, subst)) + (List.length fields,0,[],[],[]) flags (List.rev fields) (List.rev fieldimpls) in (kinds,sp_projs) open Typeclasses @@ -525,7 +530,8 @@ let declare_class def cum ubinders univs id idbuild paramimpls params arity in [cref, [Name proj_name, sub, Some proj_cst]] | _ -> - let record_data = [id, idbuild, arity, fieldimpls, fields, false, List.map (fun _ -> false) fields] in + let record_data = [id, idbuild, arity, fieldimpls, fields, false, + List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in let inds = declare_structure ~cum Declarations.BiFinite ubinders univs paramimpls params template ~kind:Method ~name:[|binder_name|] record_data in @@ -699,7 +705,11 @@ let definition_structure udecl kind ~template cum poly finite records = let map impls = implpars @ Impargs.lift_implicits (succ (List.length params)) impls in let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) = - let coe = List.map (fun (_, { rf_subclass }) -> not (Option.is_empty rf_subclass)) cfs in + let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) -> + { pf_subclass = not (Option.is_empty rf_subclass); + pf_canonical = rf_canonical }) + cfs + in id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe in let data = List.map2 map data records in diff --git a/vernac/record.mli b/vernac/record.mli index 51ab7487d7..24bb27e107 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -14,12 +14,17 @@ open Constrexpr val primitive_flag : bool ref +type projection_flags = { + pf_subclass: bool; + pf_canonical: bool; +} + val declare_projections : inductive -> Entries.universes_entry -> ?kind:Decl_kinds.definition_object_kind -> Id.t -> - bool list -> + projection_flags list -> Impargs.manual_implicits list -> Constr.rel_context -> Recordops.proj_kind list * Constant.t option list diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 279d4f0935..208210217a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -744,7 +744,7 @@ let vernac_inductive ~atts cum lo finite indl = let (coe, (lid, ce)) = l in let coe' = if coe then Some true else None in let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce), - { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] } in + { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]] else if List.for_all is_record indl then (* Mutual record case *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 34a9b9394a..7267def362 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -148,6 +148,7 @@ type record_field_attr = { rf_subclass: instance_flag; (* the projection is an implicit coercion or an instance *) rf_priority: int option; (* priority of the instance, if relevant *) rf_notation: decl_notation list; + rf_canonical: bool; (* use this projection in the search for canonical instances *) } type constructor_expr = (lident * constr_expr) with_coercion type constructor_list_or_record_decl_expr = -- cgit v1.2.3 From 34e84eafe6615055071fbdc4aaee70c4c161a0fb Mon Sep 17 00:00:00 2001 From: Vincent Laporte Date: Thu, 9 May 2019 13:39:25 +0000 Subject: [Attributes] Allow explicit value for two-valued attributes Attributes that enable/disable a feature can have an explicit value (default is enable when the attribute is present). Three-valued boolean attributes do not support this: what would `#[local(false)]` mean? --- vernac/attributes.ml | 32 +++++++++++++++++++++++++------- vernac/attributes.mli | 2 +- vernac/g_vernac.mlg | 2 +- 3 files changed, 27 insertions(+), 9 deletions(-) (limited to 'vernac') diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 31b0b7e49a..1ad5862d5d 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -82,9 +82,12 @@ let assert_empty k v = if v <> VernacFlagEmpty then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments") +let error_twice ~name : 'a = + user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.") + let assert_once ~name prev = if Option.has_some prev then - user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.") + error_twice ~name let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute = let rec p extra v = function @@ -107,6 +110,24 @@ let bool_attribute ~name ~on ~off : bool option attribute = attribute_of_list [(on, single_key_parser ~name ~key:on true); (off, single_key_parser ~name ~key:off false)] +(* Variant of the [bool] attribute with only two values (bool has three). *) +let get_bool_value ~key ~default = + function + | VernacFlagEmpty -> default + | VernacFlagList [ "true", VernacFlagEmpty ] -> true + | VernacFlagList [ "false", VernacFlagEmpty ] -> false + | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.") + +let enable_attribute ~key ~default : bool attribute = + fun atts -> + let default = default () in + let this, extra = List.partition (fun (k, _) -> String.equal key k) atts in + extra, + match this with + | [] -> default + | [ _, value ] -> get_bool_value ~key ~default:true value + | _ -> error_twice ~name:key + let qualify_attribute qual (parser:'a attribute) : 'a attribute = fun atts -> let rec extract extra qualified = function @@ -139,11 +160,8 @@ let () = let open Goptions in optread = (fun () -> !program_mode); optwrite = (fun b -> program_mode:=b) } -let program_opt = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram" - -let program = program_opt >>= function - | Some b -> return b - | None -> return (!program_mode) +let program = + enable_attribute ~key:"program" ~default:(fun () -> !program_mode) let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" @@ -221,4 +239,4 @@ let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmp let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] let canonical = - bool_attribute ~name:"Canonical projection" ~on:"canonical" ~off:"not_canonical" + enable_attribute ~key:"canonical" ~default:(fun () -> true) diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 2559941354..44688ddafc 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -52,7 +52,7 @@ val program : bool attribute val template : bool option attribute val locality : bool option attribute val deprecation : deprecation option attribute -val canonical : bool option attribute +val canonical : bool attribute val program_mode_option_name : string list (** For internal use when messing with the global option. *) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index cc74121064..17675a15e1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -451,7 +451,7 @@ GRAMMAR EXTEND Gram [ [ attr = LIST0 quoted_attributes ; bd = record_binder; rf_priority = OPT [ "|"; n = natural -> { n } ]; rf_notation = decl_notation -> { - let rf_canonical = attr |> List.flatten |> parse canonical |> Option.default true in + let rf_canonical = attr |> List.flatten |> parse canonical in let rf_subclass, rf_decl = bd in rf_decl, { rf_subclass ; rf_priority ; rf_notation ; rf_canonical } } ] ] ; -- cgit v1.2.3 From beb5bdec79ff371f48a478df3c24f2cf9d68aa1f Mon Sep 17 00:00:00 2001 From: Jasper Hugunin Date: Tue, 7 May 2019 15:04:04 -0700 Subject: Use Print Custom Grammar to inspect custom entries --- vernac/g_vernac.mlg | 3 +++ vernac/metasyntax.ml | 8 +++++--- vernac/metasyntax.mli | 1 + vernac/ppvernac.ml | 2 ++ vernac/vernacentries.ml | 1 + vernac/vernacexpr.ml | 1 + 6 files changed, 13 insertions(+), 3 deletions(-) (limited to 'vernac') diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 59d2a66259..94d4ed80d1 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -1003,6 +1003,9 @@ GRAMMAR EXTEND Gram | IDENT "Grammar"; ent = IDENT -> (* This should be in "syntax" section but is here for factorization*) { PrintGrammar ent } + | IDENT "Custom"; IDENT "Grammar"; ent = IDENT -> + (* Should also be in "syntax" section *) + { PrintCustomGrammar ent } | IDENT "LoadPath"; dir = OPT dirpath -> { PrintLoadPath dir } | IDENT "Modules" -> { user_err Pp.(str "Print Modules is obsolete; use Print Libraries instead") } diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 843296d24e..50914959dc 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -50,10 +50,10 @@ let pr_entry e = str (Buffer.contents entry_buf) let pr_registered_grammar name = - let gram = try Some (Pcoq.find_grammars_by_name name) with Not_found -> None in + let gram = Pcoq.find_grammars_by_name name in match gram with - | None -> user_err Pp.(str "Unknown or unprintable grammar entry.") - | Some entries -> + | [] -> user_err Pp.(str "Unknown or unprintable grammar entry.") + | entries -> let pr_one (Pcoq.AnyEntry e) = str "Entry " ++ str (Pcoq.Entry.name e) ++ str " is" ++ fnl () ++ pr_entry e @@ -85,6 +85,8 @@ let pr_grammar = function pr_entry Pvernac.Vernac_.gallina_ext | name -> pr_registered_grammar name +let pr_custom_grammar name = pr_registered_grammar ("constr:"^name) + (**********************************************************************) (* Parse a format (every terminal starting with a letter or a single quote (except a single quote alone) must be quoted) *) diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index 38dbdf7e41..6435df23c7 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -57,6 +57,7 @@ val add_syntactic_definition : env -> Id.t -> Id.t list * constr_expr -> (** Print the Camlp5 state of a grammar *) val pr_grammar : string -> Pp.t +val pr_custom_grammar : string -> Pp.t val check_infix_modifiers : syntax_modifier list -> unit diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 889dbafabd..f2332bab8b 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -476,6 +476,8 @@ open Pputils keyword "Print Section" ++ spc() ++ Libnames.pr_qualid s | PrintGrammar ent -> keyword "Print Grammar" ++ spc() ++ str ent + | PrintCustomGrammar ent -> + keyword "Print Custom Grammar" ++ spc() ++ str ent | PrintLoadPath dir -> keyword "Print LoadPath" ++ pr_opt DirPath.print dir | PrintModules -> diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 388f6957cf..b7d5e1c543 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1883,6 +1883,7 @@ let vernac_print ~(pstate : Proof_global.t option) ~atts = | PrintSectionContext qid -> print_sec_context_typ env sigma qid | PrintInspect n -> inspect env sigma n | PrintGrammar ent -> Metasyntax.pr_grammar ent + | PrintCustomGrammar ent -> Metasyntax.pr_custom_grammar ent | PrintLoadPath dir -> (* For compatibility ? *) print_loadpath dir | PrintModules -> print_modules () | PrintModule qid -> print_module qid diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 34a9b9394a..6a51fdfe59 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -29,6 +29,7 @@ type printable = | PrintSectionContext of qualid | PrintInspect of int | PrintGrammar of string + | PrintCustomGrammar of string | PrintLoadPath of DirPath.t option | PrintModules | PrintModule of qualid -- cgit v1.2.3 From 6211fd6e067e781a160db8765dd87067428048f2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Nov 2018 23:26:06 +0100 Subject: Moving Evd.evars_of_term from constr to econstr + consequences. This impacts a lot of code, apparently in the good, removing several conversions back and forth constr. --- vernac/classes.ml | 7 ++++--- vernac/comDefinition.ml | 7 ++++--- vernac/comProgramFixpoint.ml | 17 +++++------------ vernac/obligations.ml | 34 ++++++++++++++++------------------ vernac/obligations.mli | 4 ++-- 5 files changed, 31 insertions(+), 38 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index 9f233a2551..ece9fc8937 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -374,6 +374,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po let obls, constr, typ = match term with | Some t -> + let termtype = EConstr.of_constr termtype in let obls, _, constr, typ = Obligations.eterm_obligations env id sigma 0 t termtype in obls, Some constr, typ @@ -400,7 +401,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po if not (Option.is_empty term) then let init_refine = Tacticals.New.tclTHENLIST [ - Refine.refine ~typecheck:false (fun sigma -> (sigma,EConstr.of_constr (Option.get term))); + Refine.refine ~typecheck:false (fun sigma -> (sigma, Option.get term)); Proofview.Unsafe.tclNEWGOALS (CList.map Proofview.with_empty_state gls); Tactics.New.reduce_after_refine; ] @@ -497,10 +498,10 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program (* Check that the type is free of evars now. *) Pretyping.check_evars env (Evd.from_env env) sigma termtype; let termtype = to_constr sigma termtype in - let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in let pstate = if not (Evd.has_undefined sigma) && not (Option.is_empty props) then - (declare_instance_constant k pri global imps ?hook id decl poly sigma (Option.get term) termtype; + let term = to_constr sigma (Option.get term) in + (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; None) else if program_mode || refine || Option.is_empty props then declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index 12df3215ad..d2c986fe5c 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -88,11 +88,12 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct let (c,ctx), sideff = Future.force ce.const_entry_body in assert(Safe_typing.empty_private_constants = sideff); assert(Univ.ContextSet.is_empty ctx); + Obligations.check_evars env evd; + let c = EConstr.of_constr c in let typ = match ce.const_entry_type with - | Some t -> t - | None -> EConstr.to_constr ~abort_on_undefined_evars:false evd (Retyping.get_type_of env evd (EConstr.of_constr c)) + | Some t -> EConstr.of_constr t + | None -> Retyping.get_type_of env evd c in - Obligations.check_evars env evd; let obls, _, c, cty = Obligations.eterm_obligations env ident evd 0 c typ in diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 20a2db7ca2..3befdc5885 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -230,12 +230,9 @@ let build_wellfounded (recname,pl,bl,arityc,body) poly r measure notation = in (* XXX: Capturing sigma here... bad bad *) let hook = Lemmas.mk_hook (hook sigma) in - (* XXX: Grounding non-ground terms here... bad bad *) - let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in - let fullctyp = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in Obligations.check_evars env sigma; let evars, _, evars_def, evars_typ = - Obligations.eterm_obligations env recname sigma 0 fullcoqc fullctyp + Obligations.eterm_obligations env recname sigma 0 def typ in let ctx = Evd.evar_universe_context sigma in ignore(Obligations.add_definition recname ~term:evars_def ~univdecl:decl @@ -262,17 +259,13 @@ let do_program_recursive local poly fixkind fixl ntns = let evd = nf_evar_map_undefined evd in let collect_evars id def typ imps = (* Generalize by the recursive prototypes *) - let def = - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) - and typ = - (* Worrying... *) - EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) - in + let def = nf_evar evd (Termops.it_mkNamedLambda_or_LetIn def rec_sign) in + let typ = nf_evar evd (Termops.it_mkNamedProd_or_LetIn typ rec_sign) in let evm = collect_evars_of_term evd def typ in let evars, _, def, typ = Obligations.eterm_obligations env id evm - (List.length rec_sign) def typ - in (id, def, typ, imps, evars) + (List.length rec_sign) def typ in + (id, def, typ, imps, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in let fiximps = List.map pi2 info in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 1b1c618dc7..771ae2053f 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -39,7 +39,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Constr.named_context; + ev_hyps: EConstr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; @@ -50,11 +50,11 @@ type oblinfo = (** Substitute evar references in t using de Bruijn indices, where n binders were passed through. *) -let subst_evar_constr evs n idf t = +let subst_evar_constr evm evs n idf t = let seen = ref Int.Set.empty in let transparent = ref Id.Set.empty in let evar_info id = List.assoc_f Evar.equal id evs in - let rec substrec (depth, fixrels) c = match Constr.kind c with + let rec substrec (depth, fixrels) c = match EConstr.kind evm c with | Evar (k, args) -> let { ev_name = (id, idstr) ; ev_hyps = hyps ; ev_chop = chop } = @@ -84,18 +84,18 @@ let subst_evar_constr evs n idf t = in aux hyps args [] in if List.exists - (fun x -> match Constr.kind x with + (fun x -> match EConstr.kind evm x with | Rel n -> Int.List.mem n fixrels | _ -> false) args then transparent := Id.Set.add idstr !transparent; - mkApp (idf idstr, Array.of_list args) + EConstr.mkApp (idf idstr, Array.of_list args) | Fix _ -> - Constr.map_with_binders succfix substrec (depth, 1 :: fixrels) c - | _ -> Constr.map_with_binders succfix substrec (depth, fixrels) c + EConstr.map_with_binders evm succfix substrec (depth, 1 :: fixrels) c + | _ -> EConstr.map_with_binders evm succfix substrec (depth, fixrels) c in let t' = substrec (0, []) t in - t', !seen, !transparent + EConstr.to_constr evm t', !seen, !transparent (** Substitute variable references in t using de Bruijn indices, @@ -112,18 +112,18 @@ let subst_vars acc n t = to a product : forall H1 : t1, ..., forall Hn : tn, concl. Changes evars and hypothesis references to variable references. *) -let etype_of_evar evs hyps concl = +let etype_of_evar evm evs hyps concl = let open Context.Named.Declaration in let rec aux acc n = function decl :: tl -> - let t', s, trans = subst_evar_constr evs n mkVar (NamedDecl.get_type decl) in + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar (NamedDecl.get_type decl) in let t'' = subst_vars acc 0 t' in let rest, s', trans' = aux (NamedDecl.get_id decl :: acc) (succ n) tl in let s' = Int.Set.union s s' in let trans' = Id.Set.union trans trans' in (match decl with | LocalDef (id,c,_) -> - let c', s'', trans'' = subst_evar_constr evs n mkVar c in + let c', s'', trans'' = subst_evar_constr evm evs n EConstr.mkVar c in let c' = subst_vars acc 0 c' in mkNamedProd_or_LetIn (LocalDef (id, c', t'')) rest, Int.Set.union s'' s', @@ -131,7 +131,7 @@ let etype_of_evar evs hyps concl = | LocalAssum (id,_) -> mkNamedProd_or_LetIn (LocalAssum (id, t'')) rest, s', trans') | [] -> - let t', s, trans = subst_evar_constr evs n mkVar concl in + let t', s, trans = subst_evar_constr evm evs n EConstr.mkVar concl in subst_vars acc 0 t', s, trans in aux [] 0 (List.rev hyps) @@ -209,9 +209,7 @@ let eterm_obligations env name evm fs ?status t ty = (fun (id, (n, nstr), ev) l -> let hyps = Evd.evar_filtered_context ev in let hyps = trunc_named_context nc_len hyps in - let hyps = EConstr.Unsafe.to_named_context hyps in - let concl = EConstr.Unsafe.to_constr ev.evar_concl in - let evtyp, deps, transp = etype_of_evar l hyps concl in + let evtyp, deps, transp = etype_of_evar evm l hyps ev.evar_concl in let evtyp, hyps, chop = match chop_product fs evtyp with | Some t -> t, trunc_named_context fs hyps, fs @@ -237,9 +235,9 @@ let eterm_obligations env name evm fs ?status t ty = evn [] in let t', _, transparent = (* Substitute evar refs in the term by variables *) - subst_evar_constr evts 0 mkVar t + subst_evar_constr evm evts 0 EConstr.mkVar t in - let ty, _, _ = subst_evar_constr evts 0 mkVar ty in + let ty, _, _ = subst_evar_constr evm evts 0 EConstr.mkVar ty in let evars = List.map (fun (ev, info) -> let { ev_name = (_, name); ev_status = force_status, status; @@ -252,7 +250,7 @@ let eterm_obligations env name evm fs ?status t ty = in name, typ, src, (force_status, status), deps, tac) evts in let evnames = List.map (fun (ev, info) -> ev, snd info.ev_name) evts in - let evmap f c = pi1 (subst_evar_constr evts 0 f c) in + let evmap f c = pi1 (subst_evar_constr evm evts 0 f c) in Array.of_list (List.rev evars), (evnames, evmap), t', ty let hide_obligation () = diff --git a/vernac/obligations.mli b/vernac/obligations.mli index d25daeed9c..9214ddd4b9 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -26,14 +26,14 @@ val sort_dependencies : (Evar.t * evar_info * Evar.Set.t) list -> (Evar.t * evar (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) val eterm_obligations : env -> Id.t -> evar_map -> int -> - ?status:Evar_kinds.obligation_definition_status -> constr -> types -> + ?status:Evar_kinds.obligation_definition_status -> EConstr.constr -> EConstr.types -> (Id.t * types * Evar_kinds.t Loc.located * (bool * Evar_kinds.obligation_definition_status) * Int.Set.t * unit Proofview.tactic option) array (* Existential key, obl. name, type as product, location of the original evar, associated tactic, status and dependencies as indexes into the array *) - * ((Evar.t * Id.t) list * ((Id.t -> constr) -> constr -> constr)) * + * ((Evar.t * Id.t) list * ((Id.t -> EConstr.constr) -> EConstr.constr -> constr)) * constr * types (* Translations from existential identifiers to obligation identifiers and for terms with existentials to closed terms, given a -- cgit v1.2.3 From 6608f64f001f8f1a50b2dc41fefdf63c0b84b270 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 2 Nov 2018 00:17:47 +0100 Subject: Passing evar_map to evars_of_term rather than expecting the term to be evar-nf. --- vernac/comProgramFixpoint.ml | 2 +- vernac/obligations.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac') diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 3befdc5885..69e2a209eb 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -243,7 +243,7 @@ let out_def = function | None -> user_err Pp.(str "Program Fixpoint needs defined bodies.") let collect_evars_of_term evd c ty = - let evars = Evar.Set.union (Evd.evars_of_term c) (Evd.evars_of_term ty) in + let evars = Evar.Set.union (Evd.evars_of_term evd c) (Evd.evars_of_term evd ty) in Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 771ae2053f..f768278dd7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -151,7 +151,7 @@ let evar_dependencies evm oev = let one_step deps = Evar.Set.fold (fun ev s -> let evi = Evd.find evm ev in - let deps' = evars_of_filtered_evar_info evi in + let deps' = evars_of_filtered_evar_info evm evi in if Evar.Set.mem oev deps' then invalid_arg ("Ill-formed evar map: cycle detected for evar " ^ Pp.string_of_ppcmds @@ Evar.print oev) else Evar.Set.union deps' s) -- cgit v1.2.3 From 5e1238260c32227f8568fb1328f922cdeaa8dfc8 Mon Sep 17 00:00:00 2001 From: Jim Fehrle Date: Sun, 12 May 2019 17:44:04 -0700 Subject: Handle tags shorter than "diff." without an exception --- vernac/topfmt.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac') diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 118c126970..bf2efb2542 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -201,7 +201,7 @@ let set_emacs_print_strings () = let diff = "diff." in List.iter (fun b -> let (name, attrs) = b in - if diff = (String.sub name 0 (String.length diff)) then + if CString.is_sub diff name 0 then tag_map := CString.Map.add name { attrs with prefix = Some (Printf.sprintf "<%s>" name); suffix = Some (Printf.sprintf "" name) } -- cgit v1.2.3 From 682ec8fe694e37757d2cd6c98fb5e2e609a6f08f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 9 May 2019 14:07:16 +0200 Subject: Allow run_tactic to return a value, remove hack from ltac2 --- vernac/lemmas.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'vernac') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1c7cc5e636..2dae0ad125 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -395,10 +395,10 @@ let start_proof_with_initialization ~ontop ?hook kind sigma decl recguard thms s maybe_declare_manual_implicits false ref imps; call_hook ?hook ctx [] strength ref) thms_data in let pstate = start_proof ~ontop id ~pl:decl kind sigma t ~hook ~compute_guard:guard in - let pstate, _ = Proof_global.with_current_proof (fun _ p -> + let pstate = Proof_global.simple_with_current_proof (fun _ p -> match init_tac with - | None -> p,(true,[]) - | Some tac -> Proof.run_tactic Global.(env ()) tac p) pstate in + | None -> p + | Some tac -> pi1 @@ Proof.run_tactic Global.(env ()) tac p) pstate in pstate let start_proof_com ~program_mode ~ontop ?inference_hook ?hook kind thms = -- cgit v1.2.3 From e74fce3090323b4d3734f84ee8cf6dc1f5e85953 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 13 May 2019 00:03:36 +0200 Subject: Abstract away the implementation of side-effects in Safe_typing. --- vernac/lemmas.ml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) (limited to 'vernac') diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index 1c7cc5e636..fe895098c0 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -75,13 +75,7 @@ let adjust_guardness_conditions const = function List.interval 0 (List.length ((lam_assum c)))) lemma_guard (Array.to_list fixdefs) in *) - let fold env eff = - try - let _ = Environ.lookup_constant eff.seff_constant env in - env - with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env - in - let env = List.fold_left fold env (Safe_typing.side_effects_of_private_constants eff) in + let env = Safe_typing.push_private_constants env eff in let indexes = search_guard env possible_indexes fixdecls in -- cgit v1.2.3 From a6757b089e1d268517bcba48a9fe33aa47526de2 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Jan 2019 00:06:32 +0100 Subject: Remove Refine Instance Mode option --- vernac/classes.ml | 18 ++++-------------- vernac/classes.mli | 1 - 2 files changed, 4 insertions(+), 15 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index ece9fc8937..05a75ab435 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -31,16 +31,6 @@ module NamedDecl = Context.Named.Declaration open Decl_kinds open Entries -let refine_instance = ref false - -let () = Goptions.(declare_bool_option { - optdepr = true; - optname = "definition of instances by refining"; - optkey = ["Refine";"Instance";"Mode"]; - optread = (fun () -> !refine_instance); - optwrite = (fun b -> refine_instance := b) -}) - let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) @@ -419,7 +409,7 @@ let declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~po | None -> pstate) ()) -let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = +let do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props = let props = match props with | Some (true, { CAst.v = CRecord fs }) -> @@ -503,7 +493,7 @@ let do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program let term = to_constr sigma (Option.get term) in (declare_instance_constant k pri global imps ?hook id decl poly sigma term termtype; None) - else if program_mode || refine || Option.is_empty props then + else if program_mode || Option.is_empty props then declare_instance_open ~pstate env sigma ?hook ~tac ~program_mode ~global ~poly k id pri imps decl (List.map RelDecl.get_name ctx) term termtype else CErrors.user_err Pp.(str "Unsolved obligations remaining.") in id, pstate @@ -550,7 +540,7 @@ let interp_instance_context ~program_mode env ctx ?(generalize=false) pl bk cl = sigma, cl, u, c', ctx', ctx, imps, args, decl -let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mode +let new_instance ~pstate ?(global=false) ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in @@ -566,7 +556,7 @@ let new_instance ~pstate ?(global=false) ?(refine= !refine_instance) ~program_mo Namegen.next_global_ident_away i (Termops.vars_of_env env) in let env' = push_rel_context ctx env in - do_instance ~pstate env env' sigma ?hook ~refine ~tac ~global ~poly ~program_mode + do_instance ~pstate env env' sigma ?hook ~tac ~global ~poly ~program_mode cty k u ctx ctx' pri decl imps subst id props let declare_new_instance ?(global=false) ~program_mode poly ctx (instid, bk, cl) pri = diff --git a/vernac/classes.mli b/vernac/classes.mli index e7f90ff306..57bb9ce312 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -48,7 +48,6 @@ val declare_instance_constant : val new_instance : pstate:Proof_global.t option -> ?global:bool (** Not global by default. *) -> - ?refine:bool (** Allow refinement *) -> program_mode:bool -> Decl_kinds.polymorphic -> local_binder_expr list -> -- cgit v1.2.3 From c352873936db93c251c544383853474736f128d6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 25 Jan 2019 00:48:36 +0100 Subject: Remove VtUnknown classification This clean-up removes the dependency of the current proof mode (and hence the parsing state) on unification. The current proof mode can now be known simply by parsing and elaborating attributes. We give access to attributes from the classifier for this purpose. We remove the infamous `VtUnknown` code path in the STM which is known to be buggy. Fixes #3632 #3890 #4638. --- vernac/vernacextend.ml | 1 - vernac/vernacextend.mli | 1 - 2 files changed, 2 deletions(-) (limited to 'vernac') diff --git a/vernac/vernacextend.ml b/vernac/vernacextend.ml index ef06e59316..730f5fd6da 100644 --- a/vernac/vernacextend.ml +++ b/vernac/vernacextend.ml @@ -36,7 +36,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = diff --git a/vernac/vernacextend.mli b/vernac/vernacextend.mli index 4d89eaffd9..54e08d0e95 100644 --- a/vernac/vernacextend.mli +++ b/vernac/vernacextend.mli @@ -52,7 +52,6 @@ type vernac_type = | VtProofMode of string (* To be removed *) | VtMeta - | VtUnknown and vernac_start = opacity_guarantee * Names.Id.t list and vernac_sideff_type = Names.Id.t list and opacity_guarantee = -- cgit v1.2.3 From a74c28656a7978c429057b62c34227fe2a6cc432 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 1 May 2019 19:03:05 +0200 Subject: [Classes] Use prepare_parameter from DeclareDef. This code was originally part of #8811, authored by Gaëtan Gilbert. It seems we are not very consistent on what we do when we use `ParameterEntry`, specially w.r.t. universes but as code cleanup progresses we will have a better view. Co-authored-by: Gaëtan Gilbert --- vernac/classes.ml | 10 +++------- vernac/comAssumption.ml | 5 +++++ 2 files changed, 8 insertions(+), 7 deletions(-) (limited to 'vernac') diff --git a/vernac/classes.ml b/vernac/classes.ml index 05a75ab435..5a7f60584a 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -318,6 +318,7 @@ let instance_hook k info global imps ?hook cst = (match hook with Some h -> h cst | None -> ()) let declare_instance_constant k info global imps ?hook id decl poly sigma term termtype = + (* XXX: Duplication of the declare_constant path *) let kind = IsDefinition Instance in let sigma = let levels = Univ.LSet.union (CVars.universes_of_constr termtype) @@ -339,14 +340,9 @@ let do_declare_instance env sigma ~global ~poly k u ctx ctx' pri decl imps subst in let (_, ty_constr) = instance_constructor (k,u) subst in let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in - let sigma = Evd.minimize_universes sigma in - Pretyping.check_evars env (Evd.from_env env) sigma termtype; - let univs = Evd.check_univ_decl ~poly sigma decl in - let termtype = to_constr sigma termtype in + let sigma, entry = DeclareDef.prepare_parameter ~allow_evars:false ~poly sigma decl termtype in let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id - (ParameterEntry - (None,(termtype,univs),None), Decl_kinds.IsAssumption Decl_kinds.Logical) - in + (ParameterEntry entry, Decl_kinds.IsAssumption Decl_kinds.Logical) in Declare.declare_univ_binders (ConstRef cst) (Evd.universe_binders sigma); instance_hook k pri global imps (ConstRef cst) diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 3406b6276f..27e31f486d 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -173,6 +173,11 @@ let do_assumptions ~pstate ~program_mode kind nl l = uvars, (coe,t,imps)) Univ.LSet.empty l in + (* XXX: Using `DeclareDef.prepare_parameter` here directly is not + possible as we indeed declare several parameters; however, + restrict_universe_context should be called in a centralized place + IMO, thus I think we should adapt `prepare_parameter` to handle + this case too. *) let sigma = Evd.restrict_universe_context sigma uvars in let uctx = Evd.check_univ_decl ~poly:(pi2 kind) sigma udecl in let ubinders = Evd.universe_binders sigma in -- cgit v1.2.3 From b7e4a0dd032889422a0057162c66e39f2d0187a5 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Mon, 13 May 2019 20:06:06 +0200 Subject: Remove definition-not-visible warning This lets us avoid passing ~ontop to do_definition and co, and after #10050 to even more functions. --- vernac/comAssumption.ml | 21 ++++++++------------- vernac/comAssumption.mli | 9 +++------ vernac/comDefinition.ml | 4 ++-- vernac/comDefinition.mli | 3 +-- vernac/comFixpoint.ml | 4 ++-- vernac/declareDef.ml | 13 +++---------- vernac/declareDef.mli | 6 ++---- vernac/obligations.ml | 10 +++++----- vernac/vernacentries.ml | 14 +++++++------- 9 files changed, 33 insertions(+), 51 deletions(-) (limited to 'vernac') diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 27e31f486d..635751bb24 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -43,7 +43,7 @@ let should_axiom_into_instance = function true | Global | Local -> !axiom_into_instance -let declare_assumption ~pstate is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} = +let declare_assumption is_coe (local,p,kind) (c,ctx) pl imps impl nl {CAst.v=ident} = match local with | Discharge when Lib.sections_are_opened () -> let ctx = match ctx with @@ -53,11 +53,6 @@ match local with let decl = (Lib.cwd(), SectionLocalAssum ((c,ctx),p,impl), IsAssumption kind) in let _ = declare_variable ident decl in let () = assumption_message ident in - let () = - if not !Flags.quiet && Option.has_some pstate then - Feedback.msg_info Pp.(str"Variable" ++ spc () ++ Id.print ident ++ - strbrk " is not visible from current goals") - in let r = VarRef ident in let () = maybe_declare_manual_implicits true r imps in let env = Global.env () in @@ -101,11 +96,11 @@ let next_uctx = | Polymorphic_entry _ as uctx -> uctx | Monomorphic_entry _ -> empty_uctx -let declare_assumptions ~pstate idl is_coe k (c,uctx) pl imps nl = +let declare_assumptions idl is_coe k (c,uctx) pl imps nl = let refs, status, _ = List.fold_left (fun (refs,status,uctx) id -> let ref',u',status' = - declare_assumption ~pstate is_coe k (c,uctx) pl imps false nl id in + declare_assumption is_coe k (c,uctx) pl imps false nl id in (ref',u')::refs, status' && status, next_uctx uctx) ([],true,uctx) idl in @@ -137,7 +132,7 @@ let process_assumptions_udecls kind l = in udecl, List.map (fun (coe, (idl, c)) -> coe, (List.map fst idl, c)) l -let do_assumptions ~pstate ~program_mode kind nl l = +let do_assumptions ~program_mode kind nl l = let open Context.Named.Declaration in let env = Global.env () in let udecl, l = process_assumptions_udecls kind l in @@ -183,7 +178,7 @@ let do_assumptions ~pstate ~program_mode kind nl l = let ubinders = Evd.universe_binders sigma in pi2 (List.fold_left (fun (subst,status,uctx) ((is_coe,idl),t,imps) -> let t = replace_vars subst t in - let refs, status' = declare_assumptions ~pstate idl is_coe kind (t,uctx) ubinders imps nl in + let refs, status' = declare_assumptions idl is_coe kind (t,uctx) ubinders imps nl in let subst' = List.map2 (fun {CAst.v=id} (c,u) -> (id, Constr.mkRef (c,u))) idl refs @@ -231,7 +226,7 @@ let named_of_rel_context l = l ([], []) in ctx -let context ~pstate poly l = +let context poly l = let env = Global.env() in let sigma = Evd.from_env env in let sigma, (_, ((env', fullctx), impls)) = interp_context_evars ~program_mode:false env sigma l in @@ -296,12 +291,12 @@ let context ~pstate poly l = let decl = (Discharge, poly, Definitional) in let nstatus = match b with | None -> - pi3 (declare_assumption ~pstate false decl (t, univs) UnivNames.empty_binders [] impl + pi3 (declare_assumption false decl (t, univs) UnivNames.empty_binders [] impl Declaremods.NoInline (CAst.make id)) | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in - let _gr = DeclareDef.declare_definition ~ontop:pstate id decl entry UnivNames.empty_binders [] in + let _gr = DeclareDef.declare_definition id decl entry UnivNames.empty_binders [] in Lib.sections_are_opened () || Lib.is_modtype_strict () in status && nstatus diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 7c64317b70..8f37bc0ba4 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -16,8 +16,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions - : pstate:Proof_global.t option - -> program_mode:bool + : program_mode:bool -> locality * polymorphic * assumption_object_kind -> Declaremods.inline -> (ident_decl list * constr_expr) with_coercion list @@ -26,8 +25,7 @@ val do_assumptions (** returns [false] if the assumption is neither local to a section, nor in a module type and meant to be instantiated. *) val declare_assumption - : pstate:Proof_global.t option - -> coercion_flag + : coercion_flag -> assumption_kind -> Constr.types Entries.in_universes_entry -> UnivNames.universe_binders @@ -42,8 +40,7 @@ val declare_assumption (** returns [false] if, for lack of section, it declares an assumption (unless in a module type). *) val context - : pstate:Proof_global.t option - -> Decl_kinds.polymorphic + : Decl_kinds.polymorphic -> local_binder_expr list -> bool diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index d2c986fe5c..4cae4b8a74 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -79,7 +79,7 @@ let check_definition ~program_mode (ce, evd, _, imps) = check_evars_are_solved ~program_mode env evd; ce -let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ctypopt = +let do_definition ~program_mode ?hook ident k univdecl bl red_option c ctypopt = let (ce, evd, univdecl, imps as def) = interp_definition ~program_mode univdecl bl (pi2 k) red_option c ctypopt in @@ -104,4 +104,4 @@ let do_definition ~ontop ~program_mode ?hook ident k univdecl bl red_option c ct let ce = check_definition ~program_mode def in let uctx = Evd.evar_universe_context evd in let hook_data = Option.map (fun hook -> hook, uctx, []) hook in - ignore(DeclareDef.declare_definition ~ontop ident k ?hook_data ce (Evd.universe_binders evd) imps) + ignore(DeclareDef.declare_definition ident k ?hook_data ce (Evd.universe_binders evd) imps) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 12853d83e0..fa4860b079 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,8 +17,7 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition - : ontop:Proof_global.t option - -> program_mode:bool + : program_mode:bool -> ?hook:Lemmas.declaration_hook -> Id.t -> definition_kind diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 1912646ffd..00f19f545c 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -284,7 +284,7 @@ let declare_fixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,ctx let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in let fixdecls = List.map Safe_typing.mk_pure_proof fixdecls in - ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, Fixpoint) pl ctx) + ignore (List.map4 (DeclareDef.declare_fix (local, poly, Fixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) fixpoint_message (Some indexes) fixnames; @@ -319,7 +319,7 @@ let declare_cofixpoint ~ontop local poly ((fixnames,fixrs,fixdefs,fixtypes),pl,c let evd = Evd.restrict_universe_context evd vars in let ctx = Evd.check_univ_decl ~poly evd pl in let pl = Evd.universe_binders evd in - ignore (List.map4 (DeclareDef.declare_fix ~ontop (local, poly, CoFixpoint) pl ctx) + ignore (List.map4 (DeclareDef.declare_fix (local, poly, CoFixpoint) pl ctx) fixnames fixdecls fixtypes fiximps); (* Declare the recursive definitions *) cofixpoint_message fixnames; diff --git a/vernac/declareDef.ml b/vernac/declareDef.ml index 052832244b..bdda3314ca 100644 --- a/vernac/declareDef.ml +++ b/vernac/declareDef.ml @@ -14,12 +14,6 @@ open Entries open Globnames open Impargs -let warn_definition_not_visible = - CWarnings.create ~name:"definition-not-visible" ~category:"implicits" - Pp.(fun ident -> - strbrk "Section definition " ++ - Names.Id.print ident ++ strbrk " is not visible from current goals") - let warn_local_declaration = CWarnings.create ~name:"local-declaration" ~category:"scope" Pp.(fun (id,kind) -> @@ -33,12 +27,11 @@ let get_locality id ~kind = function | Local -> true | Global -> false -let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps = +let declare_definition ident (local, p, k) ?hook_data ce pl imps = let fix_exn = Future.fix_exn_of ce.const_entry_body in let gr = match local with | Discharge when Lib.sections_are_opened () -> let _ = declare_variable ident (Lib.cwd(), SectionLocalDef ce, IsDefinition k) in - let () = if Option.has_some ontop then warn_definition_not_visible ident in VarRef ident | Discharge | Local | Global -> let local = get_locality ident ~kind:"definition" local in @@ -57,9 +50,9 @@ let declare_definition ~ontop ident (local, p, k) ?hook_data ce pl imps = end; gr -let declare_fix ~ontop ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = +let declare_fix ?(opaque = false) ?hook_data (_,poly,_ as kind) pl univs f ((def,_),eff) t imps = let ce = definition_entry ~opaque ~types:t ~univs ~eff def in - declare_definition ~ontop f kind ?hook_data ce pl imps + declare_definition f kind ?hook_data ce pl imps let check_definition_evars ~allow_evars sigma = let env = Global.env () in diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 8e4f4bf7fb..c4500d0a6b 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -14,8 +14,7 @@ open Decl_kinds val get_locality : Id.t -> kind:string -> Decl_kinds.locality -> bool val declare_definition - : ontop:Proof_global.t option - -> Id.t + : Id.t -> definition_kind -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) -> Safe_typing.private_constants Entries.definition_entry @@ -24,8 +23,7 @@ val declare_definition -> GlobRef.t val declare_fix - : ontop:Proof_global.t option - -> ?opaque:bool + : ?opaque:bool -> ?hook_data:(Lemmas.declaration_hook * UState.t * (Id.t * Constr.t) list) -> definition_kind -> UnivNames.universe_binders diff --git a/vernac/obligations.ml b/vernac/obligations.ml index f768278dd7..46c4422d17 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -454,7 +454,7 @@ let obligation_substitution expand prg = let ints = intset_to (pred (Array.length obls)) in obl_substitution expand obls ints -let declare_definition ~ontop prg = +let declare_definition prg = let varsubst = obligation_substitution true prg in let body, typ = subst_prog varsubst prg in let nf = UnivSubst.nf_evars_and_universes_opt_subst (fun x -> None) @@ -473,7 +473,7 @@ let declare_definition ~ontop prg = let () = progmap_remove prg in let ubinders = UState.universe_binders uctx in let hook_data = Option.map (fun hook -> hook, uctx, obls) prg.prg_hook in - DeclareDef.declare_definition ~ontop prg.prg_name + DeclareDef.declare_definition prg.prg_name prg.prg_kind ce ubinders prg.prg_implicits ?hook_data let rec lam_index n t acc = @@ -552,7 +552,7 @@ let declare_mutual_definition l = (* Declare the recursive definitions *) let univs = UState.univ_entry ~poly first.prg_ctx in let fix_exn = Hook.get get_fix_exn () in - let kns = List.map4 (DeclareDef.declare_fix ~ontop:None ~opaque (local, poly, kind) UnivNames.empty_binders univs) + let kns = List.map4 (DeclareDef.declare_fix ~opaque (local, poly, kind) UnivNames.empty_binders univs) fixnames fixdecls fixtypes fiximps in (* Declare notations *) List.iter (Metasyntax.add_notation_interpretation (Global.env())) first.prg_notations; @@ -759,7 +759,7 @@ let update_obls prg obls rem = else ( match prg'.prg_deps with | [] -> - let kn = declare_definition ~ontop:None prg' in + let kn = declare_definition prg' in progmap_remove prg'; Defined kn | l -> @@ -1110,7 +1110,7 @@ let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl) let obls,_ = prg.prg_obligations in if Int.equal (Array.length obls) 0 then ( Flags.if_verbose Feedback.msg_info (info ++ str "."); - let cst = declare_definition ~ontop:None prg in + let cst = declare_definition prg in Defined cst) else ( let len = Array.length obls in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index e1d134f3a9..918852239a 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -605,7 +605,7 @@ let vernac_definition ~atts ~pstate discharge kind ({loc;v=id}, pl) def = | Some r -> let sigma, env = get_current_or_global_context ~pstate in Some (snd (Hook.get f_interp_redexp env sigma r)) in - ComDefinition.do_definition ~ontop:pstate ~program_mode name + ComDefinition.do_definition ~program_mode name (local, atts.polymorphic, kind) pl bl red_option c typ_opt ?hook; pstate ) @@ -632,7 +632,7 @@ let vernac_exact_proof ~pstate c = if not status then Feedback.feedback Feedback.AddedAxiom; pstate -let vernac_assumption ~atts ~pstate discharge kind l nl = +let vernac_assumption ~atts discharge kind l nl = let open DefAttributes in let local = enforce_locality_exp atts.locality discharge in let global = local == Global in @@ -642,7 +642,7 @@ let vernac_assumption ~atts ~pstate discharge kind l nl = List.iter (fun (lid, _) -> if global then Dumpglob.dump_definition lid false "ax" else Dumpglob.dump_definition lid true "var") idl) l; - let status = ComAssumption.do_assumptions ~pstate ~program_mode:atts.program kind nl l in + let status = ComAssumption.do_assumptions ~program_mode:atts.program kind nl l in if not status then Feedback.feedback Feedback.AddedAxiom let is_polymorphic_inductive_cumulativity = @@ -1075,8 +1075,8 @@ let vernac_declare_instance ~atts sup inst pri = Dumpglob.dump_definition (fst (pi1 inst)) false "inst"; Classes.declare_new_instance ~program_mode:atts.program ~global atts.polymorphic sup inst pri -let vernac_context ~pstate ~poly l = - if not (ComAssumption.context ~pstate poly l) then Feedback.feedback Feedback.AddedAxiom +let vernac_context ~poly l = + if not (ComAssumption.context poly l) then Feedback.feedback Feedback.AddedAxiom let vernac_existing_instance ~section_local insts = let glob = not section_local in @@ -2300,7 +2300,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = unsupported_attributes atts; vernac_require_open_proof ~pstate (vernac_exact_proof c) | VernacAssumption ((discharge,kind),nl,l) -> - with_def_attributes ~atts vernac_assumption ~pstate discharge kind l nl; + with_def_attributes ~atts vernac_assumption discharge kind l nl; pstate | VernacInductive (cum, priv, finite, l) -> vernac_inductive ~atts cum priv finite l; @@ -2383,7 +2383,7 @@ let rec interp_expr ?proof ~atts ~st c : Proof_global.t option = with_def_attributes ~atts vernac_declare_instance sup inst info; pstate | VernacContext sup -> - let () = vernac_context ~pstate ~poly:(only_polymorphism atts) sup in + let () = vernac_context ~poly:(only_polymorphism atts) sup in pstate | VernacExistingInstance insts -> with_section_locality ~atts vernac_existing_instance insts; -- cgit v1.2.3