added include' to include everything but preferences (aka aliases)

[helm.git] / helm / software / components / lexicon / lexiconAstPp.ml

diff --git a/helm/software/components/lexicon/lexiconAstPp.ml b/helm/software/components/lexicon/lexiconAstPp.ml
index e49a66f607b7a305463b592ff9962564c8374269..4b20958aa084fc3b672243229355fa2d25b47edb 100644 (file)
--- a/helm/software/components/lexicon/lexiconAstPp.ml
+++ b/helm/software/components/lexicon/lexiconAstPp.ml
@@ -75,7 +75,11 @@ let pp_notation dir_opt l1_pattern assoc prec l2_pattern =
     (pp_l2_pattern l2_pattern)
     
 let pp_command = function
-  | Include (_,path) -> "include " ^ path
+  | Include (_,path,mode) -> 
+      if mode = WithPreferences then
+        "include " ^ path
+      else
+        "include' " ^ path
   | Alias (_,s) -> pp_alias s
   | Interpretation (_, dsc, (symbol, arg_patterns), cic_appl_pattern) ->
       pp_interpretation dsc symbol arg_patterns cic_appl_pattern