Procedural: bug fix in the procedural rendering of the abstraction

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 8e99a93322fa6075ca339ce36b63f2a439612592..dd59d1f6e5305dfb74b04ea21dd7c035a21f62b1 100644 (file)
--- 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