| NId _ -> "nid"
| NIntro (_,n) -> "#" ^ n
| NRewrite (_,dir,n,where) -> "nrewrite" ^ assert false
+ | NReduce _ | NGeneralize _ | NLetIn _ | NAssert _ -> assert false
;;
let rec pp_tactic ~map_unicode_to_tex ~term_pp ~lazy_term_pp =
"unification hint " ^ string_of_int n ^ " " ^ term_pp t
| Default (_,what,uris) -> pp_default what uris
| Drop _ -> "drop"
- | Include (_,path) -> "include \"" ^ path ^ "\""
+ | Include (_,false,path) -> "include \"" ^ path ^ "\""
+ | Include (_,true,path) -> "include source \"" ^ path ^ "\""
| Obj (_,obj) -> obj_pp obj
| Qed _ -> "qed"
| Relation (_,id,a,aeq,refl,sym,trans) ->
| NonPunctuationTactical (_, tac, punct) ->
pp_non_punctuation_tactical tac
^ pp_punctuation_tactical punct
+ | NNonPunctuationTactical (_, tac, punct) ->
+ pp_non_punctuation_tactical tac
+ ^ pp_punctuation_tactical punct
| Command (_, cmd) -> pp_command ~term_pp ~obj_pp cmd ^ "."
let pp_comment ~map_unicode_to_tex ~term_pp ~lazy_term_pp ~obj_pp =