Commit 9cd2cacb authored by Martin Clochard's avatar Martin Clochard

bugfix: compute also used goals as rewrite rules

parent e0a52cb1
......@@ -39,9 +39,7 @@ let rule_label = Ident.create_label "rewrite"
let collect_rule_decl prs e d =
match d.Decl.d_node with
| Decl.Dtype _ | Decl.Ddata _ | Decl.Dparam _ | Decl.Dind _
| Decl.Dlogic _ -> e
| Decl.Dprop(_, pr, t) ->
| Decl.Dprop((Plemma|Paxiom), pr, t) ->
if Decl.Spr.mem pr prs || Ident.Slab.mem rule_label t.t_label then
try add_rule t e
with NotARewriteRule msg ->
......@@ -49,6 +47,7 @@ let collect_rule_decl prs e d =
Pretty.print_pr pr msg;
e
else e
| _ -> e
let collect_rules p env km prs t =
Task.task_fold
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment