aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_coqast.ml42
-rw-r--r--intf/tacexpr.mli1
-rw-r--r--parsing/g_ltac.ml41
-rw-r--r--printing/pptactic.ml3
-rw-r--r--proofs/refiner.ml38
-rw-r--r--proofs/refiner.mli1
-rw-r--r--tactics/tacinterp.ml4
-rw-r--r--tactics/tacticals.ml1
-rw-r--r--tactics/tacticals.mli1
9 files changed, 51 insertions, 1 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 3fd4600587..aae1d9de2a 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -449,6 +449,8 @@ and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function
<:expr< Tacexpr.TacRepeat $mlexpr_of_tactic t$ >>
| Tacexpr.TacProgress t ->
<:expr< Tacexpr.TacProgress $mlexpr_of_tactic t$ >>
+ | Tacexpr.TacShowHyps t ->
+ <:expr< Tacexpr.TacShowHyps $mlexpr_of_tactic t$ >>
| Tacexpr.TacId l ->
<:expr< Tacexpr.TacId $mlexpr_of_list mlexpr_of_message_token l$ >>
| Tacexpr.TacFail (n,l) ->
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index b07b86fbf9..3612635d6e 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -183,6 +183,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr =
| TacTimeout of int or_var * ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
| TacRepeat of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
| TacProgress of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
+ | TacShowHyps of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr
| TacAbstract of ('constr,'pat,'cst,'ind,'ref,'id,'tac,'lev) gen_tactic_expr * identifier option
| TacId of 'id message_token list
| TacFail of int or_var * 'id message_token list
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 51839ee880..bc2803ae5e 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -61,6 +61,7 @@ GEXTEND Gram
| IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta)
| IDENT "repeat"; ta = tactic_expr -> TacRepeat ta
| IDENT "progress"; ta = tactic_expr -> TacProgress ta
+ | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta
(*To do: put Abstract in Refiner*)
| IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None)
| IDENT "abstract"; tc = NEXT; "using"; s = ident ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index c317d4f3f9..8bdea1356b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -906,6 +906,9 @@ let rec pr_tac inherited tac =
| TacProgress t ->
hov 1 (str "progress" ++ spc () ++ pr_tac (ltactical,E) t),
ltactical
+ | TacShowHyps t ->
+ hov 1 (str "infoH" ++ spc () ++ spc () ++ pr_tac (ltactical,E) t),
+ ltactical
| TacInfo t ->
hov 1 (str "info" ++ spc () ++ pr_tac (ltactical,E) t),
linfo
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 0652f19864..a41bfdd49f 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -230,6 +230,44 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
(str"Tactic generated a subgoal identical to the original goal.")
else rslt
+let rec subtrac l1 l2 =
+ match l1,l2 with
+ | [],l -> l
+ | _,[] -> []
+ | _,(e2::l2') ->
+ if List.mem e2 l1 then subtrac l1 l2'
+ else e2:: subtrac l1 l2'
+
+
+(* Execute tac and show the names of hypothesis create by tac in
+ the "as" format. The resulting goals are printed *after* the
+ as-expression, which forces pg to some gymnastic. TODO: Have
+ something similar (better?) in the xml protocol. *)
+let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
+ :Proof_type.goal list Evd.sigma =
+ let oldhyps:Sign.named_context = pf_hyps goal in
+ let rslt:Proof_type.goal list Evd.sigma = tac goal in
+ let {it=gls;sigma=sigma} = rslt in
+ let hyps:Sign.named_context list = List.map (fun gl -> pf_hyps { it = gl; sigma=sigma}) gls in
+ let newhyps =
+ List.map (fun hypl -> subtrac oldhyps hypl)
+ hyps in
+ let emacs_str s =
+ if !Flags.print_emacs then s else "" in
+ let s =
+ let frst = ref true in
+ List.fold_left
+ (fun acc lh -> acc ^ (if !frst then (frst:=false;"") else " | ")
+ ^ (List.fold_left
+ (fun acc (nm,_,_) -> (Names.string_of_id nm) ^ " " ^ acc)
+ "" lh))
+ "" newhyps in
+ pp (str (emacs_str "<infoH>")
+ ++ (hov 0 (str s))
+ ++ (str (emacs_str "</infoH>")) ++ fnl());
+ rslt;;
+
+
let catch_failerror e =
if catchable_exception e then check_for_interrupt ()
else match e with
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 4e30c9c0b2..b5fc9ee66f 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -136,6 +136,7 @@ val tclDO : int -> tactic -> tactic
val tclTIMEOUT : int -> tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS : tactic -> tactic
+val tclSHOWHYPS : tactic -> tactic
val tclNOTSAMEGOAL : tactic -> tactic
(** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then,
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 057a268f56..9bbb095893 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -839,7 +839,7 @@ and intern_tactic_seq onlytac ist = function
| TacId l -> ist.ltacvars, TacId (intern_message ist l)
| TacFail (n,l) ->
ist.ltacvars, TacFail (intern_or_var ist n,intern_message ist l)
- | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac)
+ | TacProgress tac -> ist.ltacvars, TacProgress (intern_pure_tactic ist tac) | TacShowHyps tac -> ist.ltacvars, TacShowHyps (intern_pure_tactic ist tac)
| TacAbstract (tac,s) ->
ist.ltacvars, TacAbstract (intern_pure_tactic ist tac,s)
| TacThen (t1,[||],t2,[||]) ->
@@ -1809,6 +1809,7 @@ and eval_tactic ist = function
db_breakpoint ist.debug s; res
| TacFail (n,s) -> fun gl -> tclFAIL (interp_int_or_var ist n) (interp_message ist gl s) gl
| TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
+ | TacShowHyps tac -> tclSHOWHYPS (interp_tactic ist tac)
| TacAbstract (tac,ido) ->
fun gl -> Tactics.tclABSTRACT
(Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl
@@ -2940,6 +2941,7 @@ and subst_tactic subst (t:glob_tactic_expr) = match t with
TacMatch (lz,subst_tactic subst c,subst_match_rule subst lmr)
| TacId _ | TacFail _ as x -> x
| TacProgress tac -> TacProgress (subst_tactic subst tac:glob_tactic_expr)
+ | TacShowHyps tac -> TacShowHyps (subst_tactic subst tac:glob_tactic_expr)
| TacAbstract (tac,s) -> TacAbstract (subst_tactic subst tac,s)
| TacThen (t1,tf,t2,tl) ->
TacThen (subst_tactic subst t1,Array.map (subst_tactic subst) tf,
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 637269a663..69cee21487 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -53,6 +53,7 @@ let tclDO = Refiner.tclDO
let tclTIMEOUT = Refiner.tclTIMEOUT
let tclWEAK_PROGRESS = Refiner.tclWEAK_PROGRESS
let tclPROGRESS = Refiner.tclPROGRESS
+let tclSHOWHYPS = Refiner.tclSHOWHYPS
let tclNOTSAMEGOAL = Refiner.tclNOTSAMEGOAL
let tclTHENTRY = Refiner.tclTHENTRY
let tclIFTHENELSE = Refiner.tclIFTHENELSE
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 4e9198d37d..39f60e1968 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -54,6 +54,7 @@ val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic
val tclDO : int -> tactic -> tactic
val tclWEAK_PROGRESS : tactic -> tactic
val tclPROGRESS : tactic -> tactic
+val tclSHOWHYPS : tactic -> tactic
val tclNOTSAMEGOAL : tactic -> tactic
val tclTHENTRY : tactic -> tactic -> tactic
val tclMAP : ('a -> tactic) -> 'a list -> tactic
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-15 00:40:36 +0000