X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicReductionMachine.ml;h=93335625a25c0951ef4ade711069f75ef3bc19fd;hb=89262281b6e83bd2321150f81f1a0583645eb0c8;hp=d0e103521b88fedf16615c79c05cb2b79c8c858a;hpb=37f08b2aba9f17d9d609ca0f57d607f437a3d3fc;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReductionMachine.ml b/helm/ocaml/cic_proof_checking/cicReductionMachine.ml index d0e103521..93335625a 100644 --- 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, [])