Initial revision

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

diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
index d0e103521b88fedf16615c79c05cb2b79c8c858a..93335625a25c0951ef4ade711069f75ef3bc19fd 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
+++ b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml
@@ -75,7 +75,6 @@ let unwind' m k e t =
     | C.LetIn (n,s,t) -> C.LetIn (n, unwind_aux m s, unwind_aux (m + 1) t)
     | C.Appl l -> C.Appl (List.map (unwind_aux m) l)
     | C.Const _ as t -> t
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase (sp,cookingsno,i,outt,t,pl) ->
@@ -172,7 +171,6 @@ let rec reduce : config -> Cic.term =
          | C.CurrentProof (_,_,body,_) -> reduce (0, [], body, s)
          | C.InductiveDefinition _ -> raise ReferenceToInductiveDefinition
        )
-    | (k, e, (C.Abst _ as t), s) -> t (* s should be empty ????? *)
     | (k, e, (C.MutInd (uri,_,_) as t),s) -> let t' = unwind k e t in 
                                          if s = [] then t' else C.Appl (t'::s)
     | (k, e, (C.MutConstruct (uri,_,_,_) as t),s) -> 
@@ -230,7 +228,7 @@ let rec reduce : config -> Cic.term =
                  eat_first (num_to_eat,tl)
               in
                reduce (k, e, (List.nth pl (j-1)),(ts@s)) 
-         | C.Abst _| C.Cast _ | C.Implicit ->
+         | C.Cast _ | C.Implicit ->
             raise (Impossible 2) (* we don't trust our whd ;-) *)
          | _ -> let t' = unwind k e t in
                 if s = [] then t' else C.Appl (t'::s)
@@ -294,7 +292,6 @@ let rec whd = let module C = Cic in
     | C.Appl [] -> raise (Impossible 1)
     | C.Appl (he::tl) -> reduce (0, [], he, tl)
     | C.Const _ as t -> reduce (0, [], t, [])
-    | C.Abst _ as t -> t
     | C.MutInd _ as t -> t
     | C.MutConstruct _ as t -> t
     | C.MutCase _ as t -> reduce (0, [], t, [])