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

[helm.git] / helm / ocaml / tactics / metadataQuery.ml

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index a232c67e4e621244ebae425102b1303b6c6608b1..d91bec9743aea312a14afda79f891e1744f7a655 100644 (file)
--- 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]);
     ]