]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAstPp.ml
- cicInspect: relevant nodes count updated: letin nodes are not relevant
[helm.git] / helm / software / components / grafite / grafiteAstPp.ml
index 70acd56d8fc15730e8a40564c7d6bb201a1a62a1..b74677949f5dc309e914f60b5b22317da298abd3 100644 (file)
@@ -341,7 +341,8 @@ let pp_command ~term_pp ~obj_pp = function
       "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) ->