Merge branch 'v8.5'

8 files changed, 1289 insertions, 16 deletions

diff --git a/Makefile.build b/Makefile.build
index ffac80cb8..f4319243c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -69,7 +69,7 @@ TIMED=          # non-empty will activate a default time command
 
 TIMECMD=	# if you prefer a specific time command instead of $(STDTIME)
                 # e.g. "'time -p'"
-CAMLFLAGS:=${CAMLFLAGS} -w -3
+
 # NB: if you want to collect compilation timings of .v and import them
 # in a spreadsheet, I suggest something like:
 #   make TIMED=1 2> timings.csv
diff --git a/lib/spawn.ml b/lib/spawn.ml
index 4d35ded90..fda4b4239 100644
--- a/lib/spawn.ml
+++ b/lib/spawn.ml
@@ -220,10 +220,13 @@ let stats { oob_req; oob_resp; alive } =
   input_value oob_resp
 
 let rec wait p =
-  try snd (Unix.waitpid [] p.pid)
-  with
-  | Unix.Unix_error (Unix.EINTR, _, _) -> wait p
-  | Unix.Unix_error _ -> Unix.WEXITED 0o400
+  (* On windows kill is not reliable, so wait may never return. *) 
+  if Sys.os_type = "Unix" then 
+    try snd (Unix.waitpid [] p.pid)
+    with
+    | Unix.Unix_error (Unix.EINTR, _, _) -> wait p
+    | Unix.Unix_error _ -> Unix.WEXITED 0o400
+  else Unix.WEXITED 0o400
 
 end
 
@@ -267,8 +270,13 @@ let stats { oob_req; oob_resp; alive } =
   flush oob_req;
   let RespStats g = input_value oob_resp in g
 
-let wait { pid = unixpid } =
-  try snd (Unix.waitpid [] unixpid)
-  with Unix.Unix_error _ -> Unix.WEXITED 0o400
+let rec wait p =
+  (* On windows kill is not reliable, so wait may never return. *) 
+  if Sys.os_type = "Unix" then 
+    try snd (Unix.waitpid [] p.pid)
+    with
+    | Unix.Unix_error (Unix.EINTR, _, _) -> wait p
+    | Unix.Unix_error _ -> Unix.WEXITED 0o400
+  else Unix.WEXITED 0o400
 
 end
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 98fd658f2..03a700e17 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -363,6 +363,22 @@ let set_no_delta_flags flags = {
   resolve_evars = flags.resolve_evars
 }
 
+(* For the first phase of keyed unification, restrict
+  to conversion (including beta-iota) only on closed terms *)
+let set_no_delta_open_core_flags flags = { flags with
+  modulo_delta = empty_transparent_state;
+  modulo_betaiota = false;
+}
+
+let set_no_delta_open_flags flags = {
+  core_unify_flags = set_no_delta_open_core_flags flags.core_unify_flags;
+  merge_unify_flags = set_no_delta_open_core_flags flags.merge_unify_flags;
+  subterm_unify_flags = set_no_delta_open_core_flags flags.subterm_unify_flags;
+  allow_K_in_toplevel_higher_order_unification =
+      flags.allow_K_in_toplevel_higher_order_unification;
+  resolve_evars = flags.resolve_evars
+}
+
 (* Default flag for the "simple apply" version of unification of a *)
 (* type against a type (e.g. apply) *)
 (* We set only the flags available at the time the new "apply" extended *)
@@ -1819,17 +1835,25 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
         let allow_K = flags.allow_K_in_toplevel_higher_order_unification in
         let flags =
           if occur_meta_or_existential op || !keyed_unification then
+	    (* This is up to delta for subterms w/o metas ... *)
             flags
           else
             (* up to Nov 2014, unification was bypassed on evar/meta-free terms;
                now it is called in a minimalistic way, at least to possibly
                unify pre-existing non frozen evars of the goal or of the
                pattern *)
-            set_no_delta_flags flags in
+          set_no_delta_flags flags in
+	let t' = (strip_outer_cast op,t) in
         let (evd',cl) =
           try
-	    (* This is up to delta for subterms w/o metas ... *)
-	    w_unify_to_subterm env evd ~flags (strip_outer_cast op,t)
+  	    if is_keyed_unification () then
+    	      try (* First try finding a subterm w/o conversion on open terms *)
+	        let flags = set_no_delta_open_flags flags in
+		w_unify_to_subterm env evd ~flags t'
+	      with e ->
+		(* If this fails, try with full conversion *)
+		w_unify_to_subterm env evd ~flags t'
+	    else w_unify_to_subterm env evd ~flags t'
 	  with PretypeError (env,_,NoOccurrenceFound _) when
               allow_K ||
                 (* w_unify_to_subterm does not go through evars, so
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 6c550e916..bc03baf26 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -230,7 +230,7 @@ let rewrite_keyed_core_unif_flags = {
     (* This is set dynamically *)
 
   restrict_conv_on_strict_subterms = false;
-  modulo_betaiota = false;
+  modulo_betaiota = true;
 
   modulo_eta = true;
 }
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
new file mode 100644
index 000000000..ae17fb145
--- /dev/null
+++ b/test-suite/bugs/closed/4533.v
@@ -0,0 +1,226 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_lex_wrong_rewrite_02") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 1125 lines to 
+346 lines, then from 360 lines to 346 lines, then from 822 lines to 271 lines, 
+then from 285 lines to 271 lines *)
+(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
+4.01.0
+   coqtop version 8.5 (January 2016) *)
+Inductive False := .
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Coq.Init.Datatypes.
+Import Coq.Init.Notations.
+Global Set Universe Polymorphism.
+Global Set Primitive Projections.
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Module Export Datatypes.
+  Set Implicit Arguments.
+  Notation nat := Coq.Init.Datatypes.nat.
+  Notation S := Coq.Init.Datatypes.S.
+  Record prod (A B : Type) := pair { fst : A ; snd : B }.
+  Notation "x * y" := (prod x y) : type_scope.
+  Delimit Scope nat_scope with nat.
+  Open Scope nat_scope.
+End Datatypes.
+Module Export Specif.
+  Set Implicit Arguments.
+  Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P 
+proj1_sig }.
+  Notation sigT := sig (only parsing).
+  Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+  Notation projT1 := proj1_sig (only parsing).
+  Notation projT2 := proj2_sig (only parsing).
+End Specif.
+Global Set Keyed Unification.
+Global Unset Strict Universe Declaration.
+Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in 
+Type@{i}.
+Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in
+                                        let ge := ((fun x => x) : Type1@{j} -> 
+Type@{i}) in Type@{i}.
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Open Scope fibration_scope.
+Open Scope function_scope.
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+Notation compose := (fun g f x => g (f x)).
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left 
+associativity) : function_scope.
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a.
+Arguments idpath {A a} , [A] a.
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+Notation "1" := idpath : path_scope.
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : 
+type_scope.
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+                                               equiv_inv : B -> A ;
+                                               eisretr : Sect equiv_inv f;
+                                               eissect : Sect f equiv_inv;
+                                               eisadj : forall x : A, eisretr 
+(f x) = ap f (eissect x)
+                                             }.
+Arguments eissect {A B}%type_scope f%function_scope {_} _.
+Inductive Unit : Type1 := tt : Unit.
+Local Open Scope path_scope.
+Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z 
+= t) :
+  p @ (q @ r) = (p @ q) @ r :=
+  match r with idpath =>
+               match q with idpath =>
+                            match p with idpath => 1
+                            end end end.
+Section Adjointify.
+  Context {A B : Type} (f : A -> B) (g : B -> A).
+  Context (isretr : Sect g f) (issect : Sect f g).
+  Let issect' := fun x =>
+                   ap g (ap f (issect x)^)  @  ap g (isretr (f x))  @  issect x.
+
+  Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a).
+    admit.
+  Defined.
+
+  Definition isequiv_adjointify : IsEquiv f
+    := BuildIsEquiv A B f g isretr issect' is_adjoint'.
+End Adjointify.
+Definition ExtensionAlong {A B : Type} (f : A -> B)
+           (P : B -> Type) (d : forall x:A, P (f x))
+  := { s : forall y:B, P y & forall x:A, s (f x) = d x }.
+Fixpoint ExtendableAlong@{i j k l}
+         (n : nat) {A : Type@{i}} {B : Type@{j}}
+         (f : A -> B) (C : B -> Type@{k}) : Type@{l}
+  := match n with
+     | 0 => Unit@{l}
+     | S n => (forall (g : forall a, C (f a)),
+                  ExtensionAlong@{i j k l l} f C g) *
+              forall (h k : forall b, C b),
+                ExtendableAlong n f (fun b => h b = k b)
+     end.
+
+Definition ooExtendableAlong@{i j k l}
+           {A : Type@{i}} {B : Type@{j}}
+           (f : A -> B) (C : B -> Type@{k}) : Type@{l}
+  := forall n, ExtendableAlong@{i j k l} n f C.
+
+Module Type ReflectiveSubuniverses.
+
+  Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}.
+
+  Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+      Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+      Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : 
+Type@{i}),
+      In@{u a i} O (O_reflector@{u a i} O T).
+
+  Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : 
+Type@{i}),
+      T -> O_reflector@{u a i} O T.
+
+  Parameter extendable_to_O@{u a i j k}
+    : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : 
+Type2le@{j a}} {Q_inO : In@{u a j} O Q},
+      ooExtendableAlong@{i i j k} (to O P) (fun _ => Q).
+
+End ReflectiveSubuniverses.
+
+Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses).
+  Export Os.
+  Existing Class In.
+  Module Export Coercions.
+    Coercion O_reflector : ReflectiveSubuniverse >-> Funclass.
+  End Coercions.
+  Global Existing Instance O_inO.
+
+  Section ORecursion.
+    Context {O : ReflectiveSubuniverse}.
+
+    Definition O_rec {P Q : Type} {Q_inO : In O Q}
+               (f : P -> Q)
+      : O P -> Q
+      := (fst (extendable_to_O O 1%nat) f).1.
+
+    Definition O_rec_beta {P Q : Type} {Q_inO : In O Q}
+               (f : P -> Q) (x : P)
+      : O_rec f (to O P x) = f x
+      := (fst (extendable_to_O O 1%nat) f).2 x.
+
+    Definition O_indpaths {P Q : Type} {Q_inO : In O Q}
+               (g h : O P -> Q) (p : g o to O P == h o to O P)
+      : g == h
+      := (fst (snd (extendable_to_O O 2) g h) p).1.
+
+  End ORecursion.
+
+
+  Section Reflective_Subuniverse.
+    Context (O : ReflectiveSubuniverse@{Ou Oa}).
+
+    Definition isequiv_to_O_inO@{u a i} (T : Type@{i}) `{In@{u a i} O T} : 
+IsEquiv@{i i} (to O T).
+    Proof.
+
+      pose (g := O_rec@{u a i i i i i} idmap).
+      refine (isequiv_adjointify (to O T) g _ _).
+      -
+        refine (O_indpaths@{u a i i i i i} (to O T o g) idmap _).
+        intros x.
+        apply ap.
+        apply O_rec_beta.
+      -
+        intros x.
+        apply O_rec_beta.
+    Defined.
+    Global Existing Instance isequiv_to_O_inO.
+
+  End Reflective_Subuniverse.
+
+End ReflectiveSubuniverses_Theory.
+
+Module Type Preserves_Fibers (Os : ReflectiveSubuniverses).
+  Module Export Os_Theory := ReflectiveSubuniverses_Theory Os.
+End Preserves_Fibers.
+
+Opaque eissect.
+Module Lex_Reflective_Subuniverses
+       (Os : ReflectiveSubuniverses) (Opf : Preserves_Fibers Os).
+  Import Opf.
+  Goal forall (O : ReflectiveSubuniverse) (A : Type) (B : A -> Type) (A_inO : 
+In O A),
+
+      forall g,
+      forall (x : O {x : A & B x}) v v' v'' (p2 : v'' = v') (p0 : v' = v) (p1 : 
+v = _) r,
+        (p2
+           @ (p0
+                @ p1))
+          @ eissect (to O A) (g x) = r.
+    intros.
+    cbv zeta.
+    rewrite concat_p_pp.
+    match goal with
+    | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
+    | [ |- ?G ] => fail 1 "bad" G
+    end.
+    Fail rewrite concat_p_pp.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
new file mode 100644
index 000000000..d14cc86fc
--- /dev/null
+++ b/test-suite/bugs/closed/4544.v
@@ -0,0 +1,1007 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-nois" "-indices-matter" "-R" "." "Top" "-top" "bug_oog_looping_rewrite_01") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
+(* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
+   coqtop version 8.5 (January 2016) *)
+Inductive False := .
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Coq.Init.Datatypes.
+
+Import Coq.Init.Notations.
+
+Global Set Universe Polymorphism.
+
+Notation "A -> B" := (forall (_ : A), B) : type_scope.
+Global Set Primitive Projections.
+
+Inductive sum (A B : Type) : Type :=
+  | inl : A -> sum A B
+  | inr : B -> sum A B.
+Notation nat := Coq.Init.Datatypes.nat.
+Notation S := Coq.Init.Datatypes.S.
+Notation "x + y" := (sum x y) : type_scope.
+
+Record prod (A B : Type) := pair { fst : A ; snd : B }.
+
+Notation "x * y" := (prod x y) : type_scope.
+Module Export Specif.
+
+Set Implicit Arguments.
+
+Record sig {A} (P : A -> Type) := exist { proj1_sig : A ; proj2_sig : P proj1_sig }.
+Arguments proj1_sig {A P} _ / .
+
+Notation sigT := sig (only parsing).
+Notation existT := exist (only parsing).
+
+Notation "{ x : A  & P }" := (sigT (fun x:A => P)) : type_scope.
+
+Notation projT1 := proj1_sig (only parsing).
+Notation projT2 := proj2_sig (only parsing).
+
+End Specif.
+Module Export HoTT_DOT_Basics_DOT_Overture.
+Module Export HoTT.
+Module Export Basics.
+Module Export Overture.
+
+Global Set Keyed Unification.
+
+Global Unset Strict Universe Declaration.
+
+Notation Type0 := Set.
+
+Definition Type1@{i} := Eval hnf in let gt := (Set : Type@{i}) in Type@{i}.
+
+Definition Type2@{i j} := Eval hnf in let gt := (Type1@{j} : Type@{i}) in Type@{i}.
+
+Definition Type2le@{i j} := Eval hnf in let gt := (Set : Type@{i}) in
+                                        let ge := ((fun x => x) : Type1@{j} -> Type@{i}) in Type@{i}.
+
+Notation idmap := (fun x => x).
+Delimit Scope function_scope with function.
+Delimit Scope path_scope with path.
+Delimit Scope fibration_scope with fibration.
+Delimit Scope trunc_scope with trunc.
+
+Open Scope trunc_scope.
+Open Scope path_scope.
+Open Scope fibration_scope.
+Open Scope nat_scope.
+Open Scope function_scope.
+
+Notation "( x ; y )" := (existT _ x y) : fibration_scope.
+
+Notation pr1 := projT1.
+Notation pr2 := projT2.
+
+Notation "x .1" := (pr1 x) (at level 3, format "x '.1'") : fibration_scope.
+Notation "x .2" := (pr2 x) (at level 3, format "x '.2'") : fibration_scope.
+
+Notation compose := (fun g f x => g (f x)).
+
+Notation "g 'o' f" := (compose g%function f%function) (at level 40, left associativity) : function_scope.
+
+Inductive paths {A : Type} (a : A) : A -> Type :=
+  idpath : paths a a.
+
+Arguments idpath {A a} , [A] a.
+
+Notation "x = y :> A" := (@paths A x y) : type_scope.
+Notation "x = y" := (x = y :>_) : type_scope.
+
+Definition inverse {A : Type} {x y : A} (p : x = y) : y = x
+  := match p with idpath => idpath end.
+
+Definition concat {A : Type} {x y z : A} (p : x = y) (q : y = z) : x = z :=
+  match p, q with idpath, idpath => idpath end.
+
+Notation "1" := idpath : path_scope.
+
+Notation "p @ q" := (concat p%path q%path) (at level 20) : path_scope.
+
+Notation "p ^" := (inverse p%path) (at level 3, format "p '^'") : path_scope.
+
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y :=
+  match p with idpath => u end.
+
+Notation "p # x" := (transport _ p x) (right associativity, at level 65, only parsing) : path_scope.
+
+Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y
+  := match p with idpath => idpath end.
+
+Definition pointwise_paths {A} {P:A->Type} (f g:forall x:A, P x)
+  := forall x:A, f x = g x.
+
+Notation "f == g" := (pointwise_paths f g) (at level 70, no associativity) : type_scope.
+
+Definition Sect {A B : Type} (s : A -> B) (r : B -> A) :=
+  forall x : A, r (s x) = x.
+
+Class IsEquiv {A B : Type} (f : A -> B) := BuildIsEquiv {
+  equiv_inv : B -> A ;
+  eisretr : Sect equiv_inv f;
+  eissect : Sect f equiv_inv;
+  eisadj : forall x : A, eisretr (f x) = ap f (eissect x)
+}.
+
+Arguments eisretr {A B}%type_scope f%function_scope {_} _.
+
+Record Equiv A B := BuildEquiv {
+  equiv_fun : A -> B ;
+  equiv_isequiv : IsEquiv equiv_fun
+}.
+
+Coercion equiv_fun : Equiv >-> Funclass.
+
+Global Existing Instance equiv_isequiv.
+
+Notation "A <~> B" := (Equiv A B) (at level 85) : type_scope.
+
+Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : function_scope.
+
+Class Contr_internal (A : Type) := BuildContr {
+  center : A ;
+  contr : (forall y : A, center = y)
+}.
+
+Arguments center A {_}.
+
+Inductive trunc_index : Type :=
+| minus_two : trunc_index
+| trunc_S : trunc_index -> trunc_index.
+
+Notation "n .+1" := (trunc_S n) (at level 2, left associativity, format "n .+1") : trunc_scope.
+Notation "-2" := minus_two (at level 0) : trunc_scope.
+Notation "-1" := (-2.+1) (at level 0) : trunc_scope.
+Notation "0" := (-1.+1) : trunc_scope.
+
+Fixpoint IsTrunc_internal (n : trunc_index) (A : Type) : Type :=
+  match n with
+    | -2 => Contr_internal A
+    | n'.+1 => forall (x y : A), IsTrunc_internal n' (x = y)
+  end.
+
+Class IsTrunc (n : trunc_index) (A : Type) : Type :=
+  Trunc_is_trunc : IsTrunc_internal n A.
+
+Global Instance istrunc_paths (A : Type) n `{H : IsTrunc n.+1 A} (x y : A)
+: IsTrunc n (x = y)
+  := H x y.
+
+Notation Contr := (IsTrunc -2).
+Notation IsHProp := (IsTrunc -1).
+
+Hint Extern 0 => progress change Contr_internal with Contr in * : typeclass_instances.
+
+Monomorphic Axiom dummy_funext_type : Type0.
+Monomorphic Class Funext := { dummy_funext_value : dummy_funext_type }.
+
+Inductive Unit : Type1 :=
+    tt : Unit.
+
+Class IsPointed (A : Type) := point : A.
+
+Arguments point A {_}.
+
+Record pType :=
+  { pointed_type : Type ;
+    ispointed_type : IsPointed pointed_type }.
+
+Coercion pointed_type : pType >-> Sortclass.
+
+Global Existing Instance ispointed_type.
+
+Definition hfiber {A B : Type} (f : A -> B) (y : B) := { x : A & f x = y }.
+
+Ltac revert_opaque x :=
+  revert x;
+  match goal with
+    | [ |- forall _, _ ] => idtac
+    | _ => fail 1 "Reverted constant is not an opaque variable"
+  end.
+
+End Overture.
+
+End Basics.
+
+End HoTT.
+
+End HoTT_DOT_Basics_DOT_Overture.
+Module Export HoTT_DOT_Basics_DOT_PathGroupoids.
+Module Export HoTT.
+Module Export Basics.
+Module Export PathGroupoids.
+
+Local Open Scope path_scope.
+
+Definition concat_p1 {A : Type} {x y : A} (p : x = y) :
+  p @ 1 = p
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_1p {A : Type} {x y : A} (p : x = y) :
+  1 @ p = p
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_p_pp {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+  p @ (q @ r) = (p @ q) @ r :=
+  match r with idpath =>
+    match q with idpath =>
+      match p with idpath => 1
+      end end end.
+
+Definition concat_pp_p {A : Type} {x y z t : A} (p : x = y) (q : y = z) (r : z = t) :
+  (p @ q) @ r = p @ (q @ r) :=
+  match r with idpath =>
+    match q with idpath =>
+      match p with idpath => 1
+      end end end.
+
+Definition concat_pV {A : Type} {x y : A} (p : x = y) :
+  p @ p^ = 1
+  :=
+  match p with idpath => 1 end.
+
+Definition moveR_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
+  p = r @ q -> r^ @ p = q.
+admit.
+Defined.
+
+Definition moveL_Vp {A : Type} {x y z : A} (p : x = z) (q : y = z) (r : x = y) :
+  r @ q = p -> q = r^ @ p.
+admit.
+Defined.
+
+Definition moveR_M1 {A : Type} {x y : A} (p q : x = y) :
+  1 = p^ @ q -> p = q.
+admit.
+Defined.
+
+Definition ap_pp {A B : Type} (f : A -> B) {x y z : A} (p : x = y) (q : y = z) :
+  ap f (p @ q) = (ap f p) @ (ap f q)
+  :=
+  match q with
+    idpath =>
+    match p with idpath => 1 end
+  end.
+
+Definition ap_V {A B : Type} (f : A -> B) {x y : A} (p : x = y) :
+  ap f (p^) = (ap f p)^
+  :=
+  match p with idpath => 1 end.
+
+Definition ap_compose {A B C : Type} (f : A -> B) (g : B -> C) {x y : A} (p : x = y) :
+  ap (g o f) p = ap g (ap f p)
+  :=
+  match p with idpath => 1 end.
+
+Definition concat_pA1 {A : Type} {f : A -> A} (p : forall x, x = f x) {x y : A} (q : x = y) :
+  (p x) @ (ap f q) =  q @ (p y)
+  :=
+  match q as i in (_ = y) return (p x @ ap f i = i @ p y) with
+    | idpath => concat_p1 _ @ (concat_1p _)^
+  end.
+
+End PathGroupoids.
+
+End Basics.
+
+End HoTT.
+
+End HoTT_DOT_Basics_DOT_PathGroupoids.
+Module Export HoTT_DOT_Basics_DOT_Equivalences.
+Module Export HoTT.
+Module Export Basics.
+Module Export Equivalences.
+
+Definition isequiv_commsq {A B C D}
+           (f : A -> B) (g : C -> D) (h : A -> C) (k : B -> D)
+           (p : k o f == g o h)
+           `{IsEquiv _ _ f} `{IsEquiv _ _ h} `{IsEquiv _ _ k}
+: IsEquiv g.
+admit.
+Defined.
+
+Section Adjointify.
+
+  Context {A B : Type} (f : A -> B) (g : B -> A).
+  Context (isretr : Sect g f) (issect : Sect f g).
+
+  Let issect' := fun x =>
+    ap g (ap f (issect x)^)  @  ap g (isretr (f x))  @  issect x.
+
+  Let is_adjoint' (a : A) : isretr (f a) = ap f (issect' a).
+  Proof.
+    unfold issect'.
+    apply moveR_M1.
+    repeat rewrite ap_pp, concat_p_pp; rewrite <- ap_compose.
+    rewrite (concat_pA1 (fun b => (isretr b)^) (ap f (issect a)^)).
+    repeat rewrite concat_pp_p; rewrite ap_V; apply moveL_Vp; rewrite concat_p1.
+    rewrite concat_p_pp, <- ap_compose.
+    rewrite (concat_pA1 (fun b => (isretr b)^) (isretr (f a))).
+    rewrite concat_pV, concat_1p; reflexivity.
+  Qed.
+
+  Definition isequiv_adjointify : IsEquiv f
+    := BuildIsEquiv A B f g isretr issect' is_adjoint'.
+
+End Adjointify.
+
+End Equivalences.
+
+End Basics.
+
+End HoTT.
+
+End HoTT_DOT_Basics_DOT_Equivalences.
+Module Export HoTT_DOT_Basics_DOT_Trunc.
+Module Export HoTT.
+Module Export Basics.
+Module Export Trunc.
+Generalizable Variables A B m n f.
+
+Definition trunc_equiv A {B} (f : A -> B)
+  `{IsTrunc n A} `{IsEquiv A B f}
+  : IsTrunc n B.
+admit.
+Defined.
+
+Record TruncType (n : trunc_index) := BuildTruncType {
+  trunctype_type : Type ;
+  istrunc_trunctype_type : IsTrunc n trunctype_type
+}.
+
+Arguments BuildTruncType _ _ {_}.
+
+Coercion trunctype_type : TruncType >-> Sortclass.
+
+Notation "n -Type" := (TruncType n) (at level 1) : type_scope.
+Notation hProp := (-1)-Type.
+
+Notation BuildhProp := (BuildTruncType -1).
+
+End Trunc.
+
+End Basics.
+
+End HoTT.
+
+End HoTT_DOT_Basics_DOT_Trunc.
+Module Export HoTT_DOT_Types_DOT_Unit.
+Module Export HoTT.
+Module Export Types.
+Module Export Unit.
+
+Notation unit_name x := (fun (_ : Unit) => x).
+
+End Unit.
+
+End Types.
+
+End HoTT.
+
+End HoTT_DOT_Types_DOT_Unit.
+Module Export HoTT_DOT_Types_DOT_Sigma.
+Module Export HoTT.
+Module Export Types.
+Module Export Sigma.
+Local Open Scope path_scope.
+
+Definition path_sigma_uncurried {A : Type} (P : A -> Type) (u v : sigT P)
+           (pq : {p : u.1 = v.1 & p # u.2 = v.2})
+: u = v
+  := match pq.2 in (_ = v2) return u = (v.1; v2) with
+       | 1 => match pq.1 as p in (_ = v1) return u = (v1; p # u.2) with
+                | 1 => 1
+              end
+     end.
+
+Definition path_sigma {A : Type} (P : A -> Type) (u v : sigT P)
+           (p : u.1 = v.1) (q : p # u.2 = v.2)
+: u = v
+  := path_sigma_uncurried P u v (p;q).
+
+Definition path_sigma' {A : Type} (P : A -> Type) {x x' : A} {y : P x} {y' : P x'}
+           (p : x = x') (q : p # y = y')
+: (x;y) = (x';y')
+  := path_sigma P (x;y) (x';y') p q.
+
+Global Instance isequiv_pr1_contr {A} {P : A -> Type}
+         `{forall a, Contr (P a)}
+: IsEquiv (@pr1 A P) | 100.
+Proof.
+  refine (isequiv_adjointify (@pr1 A P)
+                             (fun a => (a ; center (P a))) _ _).
+  -
+ intros a; reflexivity.
+  -
+ intros [a p].
+    refine (path_sigma' P 1 (contr _)).
+Defined.
+
+Definition path_sigma_hprop {A : Type} {P : A -> Type}
+           `{forall x, IsHProp (P x)}
+           (u v : sigT P)
+: u.1 = v.1 -> u = v
+  := path_sigma_uncurried P u v o pr1^-1.
+
+End Sigma.
+
+End Types.
+
+End HoTT.
+
+End HoTT_DOT_Types_DOT_Sigma.
+Module Export HoTT_DOT_Extensions.
+Module Export HoTT.
+Module Export Extensions.
+
+Section Extensions.
+
+  Definition ExtensionAlong {A B : Type} (f : A -> B)
+             (P : B -> Type) (d : forall x:A, P (f x))
+    := { s : forall y:B, P y & forall x:A, s (f x) = d x }.
+
+  Fixpoint ExtendableAlong@{i j k l}
+           (n : nat) {A : Type@{i}} {B : Type@{j}}
+           (f : A -> B) (C : B -> Type@{k}) : Type@{l}
+    := match n with
+         | 0 => Unit@{l}
+         | S n => (forall (g : forall a, C (f a)),
+                     ExtensionAlong@{i j k l l} f C g) *
+                  forall (h k : forall b, C b),
+                    ExtendableAlong n f (fun b => h b = k b)
+       end.
+
+  Definition ooExtendableAlong@{i j k l}
+             {A : Type@{i}} {B : Type@{j}}
+             (f : A -> B) (C : B -> Type@{k}) : Type@{l}
+    := forall n, ExtendableAlong@{i j k l} n f C.
+
+End Extensions.
+
+End Extensions.
+
+End HoTT.
+
+End HoTT_DOT_Extensions.
+Module Export HoTT.
+Module Export Modalities.
+Module Export ReflectiveSubuniverse.
+
+Module Type ReflectiveSubuniverses.
+
+  Parameter ReflectiveSubuniverse@{u a} : Type2@{u a}.
+
+  Parameter O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                            Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                   Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
+                               In@{u a i} O (O_reflector@{u a i} O T).
+
+  Parameter to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
+                   T -> O_reflector@{u a i} O T.
+
+  Parameter inO_equiv_inO@{u a i j k} :
+      forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j})
+             (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
+
+        let gei := ((fun x => x) : Type@{i} -> Type@{k}) in
+        let gej := ((fun x => x) : Type@{j} -> Type@{k}) in
+        In@{u a j} O U.
+
+  Parameter hprop_inO@{u a i}
+  : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
+                IsHProp (In@{u a i} O T).
+
+  Parameter extendable_to_O@{u a i j k}
+  : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q},
+      ooExtendableAlong@{i i j k} (to O P) (fun _ => Q).
+
+End ReflectiveSubuniverses.
+
+Module ReflectiveSubuniverses_Theory (Os : ReflectiveSubuniverses).
+Export Os.
+
+Module Export Coercions.
+
+  Coercion O_reflector : ReflectiveSubuniverse >-> Funclass.
+
+End Coercions.
+
+End ReflectiveSubuniverses_Theory.
+
+Module Type ReflectiveSubuniverses_Restriction_Data (Os : ReflectiveSubuniverses).
+
+  Parameter New_ReflectiveSubuniverse@{u a} : Type2@{u a}.
+
+  Parameter ReflectiveSubuniverses_restriction@{u a}
+  : New_ReflectiveSubuniverse@{u a} -> Os.ReflectiveSubuniverse@{u a}.
+
+End ReflectiveSubuniverses_Restriction_Data.
+
+Module ReflectiveSubuniverses_Restriction
+       (Os : ReflectiveSubuniverses)
+       (Res : ReflectiveSubuniverses_Restriction_Data Os)
+<: ReflectiveSubuniverses.
+
+  Definition ReflectiveSubuniverse := Res.New_ReflectiveSubuniverse.
+
+  Definition O_reflector@{u a i} (O : ReflectiveSubuniverse@{u a})
+    := Os.O_reflector@{u a i} (Res.ReflectiveSubuniverses_restriction O).
+  Definition In@{u a i} (O : ReflectiveSubuniverse@{u a})
+    := Os.In@{u a i} (Res.ReflectiveSubuniverses_restriction O).
+  Definition O_inO@{u a i} (O : ReflectiveSubuniverse@{u a})
+    := Os.O_inO@{u a i} (Res.ReflectiveSubuniverses_restriction O).
+  Definition to@{u a i} (O : ReflectiveSubuniverse@{u a})
+    := Os.to@{u a i} (Res.ReflectiveSubuniverses_restriction O).
+  Definition inO_equiv_inO@{u a i j k} (O : ReflectiveSubuniverse@{u a})
+    := Os.inO_equiv_inO@{u a i j k} (Res.ReflectiveSubuniverses_restriction O).
+  Definition hprop_inO@{u a i} (H : Funext) (O : ReflectiveSubuniverse@{u a})
+    := Os.hprop_inO@{u a i} H (Res.ReflectiveSubuniverses_restriction O).
+  Definition extendable_to_O@{u a i j k} (O : ReflectiveSubuniverse@{u a})
+    := @Os.extendable_to_O@{u a i j k} (Res.ReflectiveSubuniverses_restriction@{u a} O).
+
+End ReflectiveSubuniverses_Restriction.
+
+Module ReflectiveSubuniverses_FamUnion
+       (Os1 Os2 : ReflectiveSubuniverses)
+<: ReflectiveSubuniverses.
+
+  Definition ReflectiveSubuniverse@{u a} : Type2@{u a}
+    := Os1.ReflectiveSubuniverse@{u a} + Os2.ReflectiveSubuniverse@{u a}.
+
+  Definition O_reflector@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                             Type2le@{i a} -> Type2le@{i a}.
+admit.
+Defined.
+
+  Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                             Type2le@{i a} -> Type2le@{i a}.
+  Proof.
+    intros [O|O]; [ exact (Os1.In@{u a i} O)
+                  | exact (Os2.In@{u a i} O) ].
+  Defined.
+
+  Definition O_inO@{u a i}
+  : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
+      In@{u a i} O (O_reflector@{u a i} O T).
+admit.
+Defined.
+
+  Definition to@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
+                   T -> O_reflector@{u a i} O T.
+admit.
+Defined.
+
+  Definition inO_equiv_inO@{u a i j k} :
+      forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j})
+             (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
+        In@{u a j} O U.
+  Proof.
+    intros [O|O]; [ exact (Os1.inO_equiv_inO@{u a i j k} O)
+                  | exact (Os2.inO_equiv_inO@{u a i j k} O) ].
+  Defined.
+
+  Definition hprop_inO@{u a i}
+  : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
+                IsHProp (In@{u a i} O T).
+admit.
+Defined.
+
+  Definition extendable_to_O@{u a i j k}
+  : forall (O : ReflectiveSubuniverse@{u a}) {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q},
+      ooExtendableAlong@{i i j k} (to O P) (fun _ => Q).
+admit.
+Defined.
+
+End ReflectiveSubuniverses_FamUnion.
+
+End ReflectiveSubuniverse.
+
+End Modalities.
+
+End HoTT.
+
+Module Type Modalities.
+
+  Parameter Modality@{u a} : Type2@{u a}.
+
+  Parameter O_reflector@{u a i} : forall (O : Modality@{u a}),
+                            Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter In@{u a i} : forall (O : Modality@{u a}),
+                            Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter O_inO@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}),
+                               In@{u a i} O (O_reflector@{u a i} O T).
+
+  Parameter to@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}),
+                   T -> O_reflector@{u a i} O T.
+
+  Parameter inO_equiv_inO@{u a i j k} :
+      forall (O : Modality@{u a}) (T : Type@{i}) (U : Type@{j})
+             (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
+
+        let gei := ((fun x => x) : Type@{i} -> Type@{k}) in
+        let gej := ((fun x => x) : Type@{j} -> Type@{k}) in
+        In@{u a j} O U.
+
+  Parameter hprop_inO@{u a i}
+  : Funext -> forall (O : Modality@{u a}) (T : Type@{i}),
+                IsHProp (In@{u a i} O T).
+
+End Modalities.
+
+Module Modalities_to_ReflectiveSubuniverses
+       (Os : Modalities) <: ReflectiveSubuniverses.
+
+  Import Os.
+
+  Fixpoint O_extendable@{u a i j k} (O : Modality@{u a})
+           (A : Type@{i}) (B : O_reflector O A -> Type@{j})
+           (B_inO : forall a, In@{u a j} O (B a)) (n : nat)
+  : ExtendableAlong@{i i j k} n (to O A) B.
+admit.
+Defined.
+
+  Definition ReflectiveSubuniverse := Modality.
+
+  Definition O_reflector := O_reflector.
+
+  Definition In@{u a i} : forall (O : ReflectiveSubuniverse@{u a}),
+                   Type2le@{i a} -> Type2le@{i a}
+    := In@{u a i}.
+  Definition O_inO@{u a i} : forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
+                               In@{u a i} O (O_reflector@{u a i} O T)
+    := O_inO@{u a i}.
+  Definition to := to.
+  Definition inO_equiv_inO@{u a i j k} :
+      forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}) (U : Type@{j})
+             (T_inO : In@{u a i} O T) (f : T -> U) (feq : IsEquiv f),
+        In@{u a j} O U
+    := inO_equiv_inO@{u a i j k}.
+  Definition hprop_inO@{u a i}
+  : Funext -> forall (O : ReflectiveSubuniverse@{u a}) (T : Type@{i}),
+                IsHProp (In@{u a i} O T)
+    := hprop_inO@{u a i}.
+
+  Definition extendable_to_O@{u a i j k} (O : ReflectiveSubuniverse@{u a})
+             {P : Type2le@{i a}} {Q : Type2le@{j a}} {Q_inO : In@{u a j} O Q}
+  : ooExtendableAlong@{i i j k} (to O P) (fun _ => Q)
+    := fun n => O_extendable O P (fun _ => Q) (fun _ => Q_inO) n.
+
+End Modalities_to_ReflectiveSubuniverses.
+
+Module Type EasyModalities.
+
+  Parameter Modality@{u a} : Type2@{u a}.
+
+  Parameter O_reflector@{u a i} : forall (O : Modality@{u a}),
+                            Type2le@{i a} -> Type2le@{i a}.
+
+  Parameter to@{u a i} : forall (O : Modality@{u a}) (T : Type@{i}),
+                   T -> O_reflector@{u a i} O T.
+
+  Parameter minO_pathsO@{u a i}
+  : forall (O : Modality@{u a}) (A : Type@{i})
+           (z z' : O_reflector@{u a i} O A),
+      IsEquiv (to@{u a i} O (z = z')).
+
+End EasyModalities.
+
+Module EasyModalities_to_Modalities (Os : EasyModalities)
+<: Modalities.
+
+  Import Os.
+
+  Definition Modality := Modality.
+
+  Definition O_reflector@{u a i} := O_reflector@{u a i}.
+  Definition to@{u a i} := to@{u a i}.
+
+  Definition In@{u a i}
+  : forall (O : Modality@{u a}), Type@{i} -> Type@{i}
+  := fun O A => IsEquiv@{i i} (to O A).
+
+  Definition hprop_inO@{u a i} `{Funext} (O : Modality@{u a})
+             (T : Type@{i})
+  : IsHProp (In@{u a i} O T).
+admit.
+Defined.
+
+  Definition O_ind_internal@{u a i j k} (O : Modality@{u a})
+             (A : Type@{i}) (B : O_reflector@{u a i} O A -> Type@{j})
+             (B_inO : forall oa, In@{u a j} O (B oa))
+  : let gei := ((fun x => x) : Type@{i} -> Type@{k}) in
+    let gej := ((fun x => x) : Type@{j} -> Type@{k}) in
+    (forall a, B (to O A a)) -> forall oa, B oa.
+admit.
+Defined.
+
+  Definition O_ind_beta_internal@{u a i j k} (O : Modality@{u a})
+             (A : Type@{i}) (B : O_reflector@{u a i} O A -> Type@{j})
+             (B_inO : forall oa, In@{u a j} O (B oa))
+             (f : forall a : A, B (to O A a)) (a:A)
+  : O_ind_internal@{u a i j k} O A B B_inO f (to O A a) = f a.
+admit.
+Defined.
+
+  Definition O_inO@{u a i} (O : Modality@{u a}) (A : Type@{i})
+  : In@{u a i} O (O_reflector@{u a i} O A).
+admit.
+Defined.
+
+  Definition inO_equiv_inO@{u a i j k} (O : Modality@{u a}) (A : Type@{i}) (B : Type@{j})
+    (A_inO : In@{u a i} O A) (f : A -> B) (feq : IsEquiv f)
+  : In@{u a j} O B.
+  Proof.
+    simple refine (isequiv_commsq (to O A) (to O B) f
+             (O_ind_internal O A (fun _ => O_reflector O B) _ (fun a => to O B (f a))) _).
+    -
+ intros; apply O_inO.
+    -
+ intros a; refine (O_ind_beta_internal@{u a i j k} O A (fun _ => O_reflector O B) _ _ a).
+    -
+ apply A_inO.
+    -
+ simple refine (isequiv_adjointify _
+               (O_ind_internal O B (fun _ => O_reflector O A) _ (fun b => to O A (f^-1 b))) _ _);
+        intros x.
+      +
+ apply O_inO.
+      +
+ pattern x; refine (O_ind_internal O B _ _ _ x); intros.
+        *
+ apply minO_pathsO.
+        *
+ simpl; admit.
+      +
+ pattern x; refine (O_ind_internal O A _ _ _ x); intros.
+        *
+ apply minO_pathsO.
+        *
+ simpl; admit.
+  Defined.
+
+End EasyModalities_to_Modalities.
+
+Module Modalities_Theory (Os : Modalities).
+
+Export Os.
+Module Export Os_ReflectiveSubuniverses
+  := Modalities_to_ReflectiveSubuniverses Os.
+Module Export RSU
+  := ReflectiveSubuniverses_Theory Os_ReflectiveSubuniverses.
+
+Module Export Coercions.
+  Coercion modality_to_reflective_subuniverse
+    := idmap : Modality -> ReflectiveSubuniverse.
+End Coercions.
+
+Class IsConnected (O : Modality@{u a}) (A : Type@{i})
+
+  := isconnected_contr_O : IsTrunc@{i} -2 (O A).
+
+Class IsConnMap (O : Modality@{u a})
+      {A : Type@{i}} {B : Type@{j}} (f : A -> B)
+  := isconnected_hfiber_conn_map
+
+     : forall b:B, IsConnected@{u a k} O (hfiber@{i j} f b).
+
+End Modalities_Theory.
+
+Private Inductive Trunc (n : trunc_index) (A :Type) : Type :=
+  tr : A -> Trunc n A.
+Arguments tr {n A} a.
+
+Global Instance istrunc_truncation (n : trunc_index) (A : Type@{i})
+: IsTrunc@{j} n (Trunc@{i} n A).
+Admitted.
+
+Definition Trunc_ind {n A}
+  (P : Trunc n A -> Type) {Pt : forall aa, IsTrunc n (P aa)}
+  : (forall a, P (tr a)) -> (forall aa, P aa)
+:= (fun f aa => match aa with tr a => fun _ => f a end Pt).
+
+Definition Truncation_Modality := trunc_index.
+
+Module Truncation_Modalities <: Modalities.
+
+  Definition Modality : Type2@{u a} := Truncation_Modality.
+
+  Definition O_reflector (n : Modality@{u u'}) A := Trunc n A.
+
+  Definition In (n : Modality@{u u'}) A := IsTrunc n A.
+
+  Definition O_inO (n : Modality@{u u'}) A : In n (O_reflector n A).
+admit.
+Defined.
+
+  Definition to (n : Modality@{u u'}) A := @tr n A.
+
+  Definition inO_equiv_inO (n : Modality@{u u'})
+             (A : Type@{i}) (B : Type@{j}) Atr f feq
+  : let gei := ((fun x => x) : Type@{i} -> Type@{k}) in
+    let gej := ((fun x => x) : Type@{j} -> Type@{k}) in
+    In n B
+  := @trunc_equiv A B f n Atr feq.
+
+  Definition hprop_inO `{Funext} (n : Modality@{u u'}) A
+  : IsHProp (In n A).
+admit.
+Defined.
+
+End Truncation_Modalities.
+
+Module Import TrM := Modalities_Theory Truncation_Modalities.
+
+Definition merely (A : Type@{i}) : hProp@{i} := BuildhProp (Trunc -1 A).
+
+Notation IsSurjection := (IsConnMap -1).
+
+Definition BuildIsSurjection {A B} (f : A -> B) :
+  (forall b, merely (hfiber f b)) -> IsSurjection f.
+admit.
+Defined.
+
+Ltac strip_truncations :=
+
+  progress repeat match goal with
+                    | [ T : _ |- _ ]
+                      => revert_opaque T;
+                        refine (@Trunc_ind _ _ _ _ _);
+
+                        [];
+                        intro T
+                  end.
+Local Open Scope trunc_scope.
+
+Global Instance conn_pointed_type {n : trunc_index} {A : Type} (a0:A)
+ `{IsConnMap n _ _ (unit_name a0)} : IsConnected n.+1 A | 1000.
+admit.
+Defined.
+
+Definition loops (A : pType) : pType :=
+  Build_pType (point A = point A) idpath.
+
+Record pMap (A B : pType) :=
+  { pointed_fun : A -> B ;
+    point_eq : pointed_fun (point A) = point B }.
+
+Arguments point_eq {A B} f : rename.
+Coercion pointed_fun : pMap >-> Funclass.
+
+Infix "->*" := pMap (at level 99) : pointed_scope.
+Local Open Scope pointed_scope.
+
+Definition pmap_compose {A B C : pType}
+           (g : B ->* C) (f : A ->* B)
+: A ->* C
+  := Build_pMap A C (g o f)
+                (ap g (point_eq f) @ point_eq g).
+
+Record pHomotopy {A B : pType} (f g : pMap A B) :=
+  { pointed_htpy : f == g ;
+    point_htpy : pointed_htpy (point A) @ point_eq g = point_eq f }.
+Arguments pointed_htpy {A B f g} p x.
+
+Infix "==*" := pHomotopy (at level 70, no associativity) : pointed_scope.
+
+Definition loops_functor {A B : pType} (f : A ->* B)
+: (loops A) ->* (loops B).
+Proof.
+  refine (Build_pMap (loops A) (loops B)
+            (fun p => (point_eq f)^ @ (ap f p @ point_eq f)) _).
+  apply moveR_Vp; simpl.
+  refine (concat_1p _ @ (concat_p1 _)^).
+Defined.
+
+Definition loops_functor_compose {A B C : pType}
+           (g : B ->* C) (f : A ->* B)
+: (loops_functor (pmap_compose g f))
+   ==* (pmap_compose (loops_functor g) (loops_functor f)).
+admit.
+Defined.
+
+Local Open Scope path_scope.
+
+Record ooGroup :=
+  { classifying_space : pType@{i} ;
+    isconn_classifying_space : IsConnected@{u a i} 0 classifying_space
+  }.
+
+Local Notation B := classifying_space.
+
+Definition group_type (G : ooGroup) : Type
+  := point (B G) = point (B G).
+
+Coercion group_type : ooGroup >-> Sortclass.
+
+Definition group_loops (X : pType)
+: ooGroup.
+Proof.
+
+  pose (x0 := point X);
+  pose (BG := (Build_pType
+               { x:X & merely (x = point X) }
+               (existT (fun x:X => merely (x = point X)) x0 (tr 1)))).
+
+  cut (IsConnected 0 BG).
+  {
+ exact (Build_ooGroup BG).
+}
+  cut (IsSurjection (unit_name (point BG))).
+  {
+ intros; refine (conn_pointed_type (point _)).
+}
+  apply BuildIsSurjection; simpl; intros [x p].
+  strip_truncations; apply tr; exists tt.
+  apply path_sigma_hprop; simpl.
+  exact (p^).
+Defined.
+
+Definition loops_group (X : pType)
+: loops X <~> group_loops X.
+admit.
+Defined.
+
+Definition ooGroupHom (G H : ooGroup)
+  := pMap (B G) (B H).
+
+Definition grouphom_fun {G H} (phi : ooGroupHom G H) : G -> H
+  := loops_functor phi.
+
+Coercion grouphom_fun : ooGroupHom >-> Funclass.
+
+Definition group_loops_functor
+           {X Y : pType} (f : pMap X Y)
+: ooGroupHom (group_loops X) (group_loops Y).
+Proof.
+  simple refine (Build_pMap _ _ _ _); simpl.
+  -
+ intros [x p].
+    exists (f x).
+    strip_truncations; apply tr.
+    exact (ap f p @ point_eq f).
+  -
+ apply path_sigma_hprop; simpl.
+    apply point_eq.
+Defined.
+
+Definition loops_functor_group
+           {X Y : pType} (f : pMap X Y)
+: loops_functor (group_loops_functor f) o loops_group X
+  == loops_group Y o loops_functor f.
+admit.
+Defined.
+
+Definition grouphom_compose {G H K : ooGroup}
+           (psi : ooGroupHom H K) (phi : ooGroupHom G H)
+: ooGroupHom G K
+  := pmap_compose psi phi.
+
+Definition group_loops_functor_compose
+           {X Y Z : pType}
+           (psi : pMap Y Z) (phi : pMap X Y)
+: grouphom_compose (group_loops_functor psi) (group_loops_functor phi)
+  == group_loops_functor (pmap_compose psi phi).
+Proof.
+  intros g.
+  unfold grouphom_fun, grouphom_compose.
+  refine (pointed_htpy (loops_functor_compose _ _) g @ _).
+  pose (p := eisretr (loops_group X) g).
+  change (loops_functor (group_loops_functor psi)
+            (loops_functor (group_loops_functor phi) g)
+          = loops_functor (group_loops_functor
+                                 (pmap_compose psi phi)) g).
+  rewrite <- p.
+  Fail Timeout 1 Time rewrite !loops_functor_group.
+  (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
+  Timeout 1 do 3 rewrite loops_functor_group.
+Abort.
\ No newline at end of file
diff --git a/test-suite/success/keyedrewrite.v b/test-suite/success/keyedrewrite.v
index 5b0502cf1..b88c142be 100644
--- a/test-suite/success/keyedrewrite.v
+++ b/test-suite/success/keyedrewrite.v
@@ -58,4 +58,5 @@ Qed.
 
    Lemma test b : b && true = b.
     Fail rewrite andb_true_l.
-   Admitted.
\ No newline at end of file
+   Admitted.
+   
\ No newline at end of file
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 251d14af7..367425546 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -151,12 +151,14 @@ let alarm what internal msg =
   | InternalTacticRequest ->
     (if debug then
       msg_warning
-	(hov 0 msg ++ fnl () ++ what ++ str " not defined."))
-  | _ -> errorlabstrm "" msg
+	(hov 0 msg ++ fnl () ++ what ++ str " not defined.")); None
+  | _ -> Some msg
 
 let try_declare_scheme what f internal names kn =
   try f internal names kn
-  with
+  with e ->
+  let e = Errors.push e in
+  let msg = match fst e with
     | ParameterWithoutEquality cst ->
 	alarm what internal
 	  (str "Boolean equality not found for parameter " ++ pr_con cst ++
@@ -187,6 +189,11 @@ let try_declare_scheme what f internal names kn =
     | e when Errors.noncritical e ->
         alarm what internal
 	  (str "Unexpected error during scheme creation: " ++ Errors.print e)
+    | _ -> iraise e
+  in
+  match msg with
+  | None -> ()
+  | Some msg -> iraise (UserError ("", msg), snd e)
 
 let beq_scheme_msg mind =
   let mib = Global.lookup_mind mind in