]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/paramodulation/utils.mli
removed no longer used METAs
[helm.git] / helm / ocaml / tactics / paramodulation / utils.mli
index 2b09e59ae5655024cdb5fc2521ecbf4cc836d18e..ce14d480f0735a426035191df6d833385258b181 100644 (file)
@@ -63,7 +63,7 @@ val ao: Cic.term -> Cic.term -> comparison
 (** term-ordering function settable by the user *)
 val compare_terms: (Cic.term -> Cic.term -> comparison) ref
 
-val guarded_simpl:  Cic.context -> Cic.term -> Cic.term
+val guarded_simpl:  ?debug:bool -> Cic.context -> Cic.term -> Cic.term
 
 type equality_sign = Negative | Positive