Merge pull request idris-lang#3753 from justjoheinz/docs/fix_refl

Fix references to refl in misc reference

docs/reference/misc.rst

@@ -51,7 +51,7 @@ some constructors of proofs.
 
 ::
 
-    syntax Trivial = (| oh, refl |)
+    syntax Trivial = (| Oh, Refl |)
 
 
 Totality checking assertions
@@ -296,13 +296,13 @@ can be used in proofs, for example:
     -- Base case
     (Z + m = m + Z) <== plus_comm =
         rewrite ((m + Z = m) <== plusZeroRightNeutral) ==>
-                (Z + m = m) in refl
+                (Z + m = m) in Refl
 
     -- Step case
     (S k + m = m + S k) <== plus_comm =
         rewrite ((k + m = m + k) <== plus_comm) in
         rewrite ((S (m + k) = m + S k) <== plusSuccRightSucc) in
-            refl
+            Refl
 
 Reflection
 ==========

docs/tutorial/syntax.rst

@@ -74,14 +74,14 @@ bound is below the upper bound using ``so``:
 
     data Interval : Type where
        MkInterval : (lower : Double) -> (upper : Double) ->
-                    so (lower < upper) -> Interval
+                    So (lower < upper) -> Interval
 
-We can define a syntax which, in patterns, always matches ``oh`` for
+We can define a syntax which, in patterns, always matches ``Oh`` for
 the proof argument, and in terms requires a proof term to be provided:
 
 .. code-block:: idris
 
-    pattern syntax "[" [x] "..." [y] "]" = MkInterval x y oh
+    pattern syntax "[" [x] "..." [y] "]" = MkInterval x y Oh
     term    syntax "[" [x] "..." [y] "]" = MkInterval x y ?bounds_lemma
 
 In terms, the syntax ``[x...y]`` will generate a proof obligation