Universes speedup:

[helm.git] / helm / ocaml / tactics / paramodulation / indexing.ml

diff --git a/helm/ocaml/tactics/paramodulation/indexing.ml b/helm/ocaml/tactics/paramodulation/indexing.ml
index 8ece33e35251e9e642a95086617eea29fadf9d5b..4eed05790fd777060db24f2d757e9b97cfd69425 100644 (file)
--- a/helm/ocaml/tactics/paramodulation/indexing.ml
+++ b/helm/ocaml/tactics/paramodulation/indexing.ml
@@ -1010,7 +1010,7 @@ let rec demodulation_theorem newmeta env table theorem =
       newmeta, theorem
 ;;
 
-let demodulate_tac ~dbd ~pattern ((proof,goal) as initialstatus) = 
+let demodulate_tac ~dbd ~pattern (proof,goal) = 
   let module I = Inference in
   let curi,metasenv,pbo,pty = proof in
   let metano,context,ty = CicUtil.lookup_meta goal metasenv in