let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in
function
| NApply (_,t) -> "@" ^ NotationPp.pp_term status t
let pp_tactic_pattern = pp_tactic_pattern ~map_unicode_to_tex in
function
| NApply (_,t) -> "@" ^ NotationPp.pp_term status t
| NAuto (_,(None,flgs)) ->
"nautobatch" ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
| NAuto (_,(None,flgs)) ->
"nautobatch" ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
"nautobatch" ^ " by " ^
(String.concat "," (List.map (NotationPp.pp_term status) l)) ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
"nautobatch" ^ " by " ^
(String.concat "," (List.map (NotationPp.pp_term status) l)) ^
String.concat " " (List.map (fun a,b -> a ^ "=" ^ b) flgs)
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NConstructor (_,None,l) -> "@ " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NConstructor (_,None,l) -> "@ " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NConstructor (_,Some x,l) -> "@" ^ string_of_int x ^ " " ^
String.concat " " (List.map (NotationPp.pp_term status) l)
| NCase1 (_,n) -> "*" ^ n ^ ":"
" with " ^ NotationPp.pp_term status wwhat
| NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t
| NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *)
| NClear (_,l) -> "nclear " ^ String.concat " " l
" with " ^ NotationPp.pp_term status wwhat
| NCut (_,t) -> "ncut " ^ NotationPp.pp_term status t
(*| NDiscriminate (_,t) -> "ndiscriminate " ^ NotationPp.pp_term status t
| NSubst (_,t) -> "nsubst " ^ NotationPp.pp_term status t *)
| NClear (_,l) -> "nclear " ^ String.concat " " l
- | NDestruct (_,dom,skip) -> "ndestruct ..."
- | NElim (_,what,where) -> "nelim " ^ NotationPp.pp_term status what ^
+ | NDestruct (_,_dom,_skip) -> "ndestruct ..."
+ | NElim (_,what,_where) -> "nelim " ^ NotationPp.pp_term status what ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
| NIntros (_,l) -> "#" ^ String.concat " " l
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
| NIntros (_,l) -> "#" ^ String.concat " " l
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NLApply (_,t) -> "lapply " ^ NotationPp.pp_term status t
| NRewrite (_,dir,n,where) -> "nrewrite " ^
"...to be implemented..." ^ " " ^ "...to be implemented..."
| NLApply (_,t) -> "lapply " ^ NotationPp.pp_term status t
| NRewrite (_,dir,n,where) -> "nrewrite " ^
;;
let pp_nmacro status = function
| NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term status term)
| Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
;;
let pp_nmacro status = function
| NCheck (_, term) -> Printf.sprintf "ncheck %s" (NotationPp.pp_term status term)
| Screenshot (_, name) -> Printf.sprintf "screenshot \"%s\"" name
let pp_argument_pattern = function
| NotationPt.IdentArg (eta_depth, name) ->
let eta_buf = Buffer.create 5 in
let pp_argument_pattern = function
| NotationPt.IdentArg (eta_depth, name) ->
let eta_buf = Buffer.create 5 in