From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Tue, 17 May 2005 13:03:34 +0000 (+0000)
Subject: bugfix in elim, cardinality constraint should >= 1 not > 1
X-Git-Tag: single_binding~53
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e9aaf3fb77afbe96c033ce2940734edd8f2cde88;p=helm.git

bugfix in elim, cardinality constraint should >= 1 not > 1
---

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]);
     ]