implemented pretty printer for (mutual) (co)inductive types

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

diff --git a/helm/matita/matitaTypes.ml b/helm/matita/matitaTypes.ml
index 20ffd350dfd3d1965c8b62e524797d7065367308..cd9d34f0852e5fe9d9f3f327b5597199eb1da307 100644 (file)
--- a/helm/matita/matitaTypes.ml
+++ b/helm/matita/matitaTypes.ml
@@ -36,6 +36,7 @@ let debug_print s =
 exception No_proof  (** no current proof is available *)
 
 exception Cancel
+exception Unbound_identifier of string
 
 (*
 let untitled_con_uri = UriManager.uri_of_string "cic:/untitled.con"
@@ -73,13 +74,13 @@ class type disambiguator =
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         char Stream.t ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph)
       (** @param env @see disambiguateTerm above *)
     method disambiguateTermAst:
       ?context:Cic.context -> ?metasenv:Cic.metasenv ->
       ?env:DisambiguateTypes.environment ->
         DisambiguateTypes.term ->
-          (DisambiguateTypes.environment * Cic.metasenv * Cic.term)
+          (DisambiguateTypes.environment * Cic.metasenv * Cic.term * CicUniv.universe_graph) 
   end
 
 (*
@@ -129,23 +130,19 @@ class type interpreter =
 
       (** parse a single phrase contained in the input string. Additional
       * garbage at the end of the phrase is ignored
-      * @param transparent per default the interpreter catch all exceptions ans
-      * prints them in the console. When transparent is set to true exceptions
-      * are flow through. Defaults to false
+      * @return true if no exception has been raised by the evaluation, false
+      * otherwise
       *)
-    method evalPhrase: ?transparent:bool -> string -> unit
+    method evalPhrase: string -> bool
+
+      (** as above, evaluating a command/tactics AST *)
+    method evalAst: DisambiguateTypes.tactical -> bool
 
       (** offset from the starting of the last string parser by evalPhrase where
       * parsing stop.
       * @raise Failure when no offset has been recorded *)
     method endOffset: int
 
-(*
-      (** undo last steps phrases.
-      * @param steps number of phrases to undo; defaults to 1 *)
-    method undo: ?steps:int -> unit -> unit
-*)
-
   end
 
 (** {2 MathML widgets} *)