From 3b6225b8cbe5fe4bf7c4356f9875962f957a8ffc Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 29 Apr 2009 13:37:24 +0000 Subject: [PATCH] no typing --- helm/software/components/tactics/paramodulation/indexing.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/tactics/paramodulation/indexing.ml b/helm/software/components/tactics/paramodulation/indexing.ml index 99f66f1d1..b759427e3 100644 --- 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 = -- 2.39.2