]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/grafite_engine/grafiteTypes.mli
avoid writing in read only baseuris
[helm.git] / helm / ocaml / grafite_engine / grafiteTypes.mli
index 70089623b09479f097a41b79cbb18cf981e405c3..a8b86c27639fc9fe0f678332c7c1c94aeb4f5e1f 100644 (file)
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 exception Option_error of string * string
 exception Statement_error of string
 exception Command_error of string
 
+val command_error: string -> 'a   (** @raise Command_error *)
+
 type incomplete_proof = {
   proof: ProofEngineTypes.proof;
   stack: Continuationals.Stack.t;