name specifications added for elim_intros, elim_intros_simpl and elim_type

[helm.git] / helm / ocaml / cic_transformations / tacticAstPp.ml

diff --git a/helm/ocaml/cic_transformations/tacticAstPp.ml b/helm/ocaml/cic_transformations/tacticAstPp.ml
index 21bf33a0af6807a9429edf021a1468c67fe9a4ad..3275953651e01ddb1af92dca556b7917b78dc2ba 100644 (file)
--- a/helm/ocaml/cic_transformations/tacticAstPp.ml
+++ b/helm/ocaml/cic_transformations/tacticAstPp.ml
@@ -57,6 +57,12 @@ let pp_pattern (t, hyp, goal) =
   in
    pp_t t ^ " in " ^ pp_hyp_pattern hyp ^ " \\vdash " ^ pp_term_ast goal
 
+let pp_intros_specs = function
+   | None, []         -> ""
+   | Some num, []     -> Printf.sprintf " names %i" num
+   | None, idents     -> Printf.sprintf " names %s" (pp_idents idents)
+   | Some num, idents -> Printf.sprintf " names %i %s" num (pp_idents idents)
+
 let rec pp_tactic = function
   | Absurd (_, term) -> "absurd" ^ pp_term_ast term
   | Apply (_, term) -> "apply " ^ pp_term_ast term
@@ -76,10 +82,14 @@ let rec pp_tactic = function
   | Decompose (_, term) ->
       sprintf "decompose %s" (pp_term_ast term)
   | Discriminate (_, term) -> "discriminate " ^ pp_term_ast term
-  | Elim (_, term, using) ->
+  | Elim (_, term, using, num, idents) ->
       sprintf "elim " ^ pp_term_ast term ^
       (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
-  | ElimType (_, term) -> "elim type " ^ pp_term_ast term
+      ^ pp_intros_specs (num, idents) 
+  | ElimType (_, term, using, num, idents) ->
+      sprintf "elim type " ^ pp_term_ast term ^
+      (match using with None -> "" | Some term -> " using " ^ pp_term_ast term)
+      ^ pp_intros_specs (num, idents)
   | Exact (_, term) -> "exact " ^ pp_term_ast term
   | Exists _ -> "exists"
   | Fold (_, kind, term, pattern) ->