open GrafiteAst
-module Ast = CicNotationPt
-
let tactical_terminator = ""
let tactic_terminator = tactical_terminator
let command_terminator = tactical_terminator
sprintf "alias num (instance %d) = \"%s\"" instance desc
let pp_argument_pattern = function
- | Ast.IdentArg (eta_depth, name) ->
+ | CicNotationPt.IdentArg (eta_depth, name) ->
let eta_buf = Buffer.create 5 in
for i = 1 to eta_depth do
Buffer.add_string eta_buf "\\eta."
| Some `LeftToRight -> "> "
| Some `RightToLeft -> "< "
-let pp_metadata =
- function
- | Dependency buri -> sprintf "dependency %s" buri
- | Baseuri buri -> sprintf "baseuri %s" buri
-
let pp_command = function
| Include (_,path) -> "include " ^ path
| Qed _ -> "qed"
| Drop _ -> "drop"
| Set (_, name, value) -> sprintf "set \"%s\" \"%s\"" name value
- | Coercion (_,term) -> sprintf "coercion %s" (pp_term_ast term)
+ | Coercion (_,term, _do_composites) ->
+ sprintf "coercion %s" (pp_term_ast term)
| Alias (_,s) -> pp_alias s
| Obj (_,obj) -> CicNotationPp.pp_obj obj
| Default (_,what,uris) ->
(pp_associativity assoc)
(pp_precedence prec)
(pp_l2_pattern l2_pattern)
- | Metadata (_, m) -> sprintf "metadata %s" (pp_metadata m)
| Render _
| Dump _ -> assert false (* ZACK: debugging *)
| Include (_,path) -> "include " ^ path
| Qed _ -> "qed"
| Drop _ -> "drop"
- | Coercion (_,term) -> sprintf "coercion %s" (CicPp.ppterm term)
+ | Coercion (_,term,_add_composites) ->
+ sprintf "coercion %s" (CicPp.ppterm term)
| Set _
| Alias _
| Default _
| Render _
| Dump _
| Interpretation _
- | Metadata _
| Notation _
| Obj _ -> assert false (* not implemented *)