diff options
Diffstat (limited to 'parsing/pptactic.ml')
-rw-r--r-- | parsing/pptactic.ml | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 6571e0af8..6c45c9e70 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -124,6 +124,9 @@ let pr_clause_pattern pr_id = function (* To check *) ++ spc () ++ pr_id id) l ++ pr_opt (prlist_with_sep spc int) glopt +let pr_subterms pr occl = + hov 0 (pr_occurrences pr occl ++ spc () ++ str "with") + let pr_induction_arg prc = function | ElimOnConstr c -> prc c | ElimOnIdent (_,id) -> pr_id id @@ -452,8 +455,9 @@ and pr_atom1 = function (* Conversion *) | TacReduce (r,h) -> hov 1 (pr_red_expr (pr_constr,pr_cst) r ++ pr_clause pr_ident h) - | TacChange (c,h) -> - hov 1 (str "Change" ++ brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h) + | TacChange (occl,c,h) -> + hov 1 (str "Change" ++ pr_opt (pr_subterms pr_constr) occl ++ + brk (1,1) ++ pr_constr c ++ pr_clause pr_ident h) (* Equivalence relations *) | (TacReflexivity | TacSymmetry) as x -> pr_atom0 x |