From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
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/?p=helm.git;a=commitdiff_plain;h=513c712655ff11a969ff2eed7f09c3133bc6aec9

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