X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fng_assembly%2Ffreescale%2Foption_lemmas.ma;h=9a81564fea2fb4b95869cdee43f6a4f1b70ccb69;hb=f538a0b46ba4164a21a76e47a6ed3b3e9deb5041;hp=c04bc9df094b61ec224db740d5d9fbcbd9e83188;hpb=96881c08dcd617524621fb2f241fe38da81f2083;p=helm.git

diff --git a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
index c04bc9df0..9a81564fe 100644
--- a/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
+++ b/helm/software/matita/contribs/ng_assembly/freescale/option_lemmas.ma
@@ -32,7 +32,7 @@ nlemma option_destruct_some_some : ∀T.∀x1,x2:T.Some T x1 = Some T x2 → x1
  nchange with (match Some T x2 with [ None ⇒ False | Some a ⇒ x1 = a ]);
  nrewrite < H;
  nnormalize;
- napply (refl_eq ??).
+ napply refl_eq.
 nqed.
 
 nlemma option_destruct_some_none : ∀T.∀x:T.Some T x = None T → False.
@@ -59,11 +59,11 @@ nlemma symmetric_eqoption :
  nelim op1;
  nelim op2;
  nnormalize;
- ##[ ##1: napply (refl_eq ??)
- ##| ##2,3: #H; napply (refl_eq ??)
+ ##[ ##1: napply refl_eq
+ ##| ##2,3: #H; napply refl_eq
  ##| ##4: #a; #a0;
           nrewrite > (H a0 a);
-          napply (refl_eq ??)
+          napply refl_eq
  ##]
 nqed.
 
@@ -75,13 +75,13 @@ nlemma eq_to_eqoption :
  nelim op1;
  nelim op2;
  nnormalize;
- ##[ ##1: #H1; napply (refl_eq ??)
+ ##[ ##1: #H1; napply refl_eq
  ##| ##2: #a; #H1; nelim (option_destruct_none_some ?? H1)
  ##| ##3: #a; #H1; nelim (option_destruct_some_none ?? H1)
  ##| ##4: #a; #a0; #H1;
-          nrewrite > (option_destruct_some_some ??? H1);
-          nrewrite > (H a a (refl_eq ??));
-          napply (refl_eq ??)
+          nrewrite > (option_destruct_some_some … H1);
+          nrewrite > (H a a (refl_eq …));
+          napply refl_eq
  ##]
 nqed.
 
@@ -93,10 +93,10 @@ nlemma eqoption_to_eq :
  nelim op1;
  nelim op2;
  nnormalize;
- ##[ ##1: #H1; napply (refl_eq ??)
- ##| ##2,3: #a; #H1; napply (bool_destruct ??? H1)
+ ##[ ##1: #H1; napply refl_eq
+ ##| ##2,3: #a; #H1; napply (bool_destruct … H1)
  ##| ##4: #a; #a0; #H1;
-          nrewrite > (H ?? H1);
-          napply (refl_eq ??)
+          nrewrite > (H … H1);
+          napply refl_eq
  ##]
 nqed.