X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=86e58aa9faed497c82913b35d90f5f816292f8c5;hb=f82a5324071bc1b8fc5c9ea95ba03e40801c74ed;hp=fbfe21c447b17dbff47746ea04032315b1218328;hpb=bea50d8a7fdf4063d8bf42d2983734190457e030;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index fbfe21c44..86e58aa9f 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -212,9 +212,9 @@ let are_convertible =
               (fun b t1 t2 ->
                 b &&
                  match t1,t2 with
-                    None,None -> true
+                    None,_
+                  | _,None  -> true
                   | Some t1',Some t2' -> aux context t1' t2'
-                  | _,_ -> false
               ) true l1 l2
         | (C.Sort s1, C.Sort s2) -> true (*CSC da finire con gli universi *)
         | (C.Prod (name1,s1,t1), C.Prod(_,s2,t2)) ->