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 a4ca7b5cda395a3ec2923e7c263d52efc21a7777..b683dd258389f93b698403ac801b787354da9a46 100644 (file)
--- 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