From 91a053eb7a6ced7443122635312718a53aab803f Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen 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