freescale porting, work in progress

[helm.git] / helm / software / matita / contribs / ng_assembly / num / oct_lemmas.ma

diff --git a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
index dc7e96f8909985aefaaf55e26058195590488a25..2d754d79937f7d57beb2539560c58312fbf4d5a0 100755 (executable)
--- a/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/num/oct_lemmas.ma
@@ -127,8 +127,8 @@ nlemma decidable_oct : ∀x,y:oct.decidable (x = y).
  nnormalize;
  nelim x;
  nelim y;
- ##[ ##1,10,19,28,37,46,55,64: napply (or_introl (? = ?) (? ≠ ?) …); napply refl_eq
- ##| ##*: napply (or_intror (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (oct_destruct … H)
+ ##[ ##1,10,19,28,37,46,55,64: napply (or2_intro1 (? = ?) (? ≠ ?) …); napply refl_eq
+ ##| ##*: napply (or2_intro2 (? = ?) (? ≠ ?) …); nnormalize; #H; napply False_ind; napply (oct_destruct … H)
  ##]
 nqed.