From 91a053eb7a6ced7443122635312718a53aab803f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 5 Dec 2001 10:53:40 +0000
Subject: [PATCH] Discharging of variables with a body was bugged. Fixed.

---
 helm/ocaml/cic_proof_checking/cicCooking.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml
index 75f594a90..109c1582f 100644
--- 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
-- 
2.39.2