ncoindutive now generates a co-inductive type, not an inductive one

[helm.git] / helm / software / components / ng_refiner / nCicMetaSubst.ml

diff --git a/helm/software/components/ng_refiner/nCicMetaSubst.ml b/helm/software/components/ng_refiner/nCicMetaSubst.ml
index d18dd1b9da013d89b2bfd558189b5f744cd93dc2..9cc6ac67c755c16e4208413f1cd7565859c64557 100644 (file)
--- a/helm/software/components/ng_refiner/nCicMetaSubst.ml
+++ b/helm/software/components/ng_refiner/nCicMetaSubst.ml
@@ -433,7 +433,7 @@ let delift ~unify metasenv subst context n l t =
       let lc = NCicUtils.expand_local_context lc in
       let l = List.map (NCicSubstitution.lift shift) lc in
        if
-        List.exists (fun t-> NCicUntrusted.metas_of_term subst context t = []) l
+        List.exists (fun t-> NCicUntrusted.metas_of_term subst context t <> [])l
        then
         raise (Uncertain msg)
        else