Commit 010f394c authored by Guillaume Melquiond's avatar Guillaume Melquiond

bugfix: compute also used goals as rewrite rules

parent 8f225f0d
......@@ -37,9 +37,7 @@ let meta_begin_compute_context =
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 then
try add_rule t e
with NotARewriteRule msg ->
......@@ -47,6 +45,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