Optional callbacks have been added to tactics that need to introduce

[helm.git] / helm / ocaml / tactics / eliminationTactics.mli

diff --git a/helm/ocaml/tactics/eliminationTactics.mli b/helm/ocaml/tactics/eliminationTactics.mli
index 5e132c4966366860cad1e3cefa44b881e7aa1c2b..92d9eee016ebdcbb2d941d4ee54614f69f651760 100644 (file)
--- a/helm/ocaml/tactics/eliminationTactics.mli
+++ b/helm/ocaml/tactics/eliminationTactics.mli
@@ -25,9 +25,10 @@
 
 val elim_type_tac: term:Cic.term -> ProofEngineTypes.tactic
 
+(* The default callback always decomposes the term as much as possible *)
 val decompose_tac:
- term:Cic.term ->
- uris_choice_callback:
+ ?uris_choice_callback:
   ((UriManager.uri * int * (UriManager.uri * Cic.term) list) list ->
    (UriManager.uri * int * (UriManager.uri * Cic.term) list) list) ->
-   ProofEngineTypes.tactic
+ Cic.term ->
+  ProofEngineTypes.tactic