* Major code cleanup.

[helm.git] / helm / ocaml / cic_proof_checking / cicCooking.ml

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml
index 12c8cd15c4e5cdf2aba454423092e8a2038dfca4..75f594a90542de4f874899b1fe0362a2fa4f9e6e 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicCooking.ml
+++ b/helm/ocaml/cic_proof_checking/cicCooking.ml
@@ -136,8 +136,14 @@ let cook_gen add_binder curi cookingsno ty vars =
           C.Variable (varname, varbody, vartype) -> (varname, varbody, vartype)
         | _ -> raise (WrongUriToVariable (U.string_of_uri var))
       in
-       cookrec (add_binder (C.Name varname) varbody vartype
-        (cook curi cookingsno var ty)) tl
+       let cooked_once =
+        add_binder (C.Name varname) varbody vartype
+         (match varbody with
+             Some _ -> ty
+           | None -> cook curi cookingsno var ty
+         )
+       in
+        cookrec cooked_once tl
    | _ -> ty
   in
    cookrec ty vars