From 513c712655ff11a969ff2eed7f09c3133bc6aec9 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 16 Apr 2002 09:16:17 +0000 Subject: [PATCH] Invariant enforced: no Appl of another Appl. --- helm/ocaml/cic_proof_checking/cicSubstitution.ml | 12 ++++++++++-- 1 file changed, 10 insertions(+), 2 deletions(-) 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 -- 2.39.2