let types = List.rev_map to_ident types in
sprintf "decompose %s %s%s" (pp_idents types) (opt_string_pp what) (pp_intros_specs (None, names))
| Demodulate _ -> "demodulate"
- | Discriminate (_, term) -> "discriminate " ^ term_pp term
+ | Destruct (_, term) -> "destruct " ^ term_pp term
| Elim (_, term, using, num, idents) ->
sprintf "elim " ^ term_pp term ^
(match using with None -> "" | Some term -> " using " ^ term_pp term)
| Fail _ -> "fail"
| Fourier _ -> "fourier"
| IdTac _ -> "id"
- | Injection (_, term) -> "injection " ^ term_pp term
| Intros (_, None, []) -> "intros"
| Inversion (_, term) -> "inversion " ^ term_pp term
| Intros (_, num, idents) ->
| Right _ -> "right"
| Ring _ -> "ring"
| Split _ -> "split"
- | Subst (_, s) -> "subst " ^ s
+ | Subst _ -> "subst"
| Symmetry _ -> "symmetry"
| Transitivity (_, term) -> "transitivity " ^ term_pp term
(* Tattiche Aggiunte *)
sprintf "default \"%s\" %s" what
(String.concat " " (List.map UriManager.string_of_uri uris))
-let pp_coercion uri do_composites =
- sprintf "coercion %s (* %s *)" (UriManager.string_of_uri uri)
+let pp_coercion uri do_composites arity =
+ sprintf "coercion %s %d (* %s *)" (UriManager.string_of_uri uri) arity
(if do_composites then "compounds" else "no compounds")
-let pp_command ~obj_pp = function
+let pp_command ~term_pp ~obj_pp = function
+ | Coercion (_, uri, do_composites, i) -> pp_coercion uri do_composites i
+ | Default (_,what,uris) -> pp_default what uris
+ | Drop _ -> "drop"
| Include (_,path) -> "include \"" ^ path ^ "\""
+ | Obj (_,obj) -> obj_pp obj
| Qed _ -> "qed"
- | Drop _ -> "drop"
+ | Relation (_,id,a,aeq,refl,sym,trans) ->
+ "relation " ^ term_pp aeq ^ " on " ^ term_pp a ^
+ (match refl with
+ Some r -> " reflexivity proved by " ^ term_pp r
+ | None -> "") ^
+ (match sym with
+ Some r -> " symmetry proved by " ^ term_pp r
+ | None -> "") ^
+ (match trans with
+ Some r -> " transitivity proved by " ^ term_pp r
+ | None -> "")
| Print (_,s) -> "print " ^ s
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
- | Coercion (_, uri, do_composites) -> pp_coercion uri do_composites
- | Obj (_,obj) -> obj_pp obj
- | Default (_,what,uris) ->
- pp_default what uris
let rec pp_tactical ~term_pp ~lazy_term_pp =
let pp_tactic = pp_tactic ~lazy_term_pp ~term_pp in
| First (_, tacs) -> sprintf "tries [%s]" (pp_tacticals ~sep:" | " tacs)
| Try (_, tac) -> "try " ^ pp_tactical ~term_pp ~lazy_term_pp tac
| Solve (_, tac) -> sprintf "solve [%s]" (pp_tacticals ~sep:" | " tac)
+ | Progress (_, tac) -> "progress " ^ pp_tactical ~term_pp ~lazy_term_pp tac
| Dot _ -> "."
| Semicolon _ -> ";"
pp_tactical ~lazy_term_pp ~term_pp tac
^ pp_tactical ~lazy_term_pp ~term_pp punct
| Tactical (_, tac, None) -> pp_tactical ~lazy_term_pp ~term_pp tac
- | Command (_, cmd) -> pp_command ~obj_pp cmd ^ "."
+ | Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
let pp_comment ~term_pp ~lazy_term_pp ~obj_pp =
function