A (boring and long) once-in-a-life exercise on proving a trivial property

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

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index c4940e08989c259b403aff5e24d74034509ec93a..90a5d3ce63d7e81c94028136e0ed188e1a5c0bc8 100644 (file)
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -435,6 +435,9 @@ and unify test_eq_only metasenv subst context t1 t2 =
              with Invalid_argument _ -> 
                raise (uncert_exc metasenv subst context t1 t2))
        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
+       | _ when NCicUntrusted.metas_of_term subst context t1 = [] && 
+                NCicUntrusted.metas_of_term subst context t2 = [] -> 
+                  raise (fail_exc metasenv subst context t1 t2)
        | _ -> raise (uncert_exc metasenv subst context t1 t2)
      (*D*)  in outside(); rc with exn -> outside (); raise exn 
     in