From: Claudio Sacerdoti Coen Date: Tue, 16 Apr 2002 09:16:17 +0000 (+0000) Subject: Invariant enforced: no Appl of another Appl. X-Git-Tag: V_0_3_0_debian_8~155 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=513c712655ff11a969ff2eed7f09c3133bc6aec9;p=helm.git Invariant enforced: no Appl of another Appl. --- diff --git a/helm/ocaml/cic_proof_checking/cicSubstitution.ml b/helm/ocaml/cic_proof_checking/cicSubstitution.ml index a4ca7b5cd..b683dd258 100644 --- a/helm/ocaml/cic_proof_checking/cicSubstitution.ml +++ b/helm/ocaml/cic_proof_checking/cicSubstitution.ml @@ -85,11 +85,19 @@ let subst arg = | C.Meta _ as t -> t | C.Sort _ as t -> t | C.Implicit as t -> t - | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) (*CSC ??? *) + | C.Cast (te,ty) -> C.Cast (substaux k te, substaux k ty) | C.Prod (n,s,t) -> C.Prod (n, substaux k s, substaux (k + 1) t) | C.Lambda (n,s,t) -> C.Lambda (n, substaux k s, substaux (k + 1) t) | C.LetIn (n,s,t) -> C.LetIn (n, substaux k s, substaux (k + 1) t) - | C.Appl l -> C.Appl (List.map (substaux k) l) + | C.Appl (he::tl) -> + (* Invariant: no Appl applied to another Appl *) + let tl' = List.map (substaux k) tl in + begin + match substaux k he with + C.Appl l -> C.Appl (l@tl') + | _ as he' -> C.Appl (he'::tl') + end + | C.Appl _ -> assert false | C.Const _ as t -> t | C.Abst _ as t -> t | C.MutInd _ as t -> t