Discharging of variables with a body was bugged. Fixed.

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml
index 75f594a90542de4f874899b1fe0362a2fa4f9e6e..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
@@ -139,8 +139,8 @@ let cook_gen add_binder curi cookingsno ty vars =
        let cooked_once =
         add_binder (C.Name varname) varbody vartype
          (match varbody with
-             Some _ -> ty
-           | None -> cook curi cookingsno var ty
+             Some _ -> cook curi cookingsno var true ty
+           | None -> cook curi cookingsno var false ty
          )
        in
         cookrec cooked_once tl