diff options
Diffstat (limited to 'contrib/rtauto')
| -rw-r--r-- | contrib/rtauto/Bintree.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/rtauto/Bintree.v b/contrib/rtauto/Bintree.v index d410606a74..cd0f1afe97 100644 --- a/contrib/rtauto/Bintree.v +++ b/contrib/rtauto/Bintree.v @@ -107,7 +107,7 @@ intro ne;right;congruence. left;reflexivity. Defined. -Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left (refl_equal m). +Theorem pos_eq_dec_refl : forall m, pos_eq_dec m m = left _ (refl_equal m). fix 1;intros [mm|mm|]. simpl; rewrite pos_eq_dec_refl; reflexivity. simpl; rewrite pos_eq_dec_refl; reflexivity. @@ -116,7 +116,7 @@ Qed. Theorem pos_eq_dec_ex : forall m n, pos_eq m n =true -> exists h:m=n, - pos_eq_dec m n = left h. + pos_eq_dec m n = left _ h. fix 1;intros [mm|mm|] [nn|nn|];try (simpl;congruence). simpl;intro e. elim (pos_eq_dec_ex _ _ e). |