Procedural: now patterns for rewrite are generated correctly

[helm.git] / components / acic_procedural / acic2Procedural.ml

diff --git a/components/acic_procedural/acic2Procedural.ml b/components/acic_procedural/acic2Procedural.ml
index 6512938df3435ca46ad2273ae89d538f12cc6693..bbc358f71e7fbc0db2eebce8f7624e393d072877 100644 (file)
--- a/components/acic_procedural/acic2Procedural.ml
+++ b/components/acic_procedural/acic2Procedural.ml
@@ -252,6 +252,8 @@ and mk_fwd_proof st dtext name = function
          | None   -> [T.LetIn (name, v, dtext)] 
          | Some v -> mk_fwd_proof st dtext name v
       end
+   | C.ACast (_, v, _)                                  ->
+      mk_fwd_proof st dtext name v
    | v                                                  ->
       match get_inner_types st v with
          | Some (ity, _) ->
@@ -333,6 +335,8 @@ and mk_proof st = function
             mk_intros st script
 (*         | Some t -> mk_proof st t *)
       end
+   | C.ACast (_, t, _)                             ->
+      mk_proof st t
    | t                                             ->
       let text = Printf.sprintf "%s: %s" "UNEXPANDED" (string_of_head t) in
       let script = [T.Note text] in