moved the expansion of implicits inside the refiner in a lazy way

[helm.git] / helm / ocaml / cic_proof_checking / cicReduction.ml

diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml
index 0229f23386bf39d0d0ed3a5cee7b8f1919c05760..39133ac92a4beb9ce9a5bbd87c4ca2f27387fc79 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReduction.ml
+++ b/helm/ocaml/cic_proof_checking/cicReduction.ml
@@ -1006,8 +1006,7 @@ let are_convertible whd ?(subst=[]) ?(metasenv=[])  =
             else
               false,ugraph
         | (C.Cast _, _) | (_, C.Cast _)
-        | (C.Implicit _, _) | (_, C.Implicit _) ->
-            assert false
+        | (C.Implicit _, _) | (_, C.Implicit _) -> assert false
         | (_,_) -> false,ugraph
     end
   in