HITs: fix inconsistencies from several HITs

theories/Colimits/GraphQuotient.v

@@ -22,8 +22,8 @@ Module Export GraphQuotient.
     (gqglue' : forall a b (s : R a b), gqglue@{i j u} s # gq' a = gq' b)
     : forall x, P x := fun x =>
     match x with
-    | gq a => gq' a
-    end.
+    | gq a => fun _ => gq' a
+    end gqglue'.
 
   Axiom GraphQuotient_ind_beta_gqglue@{i j u k}
   : forall  {A : Type@{i}} {R : A -> A -> Type@{j}}

theories/HIT/Flattening.v

@@ -29,7 +29,7 @@ Definition Wtil_ind {A B f g C D} (Q : Wtil A B f g C D -> Type)
   (cct' : forall a x, Q (cct a x))
   (ppt' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
   : forall w, Q w
-  := fun w => match w with cct a x => cct' a x end.
+  := fun w => match w with cct a x => fun _ => cct' a x end ppt'.
 
 Axiom Wtil_ind_beta_ppt
   : forall {A B f g C D} (Q : Wtil A B f g C D -> Type)

theories/HIT/Interval.v

@@ -30,14 +30,6 @@ Axiom interval_ind_beta_seg : forall (P : interval -> Type)
 
 End Interval.
 
-(*   Should fail:
-Lemma test (P : interval -> Type) (a : P zero) (b : P one)
-      (p p' : seg # a = b) :
-    interval_ind P a b p = interval_ind P a b p'.
-reflexivity.
-*)
-
-
 Definition interval_rec (P : Type) (a b : P) (p : a = b)
   : interval -> P
   := interval_ind (fun _ => P) a b (transport_const _ _ @ p).

theories/HIT/README.txt

@@ -1,10 +1,5 @@
-The files in this directory require Yves Bertot's "private types"
-extension to Coq in order to implement higher inductive types (HITs).
-The "private types" extension is included in the stable branch of the
-HoTT/coq repository, so if you followed the INSTALL instructions you
-should be okay.
+The files in this directory use "private inductive types" in order to
+implement higher inductive types (HITs).
 
-The files which use HITs are currently segregated into this directory
-because the "private types" extension is a hack whose details may
-change in the future, and we are still hoping to one day have an
-actual implementation of HITs.
+Many of the files which use HITs are currently segregated into this
+directory, but they can also be found in other directories.

theories/Spaces/Torus/Torus.v

@@ -19,10 +19,8 @@ Module Export Torus.
   (* We define the induction principle for Torus *)
   Definition Torus_ind (P : Torus -> Type) (pb : P tbase)
     (pla : DPath P loop_a pb pb) (plb : DPath P loop_b pb pb)
-    (ps : DPathSquare P surf pla pla plb plb) (x : Torus) : P x.
-  Proof.
-    by destruct x.
-  Defined.
+    (ps : DPathSquare P surf pla pla plb plb) (x : Torus) : P x
+  := (match x with tbase => fun _ _ _ => pb end) pla plb ps.
 
   (* We declare propsitional computational rules for loop_a and loop_b *)
   Axiom Torus_ind_beta_loop_a : forall (P : Torus -> Type) (pb : P tbase)