| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
| NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
+(*| NDiscriminate (_,t) -> "ndiscriminate " ^ CicNotationPp.pp_term t
+ | NSubst (_,t) -> "nsubst " ^ CicNotationPp.pp_term t *)
+ | NDestruct _ -> "ndestruct"
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
+ | NInversion (_,what,where) -> "ninversion " ^ CicNotationPp.pp_term what ^
+ assert false ^ " " ^ assert false
| NLApply (_,t) -> "lapply " ^ CicNotationPp.pp_term t
| NRewrite (_,dir,n,where) -> "nrewrite " ^
(match dir with `LeftToRight -> ">" | `RightToLeft -> "<") ^
| NBranch _ -> "##["
| NShift _ -> "##|"
| NPos (_, l) -> "##" ^String.concat "," (List.map string_of_int l)^ ":"
+ | NPosbyname (_, s) -> "##" ^ s ^ ":"
| NWildcard _ -> "##*:"
| NMerge _ -> "##]"
| NFocus (_,l) ->
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
+ | NDiscriminator (_,_)
+ | NInverter (_,_,_,_,_)
| NObj (_,_)
| NUnivConstraint (_) -> "not supported"
| NCoercion (_) -> "not supported"