Demodulate_tac now depends on the universe

[helm.git] / components / tactics / tactics.mli

diff --git a/components/tactics/tactics.mli b/components/tactics/tactics.mli
index 3379fbe77b14503420f1954e65515250695ff773..88179e4c8724f3bb1b9e9e61868ebeed29606f21 100644 (file)
--- a/components/tactics/tactics.mli
+++ b/components/tactics/tactics.mli
@@ -26,7 +26,8 @@ val decompose :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->
   ?user_types:(UriManager.uri * int) list ->
   ?what:string -> dbd:HMysql.dbd -> ProofEngineTypes.tactic
-val demodulate : dbd:HMysql.dbd -> ProofEngineTypes.tactic
+val demodulate : dbd:HMysql.dbd -> 
+  universe:Universe.universe -> ProofEngineTypes.tactic
 val destruct : term:Cic.term -> ProofEngineTypes.tactic
 val elim_intros :
   ?mk_fresh_name_callback:ProofEngineTypes.mk_fresh_name_type ->