"include" command implemented.

[helm.git] / helm / matita / matitaMisc.ml

diff --git a/helm/matita/matitaMisc.ml b/helm/matita/matitaMisc.ml
index acaf2123c68690ef7edef457c8b326df963a5e98..1ea4e7e9228c52ffca09fcaa81b4a66e0b5be968 100644 (file)
--- a/helm/matita/matitaMisc.ml
+++ b/helm/matita/matitaMisc.ml
@@ -191,7 +191,7 @@ let get_proof_context status =
   | _ -> []
  
 let get_proof_aliases status = status.aliases
-  
+
 let qualify status name = get_string_option status "baseuri" ^ "/" ^ name
 
 let unopt = function None -> failwith "unopt: None" | Some v -> v