]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/grafite/grafiteAst.ml
Tracing mechanism for auto. Interface changed to solve an ambiguity between
[helm.git] / helm / software / components / grafite / grafiteAst.ml
index 1910e34ac949d279cae975f146920745f2368189..5b10a5465cc5fc9ad68889fc87a8236ad3bede2c 100644 (file)
@@ -43,7 +43,7 @@ type 'lazy_term reduction =
 
 type 'ident intros_spec = int option * 'ident option list
 
-type 'term auto_params = 'term list * (string*string) list
+type 'term auto_params = 'term list option * (string*string) list
 
 type 'term just =
  [ `Term of 'term