A pass over all formatting, after big pile of coqdoc changes

src/Coinductive.v

@@ -50,7 +50,9 @@ Section stream.
 End stream.
 
 (* begin hide *)
+(* begin thide *)
 CoInductive evilStream := Nil.
+(* end thide *)
 (* end hide *)
 
 (** The definition is surprisingly simple.  Starting from the definition of [list], we just need to change the keyword [Inductive] to [CoInductive].  We could have left a [Nil] constructor in our definition, but we will leave it out to force all of our streams to be infinite.
@@ -105,7 +107,9 @@ Eval simpl in approx trues_falses 10.
 (* end thide *)
 
 (* begin hide *)
+(* begin thide *)
 Definition looper := 0.
+(* end thide *)
 (* end hide *)
 
 (** So far, it looks like co-inductive types might be a magic bullet, allowing us to import all of the Haskeller's usual tricks.  However, there are important restrictions that are dual to the restrictions on the use of inductive types.  Fixpoints _consume_ values of inductive types, with restrictions on which _arguments_ may be passed in recursive calls.  Dually, co-fixpoints _produce_ values of co-inductive types, with restrictions on what may be done with the _results_ of co-recursive calls.
@@ -139,7 +143,9 @@ Section map.
 End map.
 
 (* begin hide *)
+(* begin thide *)
 Definition filter := 0.
+(* end thide *)
 (* end hide *)
 
 (** This code is a literal copy of that for the list [map] function, with the [nil] case removed and [Fixpoint] changed to [CoFixpoint].  Many other standard functions on lazy data structures can be implemented just as easily.  Some, like [filter], cannot be implemented.  Since the predicate passed to [filter] may reject every element of the stream, we cannot satisfy the guardedness condition.
@@ -215,7 +221,9 @@ Definition ones' := map S zeroes.
 Theorem ones_eq : ones = ones'.
 
 (* begin hide *)
+(* begin thide *)
 Definition foo := @eq.
+(* end thide *)
 (* end hide *)
 
   (** However, faced with the initial subgoal, it is not at all clear how this theorem can be proved.  In fact, it is unprovable.  The [eq] predicate that we use is fundamentally limited to equalities that can be demonstrated by finite, syntactic arguments.  To prove this equivalence, we will need to introduce a new relation. *)

src/DataStruct.v

@@ -161,7 +161,9 @@ Eval simpl in get (Cons 0 (Cons 1 (Cons 2 Nil))) (Next (Next First)).
 (* end thide *)
 
 (* begin hide *)
+(* begin thide *)
 Definition map' := map.
+(* end thide *)
 (* end hide *)
 
 (** Our [get] function is also quite easy to reason about.  We show how with a short example about an analogue to the list [map] function. *)
@@ -237,7 +239,8 @@ Section hlist.
         match mem in member ls' return (match ls' with
                                           | nil => Empty_set
                                           | x' :: ls'' =>
-                                            B x' -> (member ls'' -> B elm) -> B elm
+                                            B x' -> (member ls'' -> B elm)
+                                            -> B elm
                                         end) with
           | MFirst _ => fun x _ => x
           | MNext _ _ mem' => fun _ get_mls' => get_mls' mem'
@@ -472,7 +475,9 @@ Section fhlist.
   (** By pattern-matching on the equality proof [pf], we make that equality known to the type-checker.  Exactly why this works can be seen by studying the definition of equality. *)
 
   (* begin hide *)
-  Definition foo := (@eq, @eq_refl).
+  (* begin thide *)
+  Definition foo := @eq_refl.
+  (* end thide *)
   (* end hide *)
 
   Print eq.

src/Equality.v

@@ -154,7 +154,9 @@ Fixpoint addLists' (ls1 ls2 : list nat) {struct ls2} : list nat :=
   end.
 
 (* begin hide *)
-Definition foo := @eq.
+(* begin thide *)
+Definition foo := (@eq, plus).
+(* end thide *)
 (* end hide *)
 
 Eval compute in fun ls => addLists' ls nil.
@@ -214,7 +216,9 @@ End fhlist.
 Implicit Arguments fhget [A B elm ls].
 
 (* begin hide *)
+(* begin thide *)
 Definition map := O.
+(* end thide *)
 (* end hide *)
 
 (** We can define a [map]-like function for [fhlist]s. *)
@@ -233,9 +237,11 @@ Section fhlist_map.
   Implicit Arguments fhmap [ls].
 
   (* begin hide *)
+  (* begin thide *)
   Definition ilist := O.
   Definition get := O.
   Definition imap := O.
+  (* end thide *)
   (* end hide *)
 
   (** For the inductive versions of the [ilist] definitions, we proved a lemma about the interaction of [get] and [imap].  It was a strategic choice not to attempt such a proof for the definitions that we just gave, because that sets us on a collision course with the problems that are the subject of this chapter. *)
@@ -369,7 +375,9 @@ User error: Cannot solve a second-order unification problem
   (** We can try to prove a lemma that would simplify proofs of many facts like [lemma2]: *)
 
   (* begin hide *)
+  (* begin thide *)
   Definition lemma3' := O.
+  (* end thide *)
   (* end hide *)
 
   Lemma lemma3 : forall (x : A) (pf : x = x), pf = eq_refl x.
@@ -428,7 +436,9 @@ x = eq_rect p Q x p h ]
       The axiom %\index{Gallina terms!eq\_rect\_eq}%[eq_rect_eq] states a "fact" that seems like common sense, once the notation is deciphered.  The term [eq_rect] is the automatically generated recursion principle for [eq].  Calling [eq_rect] is another way of [match]ing on an equality proof.  The proof we match on is the argument [h], and [x] is the body of the [match].  The statement of [eq_rect_eq] just says that [match]es on proofs of [p = p], for any [p], are superfluous and may be removed.  We can see this intuition better in code by asking Coq to simplify the theorem statement with the [compute] reduction strategy (which, by the way, applies all applicable rules of the definitional equality presented in this chapter's first section). *)
 
   (* begin hide *)
+  (* begin thide *)
   Definition False' := False.
+  (* end thide *)
   (* end hide *)
 
   Eval compute in (forall (U : Type) (p : U) (Q : U -> Type) (x : Q p) (h : p = p),
@@ -445,7 +455,9 @@ x = eq_rect p Q x p h ]
       This axiom is equivalent to another that is more commonly known and mentioned in type theory circles. *)
 
   (* begin hide *)
-  Definition Streicher_K' := (Streicher_K, UIP_refl__Streicher_K).
+  (* begin thide *)
+  Definition Streicher_K' := UIP_refl__Streicher_K.
+  (* end thide *)
   (* end hide *)
 
   Print Streicher_K.
@@ -462,7 +474,9 @@ fun U : Type => UIP_refl__Streicher_K U (UIP_refl U)
 End fhlist_map.
 
 (* begin hide *)
+(* begin thide *)
 Require Eqdep_dec.
+(* end thide *)
 (* end hide *)
 
 (** It is worth remarking that it is possible to avoid axioms altogether for equalities on types with decidable equality.  The [Eqdep_dec] module of the standard library contains a parametric proof of [UIP_refl] for such cases.  To simplify presentation, we will stick with the axiom version in the rest of this chapter. *)

src/GeneralRec.v

@@ -93,7 +93,9 @@ fun (A : Type) (R : A -> A -> Prop) => forall a : A, Acc R a
 The bulk of the definitional work devolves to the%\index{accessibility relation}\index{Gallina terms!Acc}% _accessibility_ relation [Acc], whose definition we may also examine. *)
 
 (* begin hide *)
+(* begin thide *)
 Definition Acc_intro' := Acc_intro.
+(* end thide *)
 (* end hide *)
 
   Print Acc.
@@ -752,7 +754,9 @@ Notation "x <- m1 ; m2" :=
   (TBind m1 (fun x => m2)) (right associativity, at level 70).
 
 (* begin hide *)
+(* begin thide *)
 Definition fib := pred.
+(* end thide *)
 (* end hide *)
 
 (** %\vspace{-.15in}%[[

src/Generic.v

@@ -361,7 +361,9 @@ Eval cbv beta iota delta -[append] in fun A (pr : A -> string) =>
      *)
 
 (* begin hide *)
+(* begin thide *)
 Definition append' := append.
+(* end thide *)
 (* end hide *)
 
 (** Some of these simplified terms seem overly complex because we have turned off simplification of calls to [append], which is what uses of the [++] operator desugar to.  Selective [++] simplification would combine adjacent string literals, yielding more or less the code we would write manually to implement this printing scheme. *)
@@ -647,7 +649,9 @@ Theorem map_id : forall T dt
   induction r; crush.
 
   (* begin hide *)
+  (* begin thide *)
   Definition pred' := pred.
+  (* end thide *)
   (* end hide *)
 
   (** The base case is discharged automatically, and the inductive case looks like this, where [H] is the outer IH (for induction over [T] values) and [IHn] is the inner IH (for induction over the recursive arguments).

src/InductiveTypes.v

@@ -711,9 +711,11 @@ Up to this point, we have seen how to encode in Coq more and more of what is pos
 
 Given our last example of an inductive type, many readers are probably eager to try encoding the syntax of %\index{lambda calculus}%lambda calculus.  Indeed, the function-based representation technique that we just used, called%\index{higher-order abstract syntax}\index{HOAS|see{higher-order abstract syntax}}% _higher-order abstract syntax_ (HOAS)%~\cite{HOAS}%, is the representation of choice for lambda calculi in %\index{Twelf}%Twelf and in many applications implemented in Haskell and ML.  Let us try to import that choice to Coq: *)
 (* begin hide *)
+(* begin thide *)
 Inductive term : Set := App | Abs.
 Reset term.
 Definition uhoh := O.
+(* end thide *)
 (* end hide *)
 (** [[
 Inductive term : Set :=
@@ -749,11 +751,8 @@ Nonetheless, the basic insight of HOAS is a very useful one, and there are ways
 
 (** As we have emphasized a few times already, Coq proofs are actually programs, written in the same language we have been using in our examples all along.  We can get a first sense of what this means by taking a look at the definitions of some of the %\index{induction principles}%induction principles we have used.  A close look at the details here will help us construct induction principles manually, which we will see is necessary for some more advanced inductive definitions. *)
 
-(* begin hide *)
 Print unit_ind.
-(* end hide *)
-(** %\noindent%[Print] [unit_ind.] *)
-(** [[
+(** %\vspace{-.15in}%[[
   unit_ind = 
   fun P : unit -> Prop => unit_rect P
      : forall P : unit -> Prop, P tt -> forall u : unit, P u
@@ -771,11 +770,8 @@ Check unit_rect.
 
 The principle [unit_rect] gives [P] type [unit -> Type] instead of [unit -> Prop].  [Type] is another universe, like [Set] and [Prop].  In fact, it is a common supertype of both.  Later on, we will discuss exactly what the significances of the different universes are.  For now, it is just important that we can use [Type] as a sort of meta-universe that may turn out to be either [Set] or [Prop].  We can see the symmetry inherent in the subtyping relationship by printing the definition of another principle that was generated for [unit] automatically: *)
 
-(* begin hide *)
 Print unit_rec.
-(* end hide *)
-(** %\noindent%[Print] [unit_rec.] *)
-(** [[
+(** %\vspace{-.15in}%[[
   unit_rec = 
   fun P : unit -> Set => unit_rect P
      : forall P : unit -> Set, P tt -> forall u : unit, P u
@@ -794,11 +790,8 @@ Definition always_O' (u : unit) : nat :=
 
 (** Going even further down the rabbit hole, [unit_rect] itself is not even a primitive.  It is a functional program that we can write manually. *)
 
-(* begin hide *)
 Print unit_rect.
-(* end hide *)
-(** %\noindent%[Print] [unit_rect.] *)
-(** [[
+(** %\vspace{-.15in}%[[
   unit_rect = 
   fun (P : unit -> Type) (f : P tt) (u : unit) =>
   match u as u0 return (P u0) with
@@ -820,7 +813,9 @@ Definition unit_rect' (P : unit -> Type) (f : P tt) (u : unit) :=
   end.
 
 (* begin hide *)
+(* begin thide *)
 Definition foo := nat_rect.
+(* end thide *)
 (* end hide *)
 
 (** We rely on Coq's heuristics for inferring [match] annotations, which are not consulted in the pretty-printing of terms.
@@ -1020,7 +1015,9 @@ Section nat_tree_ind'.
     All P ls -> P (NNode' n ls).
 
   (* begin hide *)
+  (* begin thide *)
   Definition list_nat_tree_ind := O.
+  (* end thide *)
   (* end hide *)
 
   (** A first attempt at writing the induction principle itself follows the intuition that nested inductive type definitions are expanded into mutual inductive definitions.

src/Intro.v

@@ -211,7 +211,9 @@ At the start of the next chapter, I assume that you have installed Coq and Proof
 The extra arguments demonstrated here are the proper choices for working with the code for this book.  The ellipses stand for other Emacs customization settings you may already have.  It can be helpful to save several alternate sets of flags in your <<.emacs>> file, with all but one commented out within the <<custom-set-variables>> block at any given time.
 
 Alternatively, Proof General configuration can be set on a per-directory basis, using a %\index{.dir-locals.el file@\texttt{.dir-locals.el} file}%<<.dir-locals.el>> file in the directory of the source files for which you want the settings to apply.  Here is an example that could be written in such a file to enable use of the book source.  Note the need to include an argument that starts Coq in Emacs support mode.
-%\begin{verbatim}%#<pre>#((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src")))))#</pre>#%\end{verbatim}%
+<<
+((coq-mode . ((coq-prog-args . ("-emacs-U" "-I" "DIR/src")))))
+>>
  #</li>#
 
 #</ol>#%\end{enumerate}%

src/Large.v

@@ -463,7 +463,9 @@ Theorem reassoc_correct : forall e, eval (reassoc e) = eval e.
   info t.
 
   (* begin hide *)
+  (* begin thide *)
   Definition eir := eq_ind_r.
+  (* end thide *)
   (* end hide *)
 
   (** %\vspace{-.15in}%[[
@@ -591,7 +593,9 @@ Finished transaction in 2. secs (1.264079u,0.s)
     debug eauto 6.
 
     (* begin hide *)
+    (* begin thide *)
     Definition deeeebug := (@eq_refl, @sym_eq).
+    (* end thide *)
     (* end hide *)
 
     (** The output is a large proof tree.  The beginning of the tree is enough to reveal what is happening:
@@ -755,6 +759,7 @@ Qed.
 (** * Build Processes *)
 
 (* begin hide *)
+(* begin thide *)
 Module Lib.
   Module A.
   End A.
@@ -769,6 +774,7 @@ Module Client.
   Module E.
   End E.
 End Client.
+(* end thide *)
 (* end hide *)
 
 (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries.  Coq and Proof General provide very good support for these activities.

src/LogicProg.v

@@ -77,7 +77,9 @@ Qed.
 (* end thide *)
 
 (* begin hide *)
+(* begin thide *)
 Definition er := @eq_refl.
+(* end thide *)
 (* end hide *)
 
 Print four_plus_three.
@@ -356,6 +358,12 @@ Finished transaction in 2. secs (1.92012u,0.044003s)
 
 (** We see worrying exponential growth in running time, and the %\index{tactics!debug}%[debug] tactical helps us see where [eauto] is wasting its time, outputting a trace of every proof step that is attempted.  The rule [eq_trans] applies at every node of a proof tree, and [eauto] tries all such positions. *)
 
+(* begin hide *)
+(* begin thide *)
+Definition syms := (eq_sym, plus_n_O, eq_add_S, f_equal2).
+(* end thide *)
+(* end hide *)
+
     debug eauto 3.
 (** [[
 1 depth=3 
@@ -403,7 +411,7 @@ This [eauto] fails to prove the goal, but it least it takes substantially less t
 Abort.
 (* end thide *)
 
-(** One simple example from before runs in the same amount of time, avoiding pollution by transivity. *)
+(** One simple example from before runs in the same amount of time, avoiding pollution by transitivity. *)
 
 Example seven_minus_three_again : exists x, x + 3 = 7.
 (* begin thide *)
@@ -510,7 +518,9 @@ Abort.
 (** We see that the two unification variables stand for the two elements of the list.  Indeed, list length is independent of data values.  Paradoxically, we can make the proof search process easier by constraining the list further, so that proof search naturally locates appropriate data elements by unification.  The library predicate [Forall] will be helpful. *)
 
 (* begin hide *)
+(* begin thide *)
 Definition Forall_c := (@Forall_nil, @Forall_cons).
+(* end thide *)
 (* end hide *)
 
 Print Forall.
@@ -532,7 +542,9 @@ Qed.
 (** We can see which list [eauto] found by printing the proof term. *)
 
 (* begin hide *)
+(* begin thide *)
 Definition conj' := (conj, le_n).
+(* end thide *)
 (* end hide *)
 
 Print length_is_2.
@@ -674,7 +686,9 @@ Qed.
 (* end thide *)
 
 (* begin hide *)
+(* begin thide *)
 Definition e1s := eval1'_subproof.
+(* end thide *)
 (* end hide *)
 
 Print eval1'.
@@ -812,7 +826,9 @@ Theorem bool_neq : true <> false.
 Abort.
 
 (* begin hide *)
+(* begin thide *)
 Definition boool := bool.
+(* end thide *)
 (* end hide *)
 
 (** It is hard to come up with a [bool]-specific hint that is not just a restatement of the theorem we mean to prove.  Luckily, a simpler form suffices, by appealing to the built-in tactic %\index{tactics!congruence}%[congruence], a complete procedure for the theory of equality, uninterpreted functions, and datatype constructors. *)
@@ -852,7 +868,9 @@ Section forall_and.
 End forall_and.
 
 (* begin hide *)
+(* begin thide *)
 Definition noot := (not, @eq).
+(* end thide *)
 (* end hide *)
 
 (** After our success on this example, we might get more ambitious and seek to generalize the hint to all possible predicates [P].

src/Match.v

@@ -402,7 +402,9 @@ Abort.
 (* EX: Write a list map function in Ltac. *)
 
 (* begin hide *)
+(* begin thide *)
 Definition mapp := (map, list).
+(* end thide *)
 (* end hide *)
 
 (** We can also use anonymous function expressions and local function definitions in Ltac, as this example of a standard list [map] function shows. *)

src/MoreDep.v

@@ -234,6 +234,12 @@ Fixpoint expDenote t (e : exp t) : typeDenote t :=
     | Snd _ _ e' => snd (expDenote e')
   end.
 
+(* begin hide *)
+(* begin thide *)
+Definition sumboool := sumbool.
+(* end thide *)
+(* end hide *)
+
 (** Despite the fancy type, the function definition is routine.  In fact, it is less complicated than what we would write in ML or Haskell 98, since we do not need to worry about pushing final values in and out of an algebraic datatype.  The only unusual thing is the use of an expression of the form [if E then true else false] in the [Eq] case.  Remember that [eq_nat_dec] has a rich dependent type, rather than a simple boolean type.  Coq's native [if] is overloaded to work on a test of any two-constructor type, so we can use [if] to build a simple boolean from the [sumbool] that [eq_nat_dec] returns.
 
    We can implement our old favorite, a constant folding function, and prove it correct.  It will be useful to write a function [pairOut] that checks if an [exp] of [Prod] type is a pair, returning its two components if so.  Unsurprisingly, a first attempt leads to a type error.
@@ -528,10 +534,6 @@ Section present.
     end.
 End present.
 
-(* begin hide *)
-Definition sigT' := sigT.
-(* end hide *)
-
 (** Insertion relies on two balancing operations.  It will be useful to give types to these operations using a relative of the subset types from last chapter.  While subset types let us pair a value with a proof about that value, here we want to pair a value with another non-proof dependently typed value.  The %\index{Gallina terms!sigT}%[sigT] type fills this role. *)
 
 Locate "{ _ : _ & _ }".

src/Reflection.v

@@ -58,7 +58,9 @@ Even_SS
     For this example, we begin by using a type from the [MoreSpecif] module (included in the book source) to write a certified evenness checker. *)
 
 (* begin hide *)
+(* begin thide *)
 Definition paartial := partial.
+(* end thide *)
 (* end hide *)
 
 Print partial.
@@ -161,7 +163,9 @@ Theorem true_galore : (True /\ True) -> (True \/ (True /\ (True -> True))).
 Qed.
 
 (* begin hide *)
+(* begin thide *)
 Definition tg := (and_ind, or_introl).
+(* end thide *)
 (* end hide *)
 
 Print true_galore.
@@ -560,7 +564,9 @@ Theorem mt2 : forall x y : nat, x = y --> x = y.
 Qed.
 
 (* begin hide *)
+(* begin thide *)
 Definition nvm := (Node_vm, Empty_vm, End_idx, Left_idx, Right_idx).
+(* end thide *)
 (* end hide *)
 
 Print mt2.
@@ -624,7 +630,9 @@ Theorem mt4' : True /\ True /\ True /\ True /\ True /\ True /\ False -> False.
 Qed.
 
 (* begin hide *)
+(* begin thide *)
 Definition fi := False_ind.
+(* end thide *)
 (* end hide *)
 
 Print mt4'.

src/Subset.v

@@ -29,10 +29,6 @@ Set Implicit Arguments.
 
 (** Let us consider several ways of implementing the natural number predecessor function.  We start by displaying the definition from the standard library: *)
 
-(* begin hide *)
-Definition foo := pred.
-(* end hide *)
-
 Print pred.
 (** %\vspace{-.15in}% [[
 pred = fun n : nat => match n with
@@ -147,7 +143,9 @@ let pred_strong1 = function
 We can reimplement our dependently typed [pred] based on%\index{subset types}% _subset types_, defined in the standard library with the type family %\index{Gallina terms!sig}%[sig]. *)
 
 (* begin hide *)
-Definition bar := (sig, ex).
+(* begin thide *)
+Definition bar := ex.
+(* end thide *)
 (* end hide *)
 
 Print sig.
@@ -219,7 +217,9 @@ Eval compute in pred_strong3 (exist _ 2 two_gt0).
      *)
 
 (* begin hide *)
+(* begin thide *)
 Definition pred_strong := 0.
+(* end thide *)
 (* end hide *)
 
 (** The function %\index{Gallina terms!proj1\_sig}%[proj1_sig] extracts the base value from a subset type.  It turns out that we need to include an explicit [return] clause here, since Coq's heuristics are not smart enough to propagate the result type that we wrote earlier.
@@ -386,10 +386,6 @@ In this case, we see that the new definition yields the same computational behav
 
 (** There is another type in the standard library which captures the idea of program values that indicate which of two propositions is true.%\index{Gallina terms!sumbool}% *)
 
-(* begin hide *)
-Definition baz := sumbool.
-(* end hide *)
-
 Print sumbool.
 (** %\vspace{-.15in}% [[
 Inductive sumbool (A : Prop) (B : Prop) : Set :=
@@ -607,10 +603,6 @@ Eval compute in pred_strong7 0.
 
      Because we used [maybe], one valid implementation of the type we gave [pred_strong7] would return [??] in every case.  We can strengthen the type to rule out such vacuous implementations, and the type family %\index{Gallina terms!sumor}%[sumor] from the standard library provides the easiest starting point.  For type [A] and proposition [B], [A + {B}] desugars to [sumor A B], whose values are either values of [A] or proofs of [B]. *)
 
-(* begin hide *)
-Definition sumor' := sumor.
-(* end hide *)
-
 Print sumor.
 (** %\vspace{-.15in}% [[
 Inductive sumor (A : Type) (B : Prop) : Type :=

src/Universes.v

@@ -272,8 +272,10 @@ The command outputs many more constraints, but we have collected only those that
 The next constraint, for [Top.15], is more complicated.  This is the universe of the second argument to the [Pair] constructor.  Not only must [Top.15] be less than [Top.8], but it also comes out that [Top.8] must be less than [Coq.Init.Datatypes.38].  What is this new universe variable?  It is from the definition of the [prod] inductive family, to which types of the form [A * B] are desugared. *)
 
 (* begin hide *)
+(* begin thide *)
 Inductive prod := pair.
 Reset prod.
+(* end thide *)
 (* end hide *)
 
 (** [[
@@ -477,7 +479,9 @@ Definition projS A (P : A -> Prop) (x : sig P) : A :=
   end.
 
 (* begin hide *)
+(* begin thide *)
 Definition projE := O.
+(* end thide *)
 (* end hide *)
 
 (** We run into trouble with a version that has been changed to work with [ex].
@@ -777,7 +781,9 @@ Corollary UIP : forall A (x y : A) (pf1 pf2 : x = y), pf1 = pf2.
 Qed.
 
 (* begin hide *)
+(* begin thide *)
 Require Eqdep_dec.
+(* end thide *)
 (* end hide *)
 
 (** These corollaries are special cases of proof irrelevance.  In developments that only need proof irrelevance for equality, there is no need to assert full irrelevance.
@@ -849,7 +855,9 @@ Check dependent_unique_choice.
   This axiom lets us convert a relational specification [R] into a function implementing that specification.  We need only prove that [R] is truly a function.  An alternate, stronger formulation applies to cases where [R] maps each input to one or more outputs.  We also simplify the statement of the theorem by considering only non-dependent function types. *)
 
 (* begin hide *)
+(* begin thide *)
 Require RelationalChoice.
+(* end thide *)
 (* end hide *)
 
 Require Import ClassicalChoice.
@@ -967,7 +975,9 @@ Qed.
 
 (* begin hide *)
 Require Import JMeq.
+(* begin thide *)
 Definition jme := (JMeq, JMeq_eq).
+(* end thide *)
 (* end hide *)
 
 Print Assumptions fin_cases.
@@ -1088,7 +1098,9 @@ Lemma proj1_again' : forall r, proof r
   injection H1; intros.
 
 (* begin hide *)
+(* begin thide *)
   Definition existT' := existT.
+(* end thide *)
 (* end hide *)
 
 (** Unfortunately, the "equality" that we expected between [p] and [p0] comes in a strange form: