diff options
26 files changed, 149 insertions, 79 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/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/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/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/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/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/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/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 |
