Procedural: bugfix in the generation of intros for letin: the bodies and types of...

now nat/minus.ma and nat/minimization.ma are fully reconstructed :)

diff --git a/helm/software/components/acic_procedural/procedural2.ml b/helm/software/components/acic_procedural/procedural2.ml
index 45444f4fc19cfd2f06136ce0d5e729ced7722cc6..e3a2d62e757c47f4b89b5376d995c69fe8e8fa54 100644 (file)
--- 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