diff --git a/test/bugs/github1758.v b/test/bugs/github1758.v
new file mode 100644
index 00000000000..ac341eb1a6f
--- /dev/null
+++ b/test/bugs/github1758.v
@@ -0,0 +1,44 @@
+From HoTT Require Import Basics.Overture HIT.Interval HIT.Flattening Colimits.GraphQuotient
+          Spaces.Torus.Torus Cubical.
+
+(* Test that various higher inductive types are defined correctly.  If they are defined in the most naive way, two uses of the induction principle that are definitionally equal on the point constructors will be considered definitionally equal, which is inconsistent.  There is an idiom that must be used in order to force Coq to regard the supplementary data as being required as well.  See, for example, Colimits/GraphQuotient.v for the idiom. *)
+
+Fail Definition test_interval (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'
+  := 1.
+
+Fail Definition test_wtil {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))
+  (ppt'' : forall b y, (ppt b y) # (cct' (f b) y) = cct' (g b) (D b y))
+  : Wtil_ind Q cct' ppt' = Wtil_ind Q cct' ppt''
+  := 1.
+
+Section GraphQuotient_bug.
+  Local Definition R : Unit -> Unit -> Type := fun x y => Unit.
+
+  (* This should be the circle. *)
+  Local Definition Q := GraphQuotient R.
+
+  (* This is the identity map. *)
+  Local Definition id : Q -> Q := GraphQuotient_rec gq (fun a b r => gqglue r).
+
+  (* This is the constant map. *)
+  Local Definition cst : Q -> Q.
+  Proof.
+    refine (GraphQuotient_rec gq _).
+    intros [] [] r.
+    reflexivity.
+  Defined.
+
+  Fail Definition test_graphquotient : id = cst := 1.
+End GraphQuotient_bug.
+
+Fail Definition test_torus (P : Torus -> Type) (pb : P tbase)
+  (pla pla' : DPath P loop_a pb pb)
+  (plb : DPath P loop_b pb pb)
+  (ps : DPathSquare P surf pla pla plb plb)
+  (ps' : DPathSquare P surf pla' pla' plb plb)
+  : Torus_ind P pb pla plb ps = Torus_ind P pb pla' plb ps'
+  := 1.
diff --git a/theories/Colimits/GraphQuotient.v b/theories/Colimits/GraphQuotient.v
index 4a803b617b1..8f2f4c0023a 100644
--- a/theories/Colimits/GraphQuotient.v
+++ b/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}}
diff --git a/theories/HIT/Flattening.v b/theories/HIT/Flattening.v
index 253b88adc23..755148a531d 100644
--- a/theories/HIT/Flattening.v
+++ b/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)
diff --git a/theories/HIT/Interval.v b/theories/HIT/Interval.v
index 7efcac67c09..b58194bcce3 100644
--- a/theories/HIT/Interval.v
+++ b/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).
diff --git a/theories/HIT/README.txt b/theories/HIT/README.txt
index 136590493b8..13a4312ddbd 100644
--- a/theories/HIT/README.txt
+++ b/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.
diff --git a/theories/Spaces/Torus/Torus.v b/theories/Spaces/Torus/Torus.v
index 6bff6b6f02c..cefef2a26c4 100644
--- a/theories/Spaces/Torus/Torus.v
+++ b/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)