X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionNaif.ml;h=f569e75cd451f196a83ef95e86db8a735e07e206;hb=6f6b8f33397548319fef9b374f9e9017e7fa151d;hp=fbfe21c447b17dbff47746ea04032315b1218328;hpb=06e9498bf967323fe12d6383ec7b279a4546a06c;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
index fbfe21c44..f569e75cd 100644
--- a/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionNaif.ml
@@ -91,7 +91,6 @@ let whd context =
          | C.CurrentProof (_,_,body,_) -> whdaux l body
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | C.Abst _ as t -> t (*CSC l should be empty ????? *)
     | C.MutInd (uri,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutConstruct (uri,_,_,_) as t -> if l = [] then t else C.Appl (t::l)
     | C.MutCase (mutind,cookingsno,i,_,term,pl) as t->
@@ -146,7 +145,7 @@ let whd context =
                  eat_first (num_to_eat,tl)
               in
                whdaux (ts@l) (List.nth pl (j-1))
-         | C.Abst _| C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ -> if l = [] then t else C.Appl (t::l)
        )
@@ -212,9 +211,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)) ->
@@ -276,7 +275,7 @@ let are_convertible =
               (fun (_,ty1,bo1) (_,ty2,bo2) b ->
                 b && aux context ty1 ty2 && aux (tys@context) bo1 bo2)
               fl1 fl2 true
-        | (C.Abst _, _) | (_, C.Abst _) | (C.Cast _, _) | (_, C.Cast _)
+        | (C.Cast _, _) | (_, C.Cast _)
         | (C.Implicit, _) | (_, C.Implicit) ->
            raise (Impossible 3) (* we don't trust our whd ;-) *)
         | (_,_) -> false