It now exits gracefully after an End-of-file.

[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 86bf3166047ef03b0654aca9bd5360c8a0a9ec09..109c1582fa45afe2640a48b1dddd73ae27c0ead8 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicCooking.ml
+++ b/helm/ocaml/cic_proof_checking/cicCooking.ml
@@ -36,7 +36,7 @@ let mem x lol =
 ;;
 
 (* cook var term *)
-let cook curi cookingsno var =
+let cook curi cookingsno var is_letin =
  let rec aux k =
   let module C = Cic in
    function
@@ -66,7 +66,7 @@ let cook curi cookingsno var =
         )
     | C.Appl [] -> raise Impossible
     | C.Const (uri,_) ->
-       if match CicEnvironment.get_obj uri with
+       if not is_letin && match CicEnvironment.get_obj uri with
            C.Definition (_,_,_,params) when mem var params -> true
          | C.Definition _ -> false
          | C.Axiom (_,_,params) when mem var params -> true
@@ -82,7 +82,7 @@ let cook curi cookingsno var =
         C.Const (uri,UriManager.relative_depth curi uri cookingsno)
     | C.Abst _ as t -> t
     | C.MutInd (uri,_,i) ->
-       if match CicEnvironment.get_obj uri with
+       if not is_letin && match CicEnvironment.get_obj uri with
            C.InductiveDefinition (_,params,_) when mem var params -> true
          | C.InductiveDefinition _ -> false
          | _ -> raise WrongUriToInductiveDefinition
@@ -91,7 +91,7 @@ let cook curi cookingsno var =
        else
         C.MutInd (uri,UriManager.relative_depth curi uri cookingsno,i)
     | C.MutConstruct (uri,_,i,j) ->
-       if match CicEnvironment.get_obj uri with
+       if not is_letin && match CicEnvironment.get_obj uri with
            C.InductiveDefinition (_,params,_) when mem var params -> true
          | C.InductiveDefinition _ -> false
          | _ -> raise WrongUriToInductiveDefinition
@@ -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 _ -> cook curi cookingsno var true ty
+           | None -> cook curi cookingsno var false ty
+         )
+       in
+        cookrec cooked_once tl
    | _ -> ty
   in
    cookrec ty vars
@@ -214,4 +220,6 @@ let cook_obj obj uri =
     cook_all_levels obj (List.rev params)
 ;;
 
-CicEnvironment.set_cooking_function cook_obj;;
+let init () =
+   CicEnvironment.set_cooking_function cook_obj
+;;