| `Auto params -> pp_auto_params ~term_pp params
;;
-let pp_ntactic ~map_unicode_to_tex = function
+let rec pp_ntactic ~map_unicode_to_tex = function
| NApply (_,t) -> "napply " ^ CicNotationPp.pp_term t
| NCases (_,what,where) -> "ncases " ^ CicNotationPp.pp_term what ^
assert false ^ " " ^ assert false
(String.concat " " (List.map string_of_int l))
| NUnfocus _ -> "##unfocus"
| NSkip _ -> "##skip"
+ | NTry (_,tac) -> "ntry (" ^ pp_ntactic ~map_unicode_to_tex tac ^ ")"
+ | NAssumption _ -> "nassumption"
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
"inverter " ^ n ^ " for " ^ term_pp ty ^ " " ^ List.fold_left (fun acc x -> acc ^ (match x with true -> "%" | _ -> "?")) "" params
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
- | Include (_,true,path) -> "include \"" ^ path ^ "\""
- | Include (_,false,path) -> "include source \"" ^ path ^ "\""
+ | Include (_,true,`OldAndNew,path) -> "include \"" ^ path ^ "\""
+ | Include (_,false,`OldAndNew,path) -> "include source \"" ^ path ^ "\""
+ | Include (_,_,`New,path) -> "RECURSIVELY INCLUDING " ^ path
| Obj (_,obj) -> obj_pp obj
| Qed _ -> "qed"
| Relation (_,id,a,aeq,refl,sym,trans) ->