| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
| NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
| NChange (_,what,wwhat) -> "nchange " ^ assert false ^
" with " ^ CicNotationPp.pp_term wwhat
| NCut (_,t) -> "ncut " ^ CicNotationPp.pp_term t
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
| NElim (_,what,where) -> "nelim " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
| NId _ -> "nid"
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t
let pp_ncommand = function
| UnificationHint (_,t, n) ->
"unification hint " ^ string_of_int n ^ " " ^ CicNotationPp.pp_term t