diff options
63 files changed, 541 insertions, 460 deletions
diff --git a/dev/doc/shield-icon.png b/dev/doc/shield-icon.png Binary files differindex 629e51a819..f4a5b6ff5e 100644 --- a/dev/doc/shield-icon.png +++ b/dev/doc/shield-icon.png diff --git a/doc/changelog/02-specification-language/13183-using-att.rst b/doc/changelog/02-specification-language/13183-using-att.rst new file mode 100644 index 0000000000..c380d932ed --- /dev/null +++ b/doc/changelog/02-specification-language/13183-using-att.rst @@ -0,0 +1,6 @@ +- **Added:** + Definition and (Co)Fixpoint now support the :attr:`using` attribute. + It has the same effect as :cmd:`Proof using`, which is only available in + interactive mode. + (`#13183 <https://github.com/coq/coq/pull/13183>`_, + by Enrico Tassi). diff --git a/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst b/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst new file mode 100644 index 0000000000..fb12c91729 --- /dev/null +++ b/doc/changelog/03-notations/13092-master+fix-13078-no-binder-in-pattern-notation.rst @@ -0,0 +1,5 @@ +- **Fixed:** + Preventing notations for constructors to involve binders + (`#13092 <https://github.com/coq/coq/pull/13092>`_, + fixes `#13078 <https://github.com/coq/coq/issues/13078>`_, + by Hugo Herbelin). diff --git a/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst b/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst new file mode 100644 index 0000000000..1eb8ef5a2a --- /dev/null +++ b/doc/changelog/05-tactic-language/13247-master+fix13241-locating-nested-ltac-errors.rst @@ -0,0 +1,6 @@ +- **Fixed:** + Miscellaneous issues with locating tactic errors + (`#13247 <https://github.com/coq/coq/pull/13247>`_, + fixes `#12773 <https://github.com/coq/coq/issues/12773>`_ + and `#12992 <https://github.com/coq/coq/issues/12992>`_, + by Hugo Herbelin). diff --git a/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst b/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst new file mode 100644 index 0000000000..f7446cc5aa --- /dev/null +++ b/doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst @@ -0,0 +1,4 @@ +- **Added:** + Support for flag :flag:`Printing Goal Names` in View menu + (`#13145 <https://github.com/coq/coq/pull/13145>`_, + by Hugo Herbelin). diff --git a/doc/sphinx/language/core/coinductive.rst b/doc/sphinx/language/core/coinductive.rst index 0520afd600..2e5dff42ac 100644 --- a/doc/sphinx/language/core/coinductive.rst +++ b/doc/sphinx/language/core/coinductive.rst @@ -28,8 +28,8 @@ More information on co-inductive definitions can be found in This command supports the :attr:`universes(polymorphic)`, :attr:`universes(monomorphic)`, :attr:`universes(template)`, :attr:`universes(notemplate)`, :attr:`universes(cumulative)`, - :attr:`universes(noncumulative)` and :attr:`private(matching)` - attributes. + :attr:`universes(noncumulative)`, :attr:`private(matching)` + and :attr:`using` attributes. .. example:: diff --git a/doc/sphinx/language/core/definitions.rst b/doc/sphinx/language/core/definitions.rst index 8d67a3cf40..1681eee6e7 100644 --- a/doc/sphinx/language/core/definitions.rst +++ b/doc/sphinx/language/core/definitions.rst @@ -87,8 +87,8 @@ Section :ref:`typing-rules`. computation on :n:`@term`. These commands also support the :attr:`universes(polymorphic)`, - :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`) and - :attr:`canonical` attributes. + :attr:`universes(monomorphic)`, :attr:`program` (see :ref:`program_definition`), + :attr:`canonical` and :attr:`using` attributes. If :n:`@term` is omitted, :n:`@type` is required and |Coq| enters proof editing mode. This can be used to define a term incrementally, in particular by relying on the :tacn:`refine` tactic. @@ -159,6 +159,8 @@ Chapter :ref:`Tactics`. The basic assertion command is: correct at some time of the interactive development of a proof, use the command :cmd:`Guarded`. + This command accepts the :attr:`using` attribute. + .. exn:: The term @term has type @type which should be Set, Prop or Type. :undocumented: diff --git a/doc/sphinx/language/core/inductive.rst b/doc/sphinx/language/core/inductive.rst index ba0ec28f8b..1642482bb1 100644 --- a/doc/sphinx/language/core/inductive.rst +++ b/doc/sphinx/language/core/inductive.rst @@ -416,6 +416,8 @@ constructions. In this case, the proof should be terminated with :cmd:`Defined` in order to define a constant for which the computational behavior is relevant. See :ref:`proof-editing-mode`. + This command accepts the :attr:`using` attribute. + .. note:: + Some fixpoints may have several arguments that fit as decreasing diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index b09d6146d8..f4aef8f879 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -199,6 +199,32 @@ list of assertion commands is given in :ref:`Assertions`. The command .. seealso:: :ref:`tactics-implicit-automation` +.. attr:: using + + This attribute can be applied to the :cmd:`Definition`, :cmd:`Example`, + :cmd:`Fixpoint` and :cmd:`CoFixpoint` commands as well as to :cmd:`Lemma` and + its variants. It takes + a :n:`@section_var_expr`, in quotes, as its value. This is equivalent to + specifying the same :n:`@section_var_expr` in + :cmd:`Proof using`. + + .. example:: + + .. coqtop:: all + + Section Test. + Variable n : nat. + Hypothesis Hn : n <> 0. + + #[using="Hn"] + Lemma example : 0 < n. + + .. coqtop:: in + + Abort. + End Test. + + Proof using options ``````````````````` diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 374cb72753..bb2873b486 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -563,6 +563,9 @@ let universes_of_constr sigma c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma u)) s in fold sigma aux s c + | Case (_,_,CaseInvert {univs;args=_},_,_) -> + let s = LSet.fold LSet.add (Instance.levels (EInstance.kind sigma univs)) s in + fold sigma aux s c | _ -> fold sigma aux s c in aux LSet.empty c diff --git a/ide/coqide/coq.ml b/ide/coqide/coq.ml index 1167b8199e..b8228df2aa 100644 --- a/ide/coqide/coq.ml +++ b/ide/coqide/coq.ml @@ -550,6 +550,7 @@ struct let existential = BoolOpt ["Printing"; "Existential"; "Instances"] let universes = BoolOpt ["Printing"; "Universes"] let unfocused = BoolOpt ["Printing"; "Unfocused"] + let goal_names = BoolOpt ["Printing"; "Goal"; "Names"] let diff = StringOpt ["Diffs"] type 'a descr = { opts : 'a t list; init : 'a; label : string } @@ -568,7 +569,8 @@ struct { opts = [universes]; init = false; label = "Display _universe levels" }; { opts = [all_basic;existential;universes]; init = false; label = "Display all _low-level contents" }; - { opts = [unfocused]; init = false; label = "Display _unfocused goals" } + { opts = [unfocused]; init = false; label = "Display _unfocused goals" }; + { opts = [goal_names]; init = false; label = "Display _goal names" } ] let diff_item = { opts = [diff]; init = "off"; label = "Display _proof diffs" } diff --git a/ide/coqide/coqide_ui.ml b/ide/coqide/coqide_ui.ml index 6540fc6fca..badfabf07e 100644 --- a/ide/coqide/coqide_ui.ml +++ b/ide/coqide/coqide_ui.ml @@ -85,6 +85,7 @@ let init () = \n <menuitem action='Display universe levels' />\ \n <menuitem action='Display all low-level contents' />\ \n <menuitem action='Display unfocused goals' />\ +\n <menuitem action='Display goal names' />\ \n <separator/>\ \n <menuitem action='Unset diff' />\ \n <menuitem action='Set diff' />\ diff --git a/ide/coqide/idetop.ml b/ide/coqide/idetop.ml index ddfa3a80bd..602acefa7c 100644 --- a/ide/coqide/idetop.ml +++ b/ide/coqide/idetop.ml @@ -195,7 +195,7 @@ let concl_next_tac = let process_goal sigma g = let env = Goal.V82.env sigma g in let min_env = Environ.reset_context env in - let id = Goal.uid g in + let id = if Printer.print_goal_names () then Names.Id.to_string (Termops.evar_suggested_name g sigma) else "" in let ccl = pr_letype_env ~goal_concl_style:true env sigma (Goal.V82.concl sigma g) in @@ -206,7 +206,7 @@ let process_goal sigma g = let (_env, hyps) = Context.Compacted.fold process_hyp (Termops.compact_named_context (Environ.named_context env)) ~init:(min_env,[]) in - { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id; } + { Interface.goal_hyp = List.rev hyps; Interface.goal_ccl = ccl; Interface.goal_id = id } let process_goal_diffs diff_goal_map oldp nsigma ng = let open Evd in diff --git a/ide/coqide/wg_ProofView.ml b/ide/coqide/wg_ProofView.ml index 1de63953af..8e451c9917 100644 --- a/ide/coqide/wg_ProofView.ml +++ b/ide/coqide/wg_ProofView.ml @@ -52,7 +52,7 @@ let hook_tag_cb tag menu_content sel_cb hover_cb = let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = match goals with | [] -> assert false - | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; } :: rem_goals -> + | { Interface.goal_hyp = hyps; Interface.goal_ccl = cur_goal; Interface.goal_id = cur_id } :: rem_goals -> let on_hover sel_start sel_stop = proof#buffer#remove_tag ~start:proof#buffer#start_iter @@ -68,11 +68,11 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat let head_str = Printf.sprintf "%d subgoal%s\n" goals_cnt (if 1 < goals_cnt then "s" else "") in - let goal_str ?(shownum=false) index total = - if shownum then Printf.sprintf - "______________________________________(%d/%d)\n" index total - else Printf.sprintf - "______________________________________\n" + let goal_str ?(shownum=false) index total id = + let annot = + if CString.is_empty id then if shownum then Printf.sprintf "(%d/%d)" index total else "" + else Printf.sprintf "(?%s)" id in + Printf.sprintf "______________________________________%s\n" annot in (* Insert current goal and its hypotheses *) let hyps_hints, goal_hints = match hints with @@ -103,13 +103,13 @@ let mode_tactic sel_cb (proof : #GText.view_skel) goals ~unfoc_goals hints = mat [tag] else [] in - proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt); + proof#buffer#insert (goal_str ~shownum:true 1 goals_cnt cur_id); insert_xml ~tags:[Tags.Proof.goal] proof#buffer (Richpp.richpp_of_pp width cur_goal); proof#buffer#insert "\n" in (* Insert remaining goals (no hypotheses) *) - let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g } = - proof#buffer#insert (goal_str ~shownum i goals_cnt); + let fold_goal ?(shownum=false) i _ { Interface.goal_ccl = g; Interface.goal_id = id } = + proof#buffer#insert (goal_str ~shownum i goals_cnt id); insert_xml proof#buffer (Richpp.richpp_of_pp width g); proof#buffer#insert "\n" in @@ -178,12 +178,16 @@ let display mode (view : #GText.view_skel) goals hints evars = | _, _, _, _ -> (* No foreground proofs, but still unfocused ones *) let total = List.length bg in - let goal_str index = Printf.sprintf - "______________________________________(%d/%d)\n" index total + let goal_str index id = + let annot = + if CString.is_empty id then Printf.sprintf "(%d/%d)" index total + else Printf.sprintf "(?%s)" id in + Printf.sprintf + "______________________________________%s\n" annot in view#buffer#insert "This subproof is complete, but there are some unfocused goals:\n\n"; let iter i goal = - let () = view#buffer#insert (goal_str (succ i)) in + let () = view#buffer#insert (goal_str (succ i) goal.Interface.goal_id) in insert_xml view#buffer (Richpp.richpp_of_pp width goal.Interface.goal_ccl); view#buffer#insert "\n" in diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 2853eef5c5..ee07fb6ed1 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -114,8 +114,8 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp ungeneralizable loc id) vars; vars -let rec make_fresh ids env x = - if is_freevar ids env x then x else make_fresh ids env (Nameops.increment_subscript x) +let make_fresh ids env x = + Namegen.next_ident_away_from x (fun x -> not (is_freevar ids env x)) let next_name_away_from na avoid = match na with diff --git a/interp/notation.ml b/interp/notation.ml index 269e20c16e..c150ae7abb 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -341,22 +341,27 @@ type notation_rule = interp_rule * interpretation * notation_applicative_status let notation_rule_eq (rule1,pat1,s1 as x1) (rule2,pat2,s2 as x2) = x1 == x2 || (rule1 = rule2 && interpretation_eq pat1 pat2 && s1 = s2) +let also_cases_notation_rule_eq (also_cases1,rule1) (also_cases2,rule2) = + (* No need in principle to compare also_cases as it is inferred *) + also_cases1 = also_cases2 && notation_rule_eq rule1 rule2 + let keymap_add key interp map = let old = try KeyMap.find key map with Not_found -> [] in (* In case of re-import, no need to keep the previous copy *) - let old = try List.remove_first (notation_rule_eq interp) old with Not_found -> old in + let old = try List.remove_first (also_cases_notation_rule_eq interp) old with Not_found -> old in KeyMap.add key (interp :: old) map let keymap_remove key interp map = let old = try KeyMap.find key map with Not_found -> [] in - KeyMap.add key (List.remove_first (notation_rule_eq interp) old) map + KeyMap.add key (List.remove_first (also_cases_notation_rule_eq interp) old) map let keymap_find key map = try KeyMap.find key map with Not_found -> [] (* Scopes table : interpretation -> scope_name *) -let notations_key_table = ref (KeyMap.empty : notation_rule list KeyMap.t) +(* Boolean = for cases pattern also *) +let notations_key_table = ref (KeyMap.empty : (bool * notation_rule) list KeyMap.t) let glob_prim_constr_key c = match DAst.get c with | GRef (ref, _) -> Some (canonical_gr ref) @@ -1333,13 +1338,13 @@ let check_printing_override (scopt,ntn) data parsingdata printingdata = exists) printingdata in parsing_update, exists -let remove_uninterpretation rule (metas,c as pat) = +let remove_uninterpretation rule also_in_cases_pattern (metas,c as pat) = let (key,n) = notation_constr_key c in - notations_key_table := keymap_remove key (rule,pat,n) !notations_key_table + notations_key_table := keymap_remove key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table -let declare_uninterpretation rule (metas,c as pat) = +let declare_uninterpretation ?(also_in_cases_pattern=true) rule (metas,c as pat) = let (key,n) = notation_constr_key c in - notations_key_table := keymap_add key (rule,pat,n) !notations_key_table + notations_key_table := keymap_add key (also_in_cases_pattern,(rule,pat,n)) !notations_key_table let update_notation_data (scopt,ntn) use data table = let (parsingdata,printingdata) = @@ -1448,14 +1453,17 @@ let interp_notation ?loc ntn local_scopes = (str "Unknown interpretation for notation " ++ pr_notation ntn ++ str ".") let uninterp_notations c = - List.map_append (fun key -> keymap_find key !notations_key_table) + List.map_append (fun key -> List.map snd (keymap_find key !notations_key_table)) (glob_constr_keys c) +let filter_also_for_pattern = + List.map_filter (function (true,x) -> Some x | _ -> None) + let uninterp_cases_pattern_notations c = - keymap_find (cases_pattern_key c) !notations_key_table + filter_also_for_pattern (keymap_find (cases_pattern_key c) !notations_key_table) let uninterp_ind_pattern_notations ind = - keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table + filter_also_for_pattern (keymap_find (RefKey (canonical_gr (GlobRef.IndRef ind))) !notations_key_table) let has_active_parsing_rule_in_scope ntn sc = try @@ -1615,7 +1623,7 @@ type entry_coercion_kind = | IsEntryGlobal of string * int | IsEntryIdent of string * int -let declare_notation (scopt,ntn) pat df ~use coe deprecation = +let declare_notation (scopt,ntn) pat df ~use ~also_in_cases_pattern coe deprecation = (* Register the interpretation *) let scope = match scopt with NotationInScope s -> s | LastLonelyNotation -> default_scope in let sc = find_scope scope in @@ -1630,10 +1638,10 @@ let declare_notation (scopt,ntn) pat df ~use coe deprecation = scope_map := String.Map.add scope sc !scope_map; (* Update the uninterpretation cache *) begin match printing_update with - | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) pat + | Some pat -> remove_uninterpretation (NotationRule (scopt,ntn)) also_in_cases_pattern pat | None -> () end; - if not exists && use <> OnlyParsing then declare_uninterpretation (NotationRule (scopt,ntn)) pat; + if not exists && use <> OnlyParsing then declare_uninterpretation ~also_in_cases_pattern (NotationRule (scopt,ntn)) pat; (* Register visibility of lonely notations *) if not exists then begin match scopt with | LastLonelyNotation -> scope_stack := LonelyNotationItem ntn :: !scope_stack diff --git a/interp/notation.mli b/interp/notation.mli index d744ff41d9..4d6d640a2d 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -234,7 +234,7 @@ type notation_use = | OnlyParsing | ParsingAndPrinting -val declare_uninterpretation : interp_rule -> interpretation -> unit +val declare_uninterpretation : ?also_in_cases_pattern:bool -> interp_rule -> interpretation -> unit type entry_coercion_kind = | IsEntryCoercion of notation_entry_level @@ -243,6 +243,7 @@ type entry_coercion_kind = val declare_notation : notation_with_optional_scope * notation -> interpretation -> notation_location -> use:notation_use -> + also_in_cases_pattern:bool -> entry_coercion_kind option -> Deprecation.t option -> unit diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index fe874cd01d..24b5dfce29 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -1436,9 +1436,8 @@ let reorder_canonically_substitution terms termlists metas = List.fold_right (fun (x,(scl,typ)) (terms',termlists') -> match typ with | NtnTypeConstr -> ((Id.List.assoc x terms, scl)::terms',termlists') - | NtnTypeBinder _ -> assert false | NtnTypeConstrList -> (terms',(Id.List.assoc x termlists,scl)::termlists') - | NtnTypeBinderList -> assert false) + | NtnTypeBinder _ | NtnTypeBinderList -> anomaly (str "Unexpected binder in pattern notation.")) metas ([],[]) let match_notation_constr_cases_pattern c (metas,pat) = diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index bd3e234a91..f3ad3546ff 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -22,6 +22,7 @@ type syndef = { syndef_pattern : interpretation; syndef_onlyparsing : bool; syndef_deprecation : Deprecation.t option; + syndef_also_in_cases_pattern : bool; } let syntax_table = @@ -52,7 +53,7 @@ let open_syntax_constant i ((sp,kn),(_local,syndef)) = if not syndef.syndef_onlyparsing then (* Redeclare it to be used as (short) name in case an other (distfix) notation was declared in between *) - Notation.declare_uninterpretation (Notation.SynDefRule kn) pat + Notation.declare_uninterpretation ~also_in_cases_pattern:syndef.syndef_also_in_cases_pattern (Notation.SynDefRule kn) pat end let cache_syntax_constant d = @@ -81,11 +82,12 @@ let in_syntax_constant : (bool * syndef) -> obj = subst_function = subst_syntax_constant; classify_function = classify_syntax_constant } -let declare_syntactic_definition ~local deprecation id ~onlyparsing pat = +let declare_syntactic_definition ~local ?(also_in_cases_pattern=true) deprecation id ~onlyparsing pat = let syndef = { syndef_pattern = pat; syndef_onlyparsing = onlyparsing; syndef_deprecation = deprecation; + syndef_also_in_cases_pattern = also_in_cases_pattern; } in let _ = add_leaf id (in_syntax_constant (local,syndef)) in () diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index 66a3132f2a..31f685152c 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -13,7 +13,7 @@ open Notation_term (** Syntactic definitions. *) -val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t -> +val declare_syntactic_definition : local:bool -> ?also_in_cases_pattern:bool -> Deprecation.t option -> Id.t -> onlyparsing:bool -> interpretation -> unit val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index a23ef8fdca..952237ab99 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1165,7 +1165,7 @@ module FNativeEntries = let mkFloat env f = check_float env; - { mark = mark Norm KnownR; term = FFloat f } + { mark = mark Cstr KnownR; term = FFloat f } let mkBool env b = check_bool env; @@ -1328,10 +1328,14 @@ let rec knr info tab m stk = | FFlex(ConstKey (kn,_u as c)) when red_set info.i_flags (fCONST kn) -> (match ref_value_cache info tab (ConstKey c) with | Def v -> kni info tab v stk - | Primitive op when check_native_args op stk -> - let rargs, a, nargs, stk = get_native_args1 op c stk in - kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) - | Undef _ | OpaqueDef _ | Primitive _ -> (set_norm m; (m,stk))) + | Primitive op -> + if check_native_args op stk then + let rargs, a, nargs, stk = get_native_args1 op c stk in + kni info tab a (Zprimitive(op,c,rargs,nargs)::stk) + else + (* Similarly to fix, partially applied primitives are not Norm! *) + (m, stk) + | Undef _ | OpaqueDef _ -> (set_norm m; (m,stk))) | FFlex(VarKey id) when red_set info.i_flags (fVAR id) -> (match ref_value_cache info tab (VarKey id) with | Def v -> kni info tab v stk diff --git a/kernel/vars.ml b/kernel/vars.ml index f7e28b0cfe..a446fa413c 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -348,5 +348,8 @@ let universes_of_constr c = | Array (u,_,_,_) -> let s = LSet.fold LSet.add (Instance.levels u) s in Constr.fold aux s c + | Case (_,_,CaseInvert {univs;args=_},_,_) -> + let s = LSet.fold LSet.add (Instance.levels univs) s in + Constr.fold aux s c | _ -> Constr.fold aux s c in aux LSet.empty c diff --git a/lib/control.ml b/lib/control.ml index bb42b5727e..95ea3935a7 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -18,10 +18,12 @@ let enable_thread_delay = ref false let check_for_interrupt () = if !interrupt then begin interrupt := false; raise Sys.Break end; - incr steps; - if !enable_thread_delay && !steps = 1000 then begin - Thread.delay 0.001; - steps := 0; + if !enable_thread_delay then begin + incr steps; + if !steps = 1000 then begin + Thread.delay 0.001; + steps := 0; + end end (** This function does not work on windows, sigh... *) diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index c38a4dcd90..c54f8ffa78 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -466,7 +466,7 @@ END VERNAC COMMAND EXTEND VernacPrintLtac CLASSIFIED AS QUERY | [ "Print" "Ltac" reference(r) ] -> - { Feedback.msg_notice (Tacintern.print_ltac r) } + { Feedback.msg_notice (Tacentries.print_ltac r) } END VERNAC COMMAND EXTEND VernacLocateLtac CLASSIFIED AS QUERY diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index ee28229cb7..4c1fe6417e 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -394,8 +394,13 @@ type appl = (* Values for interpretation *) type tacvalue = - | VFun of appl * Tacexpr.ltac_trace * Loc.t option * Val.t Id.Map.t * - Name.t list * Tacexpr.glob_tactic_expr + | VFun of + appl * + Tacexpr.ltac_trace * + Loc.t option * (* when executing a global Ltac function: the location where this function was called *) + Val.t Id.Map.t * (* closure *) + Name.t list * (* binders *) + Tacexpr.glob_tactic_expr (* body *) | VRec of Val.t Id.Map.t ref * Tacexpr.glob_tactic_expr let (wit_tacvalue : (Empty.t, tacvalue, tacvalue) Genarg.genarg_type) = diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index a05b36c1b4..29e29044f1 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -528,16 +528,40 @@ let print_ltacs () = let locatable_ltac = "Ltac" +let split_ltac_fun = function + | Tacexpr.TacFun (l,t) -> (l,t) + | t -> ([],t) + +let pr_ltac_fun_arg n = spc () ++ Name.print n + +let print_ltac_body qid tac = + let filter mp = + try Some (Nametab.shortest_qualid_of_module mp) + with Not_found -> None + in + let mods = List.map_filter filter tac.Tacenv.tac_redef in + let redefined = match mods with + | [] -> mt () + | mods -> + let redef = prlist_with_sep fnl pr_qualid mods in + fnl () ++ str "Redefined by:" ++ fnl () ++ redef + in + let l,t = split_ltac_fun tac.Tacenv.tac_body in + hv 2 ( + hov 2 (str "Ltac" ++ spc() ++ pr_qualid qid ++ + prlist pr_ltac_fun_arg l ++ spc () ++ str ":=") + ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined + let () = let open Prettyp in - let locate qid = try Some (Tacenv.locate_tactic qid) with Not_found -> None in - let locate_all = Tacenv.locate_extended_all_tactic in - let shortest_qualid = Tacenv.shortest_qualid_of_tactic in - let name kn = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in - let print kn = - let qid = qualid_of_path (Tacenv.path_of_tactic kn) in - Tacintern.print_ltac qid - in + let locate qid = try Some (qid, Tacenv.locate_tactic qid) with Not_found -> None in + let locate_all qid = List.map (fun kn -> (qid,kn)) (Tacenv.locate_extended_all_tactic qid) in + let shortest_qualid (qid,kn) = Tacenv.shortest_qualid_of_tactic kn in + let name (qid,kn) = str "Ltac" ++ spc () ++ pr_path (Tacenv.path_of_tactic kn) in + let print (qid,kn) = + let entries = Tacenv.ltac_entries () in + let tac = KNmap.find kn entries in + print_ltac_body qid tac in let about = name in register_locatable locatable_ltac { locate; @@ -551,6 +575,17 @@ let () = let print_located_tactic qid = Feedback.msg_notice (Prettyp.print_located_other locatable_ltac qid) +let print_ltac id = + try + let kn = Tacenv.locate_tactic id in + let entries = Tacenv.ltac_entries () in + let tac = KNmap.find kn entries in + print_ltac_body id tac + with + Not_found -> + user_err ~hdr:"print_ltac" + (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") + (** Grammar *) let () = diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli index 6ee3ce091b..fc9ab54eba 100644 --- a/plugins/ltac/tacentries.mli +++ b/plugins/ltac/tacentries.mli @@ -69,6 +69,9 @@ val print_ltacs : unit -> unit val print_located_tactic : Libnames.qualid -> unit (** Display the absolute name of a tactic. *) +val print_ltac : Libnames.qualid -> Pp.t +(** Display the definition of a tactic. *) + (** {5 Low-level registering of tactics} *) type (_, 'a) ml_ty_sig = diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 9c3b05fdf1..47f1d3bf66 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -769,38 +769,6 @@ let glob_tactic_env l env x = (intern_pure_tactic { (Genintern.empty_glob_sign env) with ltacvars }) x -let split_ltac_fun = function - | TacFun (l,t) -> (l,t) - | t -> ([],t) - -let pr_ltac_fun_arg n = spc () ++ Name.print n - -let print_ltac id = - try - let kn = Tacenv.locate_tactic id in - let entries = Tacenv.ltac_entries () in - let tac = KNmap.find kn entries in - let filter mp = - try Some (Nametab.shortest_qualid_of_module mp) - with Not_found -> None - in - let mods = List.map_filter filter tac.Tacenv.tac_redef in - let redefined = match mods with - | [] -> mt () - | mods -> - let redef = prlist_with_sep fnl pr_qualid mods in - fnl () ++ str "Redefined by:" ++ fnl () ++ redef - in - let l,t = split_ltac_fun tac.Tacenv.tac_body in - hv 2 ( - hov 2 (str "Ltac" ++ spc() ++ pr_qualid id ++ - prlist pr_ltac_fun_arg l ++ spc () ++ str ":=") - ++ spc() ++ Pptactic.pr_glob_tactic (Global.env ()) t) ++ redefined - with - Not_found -> - user_err ~hdr:"print_ltac" - (pr_qualid id ++ spc() ++ str "is not a user defined tactic.") - (** Registering *) let lift intern = (); fun ist x -> (ist, intern ist x) diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index 22ec15566b..f779aa470c 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -55,9 +55,6 @@ val intern_hyp : glob_sign -> lident -> lident val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument -(** printing *) -val print_ltac : Libnames.qualid -> Pp.t - (** Reduction expressions *) val intern_red_expr : glob_sign -> raw_red_expr -> glob_red_expr diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 7728415ddd..3d734d3a66 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -153,11 +153,15 @@ let add_extra_loc loc extra = match loc with | None -> extra | Some loc -> TacStore.set extra f_loc loc -let add_loc loc ist = +let extract_loc ist = TacStore.get ist.extra f_loc + +let ensure_loc loc ist = match loc with | None -> ist - | Some loc -> { ist with extra = TacStore.set ist.extra f_loc loc } -let extract_loc ist = TacStore.get ist.extra f_loc + | Some loc -> + match extract_loc ist with + | None -> { ist with extra = TacStore.set ist.extra f_loc loc } + | Some _ -> ist let print_top_val env v = Pptactic.pr_value Pptactic.ltop v @@ -1175,7 +1179,7 @@ and eval_tactic_ist ist tac : unit Proofview.tactic = match tac with | TacFirst l -> Tacticals.New.tclFIRST (List.map (interp_tactic ist) l) | TacSolve l -> Tacticals.New.tclSOLVE (List.map (interp_tactic ist) l) | TacComplete tac -> Tacticals.New.tclCOMPLETE (interp_tactic ist tac) - | TacArg {CAst.loc} -> Ftactic.run (val_interp (add_loc loc ist) tac) (fun v -> tactic_of_value ist v) + | TacArg {CAst.loc} -> Ftactic.run (val_interp (ensure_loc loc ist) tac) (fun v -> tactic_of_value ist v) | TacSelect (sel, tac) -> Tacticals.New.tclSELECT sel (interp_tactic ist tac) (* For extensions *) | TacAlias {loc; v=(s,l)} -> @@ -1254,9 +1258,12 @@ and interp_ltac_reference ?loc' mustbetac ist r : Val.t Ftactic.t = let extra = TacStore.set extra f_trace trace in let ist = { lfun = Id.Map.empty; poly; extra } in let appl = GlbAppl[r,[]] in + (* We call a global ltac reference: add a loc on its executation only if not + already in another global reference *) + let ist = ensure_loc loc ist in Profile_ltac.do_profile "interp_ltac_reference" trace ~count_call:false - (catch_error_tac_loc (* interp *) loc false trace - (val_interp ~appl (add_loc (* exec *) loc ist) (Tacenv.interp_ltac r))) + (catch_error_tac_loc (* loc for interpretation *) loc false trace + (val_interp ~appl ist (Tacenv.interp_ltac r))) and interp_tacarg ist arg : Val.t Ftactic.t = match arg with @@ -1325,7 +1332,7 @@ and interp_app loc ist fv largs : Val.t Ftactic.t = ; extra = TacStore.set ist.extra f_trace [] } in Profile_ltac.do_profile "interp_app" trace ~count_call:false - (catch_error_tac_loc loc false trace (val_interp (add_loc loc ist) body)) >>= fun v -> + (catch_error_tac_loc loc false trace (val_interp (ensure_loc loc ist) body)) >>= fun v -> Ftactic.return (name_vfun (push_appl appl largs) v) end begin fun (e, info) -> diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 8da1d636f0..45d0e39ed6 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -681,13 +681,10 @@ let tag_var = tag Tag.variable | CDelimiters (sc,a) -> return (pr_delimiters sc (pr mt (LevelLe ldelim) a), ldelim) | CArray(u, t,def,ty) -> - let pp = ref (str " |"++ spc () ++ pr mt ltop def - ++ pr_opt_type_spc (pr mt) ty ++ str " |]" ++ pr_universe_instance u) in - for i = Array.length t - 1 downto 1 do - pp := str ";" ++ pr mt ltop t.(i) ++ !pp - done; - pp := pr mt ltop t.(0) ++ !pp; - hov 0 (str "[|" ++ !pp), 0 + hov 0 (str "[| " ++ prvect_with_sep (fun () -> str "; ") (pr mt ltop) t ++ + (if not (Array.is_empty t) then str " " else mt()) ++ + str "|" ++ spc() ++ pr mt ltop def ++ pr_opt_type_spc (pr mt) ty ++ + str " |]" ++ pr_universe_instance u), 0 in let loc = constr_loc a in pr_with_comments ?loc diff --git a/printing/printer.ml b/printing/printer.ml index be1cc0d64a..ea718526de 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -45,6 +45,8 @@ let should_gname = ~key:["Printing";"Goal";"Names"] ~value:false +let print_goal_names = should_gname (* for export *) + (**********************************************************************) (** Terms *) diff --git a/printing/printer.mli b/printing/printer.mli index a25cbebe91..ea388ae57e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -264,3 +264,6 @@ val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t val pr_goal_emacs : proof:Proof.t option -> int -> int -> Pp.t val pr_typing_flags : Declarations.typing_flags -> Pp.t + +(** Tells if flag "Printing Goal Names" is activated *) +val print_goal_names : unit -> bool diff --git a/stm/stm.ml b/stm/stm.ml index 85f889c879..df7e35beb5 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -2275,8 +2275,9 @@ let known_state ~doc ?(redefine_qed=false) ~cache id = ), true, true | `MaybeASync (start, nodes, name, delegate) -> (fun () -> reach ~cache:true start; - (* no sections *) - if CList.is_empty (Environ.named_context (Global.env ())) + if CList.is_empty (Environ.named_context (Global.env ())) (* no sections *) + || PG_compat.get_pstate () |> (* #[using] attribute *) + Option.cata (fun x -> Option.has_some (Declare.Proof.get_used_variables x)) false then Util.pi1 (aux (`ASync (start, nodes, name, delegate))) () else Util.pi1 (aux (`Sync (name, `NoPU_NoHint_NoES))) () ), not redefine_qed, true diff --git a/test-suite/bugs/closed/bug_13078.v b/test-suite/bugs/closed/bug_13078.v new file mode 100644 index 0000000000..ec04408fd1 --- /dev/null +++ b/test-suite/bugs/closed/bug_13078.v @@ -0,0 +1,10 @@ +(* Check that rules with patterns are not registered for cases patterns *) +Module PrintingTest. +Declare Custom Entry test. +Notation "& x" := (Some x) (in custom test at level 0, x pattern). +Check fun x => match x with | None => None | Some tt => Some tt end. +Notation "& x" := (Some x) (at level 0, x pattern). +Check fun x => match x with | None => None | Some tt => Some tt end. +End PrintingTest. + +Fail Notation "x &" := (Some x) (at level 0, x pattern). diff --git a/test-suite/bugs/closed/bug_13131.v b/test-suite/bugs/closed/bug_13131.v new file mode 100644 index 0000000000..b358ae3ecc --- /dev/null +++ b/test-suite/bugs/closed/bug_13131.v @@ -0,0 +1,6 @@ +Set Mangle Names. + +Class A := {}. + +Lemma foo `{A} : A. +Proof. Fail exact H. assumption. Qed. diff --git a/test-suite/bugs/closed/bug_13178.v b/test-suite/bugs/closed/bug_13178.v new file mode 100644 index 0000000000..d9c516c362 --- /dev/null +++ b/test-suite/bugs/closed/bug_13178.v @@ -0,0 +1,3 @@ +Primitive array := #array_type. + +Check [| | 0 |]. diff --git a/test-suite/bugs/closed/bug_13276.v b/test-suite/bugs/closed/bug_13276.v new file mode 100644 index 0000000000..15ac7e7b36 --- /dev/null +++ b/test-suite/bugs/closed/bug_13276.v @@ -0,0 +1,9 @@ +From Coq Require Import Floats. +Open Scope float_scope. + +Lemma foo : + let n := opp 0 in sub n 0 = n. +Proof. +cbv. +apply eq_refl. +Qed. diff --git a/test-suite/bugs/opened/bug_3395.v b/test-suite/bugs/opened/bug_3395.v deleted file mode 100644 index 70b3a48a06..0000000000 --- a/test-suite/bugs/opened/bug_3395.v +++ /dev/null @@ -1,232 +0,0 @@ -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) -Generalizable All Variables. -Set Implicit Arguments. - -Arguments fst {_ _} _. -Arguments snd {_ _} _. - -Axiom cheat : forall {T}, T. - -Reserved Notation "g 'o' f" (at level 40, left associativity). - -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. -Arguments idpath {A a} , [A] a. -Notation "x = y" := (paths x y) : type_scope. - -Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x - := match p with idpath => idpath end. - -Delimit Scope morphism_scope with morphism. -Delimit Scope category_scope with category. -Delimit Scope object_scope with object. -Record PreCategory (object : Type) := - Build_PreCategory' { - object :> Type := object; - morphism : object -> object -> Type; - identity : forall x, morphism x x; - compose : forall s d d', - morphism d d' - -> morphism s d - -> morphism s d' - where "f 'o' g" := (compose f g); - associativity : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - (m3 o m2) o m1 = m3 o (m2 o m1); - associativity_sym : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - m3 o (m2 o m1) = (m3 o m2) o m1; - left_identity : forall a b (f : morphism a b), identity b o f = f; - right_identity : forall a b (f : morphism a b), f o identity a = f; - identity_identity : forall x, identity x o identity x = identity x - }. -Bind Scope category_scope with PreCategory. -Arguments PreCategory {_}. -Arguments identity {_} [!C%category] x%object : rename. - -Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. - -Infix "o" := compose : morphism_scope. - -Delimit Scope functor_scope with functor. -Local Open Scope morphism_scope. -Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := - { - object_of :> C -> D; - morphism_of : forall s d, morphism C s d - -> morphism D (object_of s) (object_of d); - composition_of : forall s d d' - (m1 : morphism C s d) (m2: morphism C d d'), - morphism_of _ _ (m2 o m1) - = (morphism_of _ _ m2) o (morphism_of _ _ m1); - identity_of : forall x, morphism_of _ _ (identity x) - = identity (object_of x) - }. -Bind Scope functor_scope with Functor. - -Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. - -Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. - -Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := - { - morphism_inverse : morphism C d s; - left_inverse : morphism_inverse o m = identity _; - right_inverse : m o morphism_inverse = identity _ - }. - -Definition opposite `(C : @PreCategory objC) : PreCategory - := @Build_PreCategory' - C - (fun s d => morphism C d s) - (identity (C := C)) - (fun _ _ _ m1 m2 => m2 o m1) - (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) - (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) - (fun _ _ => @right_identity _ _ _ _) - (fun _ _ => @left_identity _ _ _ _) - (@identity_identity _ C). - -Notation "C ^op" := (opposite C) (at level 3) : category_scope. - -Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). - refine (@Build_PreCategory' - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) - * morphism D (snd s) (snd d))%type) - (fun x => (identity (fst x), identity (snd x))) - (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) - _ - _ - _ - _ - _); admit. -Defined. -Infix "*" := prod : category_scope. - -Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E - := Build_Functor - C E - (fun c => G (F c)) - (fun _ _ m => morphism_of G (morphism_of F m)) - cheat - cheat. - -Infix "o" := compose_functor : functor_scope. - -Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := - Build_NaturalTransformation' { - components_of :> forall c, morphism D (F c) (G c); - commutes : forall s d (m : morphism C s d), - components_of d o F _1 m = G _1 m o components_of s; - - commutes_sym : forall s d (m : C.(morphism) s d), - G _1 m o components_of s = components_of d o F _1 m - }. -Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory - := @Build_PreCategory' (Functor C D) - (@NaturalTransformation _ C _ D) - cheat - cheat - cheat - cheat - cheat - cheat - cheat. - -Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op - := Build_Functor (C^op) (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). - -Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op - := Build_Functor C (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). -Notation "F ^op" := (opposite_functor F) : functor_scope. - -Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. -Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C - := Build_Functor (C * D) C - (@fst _ _) - (fun _ _ => @fst _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). - -Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D - := Build_Functor (C * D) D - (@snd _ _) - (fun _ _ => @snd _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). -Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') -: Functor C (D * D') - := Build_Functor - C (D * D') - (fun c => (F c, F' c)) - (fun s d m => (F _1 m, F' _1 m))%morphism - cheat - cheat. -Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') - := (prod_functor (F o fst) (F' o snd))%functor. -Notation cat_of obj := - (@Build_PreCategory' obj - (fun x y => forall _ : x, y) - (fun _ x => x) - (fun _ _ _ f g x => f (g x))%core - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ => idpath)). - -Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) - := Build_Functor _ _ cheat cheat cheat cheat. - -Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) -: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) - := Build_NaturalTransformation' _ _ cheat cheat cheat. - -Class IsFullyFaithful `(F : @Functor objC C objD D) - := is_fully_faithful - : forall x y : C, - IsIsomorphism (induced_hom_natural_transformation F (x, y)). - -Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) - := cheat. - -Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) - := (((coyoneda A^op)^op'L)^op'L)%functor. -Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). -Admitted. - -Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda. - Time let t := (type of CYE) in - let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) - Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). - Time let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) -Fail Timeout 2 Defined. -Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) - -Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda; simpl in *. - Fail Timeout 1 exact CYE. - Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) -Abort. diff --git a/test-suite/output/ErrorLocation_13241_1.out b/test-suite/output/ErrorLocation_13241_1.out new file mode 100644 index 0000000000..d899dd5d46 --- /dev/null +++ b/test-suite/output/ErrorLocation_13241_1.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_13241_1.v b/test-suite/output/ErrorLocation_13241_1.v new file mode 100644 index 0000000000..ff92085133 --- /dev/null +++ b/test-suite/output/ErrorLocation_13241_1.v @@ -0,0 +1,4 @@ +Ltac a := intro. +Ltac b := a. +Goal True. +b. diff --git a/test-suite/output/ErrorLocation_13241_2.out b/test-suite/output/ErrorLocation_13241_2.out new file mode 100644 index 0000000000..d899dd5d46 --- /dev/null +++ b/test-suite/output/ErrorLocation_13241_2.out @@ -0,0 +1,3 @@ +File "stdin", line 4, characters 0-1: +Error: No product even after head-reduction. + diff --git a/test-suite/output/ErrorLocation_13241_2.v b/test-suite/output/ErrorLocation_13241_2.v new file mode 100644 index 0000000000..280d4a3506 --- /dev/null +++ b/test-suite/output/ErrorLocation_13241_2.v @@ -0,0 +1,4 @@ +Ltac a _ := intro. +Ltac b := a (). +Goal True. +b. diff --git a/test-suite/output/bug_13004.out b/test-suite/output/bug_13004.out index 2bd7d67535..28bc580202 100644 --- a/test-suite/output/bug_13004.out +++ b/test-suite/output/bug_13004.out @@ -1,2 +1,2 @@ -Ltac bug_13004.t := ltac2:(print (of_string "hi")) -Ltac bug_13004.u := ident:(H) +Ltac t := ltac2:(print (of_string "hi")) +Ltac u := ident:(H) diff --git a/test-suite/output/bug_13238.out b/test-suite/output/bug_13238.out index bda21aa9e3..a17d05200d 100644 --- a/test-suite/output/bug_13238.out +++ b/test-suite/output/bug_13238.out @@ -1,4 +1,4 @@ -Ltac bug_13238.t1 x := replace (x x) with (x x) -Ltac bug_13238.t2 x := case : x -Ltac bug_13238.t3 := by move -> -Ltac bug_13238.t4 := congr True +Ltac t1 x := replace (x x) with (x x) +Ltac t2 x := case : x +Ltac t3 := by move -> +Ltac t4 := congr True diff --git a/test-suite/output/prim_array.out b/test-suite/output/prim_array.out new file mode 100644 index 0000000000..6c12153ab9 --- /dev/null +++ b/test-suite/output/prim_array.out @@ -0,0 +1,9 @@ +[| | 0 : nat |] + : array nat +[| 1; 2; 3 | 0 : nat |] + : array nat +[| | 0 : nat |]@{Set} + : array@{Set} nat +[| bool; list nat | nat : Set |]@{prim_array.4} + : array@{prim_array.4} Set +(* {prim_array.4} |= Set < prim_array.4 *) diff --git a/test-suite/output/prim_array.v b/test-suite/output/prim_array.v new file mode 100644 index 0000000000..a82f6a16f1 --- /dev/null +++ b/test-suite/output/prim_array.v @@ -0,0 +1,10 @@ +Primitive array := #array_type. + +Check [| | 0 |]. + +Check [| 1; 2; 3 | 0 |]. + +Set Printing Universes. +Check [| | 0 |]. + +Check [| bool; list nat | nat |]. diff --git a/test-suite/success/definition_using.v b/test-suite/success/definition_using.v new file mode 100644 index 0000000000..120e62b145 --- /dev/null +++ b/test-suite/success/definition_using.v @@ -0,0 +1,68 @@ +Require Import Program. +Axiom bogus : Type. + +Section A. +Variable x : bogus. + +#[using="All"] +Definition c1 : bool := true. + +#[using="All"] +Fixpoint c2 n : bool := + match n with + | O => true + | S p => c3 p + end +with c3 n : bool := + match n with + | O => true + | S p => c2 p +end. + +#[using="All"] +Definition c4 : bool. Proof. exact true. Qed. + +#[using="All"] +Fixpoint c5 (n : nat) {struct n} : bool. Proof. destruct n as [|p]. exact true. exact (c5 p). Qed. + +#[using="All", program] +Definition c6 : bool. Proof. exact true. Qed. + +#[using="All", program] +Fixpoint c7 (n : nat) {struct n} : bool := + match n with + | O => true + | S p => c7 p + end. + +End A. + +Check c1 : bogus -> bool. +Check c2 : bogus -> nat -> bool. +Check c3 : bogus -> nat -> bool. +Check c4 : bogus -> bool. +Check c5 : bogus -> nat -> bool. +Check c6 : bogus -> bool. +Check c7 : bogus -> nat -> bool. + +Section B. + +Variable a : bogus. +Variable h : c1 a = true. + +#[using="a*"] +Definition c8 : bogus := a. + +Collection ccc := a h. + +#[using="ccc"] +Definition c9 : bogus := a. + +#[using="ccc - h"] +Definition c10 : bogus := a. + +End B. + +Check c8 : forall a, c1 a = true -> bogus. +Check c9 : forall a, c1 a = true -> bogus. +Check c10: bogus -> bogus. diff --git a/vernac/attributes.ml b/vernac/attributes.ml index fb308fd316..efba6d332a 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -224,3 +224,11 @@ let canonical_field = enable_attribute ~key:"canonical" ~default:(fun () -> true) let canonical_instance = enable_attribute ~key:"canonical" ~default:(fun () -> false) + +let uses_parser : string key_parser = fun orig args -> + assert_once ~name:"using" orig; + match args with + | VernacFlagLeaf str -> str + | _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute") + +let using = attribute_of_list ["using",uses_parser] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 51bab79938..1969665082 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -51,6 +51,7 @@ val option_locality : Goptions.option_locality attribute val deprecation : Deprecation.t option attribute val canonical_field : bool attribute val canonical_instance : bool attribute +val using : string option attribute val program_mode_option_name : string list (** For internal use when messing with the global option. *) diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml index c1dbf0a1ea..3fc74cba5b 100644 --- a/vernac/comDefinition.ml +++ b/vernac/comDefinition.ml @@ -110,7 +110,7 @@ let interp_definition ~program_mode env evd impl_env bl red_option c ctypopt = let tyopt = Option.map (fun ty -> EConstr.it_mkProd_or_LetIn ty ctx) tyopt in evd, (c, tyopt), imps -let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = +let do_definition ?hook ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt = let program_mode = false in let env = Global.env() in (* Explicitly bound universes and constraints *) @@ -118,14 +118,19 @@ let do_definition ?hook ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = let evd, (body, types), impargs = interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in + let using = using |> Option.map (fun expr -> + let terms = body :: match types with Some x -> [x] | None -> [] in + let l = Proof_using.process_expr (Global.env()) evd expr terms in + Names.Id.Set.(List.fold_right add l empty)) + in let kind = Decls.IsDefinition kind in - let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types () in + let cinfo = Declare.CInfo.make ~name ~impargs ~typ:types ?using () in let info = Declare.Info.make ~scope ~kind ?hook ~udecl ~poly () in let _ : Names.GlobRef.t = Declare.declare_definition ~info ~cinfo ~opaque:false ~body evd in () -let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option c ctypopt = +let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind ?using udecl bl red_option c ctypopt = let program_mode = true in let env = Global.env() in (* Explicitly bound universes and constraints *) @@ -133,9 +138,14 @@ let do_definition_program ?hook ~pm ~name ~scope ~poly ~kind udecl bl red_option let evd, (body, types), impargs = interp_definition ~program_mode env evd empty_internalization_env bl red_option c ctypopt in + let using = using |> Option.map (fun expr -> + let terms = body :: match types with Some x -> [x] | None -> [] in + let l = Proof_using.process_expr (Global.env()) evd expr terms in + Names.Id.Set.(List.fold_right add l empty)) + in let term, typ, uctx, obls = Declare.Obls.prepare_obligation ~name ~body ~types evd in let pm, _ = - let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in + let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in let info = Declare.Info.make ~udecl ~scope ~poly ~kind ?hook () in Declare.Obls.add_definition ~pm ~cinfo ~info ~term ~uctx obls in pm diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 7420235449..5e1b705ae4 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -31,6 +31,7 @@ val do_definition -> scope:Locality.locality -> poly:bool -> kind:Decls.definition_object_kind + -> ?using:Vernacexpr.section_subset_expr -> universe_decl_expr option -> local_binder_expr list -> red_expr option @@ -45,6 +46,7 @@ val do_definition_program -> scope:Locality.locality -> poly:bool -> kind:Decls.logical_kind + -> ?using:Vernacexpr.section_subset_expr -> universe_decl_expr option -> local_binder_expr list -> red_expr option diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 78572c6aa6..29bf5fbcc2 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -251,15 +251,22 @@ let interp_fixpoint ?(check_recursivity=true) ~cofix l : let uctx,fix = ground_fixpoint env evd fix in (fix,pl,uctx,info) -let build_recthms ~indexes fixnames fixtypes fiximps = +let build_recthms ~indexes ?using fixnames fixtypes fiximps = let fix_kind, cofix = match indexes with | Some indexes -> Decls.Fixpoint, false | None -> Decls.CoFixpoint, true in let thms = List.map3 (fun name typ (ctx,impargs,_) -> + let using = using |> Option.map (fun expr -> + let terms = [EConstr.of_constr typ] in + let env = Global.env() in + let sigma = Evd.from_env env in + let l = Proof_using.process_expr env sigma expr terms in + Names.Id.Set.(List.fold_right add l empty)) + in let args = List.map Context.Rel.Declaration.get_name ctx in - Declare.CInfo.make ~name ~typ ~args ~impargs () + Declare.CInfo.make ~name ~typ ~args ~impargs ?using () ) fixnames fixtypes fiximps in fix_kind, cofix, thms @@ -277,9 +284,9 @@ let declare_fixpoint_interactive_generic ?indexes ~scope ~poly ((fixnames,_fixrs List.iter (Metasyntax.add_notation_interpretation (Global.env())) ntns; lemma -let declare_fixpoint_generic ?indexes ~scope ~poly ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = +let declare_fixpoint_generic ?indexes ~scope ~poly ?using ((fixnames,fixrs,fixdefs,fixtypes),udecl,uctx,fiximps) ntns = (* We shortcut the proof process *) - let fix_kind, cofix, fixitems = build_recthms ~indexes fixnames fixtypes fiximps in + let fix_kind, cofix, fixitems = build_recthms ~indexes ?using fixnames fixtypes fiximps in let fixdefs = List.map Option.get fixdefs in let rec_declaration = prepare_recursive_declaration fixnames fixrs fixtypes fixdefs in let fix_kind = Decls.IsDefinition fix_kind in @@ -328,9 +335,9 @@ let do_fixpoint_interactive ~scope ~poly l : Declare.Proof.t = let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in lemma -let do_fixpoint ~scope ~poly l = +let do_fixpoint ~scope ~poly ?using l = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns + declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly ?using fix ntns let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in @@ -342,6 +349,6 @@ let do_cofixpoint_interactive ~scope ~poly l = let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in lemma -let do_cofixpoint ~scope ~poly l = +let do_cofixpoint ~scope ~poly ?using l = let cofix, ntns = do_cofixpoint_common l in - declare_fixpoint_generic ~scope ~poly cofix ntns + declare_fixpoint_generic ~scope ~poly ?using cofix ntns diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index aa5446205c..a36aba7672 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -19,13 +19,13 @@ val do_fixpoint_interactive : scope:Locality.locality -> poly:bool -> fixpoint_expr list -> Declare.Proof.t val do_fixpoint : - scope:Locality.locality -> poly:bool -> fixpoint_expr list -> unit + scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> unit val do_cofixpoint_interactive : scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> Declare.Proof.t val do_cofixpoint : - scope:Locality.locality -> poly:bool -> cofixpoint_expr list -> unit + scope:Locality.locality -> poly:bool -> ?using:Vernacexpr.section_subset_expr -> cofixpoint_expr list -> unit (************************************************************************) (** Internal API *) diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 55901fd604..9623317ddf 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -109,7 +109,7 @@ let telescope env sigma l = let nf_evar_context sigma ctx = List.map (map_constr (fun c -> Evarutil.nf_evar sigma c)) ctx -let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation = +let build_wellfounded pm (recname,pl,bl,arityc,body) poly ?using r measure notation = let open EConstr in let open Vars in let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in @@ -259,8 +259,13 @@ let build_wellfounded pm (recname,pl,bl,arityc,body) poly r measure notation = let evars, _, evars_def, evars_typ = RetrieveObl.retrieve_obligations env recname sigma 0 def typ in + let using = using |> Option.map (fun expr -> + let terms = List.map EConstr.of_constr [evars_def; evars_typ] in + let l = Proof_using.process_expr env sigma expr terms in + Names.Id.Set.(List.fold_right add l empty)) + in let uctx = Evd.evar_universe_context sigma in - let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ () in + let cinfo = Declare.CInfo.make ~name:recname ~typ:evars_typ ?using () in let info = Declare.Info.make ~udecl ~poly ~hook () in let pm, _ = Declare.Obls.add_definition ~pm ~cinfo ~info ~term:evars_def ~uctx evars in @@ -275,7 +280,7 @@ let collect_evars_of_term evd c ty = Evar.Set.fold (fun ev acc -> Evd.add acc ev (Evd.find_undefined evd ev)) evars (Evd.from_ctx (Evd.evar_universe_context evd)) -let do_program_recursive ~pm ~scope ~poly fixkind fixl = +let do_program_recursive ~pm ~scope ~poly ?using fixkind fixl = let cofix = fixkind = Declare.Obls.IsCoFixpoint in let (env, rec_sign, udecl, evd), fix, info = interp_recursive ~cofix ~program_mode:true fixl @@ -287,13 +292,18 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl = let evd = nf_evar_map_undefined evd in let collect_evars name def typ impargs = (* Generalize by the recursive prototypes *) + let using = using |> Option.map (fun expr -> + let terms = [def; typ] in + let l = Proof_using.process_expr env evd expr terms in + Names.Id.Set.(List.fold_right add l empty)) + 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 = RetrieveObl.retrieve_obligations env name evm (List.length rec_sign) def typ in - let cinfo = Declare.CInfo.make ~name ~typ ~impargs () in + let cinfo = Declare.CInfo.make ~name ~typ ~impargs ?using () in (cinfo, def, evars) in let (fixnames,fixrs,fixdefs,fixtypes) = fix in @@ -325,13 +335,13 @@ let do_program_recursive ~pm ~scope ~poly fixkind fixl = let info = Declare.Info.make ~poly ~scope ~kind ~udecl () in Declare.Obls.add_mutual_definitions ~pm defs ~info ~uctx ~ntns fixkind -let do_fixpoint ~pm ~scope ~poly l = +let do_fixpoint ~pm ~scope ~poly ?using l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], [ Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations} ] -> let recarg = mkIdentC n.CAst.v in - build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly r recarg notations + build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using r recarg notations | [Some { CAst.v = CMeasureRec (n, m, r) }], [Vernacexpr.{fname={CAst.v=id}; univs; binders; rtype; body_def; notations }] -> @@ -344,7 +354,7 @@ let do_fixpoint ~pm ~scope ~poly l = user_err Pp.(str"Measure takes only two arguments in Program Fixpoint.") | _, _ -> r in - build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly + build_wellfounded pm (id, univs, binders, rtype, out_def body_def) poly ?using (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m notations | _, _ when List.for_all (fun ro -> match ro with None | Some { CAst.v = CStructRec _} -> true | _ -> false) g -> @@ -352,11 +362,11 @@ let do_fixpoint ~pm ~scope ~poly l = Vernacexpr.(ComFixpoint.adjust_rec_order ~structonly:true fix.binders fix.rec_order)) l in let fixkind = Declare.Obls.IsFixpoint annots in let l = List.map2 (fun fix rec_order -> { fix with Vernacexpr.rec_order }) l annots in - do_program_recursive ~pm ~scope ~poly fixkind l + do_program_recursive ~pm ~scope ~poly ?using fixkind l | _, _ -> CErrors.user_err ~hdr:"do_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let do_cofixpoint ~pm ~scope ~poly fixl = +let do_cofixpoint ~pm ~scope ~poly ?using fixl = let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in - do_program_recursive ~pm ~scope ~poly Declare.Obls.IsCoFixpoint fixl + do_program_recursive ~pm ~scope ~poly ?using Declare.Obls.IsCoFixpoint fixl diff --git a/vernac/comProgramFixpoint.mli b/vernac/comProgramFixpoint.mli index 7935cf27fb..30bf3ae8f8 100644 --- a/vernac/comProgramFixpoint.mli +++ b/vernac/comProgramFixpoint.mli @@ -15,6 +15,7 @@ val do_fixpoint : pm:Declare.OblState.t -> scope:Locality.locality -> poly:bool + -> ?using:Vernacexpr.section_subset_expr -> fixpoint_expr list -> Declare.OblState.t @@ -22,5 +23,6 @@ val do_cofixpoint : pm:Declare.OblState.t -> scope:Locality.locality -> poly:bool + -> ?using:Vernacexpr.section_subset_expr -> cofixpoint_expr list -> Declare.OblState.t diff --git a/vernac/declare.ml b/vernac/declare.ml index 3a8ceb0e0f..0baae6eca5 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -55,11 +55,13 @@ module CInfo = struct (** Names to pre-introduce *) ; impargs : Impargs.manual_implicits (** Explicitily declared implicit arguments *) + ; using : Names.Id.Set.t option + (** Explicit declaration of section variables used by the constant *) } - let make ~name ~typ ?(args=[]) ?(impargs=[]) () = - { name; typ; args; impargs } + let make ~name ~typ ?(args=[]) ?(impargs=[]) ?using () = + { name; typ; args; impargs; using } let to_constr sigma thm = { thm with typ = EConstr.to_constr sigma thm.typ } @@ -108,10 +110,10 @@ let default_univ_entry = Entries.Monomorphic_entry Univ.ContextSet.empty (** [univsbody] are universe-constraints attached to the body-only, used in vio-delayed opaque constants and private poly universes *) -let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_vars ?types +let definition_entry_core ?(opaque=false) ?using ?(inline=false) ?feedback_id ?types ?(univs=default_univ_entry) ?(eff=Evd.empty_side_effects) ?(univsbody=Univ.ContextSet.empty) body = { proof_entry_body = Future.from_val ((body,univsbody), eff); - proof_entry_secctx = section_vars; + proof_entry_secctx = using; proof_entry_type = types; proof_entry_universes = univs; proof_entry_opaque = opaque; @@ -119,7 +121,7 @@ let definition_entry_core ?(opaque=false) ?(inline=false) ?feedback_id ?section_ proof_entry_inline_code = inline} let definition_entry = - definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None ?section_vars:None + definition_entry_core ?eff:None ?univsbody:None ?feedback_id:None type 'a constant_entry = | DefinitionEntry of 'a proof_entry @@ -236,9 +238,9 @@ let pure_definition_entry ?(opaque=false) ?(inline=false) ?types proof_entry_feedback = None; proof_entry_inline_code = inline} -let delayed_definition_entry ~opaque ?feedback_id ~section_vars ~univs ?types body = +let delayed_definition_entry ~opaque ?feedback_id ~using ~univs ?types body = { proof_entry_body = body - ; proof_entry_secctx = section_vars + ; proof_entry_secctx = using ; proof_entry_type = types ; proof_entry_universes = univs ; proof_entry_opaque = opaque @@ -608,8 +610,8 @@ let declare_mutually_recursive_core ~info ~cinfo ~opaque ~ntns ~uctx ~rec_declar uctx, univs in let csts = CList.map2 - (fun CInfo.{ name; typ; impargs } body -> - let entry = definition_entry ~opaque ~types:typ ~univs body in + (fun CInfo.{ name; typ; impargs; using } body -> + let entry = definition_entry ~opaque ~types:typ ~univs ?using body in declare_entry ~name ~scope ~kind ~impargs ~uctx entry) cinfo fixdecls in @@ -660,7 +662,7 @@ let check_evars_are_solved env sigma t = let evars = Evarutil.undefined_evars_of_term sigma t in if not (Evar.Set.is_empty evars) then error_unresolved_evars env sigma t evars -let prepare_definition ~info ~opaque ~body ~typ sigma = +let prepare_definition ~info ~opaque ?using ~body ~typ sigma = let { Info.poly; udecl; inline; _ } = info in let env = Global.env () in let sigma, (body, types) = Evarutil.finalize ~abort_on_undefined_evars:false @@ -669,13 +671,13 @@ let prepare_definition ~info ~opaque ~body ~typ sigma = Option.iter (check_evars_are_solved env sigma) types; check_evars_are_solved env sigma body; let univs = Evd.check_univ_decl ~poly sigma udecl in - let entry = definition_entry ~opaque ~inline ?types ~univs body in + let entry = definition_entry ~opaque ?using ~inline ?types ~univs body in let uctx = Evd.evar_universe_context sigma in entry, uctx let declare_definition_core ~info ~cinfo ~opaque ~obls ~body sigma = - let { CInfo.name; impargs; typ; _ } = cinfo in - let entry, uctx = prepare_definition ~info ~opaque ~body ~typ sigma in + let { CInfo.name; impargs; typ; using; _ } = cinfo in + let entry, uctx = prepare_definition ~info ~opaque ?using ~body ~typ sigma in let { Info.scope; kind; hook; _ } = info in declare_entry_core ~name ~scope ~kind ~impargs ~obls ?hook ~uctx entry, uctx @@ -803,6 +805,7 @@ module ProgramDecl = struct let set_uctx ~uctx prg = {prg with prg_uctx = uctx} let get_poly prg = prg.prg_info.Info.poly let get_obligations prg = prg.prg_obligations + let get_using prg = prg.prg_cinfo.CInfo.using end end @@ -1137,7 +1140,7 @@ let declare_mutual_definition ~pm l = in let term = EConstr.to_constr sigma term in let typ = EConstr.to_constr sigma typ in - let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs) in + let def = (x.prg_reduce term, r, x.prg_reduce typ, x.prg_cinfo.CInfo.impargs, x.prg_cinfo.CInfo.using) in let oblsubst = List.map (fun (id, (_, c)) -> (id, c)) oblsubst in (def, oblsubst) in @@ -1151,11 +1154,11 @@ let declare_mutual_definition ~pm l = (* let fixdefs = List.map reduce_fix fixdefs in *) let fixdefs, fixrs, fixtypes, fixitems = List.fold_right2 - (fun (d, r, typ, impargs) name (a1, a2, a3, a4) -> + (fun (d, r, typ, impargs, using) name (a1, a2, a3, a4) -> ( d :: a1 , r :: a2 , typ :: a3 - , CInfo.{name; typ; impargs; args = []} :: a4 )) + , CInfo.{name; typ; impargs; args = []; using } :: a4 )) defs first.prg_deps ([], [], [], []) in let fixkind = Option.get first.prg_fixkind in @@ -1376,7 +1379,7 @@ end type t = { endline_tactic : Genarg.glob_generic_argument option - ; section_vars : Id.Set.t option + ; using : Id.Set.t option ; proof : Proof.t ; initial_euctx : UState.t (** The initial universe context (for the statement) *) @@ -1435,7 +1438,7 @@ let start_proof_core ~name ~typ ~pinfo ?(sign=initialize_named_context_for_proof let initial_euctx = Evd.evar_universe_context Proof.((data proof).sigma) in { proof ; endline_tactic = None - ; section_vars = None + ; using = None ; initial_euctx ; pinfo } @@ -1458,7 +1461,7 @@ let start_dependent ~info ~name ~proof_ending goals = let pinfo = Proof_info.make ~info ~cinfo ~proof_ending () in { proof ; endline_tactic = None - ; section_vars = None + ; using = None ; initial_euctx ; pinfo } @@ -1523,7 +1526,7 @@ let start_mutual_with_initialization ~info ~cinfo ~mutual_info sigma snl = map lemma ~f:(fun p -> pi1 @@ Proof.run_tactic Global.(env ()) init_tac p) -let get_used_variables pf = pf.section_vars +let get_used_variables pf = pf.using let get_universe_decl pf = pf.pinfo.Proof_info.info.Info.udecl let set_used_variables ps l = @@ -1547,9 +1550,9 @@ let set_used_variables ps l = else (ctx, all_safe) in let ctx, _ = Environ.fold_named_context aux env ~init:(ctx,ctx_set) in - if not (Option.is_empty ps.section_vars) then + if not (Option.is_empty ps.using) then CErrors.user_err Pp.(str "Used section variables can be declared only once"); - ctx, { ps with section_vars = Some (Context.Named.to_vars ctx) } + ctx, { ps with using = Some (Context.Named.to_vars ctx) } let get_open_goals ps = let Proof.{ goals; stack; sigma } = Proof.data ps.proof in @@ -1646,7 +1649,7 @@ let make_univs ~poly ~uctx ~udecl (used_univs_typ, typ) (used_univs_body, body) let close_proof ~opaque ~keep_body_ucst_separate ps = - let { section_vars; proof; initial_euctx; pinfo } = ps in + let { using; proof; initial_euctx; pinfo } = ps in let { Proof_info.info = { Info.udecl } } = pinfo in let { Proof.name; poly } = Proof.data proof in let unsafe_typ = keep_body_ucst_separate && not poly in @@ -1667,7 +1670,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = then make_univs_private_poly ~poly ~uctx ~udecl t b else make_univs ~poly ~uctx ~udecl t b in - definition_entry_core ~opaque ?section_vars ~univs:utyp ~univsbody:ubody ~types:typ ~eff body + definition_entry_core ~opaque ?using ~univs:utyp ~univsbody:ubody ~types:typ ~eff body in let entries = CList.map make_entry elist in { name; entries; uctx } @@ -1675,7 +1678,7 @@ let close_proof ~opaque ~keep_body_ucst_separate ps = type closed_proof_output = (Constr.t * Evd.side_effects) list * UState.t let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.computation) = - let { section_vars; proof; initial_euctx; pinfo } = ps in + let { using; proof; initial_euctx; pinfo } = ps in let { Proof_info.info = { Info.udecl } } = pinfo in let { Proof.name; poly; entry; sigma } = Proof.data proof in @@ -1712,7 +1715,7 @@ let close_proof_delayed ~feedback_id ps (fpl : closed_proof_output Future.comput let univs = UState.restrict uctx used_univs in let univs = UState.check_mono_univ_decl univs udecl in (pt,univs),eff) - |> delayed_definition_entry ~opaque ~feedback_id ~section_vars ~univs ~types + |> delayed_definition_entry ~opaque ~feedback_id ~using ~univs ~types in let entries = Future.map2 make_entry fpl (Proofview.initial_goals entry) in { name; entries; uctx = initial_euctx } @@ -2289,7 +2292,8 @@ let rec solve_obligation prg num tac = let name = Internal.get_name prg in Proof_ending.End_obligation {name; num; auto} in - let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) () in + let using = Internal.get_using prg in + let cinfo = CInfo.make ~name:obl.obl_name ~typ:(EConstr.of_constr obl.obl_type) ?using () in let poly = Internal.get_poly prg in let info = Info.make ~scope ~kind ~poly () in let lemma = Proof.start_core ~cinfo ~info ~proof_ending evd in diff --git a/vernac/declare.mli b/vernac/declare.mli index 1ad79928d5..0520bf8717 100644 --- a/vernac/declare.mli +++ b/vernac/declare.mli @@ -79,6 +79,7 @@ module CInfo : sig -> typ:'constr -> ?args:Name.t list -> ?impargs:Impargs.manual_implicits + -> ?using:Names.Id.Set.t -> unit -> 'constr t @@ -244,6 +245,12 @@ module Proof : sig * (w.r.t. type dependencies and let-ins covered by it) *) val set_used_variables : t -> Names.Id.t list -> Constr.named_context * t + (** Gets the set of variables declared to be used by the proof. None means + no "Proof using" or #[using] was given *) + val get_used_variables : t -> Id.Set.t option + + (** Compacts the representation of the proof by pruning all intermediate + terms *) val compact : t -> t (** Update the proof's universe information typically after a @@ -333,6 +340,7 @@ type 'a proof_entry val definition_entry : ?opaque:bool + -> ?using:Names.Id.Set.t -> ?inline:bool -> ?types:Constr.types -> ?univs:Entries.universes_entry diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 3d6a93c888..f192d67624 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -113,7 +113,8 @@ GRAMMAR EXTEND Gram ] ; attribute: - [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v } ] + [ [ k = ident ; v = attr_value -> { Names.Id.to_string k, v } + | "using" ; v = attr_value -> { "using", v } ] ] ; attr_value: diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 185abcf35b..8477870cb4 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -1042,6 +1042,13 @@ let interp_non_syntax_modifiers mods = in List.fold_left (fun st modif -> Option.bind st @@ set modif) (Some (false,false,InConstrEntry)) mods +(* Check if an interpretation can be used for printing a cases printing *) +let has_no_binders_type = + List.for_all (fun (_,(_,typ)) -> + match typ with + | NtnTypeBinder _ | NtnTypeBinderList -> false + | NtnTypeConstr | NtnTypeConstrList -> true) + (* Compute precedences from modifiers (or find default ones) *) let set_entry_type from n etyps (x,typ) = @@ -1226,6 +1233,9 @@ let find_precedence custom lev etyps symbols onlyprint = | _ -> user_err Pp.(str "A notation starting with an atomic expression must be at level 0.") end + | (ETPattern _ | ETBinder _), InConstrEntry when not onlyprint -> + (* Don't know exactly if we can make sense of this case *) + user_err Pp.(str "Binders or patterns not supported in leftmost position.") | (ETPattern _ | ETBinder _ | ETConstr _), _ -> (* Give a default ? *) if Option.is_empty lev then @@ -1416,6 +1426,7 @@ type notation_obj = { notobj_deprecation : Deprecation.t option; notobj_notation : notation * notation_location; notobj_specific_pp_rules : syntax_printing_extension option; + notobj_also_in_cases_pattern : bool; } let load_notation_common silently_define_scope_if_undefined _ (_, nobj) = @@ -1438,9 +1449,10 @@ let open_notation i (_, nobj) = let pat = nobj.notobj_interp in let deprecation = nobj.notobj_deprecation in let scope = match scope with None -> LastLonelyNotation | Some sc -> NotationInScope sc in + let also_in_cases_pattern = nobj.notobj_also_in_cases_pattern in (* Declare the notation *) (match nobj.notobj_use with - | Some use -> Notation.declare_notation (scope,ntn) pat df ~use nobj.notobj_coercion deprecation + | Some use -> Notation.declare_notation (scope,ntn) pat df ~use ~also_in_cases_pattern nobj.notobj_coercion deprecation | None -> ()); (* Declare specific format if any *) (match nobj.notobj_specific_pp_rules with @@ -1621,19 +1633,21 @@ let add_notation_in_scope ~local deprecation df env c mods scope = let (acvars, ac, reversibility) = interp_notation_constr env nenv c in let interp = make_interpretation_vars sd.recvars (pi2 sd.level) acvars (fst sd.pa_syntax_data) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in + let vars = List.map_filter map i_vars in (* Order of elements is important here! *) + let also_in_cases_pattern = has_no_binders_type vars in let onlyparse,coe = printability (Some sd.level) sd.subentries sd.only_parsing reversibility ac in let notation, location = sd.info in let use = make_use true onlyparse sd.only_printing in let notation = { notobj_local = local; notobj_scope = scope; - notobj_interp = (List.map_filter map i_vars, ac); - (* Order is important here! *) notobj_use = use; + notobj_interp = (vars, ac); notobj_coercion = coe; notobj_deprecation = sd.deprecation; notobj_notation = (notation, location); notobj_specific_pp_rules = sy_pp_rules; + notobj_also_in_cases_pattern = also_in_cases_pattern; } in (* Ready to change the global state *) List.iter (fun f -> f ()) sd.msgs; @@ -1665,18 +1679,20 @@ let add_notation_interpretation_core ~local df env ?(impls=empty_internalization let plevel = match level with Some (from,level,l) -> level | None (* numeral: irrelevant )*) -> 0 in let interp = make_interpretation_vars recvars plevel acvars (List.combine mainvars i_typs) in let map (x, _) = try Some (x, Id.Map.find x interp) with Not_found -> None in + let vars = List.map_filter map i_vars in (* Order of elements is important here! *) + let also_in_cases_pattern = has_no_binders_type vars in let onlyparse,coe = printability level i_typs onlyparse reversibility ac in let use = make_use false onlyparse onlyprint in let notation = { notobj_local = local; notobj_scope = scope; - notobj_interp = (List.map_filter map i_vars, ac); - (* Order is important here! *) notobj_use = use; + notobj_interp = (vars, ac); notobj_coercion = coe; notobj_deprecation = deprecation; notobj_notation = df'; notobj_specific_pp_rules = pp_sy; + notobj_also_in_cases_pattern = also_in_cases_pattern; } in Lib.add_anonymous_leaf (inNotation notation); df' @@ -1850,8 +1866,9 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,InternalProd))) in let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] 0 acvars (List.map in_pat vars) in let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in + let also_in_cases_pattern = has_no_binders_type vars in let onlyparsing = onlyparsing || fst (printability None [] false reversibility pat) in - Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat) + Syntax_def.declare_syntactic_definition ~local ~also_in_cases_pattern deprecation ident ~onlyparsing (vars,pat) (**********************************************************************) (* Declaration of custom entry *) diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 95680c2a4e..bdb0cabacf 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -18,30 +18,30 @@ module NamedDecl = Context.Named.Declaration let known_names = Summary.ref [] ~name:"proofusing-nameset" -let rec close_fwd e s = +let rec close_fwd env sigma s = let s' = List.fold_left (fun s decl -> let vb = match decl with | LocalAssum _ -> Id.Set.empty - | LocalDef (_,b,_) -> global_vars_set e b + | LocalDef (_,b,_) -> Termops.global_vars_set env sigma b in - let vty = global_vars_set e (NamedDecl.get_type decl) in + let vty = Termops.global_vars_set env sigma (NamedDecl.get_type decl) in let vbty = Id.Set.union vb vty in if Id.Set.exists (fun v -> Id.Set.mem v s) vbty then Id.Set.add (NamedDecl.get_id decl) (Id.Set.union s vbty) else s) - s (named_context e) + s (EConstr.named_context env) in - if Id.Set.equal s s' then s else close_fwd e s' + if Id.Set.equal s s' then s else close_fwd env sigma s' -let set_of_type env ty = +let set_of_type env sigma ty = List.fold_left (fun acc ty -> - Id.Set.union (global_vars_set env ty) acc) + Id.Set.union (Termops.global_vars_set env sigma ty) acc) Id.Set.empty ty let full_set env = List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty -let process_expr env e v_ty = +let process_expr env sigma e v_ty = let rec aux = function | SsEmpty -> Id.Set.empty | SsType -> v_ty @@ -49,7 +49,7 @@ let process_expr env e v_ty = | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) | SsCompl e -> Id.Set.diff (full_set env) (aux e) - | SsFwdClose e -> close_fwd env (aux e) + | SsFwdClose e -> close_fwd env sigma (aux e) and set_of_id id = if Id.to_string id = "All" then full_set env @@ -59,9 +59,9 @@ let process_expr env e v_ty = in aux e -let process_expr env e ty = - let v_ty = set_of_type env ty in - let s = Id.Set.union v_ty (process_expr env e v_ty) in +let process_expr env sigma e ty = + let v_ty = set_of_type env sigma ty in + let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in Id.Set.elements s let name_set id expr = known_names := (id,expr) :: !known_names @@ -110,7 +110,7 @@ let suggest_common env ppid used ids_typ skip = S.empty (named_context env) in let all = S.diff all skip in - let fwd_typ = close_fwd env ids_typ in + let fwd_typ = close_fwd env (Evd.from_env env) ids_typ in if !Flags.debug then begin print (str "All " ++ pr_set false all); print (str "Type " ++ pr_set false ids_typ); diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli index dfc233e8fa..93dbd33ae4 100644 --- a/vernac/proof_using.mli +++ b/vernac/proof_using.mli @@ -11,7 +11,8 @@ (** Utility code for section variables handling in Proof using... *) val process_expr : - Environ.env -> Vernacexpr.section_subset_expr -> Constr.types list -> + Environ.env -> Evd.evar_map -> + Vernacexpr.section_subset_expr -> EConstr.types list -> Names.Id.t list val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit @@ -24,3 +25,5 @@ val get_default_proof_using : unit -> Vernacexpr.section_subset_expr option val proof_using_opt_name : string list (** For the stm *) + +val using_from_string : string -> Vernacexpr.section_subset_expr diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3ced38d6ea..bc03994ca6 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -57,14 +57,16 @@ module DefAttributes = struct program : bool; deprecated : Deprecation.t option; canonical_instance : bool; + using : Vernacexpr.section_subset_expr option; } let parse f = let open Attributes in - let (((locality, deprecated), polymorphic), program), canonical_instance = - parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance) f + let ((((locality, deprecated), polymorphic), program), canonical_instance), using = + parse Notations.(locality ++ deprecation ++ polymorphic ++ program ++ canonical_instance ++ using) f in - { polymorphic; program; locality; deprecated; canonical_instance } + let using = Option.map Proof_using.using_from_string using in + { polymorphic; program; locality; deprecated; canonical_instance; using } end let module_locality = Attributes.Notations.(locality >>= fun l -> return (make_module_locality l)) @@ -496,6 +498,25 @@ let program_inference_hook env sigma ev = user_err Pp.(str "The statement obligations could not be resolved \ automatically, write a statement definition first.") +let vernac_set_used_variables ~pstate e : Declare.Proof.t = + let env = Global.env () in + let sigma, _ = Declare.Proof.get_current_context pstate in + let initial_goals pf = Proofview.initial_goals Proof.((data pf).entry) in + let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in + let l = Proof_using.process_expr env sigma e tys in + let vars = Environ.named_context env in + List.iter (fun id -> + if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then + user_err ~hdr:"vernac_set_used_variables" + (str "Unknown variable: " ++ Id.print id)) + l; + let _, pstate = Declare.Proof.set_used_variables pstate l in + pstate +let vernac_set_used_variables_opt ?using pstate = + match using with + | None -> pstate + | Some expr -> vernac_set_used_variables ~pstate expr + (* XXX: Interpretation of lemma command, duplication with ComFixpoint / ComDefinition ? *) let interp_lemma ~program_mode ~flags ~scope env0 evd thms = @@ -525,7 +546,7 @@ let post_check_evd ~udecl ~poly evd = else (* We fix the variables to ensure they won't be lowered to Set *) Evd.fix_undefined_variables evd -let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = +let start_lemma_com ~program_mode ~poly ~scope ~kind ?using ?hook thms = let env0 = Global.env () in let flags = Pretyping.{ all_no_fail_flags with program_mode } in let decl = fst (List.hd thms) in @@ -533,17 +554,20 @@ let start_lemma_com ~program_mode ~poly ~scope ~kind ?hook thms = let evd, thms = interp_lemma ~program_mode ~flags ~scope env0 evd thms in let mut_analysis = RecLemmas.look_for_possibly_mutual_statements evd thms in let evd = Evd.minimize_universes evd in - match mut_analysis with - | RecLemmas.NonMutual thm -> - let thm = Declare.CInfo.to_constr evd thm in - let evd = post_check_evd ~udecl ~poly evd in - let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in - Declare.Proof.start_with_initialization ~info ~cinfo:thm evd - | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } -> - let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in - let evd = post_check_evd ~udecl ~poly evd in - let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in - Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards) + let pstate = + match mut_analysis with + | RecLemmas.NonMutual thm -> + let thm = Declare.CInfo.to_constr evd thm in + let evd = post_check_evd ~udecl ~poly evd in + let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in + Declare.Proof.start_with_initialization ~info ~cinfo:thm evd + | RecLemmas.Mutual { mutual_info; cinfo ; possible_guards } -> + let cinfo = List.map (Declare.CInfo.to_constr evd) cinfo in + let evd = post_check_evd ~udecl ~poly evd in + let info = Declare.Info.make ?hook ~poly ~scope ~kind ~udecl () in + Declare.Proof.start_mutual_with_initialization ~info ~cinfo evd ~mutual_info (Some possible_guards) + in + vernac_set_used_variables_opt ?using pstate let vernac_definition_hook ~canonical_instance ~local ~poly = let open Decls in function | Coercion -> @@ -583,7 +607,7 @@ let vernac_definition_interactive ~atts (discharge, kind) (lid, pl) bl t = let program_mode = atts.program in let poly = atts.polymorphic in let name = vernac_definition_name lid local in - start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?hook [(name, pl), (bl, t)] + start_lemma_com ~program_mode ~poly ~scope:local ~kind:(Decls.IsDefinition kind) ?using:atts.using ?hook [(name, pl), (bl, t)] let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_opt = let open DefAttributes in @@ -604,7 +628,7 @@ let vernac_definition ~atts ~pm (discharge, kind) (lid, pl) bl red_option c typ_ else let () = ComDefinition.do_definition ~name:name.v - ~poly:atts.polymorphic ~scope ~kind pl bl red_option c typ_opt ?hook in + ~poly:atts.polymorphic ~scope ~kind ?using:atts.using pl bl red_option c typ_opt ?hook in pm (* NB: pstate argument to use combinators easily *) @@ -613,7 +637,7 @@ let vernac_start_proof ~atts kind l = let scope = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun ((id, _), _) -> Dumpglob.dump_definition id false "prf") l; - start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) l + start_lemma_com ~program_mode:atts.program ~poly:atts.polymorphic ~scope ~kind:(Decls.IsProof kind) ?using:atts.using l let vernac_end_proof ~lemma ~pm = let open Vernacexpr in function | Admitted -> @@ -639,6 +663,8 @@ let vernac_assumption ~atts discharge kind l nl = match scope with | Global _ -> Dumpglob.dump_definition lid false "ax" | Discharge -> Dumpglob.dump_definition lid true "var") idl) l; + if Option.has_some atts.using then + Attributes.unsupported_attributes ["using",VernacFlagEmpty]; ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l let is_polymorphic_inductive_cumulativity = @@ -842,16 +868,17 @@ let vernac_fixpoint_interactive ~atts discharge l = let scope = vernac_fixpoint_common ~atts discharge l in if atts.program then CErrors.user_err Pp.(str"Program Fixpoint requires a body"); - ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l + vernac_set_used_variables_opt ?using:atts.using + (ComFixpoint.do_fixpoint_interactive ~scope ~poly:atts.polymorphic l) let vernac_fixpoint ~atts ~pm discharge l = let open DefAttributes in let scope = vernac_fixpoint_common ~atts discharge l in if atts.program then (* XXX: Switch to the attribute system and match on ~atts *) - ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic l + ComProgramFixpoint.do_fixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l else - let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic l in + let () = ComFixpoint.do_fixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in pm let vernac_cofixpoint_common ~atts discharge l = @@ -864,15 +891,16 @@ let vernac_cofixpoint_interactive ~atts discharge l = let scope = vernac_cofixpoint_common ~atts discharge l in if atts.program then CErrors.user_err Pp.(str"Program CoFixpoint requires a body"); - ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l + vernac_set_used_variables_opt ?using:atts.using + (ComFixpoint.do_cofixpoint_interactive ~scope ~poly:atts.polymorphic l) let vernac_cofixpoint ~atts ~pm discharge l = let open DefAttributes in let scope = vernac_cofixpoint_common ~atts discharge l in if atts.program then - ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic l + ComProgramFixpoint.do_cofixpoint ~pm ~scope ~poly:atts.polymorphic ?using:atts.using l else - let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic l in + let () = ComFixpoint.do_cofixpoint ~scope ~poly:atts.polymorphic ?using:atts.using l in pm let vernac_scheme l = @@ -1223,21 +1251,6 @@ let vernac_set_end_tac ~pstate tac = (* TO DO verifier s'il faut pas mettre exist s | TacId s ici*) Declare.Proof.set_endline_tactic tac pstate -let vernac_set_used_variables ~pstate e : Declare.Proof.t = - let env = Global.env () in - let initial_goals pf = Proofview.initial_goals Proof.(data pf).Proof.entry in - let tys = List.map snd (initial_goals (Declare.Proof.get pstate)) in - let tys = List.map EConstr.Unsafe.to_constr tys in - let l = Proof_using.process_expr env e tys in - let vars = Environ.named_context env in - List.iter (fun id -> - if not (List.exists (NamedDecl.get_id %> Id.equal id) vars) then - user_err ~hdr:"vernac_set_used_variables" - (str "Unknown variable: " ++ Id.print id)) - l; - let _, pstate = Declare.Proof.set_used_variables pstate l in - pstate - (*****************************) (* Auxiliary file management *) |
