From 54b16bbdde9723382f555331916e2252e23e9bbb Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 6 Dec 2001 18:24:58 +0000 Subject: [PATCH] Bug fixed: cooking w.r.t. a variable with a body must not increment the number of left parameters. --- helm/ocaml/cic_proof_checking/cicCooking.ml | 13 ++++++++++++- 1 file changed, 12 insertions(+), 1 deletion(-) 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 = -- 2.39.2