aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/09-coqide/13145-master+coqide-printing-goal-names-support.rst4
-rw-r--r--engine/eConstr.ml3
-rw-r--r--ide/coqide/coq.ml4
-rw-r--r--ide/coqide/coqide_ui.ml1
-rw-r--r--ide/coqide/idetop.ml4
-rw-r--r--ide/coqide/wg_ProofView.ml28
-rw-r--r--kernel/vars.ml3
-rw-r--r--plugins/ltac/g_ltac.mlg2
-rw-r--r--plugins/ltac/tacentries.ml51
-rw-r--r--plugins/ltac/tacentries.mli3
-rw-r--r--plugins/ltac/tacintern.ml32
-rw-r--r--plugins/ltac/tacintern.mli3
-rw-r--r--printing/printer.ml2
-rw-r--r--printing/printer.mli3
-rw-r--r--test-suite/output/bug_13004.out4
-rw-r--r--test-suite/output/bug_13238.out8
16 files changed, 90 insertions, 65 deletions
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/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/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/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/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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 10:45:23 +0000