From e9aaf3fb77afbe96c033ce2940734edd8f2cde88 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 17 May 2005 13:03:34 +0000
Subject: [PATCH] bugfix in elim, cardinality constraint should >= 1 not > 1

---
 helm/ocaml/tactics/metadataQuery.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index a232c67e4..d91bec974 100644
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -342,7 +342,7 @@ let experimental_hint
 let elim ~dbd uri =
   let constraints =
     [`Rel [`MainConclusion None];
-     `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Gt 1))]);
+     `Sort (Cic.Prop,[`MainHypothesis (Some (MetadataTypes.Ge 1))]);
      `Obj (uri,[`MainHypothesis (Some (MetadataTypes.Eq 0))]);
      `Obj (uri,[`InHypothesis]);
     ]
-- 
2.39.2