From b378b7f4f2a3a897c4b69f44d4d1d54cc4d0aa56 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Wed, 27 May 2009 18:44:41 +0000 Subject: [PATCH] Procedural: bugfix in the generation of intros for letin: the bodies and types of the actual letin and of the inferred letin must be equal upto alpha now nat/minus.ma and nat/minimization.ma are fully reconstructed :) --- helm/software/components/acic_procedural/procedural2.ml | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml index 45444f4fc..e3a2d62e7 100644 --- a/helm/software/components/acic_procedural/procedural2.ml +++ b/helm/software/components/acic_procedural/procedural2.ml @@ -138,7 +138,7 @@ try | {A.annsynthesized = st; A.annexpected = Some et} -> Some (st, et) | {A.annsynthesized = st; A.annexpected = None} -> Some (st, st) with Not_found -> None -with Invalid_argument _ -> failwith "A2P.get_inner_types" +with Invalid_argument _ -> failwith "P2.get_inner_types" let get_entry st id = let rec aux = function @@ -294,9 +294,12 @@ and proc_letin st what name v w t = let proceed, dtext = test_depth st in let script = if proceed then let st, hyp, rqv = match get_inner_types st what, get_inner_types st v with - | Some (C.ALetIn _, _), _ -> + | Some (C.ALetIn (_, _, iv, iw, _), _), _ when + H.alpha_equivalence ~flatten:true st.context (H.cic v) (H.cic iv) && + H.alpha_equivalence ~flatten:true st.context (H.cic w) (H.cic iw) + -> st, C.Def (H.cic v, H.cic w), [T.Intros (Some 1, [intro], dtext)] - | _, Some (ity, ety) -> + | _, Some (ity, ety) -> let st, rqv = match v with | C.AAppl (_, hd :: tl) when is_fwd_rewrite_right st hd tl -> mk_fwd_rewrite st dtext intro tl true v t ity ety -- 2.39.2