From 54522577365be23b788d66c851ae5c78aebe5ffb Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 12 Jul 2008 22:17:46 +0000 Subject: [PATCH] Procedural: bug fix in the procedural rendering of the abstraction --- .../acic_procedural/acic2Procedural.ml | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml index 8e99a9332..dd59d1f6e 100644 --- a/helm/software/components/acic_procedural/acic2Procedural.ml +++ b/helm/software/components/acic_procedural/acic2Procedural.ml @@ -175,7 +175,7 @@ with Invalid_argument _ -> failwith "A2P.get_ind_names" (* proof construction *******************************************************) -let used_premise = C.Name "USED" +let anonymous_premise = C.Name "PREMISE" let mk_exp_args hd tl classes synth = let meta id = C.AImplicit (id, None) in @@ -283,17 +283,9 @@ let mk_rewrite st dtext where qs tl direction t = T.Rewrite (direction, where, None, e, dtext) :: script let rec proc_lambda st what name v t = - let dno = match get_inner_types st t with - | None -> false - | Some (sty, ety) -> - let sty, ety = H.cic sty, H.cic ety in - DTI.does_not_occur 1 sty && DTI.does_not_occur 1 ety - in - let dno = dno && DTI.does_not_occur 1 (H.cic t) in - let name = match dno, name with - | true, _ -> C.Anonymous - | false, C.Anonymous -> H.mk_fresh_name st.context used_premise - | false, name -> name + let name = match name with + | C.Anonymous -> H.mk_fresh_name st.context anonymous_premise + | name -> name in let entry = Some (name, C.Decl (H.cic v)) in let intro = get_intro name in -- 2.39.2