]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/software/components/tactics/inversion_principle.mli
Added a passive table
[helm.git] / helm / software / components / tactics / inversion_principle.mli
index 30335ed6cb38cc0509f0071b1ab4f0788f0726a2..5ceec20a49a192c08af5a8290b4af1a20e4f8407 100644 (file)
@@ -25,3 +25,6 @@
 
 (* $Id: primitiveTactics.ml 9014 2008-09-26 08:03:47Z tassi $ *)
 val init: unit -> unit
+val build_inverter: add_obj:(UriManager.uri -> Cic.obj -> 'b -> 'b * UriManager.uri list) ->
+                    'b -> UriManager.uri -> UriManager.uri -> bool list -> 
+                    'b * UriManager.uri list