Changes to declarative tactics, implementation of equality chain

[helm.git] / matita / components / ng_tactics / nnAuto.mli

diff --git a/matita/components/ng_tactics/nnAuto.mli b/matita/components/ng_tactics/nnAuto.mli
index b0d7243796a06c4582b91415fb0a8b3e9babffa5..d77d32085813510d178e5848b8ff9c99bf001996 100644 (file)
--- a/matita/components/ng_tactics/nnAuto.mli
+++ b/matita/components/ng_tactics/nnAuto.mli
@@ -28,7 +28,7 @@ val auto_tac:
    ?trace_ref:NotationPt.term list ref -> 
    's NTacStatus.tactic
 
-val auto_lowtac: params:auto_params -> NTacStatus.lowtac_status -> int -> NTacStatus.lowtac_status
+val auto_lowtac: params:auto_params -> #NTacStatus.pstatus -> int -> 's NTacStatus.tactic
 
 val keys_of_type: 
   (#NTacStatus.pstatus as 'a) ->