no typing

diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml
index 99f66f1d11ccef7c114c5b4c0b93549c04641421..b759427e3dad4bb45fd3b0ae2d7f2c77c6c55817 100644 (file)
--- a/helm/software/components/tactics/paramodulation/indexing.ml
+++ b/helm/software/components/tactics/paramodulation/indexing.ml
@@ -1096,7 +1096,7 @@ let build_newg bag context goal rule expansion =
 let rec demod bag env table goal =
   let _,menv,t = goal in
   let _, context, ugraph = env in
-  let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:true)in
+  let res = demodulation_aux bag menv context ugraph table 0 t (~typecheck:false)in
   match res with
     | Some newt ->
        let newg =