some fixed done in Orsay:

[helm.git] / components / tactics / paramodulation / inference.ml

diff --git a/components/tactics/paramodulation/inference.ml b/components/tactics/paramodulation/inference.ml
index 91fcee8a22833b645784a6e62ef03996e41d8f56..6004de44ceb29ef815daf390b824678aa8863ef3 100644 (file)
--- a/components/tactics/paramodulation/inference.ml
+++ b/components/tactics/paramodulation/inference.ml
@@ -51,7 +51,7 @@ let rec check_irl start = function
 let rec is_simple_term = function
   | Cic.Appl ((Cic.Meta _)::_) -> false
   | Cic.Appl l -> List.for_all is_simple_term l
-  | Cic.Meta (i, l) -> check_irl 1 l
+  | Cic.Meta (i, l) -> let l = [] in check_irl 1 l
   | Cic.Rel _ -> true
   | Cic.Const _ -> true
   | Cic.MutInd (_, _, []) -> true