From 44fcc9da6b199bffc981a37d45d32447f4a4bd29 Mon Sep 17 00:00:00 2001
From: corbinea <corbinea@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 3 Jul 2003 07:38:46 +0000
Subject: modification ground

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4218 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/first-order/formula.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'contrib/first-order')

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 96f6930ca..4a76a4dcd 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -184,7 +184,7 @@ let build_atoms gl metagen side cciterm =
 	| Hint     -> 
 	    let rels,head=decompose_prod cciterm in
 	    let env=List.rev (List.map (fun _->mkMeta (metagen true)) rels) in
-	      build_rec env false head
+	      build_rec env false head;trivial:=false (* special for hints *)
     end;
     (!trivial,
      {positive= !positive;
-- 
cgit v1.2.3