From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 5 Dec 2001 10:53:40 +0000 (+0000)
Subject: Discharging of variables with a body was bugged. Fixed.
X-Git-Tag: mlminidom_0_2_2~24
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=91a053eb7a6ced7443122635312718a53aab803f;p=helm.git

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 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