From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 6 Dec 2001 18:24:58 +0000 (+0000)
Subject: Bug fixed: cooking w.r.t. a variable with a body must not increment
X-Git-Tag: mlminidom_0_2_2~17
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=54b16bbdde9723382f555331916e2252e23e9bbb;p=helm.git

Bug fixed: cooking w.r.t. a variable with a body must not increment
the number of left parameters.
---

diff --git a/helm/ocaml/cic_proof_checking/cicCooking.ml b/helm/ocaml/cic_proof_checking/cicCooking.ml
index 109c1582f..c382bb361 100644
--- a/helm/ocaml/cic_proof_checking/cicCooking.ml
+++ b/helm/ocaml/cic_proof_checking/cicCooking.ml
@@ -197,7 +197,18 @@ let cook_one_level obj curi cookingsno vars =
            (name,inductive,cook_prod curi cookingsno arity vars,constructors')
         ) dl
       in
-       C.InductiveDefinition (dl', params, n_ind_params + List.length vars)
+       let number_of_variables_without_a_body =
+        let is_not_letin uri =
+         match CicEnvironment.get_obj uri with
+            C.Variable (_,None,_) -> true
+          | C.Variable (_,Some _,_) -> false
+          | _ -> raise (WrongUriToVariable (UriManager.string_of_uri uri))
+        in
+         List.fold_left
+          (fun i uri -> if is_not_letin uri then i + 1 else i) 0 vars
+       in
+        C.InductiveDefinition
+         (dl', params, n_ind_params + number_of_variables_without_a_body)
 ;; 
 
 let cook_obj obj uri =