X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_proof_checking%2FcicReduction.ml;h=7ba2cffbcfaa76298770ed8c19c5a5c369badadc;hb=d0c88a989d2c41d0b816c5490d4d8c89a238cb2a;hp=813a589d603d7c2025d9cfb97686d10573e5064c;hpb=f41876ee0d76202514504fb7031c0245e56926be;p=helm.git diff --git a/helm/ocaml/cic_proof_checking/cicReduction.ml b/helm/ocaml/cic_proof_checking/cicReduction.ml index 813a589d6..7ba2cffbc 100644 --- a/helm/ocaml/cic_proof_checking/cicReduction.ml +++ b/helm/ocaml/cic_proof_checking/cicReduction.ml @@ -526,7 +526,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; let module S = CicSubstitution in let rec reduce = function - (k, e, _, (C.Rel n as t), s) -> + (k, e, _, C.Rel n, s) -> let d = try Some (RS.from_env (List.nth e (n-1))) @@ -577,14 +577,14 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; if s = [] then t' else C.Appl (t'::(RS.from_stack_list ~unwind s))) | (k, e, _, (C.Sort _ as t), s) -> t (* s should be empty *) | (k, e, _, (C.Implicit _ as t), s) -> t (* s should be empty *) - | (k, e, ens, (C.Cast (te,ty) as t), s) -> + | (k, e, ens, C.Cast (te,ty), s) -> reduce (k, e, ens, te, s) (* s should be empty *) | (k, e, ens, (C.Prod _ as t), s) -> unwind k e ens t (* s should be empty *) | (k, e, ens, (C.Lambda (_,_,t) as t'), []) -> unwind k e ens t' | (k, e, ens, C.Lambda (_,_,t), p::s) -> reduce (k+1, (RS.stack_to_env ~reduce ~unwind p)::e, ens, t,s) - | (k, e, ens, (C.LetIn (_,m,t) as t'), s) -> + | (k, e, ens, C.LetIn (_,m,t), s) -> let m' = RS.compute_to_env ~reduce ~unwind k e ens m in reduce (k+1, m'::e, ens, t, s) | (_, _, _, C.Appl [], _) -> assert false @@ -641,7 +641,7 @@ if List.mem uri params then debug_print (lazy "---- OK2") ; | (k, e, ens, (C.MutCase (mutind,i,_,term,pl) as t),s) -> let decofix = function - C.CoFix (i,fl) as t -> + C.CoFix (i,fl) -> let (_,_,body) = List.nth fl i in let body' = let counter = ref (List.length fl) in @@ -1077,7 +1077,7 @@ let rec normalize ?(delta=true) ?(subst=[]) ctx term = let t = whd ~delta ~subst ctx term in let aux = normalize ~delta ~subst in let decl name t = Some (name, C.Decl t) in - let def name t = Some (name, C.Def (t,None)) in + let def name t = Some (name, C.Def (t,None)) in match t with | C.Rel n -> t | C.Var (uri,exp_named_subst) ->