diff options
Diffstat (limited to 'contrib/firstorder/rules.ml')
| -rw-r--r-- | contrib/firstorder/rules.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/contrib/firstorder/rules.ml b/contrib/firstorder/rules.ml index 91607ec40f..fc31ee6fc7 100644 --- a/contrib/firstorder/rules.ml +++ b/contrib/firstorder/rules.ml @@ -208,9 +208,8 @@ let defined_connectives=lazy all_occurrences,EvalConstRef (destConst (constant "iff"))] let normalize_evaluables= - onAllClauses + onAllHypsAndConcl (function None->unfold_in_concl (Lazy.force defined_connectives) - | Some ((_,id),_)-> - unfold_in_hyp (Lazy.force defined_connectives) - ((Rawterm.all_occurrences_expr,id),InHypTypeOnly)) + | Some id -> + unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)) |