diff options
Diffstat (limited to 'plugins/omega/coq_omega.ml')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f98aba0a8..0dd137b6f 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1254,7 +1254,7 @@ let replay_history tactic_normalisation = and id2 = hyp_of_tag e2.id in let eq1 = val_of(decompile e1) and eq2 = val_of(decompile e2) in - if k1 =? one & e2.kind = EQUA then + if k1 =? one && e2.kind = EQUA then let tac_thm = match e1.kind with | EQUA -> Lazy.force coq_OMEGA5 |