156 files changed, 3308 insertions, 283 deletions
diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache
index e0324b0232..b3bcb5b056 100644
--- a/test-suite/.csdp.cache
+++ b/test-suite/.csdp.cache
diff --git a/test-suite/Makefile b/test-suite/Makefile
index c0bdb29fab..1744138d29 100644
--- a/test-suite/Makefile
+++ b/test-suite/Makefile
@@ -32,18 +32,21 @@ include ../Makefile.common
 # Variables
 #######################################################################
 
-# Default value when called from a freshly compiled Coq, but can be
-# easily overridden
-
+ifneq ($(wildcard ../_build),)
+BIN:=$(shell cd ..; pwd)/_build/install/default/bin/
+COQLIB:=$(shell cd ..; pwd)/_build/install/default/lib/coq
+else
 BIN := $(shell cd ..; pwd)/bin/
-COQFLAGS?=
 
 COQLIB?=
 ifeq ($(COQLIB),)
   COQLIB := $(shell ocaml ocaml_pwd.ml ..)
 endif
+endif # exists ../_build
 export COQLIB
 
+COQFLAGS?=
+
 coqc := $(BIN)coqc -q -R prerequisite TestSuite $(COQFLAGS)
 coqchk := $(BIN)coqchk -R prerequisite TestSuite
 coqdoc := $(BIN)coqdoc
@@ -99,7 +102,7 @@ INTERACTIVE := interactive
 UNIT_TESTS := unit-tests
 VSUBSYSTEMS := prerequisite success failure $(BUGS) output output-coqtop \
   output-modulo-time $(INTERACTIVE) micromega $(COMPLEXITY) modules stm \
-  coqdoc ssr arithmetic ltac2
+  coqdoc ssr primitive/uint63 primitive/float ltac2
 
 # All subsystems
 SUBSYSTEMS := $(VSUBSYSTEMS) misc bugs ide vio coqchk coqwc coq-makefile tools $(UNIT_TESTS)
@@ -128,9 +131,10 @@ bugs: $(BUGS)
 
 clean:
 	rm -f trace .nia.cache .lia.cache output/MExtraction.out
+	rm -f vos/Makefile vos/Makefile.conf
 	$(SHOW) 'RM        <**/*.stamp> <**/*.vo> <**/*.vio> <**/*.log> <**/*.glob>'
 	$(HIDE)find . \( \
-	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.log' -o -name '*.glob' \
+	  -name '*.stamp' -o -name '*.vo' -o -name '*.vio' -o -name '*.vos' -o -name '*.vok' -o -name '*.log' -o -name '*.glob' \
 	  \) -exec rm -f {} +
 	$(SHOW) 'RM        <**/*.cmx> <**/*.cmi> <**/*.o> <**/*.test>'
 	$(HIDE)find unit-tests \( \
@@ -171,6 +175,7 @@ summary:
 	  $(call summary_dir, "Miscellaneous tests", misc); \
 	  $(call summary_dir, "Complexity tests", complexity); \
 	  $(call summary_dir, "Module tests", modules); \
+	  $(call summary_dir, "Primitive tests", primitive); \
 	  $(call summary_dir, "STM tests", stm); \
 	  $(call summary_dir, "SSR tests", ssr); \
 	  $(call summary_dir, "IDE tests", ide); \
@@ -326,7 +331,7 @@ $(addsuffix .log,$(wildcard prerequisite/*.v)): %.v.log: %.v
 	} > "$@"
 
 ssr: $(wildcard ssr/*.v:%.v=%.v.log)
-$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v arithmetic/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG)
+$(addsuffix .log,$(wildcard ssr/*.v success/*.v micromega/*.v modules/*.v primitive/*/*.v ltac2/*.v)): %.v.log: %.v $(PREREQUISITELOG)
 	@echo "TEST      $< $(call get_coq_prog_args_in_parens,"$<")"
 	$(HIDE){ \
 	  opts="$(if $(findstring modules/,$<),-R modules Mods)"; \
@@ -745,3 +750,23 @@ tools/%.log : tools/%/run.sh
 	    $(FAIL); \
 	  fi; \
 	) > "$@"
+
+# vos/
+
+vos: vos/run.log
+
+vos/run.log: $(wildcard vos/*.sh) $(wildcard vos/*.v)
+	@echo "TEST      vos"
+	$(HIDE)(\
+	  export COQBIN=$(BIN);\
+	  cd vos && \
+	  bash run.sh 2>&1; \
+	if [ $$? = 0 ]; then \
+	    echo $(log_success); \
+	    echo "    $<...Ok"; \
+	  else \
+	    echo $(log_failure); \
+	    echo "    $<...Error!"; \
+	    $(FAIL); \
+	  fi; \
+	) > "$@"
diff --git a/test-suite/bugs/closed/bug_10060.v b/test-suite/bugs/closed/bug_10060.v
new file mode 100644
index 0000000000..d74f6e388b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10060.v
@@ -0,0 +1,15 @@
+Module Type T.
+  Parameter b : Set.
+End T.
+
+Module M1(N : T).
+End M1.
+
+Module M2.
+End M2.
+
+Section S.
+  Variable a : Set.
+  Definition b := a.
+  Fail Include M1.
+End S.
diff --git a/test-suite/bugs/closed/bug_10088.v b/test-suite/bugs/closed/bug_10088.v
new file mode 100644
index 0000000000..3e17bfc12a
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10088.v
@@ -0,0 +1,6 @@
+Require Import ssreflect.
+From Ltac2 Require Import Ltac2.
+
+Inductive nat_list :=
+  Nil
+| Cons of nat & nat_list.
diff --git a/test-suite/bugs/closed/bug_10097.v b/test-suite/bugs/closed/bug_10097.v
new file mode 100644
index 0000000000..12f2d4cc58
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10097.v
@@ -0,0 +1,14 @@
+From Ltac2 Require Import Ltac2.
+
+(* #10097 *)
+Ltac2 Type s := [X(int)].
+Fail Ltac2 Type s.
+Fail Ltac2 Type s := [].
+
+Ltac2 Type r := [..].
+Fail Ltac2 Type r := [].
+
+Module Other.
+  Ltac2 Type s.
+  Ltac2 Type r := [].
+End Other.
diff --git a/test-suite/bugs/closed/bug_10116.v b/test-suite/bugs/closed/bug_10116.v
new file mode 100644
index 0000000000..58caa59786
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10116.v
@@ -0,0 +1,3 @@
+From Ltac2 Require Import Ltac2.
+
+Ltac2 Eval true :: [], false.
diff --git a/test-suite/bugs/closed/bug_10196.v b/test-suite/bugs/closed/bug_10196.v
new file mode 100644
index 0000000000..d003ab323d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10196.v
@@ -0,0 +1,26 @@
+From Ltac2 Require Import Ltac2.
+
+(* true and false are valid constructors even though they are lowercase *)
+Ltac2 Eval true.
+Ltac2 Eval false.
+
+(* Otherwise constructors have to be Uppercase *)
+Ltac2 Type good_constructor := [Uppercased].
+Ltac2 Type good_constructors := [Uppercased1 | Uppercased2].
+
+Ltac2 Eval Uppercased2.
+
+Fail Ltac2 Type bad_constructor := [ notUppercased ].
+Fail Ltac2 Type bad_constructors := [ | notUppercased1 | notUppercased2 ].
+
+Fail Ltac2 Eval notUppercased2.
+
+(* And the same for open types*)
+Ltac2 Type open_type := [ .. ].
+Fail Ltac2 Type open_type ::= [ notUppercased3 ].
+Ltac2 Type open_type ::= [ Uppercased3 ].
+
+Fail Ltac2 Eval notUppercased3.
+Ltac2 Eval Uppercased3.
+
+Fail Ltac2 Type foo ::= [ | bar1 | bar2 ].
diff --git a/test-suite/bugs/closed/bug_10669.v b/test-suite/bugs/closed/bug_10669.v
new file mode 100644
index 0000000000..433e300acb
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10669.v
@@ -0,0 +1,12 @@
+
+Context (A0:Type) (B0:A0).
+Definition foo0 := B0.
+
+Set Universe Polymorphism.
+Context (A1:Type) (B1:A1).
+Definition foo1 := B1.
+
+Section S.
+  Context (A2:Type) (B2:A2).
+  Definition foo2 := B2.
+End S.
diff --git a/test-suite/bugs/closed/bug_10757.v b/test-suite/bugs/closed/bug_10757.v
new file mode 100644
index 0000000000..a531f6e563
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10757.v
@@ -0,0 +1,38 @@
+Require Import Program Extraction ExtrOcamlBasic.
+Print sig.
+Section FIXPOINT.
+
+Variable A: Type.
+
+Variable eq: A -> A -> Prop.
+Variable beq: A -> A -> bool.
+Hypothesis beq_eq: forall x y, beq x y = true -> eq x y.
+Hypothesis beq_neq: forall x y, beq x y = false -> ~eq x y.
+
+Variable le: A -> A -> Prop.
+Hypothesis le_trans: forall x y z, le x y -> le y z -> le x z.
+
+Definition gt (x y: A) := le y x /\ ~eq y x.
+Hypothesis gt_wf: well_founded gt.
+
+Variable F: A -> A.
+Hypothesis F_mon: forall x y, le x y -> le (F x) (F y).
+
+Program Fixpoint iterate
+    (x: A) (PRE: le x (F x)) (SMALL: forall z, le (F z) z -> le x z)
+    {wf gt x}
+    : {y : A | eq y (F y) /\ forall z, le (F z) z -> le y z } :=
+  let x' := F x in
+  match beq x x' with
+  | true  => x
+  | false => iterate x' _ _
+  end.
+Next Obligation.
+  split.
+- auto.
+- apply beq_neq. auto.
+Qed.
+
+End FIXPOINT.
+
+Recursive Extraction iterate.
diff --git a/test-suite/bugs/closed/bug_10778.v b/test-suite/bugs/closed/bug_10778.v
new file mode 100644
index 0000000000..25d729b7e6
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10778.v
@@ -0,0 +1,32 @@
+(* Test that fresh avoid the variables of intro patterns but also of
+   simple intro patterns *)
+
+Ltac exploit_main t T pat cleanup
+  :=
+  (lazymatch T with
+   | ?U1 -> ?U2 =>
+       let H := fresh
+       in
+idtac "H=" H;
+         assert U1 as H;
+         [cleanup () | exploit_main (t H) U2 pat ltac:(fun _ => clear H; cleanup ())]
+   | _ =>
+       pose proof t as pat;
+       cleanup ()
+   end).
+
+Tactic Notation "exploit" constr(t) "as" simple_intropattern(pat)
+  :=
+  exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
+
+Goal (True -> True) -> True.
+intro H0. exploit H0 as H.
+Abort.
+
+Tactic Notation "exploit'" constr(t) "as" intropattern(pat)
+  :=
+  exploit_main t ltac:(type of t) pat ltac:(fun _ => idtac).
+
+Goal (True -> True) -> True.
+intro H0. exploit' H0 as H.
+Abort.
diff --git a/test-suite/bugs/closed/bug_10888.v b/test-suite/bugs/closed/bug_10888.v
new file mode 100644
index 0000000000..3c2e8011d7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10888.v
@@ -0,0 +1,11 @@
+
+Module Type T.
+Context {A:Type}.
+End T.
+
+Module M(X:T).
+  Import X.
+  Check X.A.
+  Check A.
+  Definition B := A.
+End M.
diff --git a/test-suite/bugs/closed/bug_10894.v b/test-suite/bugs/closed/bug_10894.v
new file mode 100644
index 0000000000..b8c9367951
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10894.v
@@ -0,0 +1,12 @@
+(* Check that uconstrs are interpreted in the ltac-substituted environment *)
+(* Was a regression introduced in 4dab4fc (#7288) *)
+
+Tactic Notation "bind" hyp(x) "in" uconstr(f) "as" ident(h) :=
+   set (h := fun x => f).
+
+Fact test : nat -> nat.
+Proof.
+  intros n.
+  bind n in (n*n) as f.
+  assert (f 0 = 0) by reflexivity.
+Abort.
diff --git a/test-suite/bugs/closed/bug_10903.v b/test-suite/bugs/closed/bug_10903.v
new file mode 100644
index 0000000000..3da63dfbb0
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10903.v
@@ -0,0 +1,3 @@
+(* -*- coq-prog-args: ("-type-in-type"); -*- *)
+
+Inductive Ind : SProp := C : Ind -> Ind.
diff --git a/test-suite/bugs/closed/bug_10904.v b/test-suite/bugs/closed/bug_10904.v
new file mode 100644
index 0000000000..32b25ff726
--- /dev/null
+++ b/test-suite/bugs/closed/bug_10904.v
@@ -0,0 +1,8 @@
+Definition a := fun (P:SProp) (p:P) => p.
+
+Lemma foo : (let k := a in let k' := a in fun (x:nat) y => x) = (let k := a in fun x y => y).
+Proof.
+  Fail reflexivity.
+  match goal with |- ?l = _ => exact_no_check (eq_refl l) end.
+Fail Qed.
+Abort.
diff --git a/test-suite/bugs/closed/bug_11046.v b/test-suite/bugs/closed/bug_11046.v
new file mode 100644
index 0000000000..528cc4c8ff
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11046.v
@@ -0,0 +1,19 @@
+From Ltac2 Require Import Ltac2.
+
+Ltac2 Type t := [..].
+Ltac2 Type t ::= [A(int)].
+
+(* t cannot be extended with two constructors with the same name *)
+Fail Ltac2 Type t ::= [A(bool)].
+Fail Ltac2 Type t ::= [B | B(bool)].
+
+(* constructors cannot be shadowed in the same module *)
+Fail Ltac2 Type s := [A].
+
+(* constructors with the same name can be defined in distinct modules *)
+Module Other.
+  Ltac2 Type t ::= [A(bool)].
+End Other.
+Module YetAnother.
+  Ltac2 Type t := [A].
+End YetAnother.
diff --git a/test-suite/bugs/closed/bug_11048.v b/test-suite/bugs/closed/bug_11048.v
new file mode 100644
index 0000000000..d1211587f1
--- /dev/null
+++ b/test-suite/bugs/closed/bug_11048.v
@@ -0,0 +1,5 @@
+
+Inductive foo (HUGE := _) (b : HUGE) A :=
+  bar (X:match _ : HUGE as T return HUGE with T => match (A : T) -> True with _ => T end end)
+  : foo b A.
+(* uncaught destKO *)
diff --git a/test-suite/bugs/closed/bug_3481.v b/test-suite/bugs/closed/bug_3481.v
index 41e1a8e959..f54810d359 100644
--- a/test-suite/bugs/closed/bug_3481.v
+++ b/test-suite/bugs/closed/bug_3481.v
@@ -1,7 +1,6 @@
 
 Set Implicit Arguments.
 
-Require Import Logic.
 Module NonPrim.
 Local Set Nonrecursive Elimination Schemes.
 Record prodwithlet (A B : Type) : Type :=
diff --git a/test-suite/bugs/closed/bug_4498.v b/test-suite/bugs/closed/bug_4498.v
index 9b3210860c..ba63b707af 100644
--- a/test-suite/bugs/closed/bug_4498.v
+++ b/test-suite/bugs/closed/bug_4498.v
@@ -1,6 +1,7 @@
 Require Export Coq.Unicode.Utf8.
 Require Export Coq.Classes.Morphisms.
 Require Export Coq.Relations.Relation_Definitions.
+Require Export Coq.Setoids.Setoid.
 
 Set Universe Polymorphism.
 
@@ -17,8 +18,6 @@ Class Category := {
       Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C);
 }.
 
-Require Export Coq.Setoids.Setoid.
-
 Add Parametric Morphism `{Category} {A B C} : (@compose _ A B C) with
   signature equiv ==> equiv ==> equiv as compose_mor.
 Proof. apply comp_respects. Qed.
diff --git a/test-suite/bugs/closed/bug_4502.v b/test-suite/bugs/closed/bug_4502.v
new file mode 100644
index 0000000000..f1dcae9773
--- /dev/null
+++ b/test-suite/bugs/closed/bug_4502.v
@@ -0,0 +1,17 @@
+Require Import FunInd.
+
+Set Universe Polymorphism.
+Set Primitive Projections.
+Set Implicit Arguments.
+Set Strongly Strict Implicit.
+
+Function first_false (n : nat) (f : nat -> bool) : option nat :=
+  match n with
+  | O => None
+  | S m =>
+    match first_false m f with
+    | (Some _) as s => s
+    | None => if f m then None else Some m
+    end
+  end.
+(* undefined universe *)
diff --git a/test-suite/bugs/closed/bug_6323.v b/test-suite/bugs/closed/bug_6323.v
index fdc33befc6..24feb7155c 100644
--- a/test-suite/bugs/closed/bug_6323.v
+++ b/test-suite/bugs/closed/bug_6323.v
@@ -6,4 +6,5 @@ Goal True.
       simple refine (let id' : { x : X' | True } -> X' := _ in _);
       [ abstract refine (@proj1_sig _ _) | ]
     ].
-Abort.
+  exact I.
+Defined.
diff --git a/test-suite/bugs/closed/bug_8459.v b/test-suite/bugs/closed/bug_8459.v
new file mode 100644
index 0000000000..62c49e9ea7
--- /dev/null
+++ b/test-suite/bugs/closed/bug_8459.v
@@ -0,0 +1,24 @@
+Require Import Coq.Vectors.Vector.
+
+Axiom exfalso : False.
+
+Fixpoint all_then_someV (n:nat) (l:Vector.t bool n) {struct l}:
+(Vector.fold_left orb false l) = false ->
+(forall p, (Vector.nth l p  ) = false).
+Proof.
+intros.
+destruct l.
+inversion p.
+revert h l H.
+set (P := fun n p => forall (h : bool) (l : t bool n),
+fold_left orb false (cons bool h n l) = false -> @eq bool (@nth bool (S n) (cons bool h n l) p) false).
+revert n p.
+fix loop 1.
+unshelve eapply (@Fin.rectS P).
++ elim exfalso.
++ unfold P.
+  intros.
+  eapply all_then_someV.
+  exact H0.
+Fail Defined.
+Abort.
diff --git a/test-suite/bugs/closed/bug_9114.v b/test-suite/bugs/closed/bug_9114.v
new file mode 100644
index 0000000000..2cf91c1c2b
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9114.v
@@ -0,0 +1,5 @@
+Goal True.
+  assert_succeeds (exact I).
+  idtac.
+  (* Error: No such goal. *)
+Abort.
diff --git a/test-suite/bugs/closed/bug_9294.v b/test-suite/bugs/closed/bug_9294.v
new file mode 100644
index 0000000000..a079d672d3
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9294.v
@@ -0,0 +1,29 @@
+Set Printing Universes.
+
+Inductive Foo@{i} (A:Type@{i}) : Type := foo : (Set:Type@{i}) -> Foo A.
+Arguments foo {_} _.
+Print Universes Subgraph (Foo.i).
+Definition bar : Foo True -> Set := fun '(foo x) => x.
+
+Definition foo_bar (n : Foo True) : foo (bar n) = n.
+Proof. destruct n;reflexivity. Qed.
+
+Definition bar_foo (n : Set) : bar (foo n) = n.
+Proof. reflexivity. Qed.
+
+Require Import Hurkens.
+
+Inductive box (A : Set) : Prop := Box : A -> box A.
+
+Definition Paradox : False.
+Proof.
+Fail unshelve refine (
+  NoRetractFromSmallPropositionToProp.paradox
+  (Foo True)
+  (fun A => foo A)
+  (fun A => box (bar A))
+  _
+  _
+  False
+).
+Abort.
diff --git a/test-suite/bugs/closed/bug_9512.v b/test-suite/bugs/closed/bug_9512.v
new file mode 100644
index 0000000000..25285622a9
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9512.v
@@ -0,0 +1,35 @@
+Require Import Coq.ZArith.BinInt Coq.omega.Omega Coq.micromega.Lia.
+
+Set Primitive Projections.
+Record params := { width : Z }.
+Definition p : params := Build_params 64.
+
+Set Printing All.
+
+Goal width p = 0%Z -> width p = 0%Z.
+  intros.
+
+  assert_succeeds (enough True; [omega|]).
+  assert_succeeds (enough True; [lia|]).
+
+(*   H : @eq Z (width p) Z0 *)
+(*   ============================ *)
+(*   @eq Z (width p) Z0 *)
+
+  change tt with tt in H.
+
+(*   H : @eq Z (width p) Z0 *)
+(*   ============================ *)
+(*   @eq Z (width p) Z0 *)
+
+  assert_succeeds (enough True; [lia|]).
+  (* Tactic failure: <tactic closure> fails. *)
+  (* assert_succeeds (enough True; [omega|]). *)
+  (* Tactic failure: <tactic closure> fails. *)
+
+  (* omega. *)
+  (* Error: Omega can't solve this system *)
+
+  lia.
+  (* Tactic failure:  Cannot find witness. *)
+Qed.
diff --git a/test-suite/bugs/closed/bug_9851.v b/test-suite/bugs/closed/bug_9851.v
new file mode 100644
index 0000000000..1f57ce8471
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9851.v
@@ -0,0 +1,18 @@
+Require Import Ring_base.
+Record word : Type := Build_word
+  { rep : Type;
+    zero : rep; one: rep;
+    add : rep -> rep -> rep;
+    sub : rep -> rep -> rep;
+    opp : rep -> rep;
+    mul : rep -> rep -> rep;
+    }.
+Axiom rth
+     : forall (word : word ),
+       @ring_theory (@rep word)
+         (@zero word)
+         (@one word) (@add word)
+         (@mul word) (@sub word)
+         (@opp word) (@eq (@rep word)).
+
+Fail Add Ring wring: (@rth _).
diff --git a/test-suite/bugs/opened/bug_1596.v b/test-suite/bugs/opened/bug_1596.v
index 820022d995..27cb731151 100644
--- a/test-suite/bugs/opened/bug_1596.v
+++ b/test-suite/bugs/opened/bug_1596.v
@@ -69,9 +69,8 @@ Definition t := (X.t * Y.t)%type.
     elim (X.lt_not_eq H2 H3).
     elim H0;clear H0;intros.
     right.
-    split.
-    eauto.
-    eauto.
+    split;
+    eauto with ordered_type.
   Qed.
 
   Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
@@ -97,7 +96,7 @@ Definition t := (X.t * Y.t)%type.
     apply EQ.
     split;trivial.
     apply GT.
-    right;auto.
+    right;auto with ordered_type.
     apply GT.
     left;trivial.
   Defined.
diff --git a/test-suite/coqchk/inductive_functor_template.v b/test-suite/coqchk/inductive_functor_template.v
index bc5cd0fb68..4b6916af55 100644
--- a/test-suite/coqchk/inductive_functor_template.v
+++ b/test-suite/coqchk/inductive_functor_template.v
@@ -2,7 +2,7 @@
 Module Type E. Parameter T : Type. End E.
 
 Module F (X:E).
-  #[universes(template)] Inductive foo := box : X.T -> foo.
+  Inductive foo := box : X.T -> foo.
 End F.
 
 Module ME. Definition T := nat. End ME.
diff --git a/test-suite/failure/Template.v b/test-suite/failure/Template.v
new file mode 100644
index 0000000000..75b2a56169
--- /dev/null
+++ b/test-suite/failure/Template.v
@@ -0,0 +1,32 @@
+(*
+Module TestUnsetTemplateCheck.
+  Unset Template Check.
+
+  Section Foo.
+
+    Context (A : Type).
+
+    Definition cstr := nat : ltac:(let ty := type of A in exact ty).
+
+    Inductive myind :=
+    | cons : A -> myind.
+  End Foo.
+
+  (* Can only succeed if no template check is performed *)
+  Check myind True : Prop.
+
+  Print Assumptions myind.
+  (*
+  Axioms:
+  myind is template polymorphic on all its universe parameters.
+   *)
+  About myind.
+(*
+myind : Type@{Top.60} -> Type@{Top.60}
+
+myind is assumed template universe polymorphic on Top.60
+Argument scope is [type_scope]
+Expands to: Inductive Top.TestUnsetTemplateCheck.myind
+*)
+End TestUnsetTemplateCheck.
+*)
diff --git a/test-suite/ltac2/constr.v b/test-suite/ltac2/constr.v
new file mode 100644
index 0000000000..39601d99a8
--- /dev/null
+++ b/test-suite/ltac2/constr.v
@@ -0,0 +1,12 @@
+Require Import Ltac2.Constr Ltac2.Init Ltac2.Control.
+Import Unsafe.
+
+Ltac2 Eval match (kind '(nat -> bool)) with
+           | Prod a b c => a
+           | _ => throw Match_failure end.
+
+Set Allow StrictProp.
+Axiom something : SProp.
+Ltac2 Eval match (kind '(forall x : something, bool)) with
+           | Prod a b c => a
+           | _ => throw Match_failure end.
diff --git a/test-suite/ltac2/ltac2env.v b/test-suite/ltac2/ltac2env.v
new file mode 100644
index 0000000000..743e62932d
--- /dev/null
+++ b/test-suite/ltac2/ltac2env.v
@@ -0,0 +1,15 @@
+Require Import Ltac2.Ltac2.
+
+Ltac2 get_opt o := match o with None => Control.throw Not_found | Some x => x end.
+
+Goal True.
+Proof.
+(* Fails at runtime because not fully applied *)
+Fail ltac1:(ltac2:(x |- ())).
+(* Type mismatch: Ltac1.t vs. constr *)
+Fail ltac1:(ltac2:(x |- pose $x)).
+(* Check that runtime cast is OK *)
+ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t nat).
+(* Type mismatch *)
+Fail ltac1:(let t := ltac2:(x |- let c := (get_opt (Ltac1.to_constr x)) in pose $c) in t ident:(foo)).
+Abort.
diff --git a/test-suite/ltac2/term_notations.v b/test-suite/ltac2/term_notations.v
new file mode 100644
index 0000000000..85eb858d4e
--- /dev/null
+++ b/test-suite/ltac2/term_notations.v
@@ -0,0 +1,33 @@
+Require Import Ltac2.Ltac2.
+
+(* Preterms are not terms *)
+Fail Notation "[ x ]" := $x.
+
+Section Foo.
+
+Notation "[ x ]" := ltac2:(Control.refine (fun _ => Constr.pretype x)).
+
+Goal [ True ].
+Proof.
+constructor.
+Qed.
+
+End Foo.
+
+Section Bar.
+
+(* Have fun with context capture *)
+Notation "[ x ]" := ltac2:(
+  let c () := Constr.pretype x in
+  refine constr:(forall n : nat, n = ltac2:(Notations.exact0 true c))
+).
+
+Goal forall n : nat, [ n ].
+Proof.
+reflexivity.
+Qed.
+
+(* This fails currently, which is arguably a bug *)
+Fail Goal [ n ].
+
+End Bar.
diff --git a/test-suite/micromega/bug_9162.v b/test-suite/micromega/bug_9162.v
new file mode 100644
index 0000000000..4aedf57faf
--- /dev/null
+++ b/test-suite/micromega/bug_9162.v
@@ -0,0 +1,8 @@
+Require Import ZArith Lia.
+Local Open Scope Z_scope.
+
+Goal Z.of_N (Z.to_N 0) = 0.
+Proof. lia. Qed.
+
+Goal forall q, (Z.of_N (Z.to_N 0) = 0 -> q = 0) -> Z.of_N (Z.to_N 0) = q.
+Proof. lia. Qed.
diff --git a/test-suite/micromega/non_lin_ci.v b/test-suite/micromega/non_lin_ci.v
index ec39209230..2a66cc9a5a 100644
--- a/test-suite/micromega/non_lin_ci.v
+++ b/test-suite/micromega/non_lin_ci.v
@@ -43,18 +43,18 @@ Proof.
 Qed.
 
 Goal
-  forall (__x1 __x2 __x3 __x4 __x5 __x6 __x7 __x8 __x9 __x10 __x11 __x12 __x13
-  __x14 __x15 __x16 : Z)
-         (H6 : __x8 < __x10 ^ 2 * __x15 ^ 2 + 2 * __x10 * __x15 * __x14 + __x14 ^ 2)
-         (H7 : 0 <= __x8)
-         (H12 : 0 <= __x14)
-         (H0 : __x8 = __x15 * __x11 + __x9)
-         (H14 : __x10 ^ 2 * __x15 + __x10 * __x14 < __x16)
-         (H17 : __x16 <= 0)
-         (H15 : 0 <= __x9)
-         (H18 : __x9 < __x15)
-         (H16 : 0 <= __x12)
-         (H19 : __x12 < (__x10 * __x15 + __x14) * __x10)
+  forall (x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13
+  x14 x15 x16 : Z)
+         (H6 : x8 < x10 ^ 2 * x15 ^ 2 + 2 * x10 * x15 * x14 + x14 ^ 2)
+         (H7 : 0 <= x8)
+         (H12 : 0 <= x14)
+         (H0 : x8 = x15 * x11 + x9)
+         (H14 : x10 ^ 2 * x15 + x10 * x14 < x16)
+         (H17 : x16 <= 0)
+         (H15 : 0 <= x9)
+         (H18 : x9 < x15)
+         (H16 : 0 <= x12)
+         (H19 : x12 < (x10 * x15 + x14) * x10)
   , False.
 Proof.
   intros.
diff --git a/test-suite/micromega/rexample.v b/test-suite/micromega/rexample.v
index 52dc9ed2e0..354c608e23 100644
--- a/test-suite/micromega/rexample.v
+++ b/test-suite/micromega/rexample.v
@@ -24,6 +24,16 @@ Proof.
   lra.
 Qed.
 
+Goal
+  forall  (a c : R)
+         (Had : a <> a),
+    a > c.
+Proof.
+  intros.
+  lra.
+Qed.
+
+
 (* Other (simple) examples *)
 
 Lemma binomial : forall x y, ((x+y)^2 = x^2 + 2 *x*y + y^2).
@@ -32,7 +42,6 @@ Proof.
   lra.
 Qed.
 
-
 Lemma hol_light19 : forall m n, 2 * m + n = (n + m) + m.
 Proof.
   intros ; lra.
diff --git a/test-suite/micromega/rsyntax.v b/test-suite/micromega/rsyntax.v
index f02d93f911..a0afe99181 100644
--- a/test-suite/micromega/rsyntax.v
+++ b/test-suite/micromega/rsyntax.v
@@ -60,7 +60,6 @@ Proof.
   lia. (* exponent is a constant expr *)
 Qed.
 
-
 Goal (1 / IZR (Z.pow_pos 10 25) = 1 / 10 ^ 25)%R.
 Proof.
   lra.
diff --git a/test-suite/micromega/zomicron.v b/test-suite/micromega/zomicron.v
index 55691f553c..3d99af95ec 100644
--- a/test-suite/micromega/zomicron.v
+++ b/test-suite/micromega/zomicron.v
@@ -1,5 +1,63 @@
 Require Import ZArith.
 Require Import Lia.
+
+Section S.
+  Variables H1 H2 H3 H4 : True.
+
+  Lemma bug_9848 : True.
+  Proof using.
+    lia.
+  Qed.
+End S.
+
+Lemma concl_in_Type : forall   (k : nat)
+             (H : (k < 0)%nat) (F : k < 0 -> Type),
+    F H.
+Proof.
+  intros.
+  lia.
+Qed.
+
+Lemma bug_10707 : forall
+    (T : Type)
+    (t : nat -> Type)
+    (k : nat)
+    (default : T)
+    (arr : t 0 -> T)
+    (H : (k < 0)%nat) of_nat_lt,
+ match k with
+ | 0 | _ => default
+ end = arr (of_nat_lt H).
+Proof.
+  intros.
+  lia.
+Qed.
+
+Axiom decompose_nat : nat -> nat -> nat.
+Axiom inleft : forall {P}, {m : nat & P m} -> nat.
+Axiom foo : nat.
+
+Lemma bug_7886 : forall (x x0 : nat)
+                        (e : 0 = x0 + S x)
+                        (H : decompose_nat x 0 = inleft (existT (fun m : nat => 0 = m + S x) x0 e))
+                        (x1 : nat)
+                        (e0 : 0 = x1 + S (S x))
+                        (H1 : decompose_nat (S x) 0 = inleft (existT (fun m : nat => 0 = m + S (S x)) x1 e0)),
+    False.
+Proof.
+  intros.
+  lia.
+Qed.
+
+
+Lemma bug_8898 : forall (p : 0 < 0) (H: p = p), False.
+Proof.
+  intros p H.
+  lia.
+Qed.
+
+
+
 Open Scope Z_scope.
 
 Lemma two_x_eq_1 : forall x, 2 * x = 1 -> False.
@@ -34,12 +92,12 @@ Proof.
 Qed.
 
 Lemma compact_proof : forall z,
- (z < 0) ->
- (z >= 0) ->
-  (0 >= z \/ 0 < z) -> False.
+    (z < 0) ->
+    (z >= 0) ->
+    (0 >= z \/ 0 < z) -> False.
 Proof.
- intros.
- lia.
+  intros.
+  lia.
 Qed.
 
 Lemma dummy_ex : exists (x:Z),  x = x.
@@ -74,9 +132,17 @@ Proof.
   lia.
 Qed.
 
+
+Lemma fresh1 : forall (__p1 __p2 __p3 __p5:Prop) (x y z:Z), (x = 0 /\ y = 0) /\ z = 0 -> x = 0.
+Proof.
+  intros.
+  lia.
+Qed.
+
+
 Class Foo {x : Z} := { T : Type ; dec : T -> Z }.
 Goal forall bound {F : @Foo bound} (x y : T), 0 <= dec x < bound -> 0 <= dec y 
-< bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound.
+                                                                    < bound -> dec x + dec y >= bound -> dec x + dec y < 2 * bound.
 Proof.
   intros.
   lia.
@@ -98,7 +164,19 @@ Section S.
     lia.
   Qed.
 
-  End S.
+End S.
+
+Section S.
+  Variable x y: Z.
+  Variable H1 : 1 > 0 -> x = 1.
+  Variable H2 : x = y.
+
+  Goal x = y.
+  Proof using H2.
+    lia.
+  Qed.
+
+End S.
 
 (*  Bug 5073 *)
 Lemma opp_eq_0_iff a : -a = 0 <-> a = 0.
@@ -122,8 +200,50 @@ Goal forall
     (H5 : - b < r)
     (H6 : r <= 0)
     (H2 : 0 <= b),
-  b = 0 -> False.
+    b = 0 -> False.
 Proof.
   intros b q r.
   lia.
 Qed.
+
+
+Section S.
+  (* From bedrock2, used to be slow *)
+  Variables (x3 q r q2 r3 : Z)
+            (H : 2 ^ 2 <> 0 -> r3 + 3 = 2 ^ 2 * q + r)
+            (H0 : 0 < 2 ^ 2 -> 0 <= r < 2 ^ 2)
+            (H1 : 2 ^ 2 < 0 -> 2 ^ 2 < r <= 0)
+            (H2 : 2 ^ 2 = 0 -> q = 0)
+            (H3 : 2 ^ 2 = 0 -> r = 0)
+            (q0 r0 : Z)
+            (H4 : 4 <> 0 -> 0 = 4 * q0 + r0)
+            (H5 : 0 < 4 -> 0 <= r0 < 4)
+            (H6 : 4 < 0 -> 4 < r0 <= 0)
+            (H7 : 4 = 0 -> q0 = 0)
+            (H8 : 4 = 0 -> r0 = 0)
+            (q1 r1 : Z)
+            (H9 : 4 <> 0 -> q + q + (q + q) = 4 * q1 + r1)
+            (H10 : 0 < 4 -> 0 <= r1 < 4)
+            (H11 : 4 < 0 -> 4 < r1 <= 0)
+            (H12 : 4 = 0 -> q1 = 0)
+            (H13 : 4 = 0 -> r1 = 0)
+            (r2 : Z)
+            (H14 : 2 ^ 16 <> 0 ->  x3 = 2 ^ 16 * q2 + r2)
+            (H15 : 0 < 2 ^ 16 -> 0 <= r2 < 2 ^ 16)
+            (H16 : 2 ^ 16 < 0 -> 2 ^ 16 < r2 <= 0)
+            (H17 : 2 ^ 16 = 0 -> q2 = 0)
+            (H18 : 2 ^ 16 = 0 -> r2 = 0)
+            (q3 : Z)
+            (H19 : 16383 + 1 <> 0 -> q2 = (16383 + 1) * q3 + r3)
+            (H20 : 0 < 16383 + 1 -> 0 <= r3 < 16383 + 1)
+            (H21 : 16383 + 1 < 0 -> 16383 + 1 < r3 <= 0)
+            (H22 : 16383 + 1 = 0 -> q3 = 0)
+            (H23 : 16383 + 1 = 0 -> r3 = 0).
+
+  Goal r0 = r1.
+  Proof using H10 H9 H5 H4.
+    intros.
+    lia.
+  Qed.
+
+End S.
diff --git a/test-suite/misc/deps/deps.out b/test-suite/misc/deps/deps.out
index 5b79349fc2..d0263b8935 100644
--- a/test-suite/misc/deps/deps.out
+++ b/test-suite/misc/deps/deps.out
@@ -1 +1 @@
-misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
+misc/deps/client/bar.vo misc/deps/client/bar.glob misc/deps/client/bar.v.beautified misc/deps/client/bar.required_vo: misc/deps/client/bar.v misc/deps/client/foo.vo misc/deps/lib/foo.vo
diff --git a/test-suite/misc/votour.sh b/test-suite/misc/votour.sh
new file mode 100755
index 0000000000..ac26aed49b
--- /dev/null
+++ b/test-suite/misc/votour.sh
@@ -0,0 +1,3 @@
+command -v "${BIN}votour" || { echo "Missing votour"; exit 1; }
+
+"${BIN}votour" prerequisite/ssr_mini_mathcomp.vo < /dev/null
diff --git a/test-suite/output-coqtop/DependentEvars.out b/test-suite/output-coqtop/DependentEvars.out
new file mode 100644
index 0000000000..9ca3fa3357
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.out
@@ -0,0 +1,91 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+Coq < Coq < 
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  P4
+
+(dependent evars: ; in current goal:)
+
+p14 < 
+p14 < 4 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 < 
+Coq < 
+Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars.v b/test-suite/output-coqtop/DependentEvars.v
new file mode 100644
index 0000000000..5a59054073
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars.v
@@ -0,0 +1,24 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+  auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+  tauto.
+Qed.
+
+Section eex.
+  Variables P1 P2 P3 P4 : Prop.
+  Hypothesis p12 : P1 -> P2.
+  Hypothesis p123 : (P1 -> P2) -> P3.
+  Hypothesis p34 : P3 -> P4.
+
+  Lemma p14 : P4.
+  Proof.
+    eapply strange_imp_trans.
+          apply modpon.
+  Abort.
+End eex.
diff --git a/test-suite/output-coqtop/DependentEvars2.out b/test-suite/output-coqtop/DependentEvars2.out
new file mode 100644
index 0000000000..29ebba7c86
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.out
@@ -0,0 +1,120 @@
+
+Coq < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+strange_imp_trans < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+strange_imp_trans < 
+Coq < Coq < 1 subgoal
+  
+  ============================
+  forall P Q : Prop, (P -> Q) /\ P -> Q
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+modpon < No more subgoals.
+
+(dependent evars: ; in current goal:)
+
+modpon < 
+Coq < Coq < 
+Coq < P1 is declared
+P2 is declared
+P3 is declared
+P4 is declared
+
+Coq < p12 is declared
+
+Coq < p123 is declared
+
+Coq < p34 is declared
+
+Coq < Coq < 1 subgoal
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  P4
+
+(dependent evars: ; in current goal:)
+
+p14 < 
+p14 < Second proof:
+
+p14 < 4 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+subgoal 2 is:
+ ?P -> ?Q
+subgoal 3 is:
+ ?P -> ?Q
+subgoal 4 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < 1 focused subgoal
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?Q -> P4
+
+(dependent evars: ?X4:?P, ?X5:?Q; in current goal: ?X5)
+
+p14 < This subproof is complete, but there are some unfocused goals.
+Try unfocusing with "}".
+
+3 subgoals
+(shelved: 2)
+
+subgoal 1 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal:)
+
+p14 < 3 focused subgoals
+(shelved: 2)
+  
+  P1, P2, P3, P4 : Prop
+  p12 : P1 -> P2
+  p123 : (P1 -> P2) -> P3
+  p34 : P3 -> P4
+  ============================
+  ?P -> (?Goal2 -> P4) /\ ?Goal2
+
+subgoal 2 is:
+ ?P -> (?Goal2 -> P4) /\ ?Goal2
+subgoal 3 is:
+ ?P
+
+(dependent evars: ?X4:?P, ?X5 using ?X10 ?X11, ?X10 using ?X11, ?X11:?Goal2; in current goal: ?X4 ?X5 ?X10 ?X11)
+
+p14 < 
+Coq < 
+Coq < 
diff --git a/test-suite/output-coqtop/DependentEvars2.v b/test-suite/output-coqtop/DependentEvars2.v
new file mode 100644
index 0000000000..d0f3a4012e
--- /dev/null
+++ b/test-suite/output-coqtop/DependentEvars2.v
@@ -0,0 +1,27 @@
+Set Printing Dependent Evars Line.
+Lemma strange_imp_trans :
+  forall P Q R : Prop, (Q -> R) -> (P -> Q) -> (P -> Q) -> P -> R.
+Proof.
+  auto.
+Qed.
+
+Lemma modpon : forall P Q : Prop, (P -> Q) /\ P -> Q.
+Proof.
+  tauto.
+Qed.
+
+Section eex.
+  Variables P1 P2 P3 P4 : Prop.
+  Hypothesis p12 : P1 -> P2.
+  Hypothesis p123 : (P1 -> P2) -> P3.
+  Hypothesis p34 : P3 -> P4.
+
+  Lemma p14 : P4.
+  Proof.
+    idtac "Second proof:".
+    eapply strange_imp_trans.
+          {
+            apply modpon.
+          }
+  Abort.
+End eex.
diff --git a/test-suite/output-coqtop/ShowProofDiffs.out b/test-suite/output-coqtop/ShowProofDiffs.out
new file mode 100644
index 0000000000..285a3bcd89
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.out
@@ -0,0 +1,42 @@
+
+Coq < Coq < 1 subgoal
+  
+  ============================
+  [48;2;0;91;0m[48;2;0;141;0;4m[1mforall[22m i : nat, [37mexists[39m j k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k[48;2;0;91;0;24m[0m
+
+x < 
+x < 1 focused subgoal
+(shelved: 1)
+  [48;2;0;91;0m[48;2;0;141;0;4mi : nat[48;2;0;91;0;24m[0m
+  ============================
+  [48;2;0;91;0m[37mexists[39m k : nat[37m,[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m /\[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mj[39m[37m =[39m k[37m /\[39m i[37m =[39m k[0m
+
+[48;2;0;91;0m[48;2;0;141;0;4m([1mfun[22m i : nat =>[49;24m
+ [48;2;0;141;0;4mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mj[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m[0m
+
+x < 1 focused subgoal
+(shelved: 2)
+  i : nat
+  ============================
+  [48;2;0;91;0mi[37m =[39m ?j[37m /\[39m ?j[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[37m /\[39m i[37m =[39m [48;2;0;141;0;4m[94m?[39m[48;2;0;91;0;24m[94mk[39m[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+   [48;2;0;91;0m[48;2;0;141;0;4m[94m?[39m[94mj[39m (ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m[48;2;0;91;0;24m ?j[37m [39m[48;2;0;141;0;4m[37m=[39m k[37m /\[39m i[37m =[39m k) [94m?[39m[94mk[39m[48;2;0;91;0;24m ?Goal[48;2;0;141;0;4m)[48;2;0;91;0;24m)[0m
+
+x < 2 focused subgoals
+(shelved: 2)
+  i : nat
+  ============================
+  [48;2;0;91;0mi[37m =[39m ?j[0m
+
+subgoal 2 is:
+ [48;2;0;91;0m?j[37m =[39m ?k[37m /\[39m i[37m =[39m ?k[0m
+
+[48;2;0;91;0m([1mfun[22m i : nat =>[49m
+ [48;2;0;91;0mex_intro ([1mfun[22m j : nat => [37mexists[39m k : nat[37m,[39m i[37m =[39m j[37m /\[39m j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+   [48;2;0;91;0m?j[49m
+   [48;2;0;91;0m(ex_intro ([1mfun[22m k : nat => i[37m =[39m ?j[37m /\[39m ?j[37m =[39m k[37m /\[39m i[37m =[39m k) [49m
+      [48;2;0;91;0m?k [48;2;0;141;0;4m(conj[48;2;0;91;0;24m ?Goal [48;2;0;141;0;4m[94m?[39m[94mGoal0[39m)[48;2;0;91;0;24m))[0m
+
+x < 
diff --git a/test-suite/output-coqtop/ShowProofDiffs.v b/test-suite/output-coqtop/ShowProofDiffs.v
new file mode 100644
index 0000000000..4251c52cb4
--- /dev/null
+++ b/test-suite/output-coqtop/ShowProofDiffs.v
@@ -0,0 +1,6 @@
+(* coq-prog-args: ("-color" "on" "-diffs" "on") *)
+Lemma x: forall(i : nat), exists(j k : nat), i = j /\ j = k /\ i = k.
+Proof using.
+  eexists.  Show Proof Diffs.
+  eexists.  Show Proof Diffs.
+  split.  Show Proof Diffs.
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 3c1e27ba9d..6704337f80 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -1,14 +1,14 @@
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub _%nat_scope _%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub but avoid exposing match constructs
 Nat.sub is transparent
 Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub _%nat_scope / _%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub when applied to 1 argument
   but avoid exposing match constructs
 Nat.sub is transparent
@@ -16,7 +16,7 @@ Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub !_%nat_scope / _%nat_scope : simpl nomatch
 The reduction tactics unfold Nat.sub
   when the 1st argument evaluates to a constructor and
   when applied to 1 argument but avoid exposing match constructs
@@ -25,7 +25,7 @@ Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub !_%nat_scope !_%nat_scope /
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor and when applied to 2 arguments
 Nat.sub is transparent
@@ -33,7 +33,7 @@ Expands to: Constant Coq.Init.Nat.sub
 Nat.sub : nat -> nat -> nat
 
 Nat.sub is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.sub !_%nat_scope !_%nat_scope
 The reduction tactics unfold Nat.sub when the 1st and
   2nd arguments evaluate to a constructor
 Nat.sub is transparent
@@ -43,37 +43,34 @@ forall D1 C1 : Type,
 (D1 -> C1) -> forall D2 C2 : Type, (D2 -> C2) -> D1 * D2 -> C1 * C2
 
 pf is not universe polymorphic
-Arguments D2, C2 are implicit
-Arguments D1, C1 are implicit and maximally inserted
-Argument scopes are [foo_scope type_scope _ _ _ _ _]
+Arguments pf {D1%foo_scope} {C1%type_scope} _ [D2] [C2] : simpl never
 The reduction tactics never unfold pf
 pf is transparent
 Expands to: Constant Arguments.pf
 fcomp : forall A B C : Type, (B -> C) -> (A -> B) -> A -> C
 
 fcomp is not universe polymorphic
-Arguments A, B, C are implicit and maximally inserted
-Argument scopes are [type_scope type_scope type_scope _ _ _]
+Arguments fcomp {A%type_scope} {B%type_scope} {C%type_scope} _ _ _ /
 The reduction tactics unfold fcomp when applied to 6 arguments
 fcomp is transparent
 Expands to: Constant Arguments.fcomp
 volatile : nat -> nat
 
 volatile is not universe polymorphic
-Argument scope is [nat_scope]
+Arguments volatile / _%nat_scope
 The reduction tactics always unfold volatile
 volatile is transparent
 Expands to: Constant Arguments.volatile
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument scopes are [_ _ nat_scope _ nat_scope]
+Arguments f _ _ _%nat_scope _ _%nat_scope
 f is transparent
 Expands to: Constant Arguments.S1.S2.f
 f : T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument scopes are [_ _ nat_scope _ nat_scope]
+Arguments f _ _ !_%nat_scope !_ !_%nat_scope
 The reduction tactics unfold f when the 3rd, 4th and
   5th arguments evaluate to a constructor
 f is transparent
@@ -81,8 +78,7 @@ Expands to: Constant Arguments.S1.S2.f
 f : forall T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Argument T2 is implicit
-Argument scopes are [type_scope _ _ nat_scope _ nat_scope]
+Arguments f [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
 The reduction tactics unfold f when the 4th, 5th and
   6th arguments evaluate to a constructor
 f is transparent
@@ -90,8 +86,7 @@ Expands to: Constant Arguments.S1.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
-Arguments T1, T2 are implicit
-Argument scopes are [type_scope type_scope _ _ nat_scope _ nat_scope]
+Arguments f [T1%type_scope] [T2%type_scope] _ _ !_%nat_scope !_ !_%nat_scope
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
@@ -103,6 +98,7 @@ Expands to: Constant Arguments.f
 f : forall T1 T2 : Type, T1 -> T2 -> nat -> unit -> nat -> nat
 
 f is not universe polymorphic
+Arguments f _ _ _ _ !_ !_ !_
 The reduction tactics unfold f when the 5th, 6th and
   7th arguments evaluate to a constructor
 f is transparent
@@ -118,7 +114,7 @@ Extra arguments: _, _.
 volatilematch : nat -> nat
 
 volatilematch is not universe polymorphic
-Argument scope is [nat_scope]
+Arguments volatilematch / _%nat_scope : simpl nomatch
 The reduction tactics always unfold volatilematch
   but avoid exposing match constructs
 volatilematch is transparent
diff --git a/test-suite/output/ArgumentsScope.out b/test-suite/output/ArgumentsScope.out
index 69ba329ff1..7b25fd40f8 100644
--- a/test-suite/output/ArgumentsScope.out
+++ b/test-suite/output/ArgumentsScope.out
@@ -1,29 +1,29 @@
 a : bool -> bool
 
 a is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments a _%bool_scope
 Expands to: Variable a
 b : bool -> bool
 
 b is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments b _%bool_scope
 Expands to: Variable b
 negb'' : bool -> bool
 
 negb'' is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb'' _%bool_scope
 negb'' is transparent
 Expands to: Constant ArgumentsScope.A.B.negb''
 negb' : bool -> bool
 
 negb' is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb' _%bool_scope
 negb' is transparent
 Expands to: Constant ArgumentsScope.A.negb'
 negb : bool -> bool
 
 negb is not universe polymorphic
-Argument scope is [bool_scope]
+Arguments negb _%bool_scope
 negb is transparent
 Expands to: Constant Coq.Init.Datatypes.negb
 a : bool -> bool
diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 65c902202d..53d5624f6f 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -13,36 +13,21 @@ where
 ?y : [ |- nat]
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
-For eq_refl: Arguments are renamed to B, y
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments B, y are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument B is implicit
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+Arguments eq {A%type_scope}
+Arguments eq_refl {B%type_scope} {y}, [B] _
 eq_refl : forall (A : Type) (x : A), x = x
 
 eq_refl is not universe polymorphic
-Arguments are renamed to B, y
-When applied to no arguments:
-  Arguments B, y are implicit and maximally inserted
-When applied to 1 argument:
-  Argument B is implicit
-Argument scopes are [type_scope _]
+Arguments eq_refl {B%type_scope} {y}, [B] _
 Expands to: Constructor Coq.Init.Logic.eq_refl
 Inductive myEq (B : Type) (x : A) : A -> Prop :=  myrefl : B -> myEq B x x
 
-For myrefl: Arguments are renamed to C, x, _
-For myrefl: Argument C is implicit and maximally inserted
-For myEq: Argument scopes are [type_scope _ _]
-For myrefl: Argument scopes are [type_scope _ _]
+Arguments myEq _%type_scope
+Arguments myrefl {C%type_scope} x : rename
 myrefl : forall (B : Type) (x : A), B -> myEq B x x
 
 myrefl is not universe polymorphic
-Arguments are renamed to C, x, _
-Argument C is implicit and maximally inserted
-Argument scopes are [type_scope _ _]
+Arguments myrefl {C%type_scope} x : rename
 Expands to: Constructor Arguments_renaming.Test1.myrefl
 myplus = 
 fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
@@ -52,15 +37,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
@@ -70,16 +51,12 @@ Expands to: Constant Arguments_renaming.Test1.myplus
 Inductive myEq (A B : Type) (x : A) : A -> Prop :=
     myrefl : B -> myEq A B x x
 
-For myrefl: Arguments are renamed to A, C, x, _
-For myrefl: Argument C is implicit and maximally inserted
-For myEq: Argument scopes are [type_scope type_scope _ _]
-For myrefl: Argument scopes are [type_scope type_scope _ _]
+Arguments myEq _%type_scope _%type_scope
+Arguments myrefl A%type_scope {C%type_scope} x : rename
 myrefl : forall (A B : Type) (x : A), B -> myEq A B x x
 
 myrefl is not universe polymorphic
-Arguments are renamed to A, C, x, _
-Argument C is implicit and maximally inserted
-Argument scopes are [type_scope type_scope _ _]
+Arguments myrefl A%type_scope {C%type_scope} x : rename
 Expands to: Constructor Arguments_renaming.myrefl
 myrefl
      : forall (A C : Type) (x : A), C -> myEq A C x x
@@ -91,15 +68,11 @@ fix myplus (T : Type) (t : T) (n m : nat) {struct n} : nat :=
   end
      : forall T : Type, T -> nat -> nat -> nat
 
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 myplus : forall T : Type, T -> nat -> nat -> nat
 
 myplus is not universe polymorphic
-Arguments are renamed to Z, t, n, m
-Argument Z is implicit and maximally inserted
-Argument scopes are [type_scope _ nat_scope nat_scope]
+Arguments myplus {Z%type_scope} !t !n%nat_scope m%nat_scope : rename
 The reduction tactics unfold myplus when the 2nd and
   3rd arguments evaluate to a constructor
 myplus is transparent
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index cb835ab48d..7489b8987e 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -7,7 +7,7 @@ fix F (t : t) : P t :=
      : forall P : t -> Type,
        (let x := t in forall x0 : x, P x0 -> P (k x0)) -> forall t : t, P t
 
-Argument scopes are [function_scope function_scope _]
+Arguments t_rect _%function_scope _%function_scope
      = fun d : TT => match d with
                      | {| f3 := b |} => b
                      end
@@ -26,7 +26,7 @@ match Nat.eq_dec x y with
 end
      : forall (x y : nat) (P : nat -> Type), P x -> P y -> P y
 
-Argument scopes are [nat_scope nat_scope function_scope _ _]
+Arguments proj _%nat_scope _%nat_scope _%function_scope
 foo = 
 fix foo (A : Type) (l : list A) {struct l} : option A :=
   match l with
@@ -36,14 +36,14 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
   end
      : forall A : Type, list A -> option A
 
-Argument scopes are [type_scope list_scope]
+Arguments foo _%type_scope _%list_scope
 uncast = 
 fun (A : Type) (x : I A) => match x with
                             | x0 <: _ => x0
                             end
      : forall A : Type, I A -> A
 
-Argument scopes are [type_scope _]
+Arguments uncast _%type_scope
 foo' = if A 0 then true else false
      : bool
 f = 
@@ -82,7 +82,7 @@ lem2 =
 fun dd : bool => if dd as aa return (aa = aa) then eq_refl else eq_refl
      : forall k : bool, k = k
 
-Argument scope is [bool_scope]
+Arguments lem2 _%bool_scope
 lem3 = 
 fun dd : nat * nat => let (bb, cc) as aa return (aa = aa) := dd in eq_refl
      : forall k : nat * nat, k = k
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 4e949dcb04..a040b69b44 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -84,7 +84,6 @@ Print f.
 (* Was enhancement request #5142 (error message reported on the most
    general return clause heuristic) *)
 
-#[universes(template)]
 Inductive gadt : Type -> Type :=
 | gadtNat : nat -> gadt nat
 | gadtTy : forall T, T -> gadt T.
diff --git a/test-suite/output/Coercions.v b/test-suite/output/Coercions.v
index 6976f35a88..0e84bf3966 100644
--- a/test-suite/output/Coercions.v
+++ b/test-suite/output/Coercions.v
@@ -1,7 +1,7 @@
 (* Submitted by Randy Pollack *)
 
-#[universes(template)] Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
-#[universes(template)] Record rel (S : Set) : Type :=  {sr_rel :> S -> S -> Prop}.
+Record pred (S : Set) : Type :=  {sp_pred :> S -> Prop}.
+Record rel (S : Set) : Type :=  {sr_rel :> S -> S -> Prop}.
 
 Section testSection.
 Variables (S : Set) (P : pred S) (R : rel S) (x : S).
diff --git a/test-suite/output/Emacs_and_diffs.out b/test-suite/output/Emacs_and_diffs.out
new file mode 100644
index 0000000000..e69de29bb2
--- /dev/null
+++ b/test-suite/output/Emacs_and_diffs.out
diff --git a/test-suite/output/Emacs_and_diffs.v b/test-suite/output/Emacs_and_diffs.v
new file mode 100644
index 0000000000..c35fd1a11b
--- /dev/null
+++ b/test-suite/output/Emacs_and_diffs.v
@@ -0,0 +1,3 @@
+(* coq-prog-args: ("-emacs") *)
+Set Diffs "on".
+(* verify this does not produce an error message *)
diff --git a/test-suite/output/Extraction_matchs_2413.v b/test-suite/output/Extraction_matchs_2413.v
index f9398fdca9..1ecd9771eb 100644
--- a/test-suite/output/Extraction_matchs_2413.v
+++ b/test-suite/output/Extraction_matchs_2413.v
@@ -101,7 +101,7 @@ Section decoder_result.
 
  Variable inst : Type.
 
- #[universes(template)] Inductive decoder_result : Type :=
+ Inductive decoder_result : Type :=
  | DecUndefined : decoder_result
  | DecUnpredictable : decoder_result
  | DecInst : inst -> decoder_result
diff --git a/test-suite/output/Fixpoint.v b/test-suite/output/Fixpoint.v
index 9b25c2dbd3..61ae4edbd1 100644
--- a/test-suite/output/Fixpoint.v
+++ b/test-suite/output/Fixpoint.v
@@ -44,7 +44,7 @@ fix even_pos_odd_pos 2 with (odd_pos_even_pos n (H:odd n) {struct H} : n >= 1).
   omega.
 Qed.
 
-#[universes(template)] CoInductive Inf := S { projS : Inf }.
+CoInductive Inf := S { projS : Inf }.
 Definition expand_Inf (x : Inf) := S (projS x).
 CoFixpoint inf := S inf.
 Eval compute in inf.
diff --git a/test-suite/output/FloatExtraction.out b/test-suite/output/FloatExtraction.out
new file mode 100644
index 0000000000..cfd6633752
--- /dev/null
+++ b/test-suite/output/FloatExtraction.out
@@ -0,0 +1,67 @@
+
+(** val infinity : Float64.t **)
+
+let infinity =
+  (Float64.of_float (infinity))
+
+(** val neg_infinity : Float64.t **)
+
+let neg_infinity =
+  (Float64.of_float (neg_infinity))
+
+(** val nan : Float64.t **)
+
+let nan =
+  (Float64.of_float (nan))
+
+(** val one : Float64.t **)
+
+let one =
+  (Float64.of_float (0x1p+0))
+
+(** val zero : Float64.t **)
+
+let zero =
+  (Float64.of_float (0x0p+0))
+
+(** val two : Float64.t **)
+
+let two =
+  (Float64.of_float (0x1p+1))
+
+(** val list_floats : Float64.t list **)
+
+let list_floats =
+  nan :: (infinity :: (neg_infinity :: (zero :: (one :: (two :: ((Float64.of_float (0x1p-1)) :: ((Float64.of_float (0x1.47ae147ae147bp-7)) :: ((Float64.of_float (-0x1p-1)) :: ((Float64.of_float (-0x1.47ae147ae147bp-7)) :: ((Float64.of_float (0x1.e42d130773b76p+1023)) :: ((Float64.of_float (-0x0.c396c98f8d899p-1022)) :: [])))))))))))
+
+
+(** val sqrt : Float64.t -> Float64.t **)
+
+let sqrt = Float64.sqrt
+
+(** val opp : Float64.t -> Float64.t **)
+
+let opp = Float64.opp
+
+(** val mul : Float64.t -> Float64.t -> Float64.t **)
+
+let mul = Float64.mul
+
+(** val sub : Float64.t -> Float64.t -> Float64.t **)
+
+let sub = Float64.sub
+
+(** val div : Float64.t -> Float64.t -> Float64.t **)
+
+let div = Float64.div
+
+(** val discr : Float64.t -> Float64.t -> Float64.t -> Float64.t **)
+
+let discr a b c =
+  sub (mul b b) (mul (mul (Float64.of_float (0x1p+2)) a) c)
+
+(** val x1 : Float64.t -> Float64.t -> Float64.t -> Float64.t **)
+
+let x1 a b c =
+  div (sub (opp b) (sqrt (discr a b c))) (mul (Float64.of_float (0x1p+1)) a)
+
diff --git a/test-suite/output/FloatExtraction.v b/test-suite/output/FloatExtraction.v
new file mode 100644
index 0000000000..f296e8e871
--- /dev/null
+++ b/test-suite/output/FloatExtraction.v
@@ -0,0 +1,33 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+Require Import Floats ExtrOCamlFloats.
+
+Require Import List. Import ListNotations.
+
+(* from Require Import ExtrOcamlBasic. *)
+Extract Inductive list => list [ "[]" "( :: )" ].
+
+Local Open Scope float_scope.
+
+(* Avoid exponents with less than three digits as they are usually
+   displayed with two digits (1e7 is displayed 1e+07) except on
+   Windows where three digits are used (1e+007). *)
+Definition list_floats :=
+  [nan; infinity; neg_infinity; zero; one; two;
+   0.5; 0.01; -0.5; -0.01; 1.7e+308; -1.7e-308].
+
+Recursive Extraction list_floats.
+
+Definition discr a b c := b * b - 4.0 * a * c.
+
+Definition x1 a b c := (- b - sqrt (discr a b c)) / (2.0 * a).
+
+Recursive Extraction x1.
diff --git a/test-suite/output/FloatSyntax.out b/test-suite/output/FloatSyntax.out
new file mode 100644
index 0000000000..668a55977d
--- /dev/null
+++ b/test-suite/output/FloatSyntax.out
@@ -0,0 +1,40 @@
+2%float
+     : float
+2.5%float
+     : float
+(-2.5)%float
+     : float
+2.4999999999999999e+123%float
+     : float
+(-2.5000000000000001e-123)%float
+     : float
+(2 + 2)%float
+     : float
+(2.5 + 2.5)%float
+     : float
+2
+     : float
+2.5
+     : float
+-2.5
+     : float
+2.4999999999999999e+123
+     : float
+-2.5000000000000001e-123
+     : float
+2 + 2
+     : float
+2.5 + 2.5
+     : float
+2
+     : nat
+2%float
+     : float
+t = 2%flt
+     : float
+t = 2%flt
+     : float
+2
+     : nat
+2
+     : float
diff --git a/test-suite/output/FloatSyntax.v b/test-suite/output/FloatSyntax.v
new file mode 100644
index 0000000000..85f611352c
--- /dev/null
+++ b/test-suite/output/FloatSyntax.v
@@ -0,0 +1,37 @@
+Require Import Floats.
+
+Check 2%float.
+Check 2.5%float.
+Check (-2.5)%float.
+(* Avoid exponents with less than three digits as they are usually
+   displayed with two digits (1e7 is displayed 1e+07) except on
+   Windows where three digits are used (1e+007). *)
+Check 2.5e123%float.
+Check (-2.5e-123)%float.
+Check (2 + 2)%float.
+Check (2.5 + 2.5)%float.
+
+Open Scope float_scope.
+
+Check 2.
+Check 2.5.
+Check (-2.5).
+Check 2.5e123.
+Check (-2.5e-123).
+Check (2 + 2).
+Check (2.5 + 2.5).
+
+Open Scope nat_scope.
+
+Check 2.
+Check 2%float.
+
+Delimit Scope float_scope with flt.
+Definition t := 2%float.
+Print t.
+Delimit Scope nat_scope with float.
+Print t.
+Check 2.
+Close Scope nat_scope.
+Check 2.
+Close Scope float_scope.
diff --git a/test-suite/output/Implicit.out b/test-suite/output/Implicit.out
index 3b65003c29..d65d2a8f55 100644
--- a/test-suite/output/Implicit.out
+++ b/test-suite/output/Implicit.out
@@ -5,8 +5,7 @@ ex_intro (P:=fun _ : nat => True) (x:=0) I
 d2 = fun x : nat => d1 (y:=x)
      : forall x x0 : nat, x0 = x -> x0 = x
 
-Arguments x, x0 are implicit
-Argument scopes are [nat_scope nat_scope _]
+Arguments d2 [x%nat_scope] [x0%nat_scope]
 map id (1 :: nil)
      : list nat
 map id' (1 :: nil)
diff --git a/test-suite/output/Inductive.out b/test-suite/output/Inductive.out
index af202ea01c..8ff571ae55 100644
--- a/test-suite/output/Inductive.out
+++ b/test-suite/output/Inductive.out
@@ -3,5 +3,5 @@ Last occurrence of "list'" must have "A" as 1st argument in
  "A -> list' A -> list' (A * A)%type".
 Inductive foo (A : Type) (x : A) (y : A := x) : Prop :=  Foo : foo A x
 
-For foo: Argument scopes are [type_scope _]
-For Foo: Argument scopes are [type_scope _]
+Arguments foo _%type_scope
+Arguments Foo _%type_scope
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out
index c17c63e724..ce058a6d34 100644
--- a/test-suite/output/InitSyntax.out
+++ b/test-suite/output/InitSyntax.out
@@ -1,11 +1,8 @@
 Inductive sig2 (A : Type) (P Q : A -> Prop) : Type :=
     exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x}
 
-For sig2: Argument A is implicit
-For exist2: Argument A is implicit
-For sig2: Argument scopes are [type_scope type_scope type_scope]
-For exist2: Argument scopes are [type_scope function_scope function_scope _ _
-              _]
+Arguments sig2 [A%type_scope] _%type_scope _%type_scope
+Arguments exist2 [A%type_scope] _%function_scope _%function_scope
 exists x : nat, x = x
      : Prop
 fun b : bool => if b then b else b
diff --git a/test-suite/output/MExtraction.v b/test-suite/output/MExtraction.v
index c0ef9b392d..668be1fdbc 100644
--- a/test-suite/output/MExtraction.v
+++ b/test-suite/output/MExtraction.v
@@ -1,14 +1,65 @@
-Require Import micromega.MExtraction.
-Require Import RingMicromega.
-Require Import QArith.
-Require Import VarMap.
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+(*                                                                      *)
+(* Micromega: A reflexive tactic using the Positivstellensatz           *)
+(*                                                                      *)
+(*  Frédéric Besson (Irisa/Inria) 2006-2008                             *)
+(*                                                                      *)
+(************************************************************************)
+
+(* Used to generate micromega.ml *)
+
+Require Extraction.
 Require Import ZMicromega.
 Require Import QMicromega.
 Require Import RMicromega.
+Require Import VarMap.
+Require Import RingMicromega.
+Require Import NArith.
+Require Import QArith.
+
+Extract Inductive prod => "( * )" [ "(,)" ].
+Extract Inductive list => list [ "[]" "(::)" ].
+Extract Inductive bool => bool [ true false ].
+Extract Inductive sumbool => bool [ true false ].
+Extract Inductive option => option [ Some None ].
+Extract Inductive sumor => option [ Some None ].
+(** Then, in a ternary alternative { }+{ }+{ },
+   -  leftmost choice (Inleft Left) is (Some true),
+   -  middle choice (Inleft Right) is (Some false),
+   -  rightmost choice (Inright) is (None) *)
+
+
+(** To preserve its laziness, andb is normally expanded.
+    Let's rather use the ocaml && *)
+Extract Inlined Constant andb => "(&&)".
+
+Import Reals.Rdefinitions.
+
+Extract Constant R => "int".
+Extract Constant R0 => "0".
+Extract Constant R1 => "1".
+Extract Constant Rplus => "( + )".
+Extract Constant Rmult => "( * )".
+Extract Constant Ropp  => "fun x -> - x".
+Extract Constant Rinv   => "fun x -> 1 / x".
 
+(** In order to avoid annoying build dependencies the actual
+    extraction is only performed as a test in the test suite. *)
 Recursive Extraction
-Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
-           ZMicromega.cnfZ ZMicromega.Zeval_const ZMicromega.bound_problem_fr QMicromega.cnfQ
+           Tauto.mapX Tauto.foldA Tauto.collect_annot Tauto.ids_of_formula Tauto.map_bformula
+           Tauto.abst_form
+           ZMicromega.cnfZ ZMicromega.bound_problem_fr ZMicromega.Zeval_const QMicromega.cnfQ
            List.map simpl_cone (*map_cone  indexes*)
            denorm Qpower vm_add
    normZ normQ normQ n_of_Z N.of_nat ZTautoChecker ZWeakChecker QTautoChecker RTautoChecker find.
+(* Local Variables: *)
+(* coding: utf-8 *)
+(* End: *)
diff --git a/test-suite/output/NoAxiomFromR.out b/test-suite/output/NoAxiomFromR.out
new file mode 100644
index 0000000000..7d7c521343
--- /dev/null
+++ b/test-suite/output/NoAxiomFromR.out
@@ -0,0 +1 @@
+Closed under the global context
diff --git a/test-suite/output/NoAxiomFromR.v b/test-suite/output/NoAxiomFromR.v
new file mode 100644
index 0000000000..9cf6879699
--- /dev/null
+++ b/test-suite/output/NoAxiomFromR.v
@@ -0,0 +1,10 @@
+Require Import Psatz.
+
+Inductive TT : Set :=
+| C : nat -> TT.
+
+Lemma lem4 : forall (n m : nat),
+S m <= m -> C (S m) <> C n -> False.
+Proof. firstorder. Qed.
+
+Print Assumptions lem4.
diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out
index d32cf67e28..abada44da7 100644
--- a/test-suite/output/Notations3.out
+++ b/test-suite/output/Notations3.out
@@ -230,7 +230,7 @@ fun l : list nat => match l with
                     end
      : list nat -> list nat
 
-Argument scope is [list_scope]
+Arguments foo _%list_scope
 Notation
 "'exists' x .. y , p" := ex (fun x => .. (ex (fun y => p)) ..) : type_scope
 (default interpretation)
diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v
index 29614c032a..aeebc0f98b 100644
--- a/test-suite/output/Notations3.v
+++ b/test-suite/output/Notations3.v
@@ -123,7 +123,7 @@ Check fun n => foo4 n (fun x y z => (fun _ => y=0) z).
 (**********************************************************************)
 (* Test printing of #4932                                             *)
 
-#[universes(template)] Inductive ftele : Type :=
+Inductive ftele : Type :=
 | fb {T:Type} : T -> ftele
 | fr {T} : (T -> ftele) -> ftele.
 
diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out
index c1b9a2b1c6..ba4ac5a8f9 100644
--- a/test-suite/output/Notations4.out
+++ b/test-suite/output/Notations4.out
@@ -57,3 +57,5 @@ where
      |- Type] (pat, p0, p cannot be used)
 ?T0 : [y : nat  pat : ?T0 * nat  p0 : ?T0 * nat  p := p0 : ?T0 * nat
       |- Type] (pat, p0, p cannot be used)
+fun '{| |} => true
+     : R -> bool
diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v
index d1063bfd04..4b9d0abd95 100644
--- a/test-suite/output/Notations4.v
+++ b/test-suite/output/Notations4.v
@@ -133,3 +133,10 @@ Check fun y : nat => # (x,z) |-> y & y.
 Check fun y : nat => # (x,z) |-> (x + y) & (y + z).
 
 End K.
+
+Module EmptyRecordSyntax.
+
+Record R := { n : nat }.
+Check fun '{|n:=x|} => true.
+
+End EmptyRecordSyntax.
diff --git a/test-suite/output/NumeralNotations.out b/test-suite/output/NumeralNotations.out
index 460c77879c..505dc52ebe 100644
--- a/test-suite/output/NumeralNotations.out
+++ b/test-suite/output/NumeralNotations.out
@@ -180,3 +180,41 @@ let v := 4%Zlike in v : Zlike
      : Zlike
 0%Zlike
      : Zlike
+let v := 0%kt in v : ty
+     : ty
+let v := 1%kt in v : ty
+     : ty
+let v := 2%kt in v : ty
+     : ty
+let v := 3%kt in v : ty
+     : ty
+let v := 4%kt in v : ty
+     : ty
+let v := 5%kt in v : ty
+     : ty
+The command has indeed failed with message:
+Cannot interpret this number as a value of type ty
+     = 0%kt
+     : ty
+     = 1%kt
+     : ty
+     = 2%kt
+     : ty
+     = 3%kt
+     : ty
+     = 4%kt
+     : ty
+     = 5%kt
+     : ty
+let v : ty := Build_ty Empty_set zero in v : ty
+     : ty
+let v : ty := Build_ty unit one in v : ty
+     : ty
+let v : ty := Build_ty bool two in v : ty
+     : ty
+let v : ty := Build_ty Prop prop in v : ty
+     : ty
+let v : ty := Build_ty Set set in v : ty
+     : ty
+let v : ty := Build_ty Type type in v : ty
+     : ty
diff --git a/test-suite/output/NumeralNotations.v b/test-suite/output/NumeralNotations.v
index 44805ad09d..c306b15ef3 100644
--- a/test-suite/output/NumeralNotations.v
+++ b/test-suite/output/NumeralNotations.v
@@ -391,3 +391,68 @@ Module Test19.
   Check {| summands := (cons 1 (cons 2 (cons (-1) nil)))%Z |}.
   Check {| summands := nil |}.
 End Test19.
+
+Module Test20.
+  (** Test Sorts *)
+  Local Set Universe Polymorphism.
+  Inductive known_type : Type -> Type :=
+  | prop : known_type Prop
+  | set : known_type Set
+  | type : known_type Type
+  | zero : known_type Empty_set
+  | one : known_type unit
+  | two : known_type bool.
+
+  Existing Class known_type.
+  Existing Instances zero one two prop.
+  Existing Instance set | 2.
+  Existing Instance type | 4.
+
+  Record > ty := { t : Type ; kt : known_type t }.
+
+  Definition ty_of_uint (x : Decimal.uint) : option ty
+    := match Nat.of_uint x with
+       | 0 => @Some ty zero
+       | 1 => @Some ty one
+       | 2 => @Some ty two
+       | 3 => @Some ty prop
+       | 4 => @Some ty set
+       | 5 => @Some ty type
+       | _ => None
+       end.
+  Definition uint_of_ty (x : ty) : Decimal.uint
+    := Nat.to_uint match kt x with
+                   | prop => 3
+                   | set => 4
+                   | type => 5
+                   | zero => 0
+                   | one => 1
+                   | two => 2
+                   end.
+
+  Declare Scope kt_scope.
+  Delimit Scope kt_scope with kt.
+
+  Numeral Notation ty ty_of_uint uint_of_ty : kt_scope.
+
+  Check let v := 0%kt in v : ty.
+  Check let v := 1%kt in v : ty.
+  Check let v := 2%kt in v : ty.
+  Check let v := 3%kt in v : ty.
+  Check let v := 4%kt in v : ty.
+  Check let v := 5%kt in v : ty.
+  Fail Check let v := 6%kt in v : ty.
+  Eval cbv in (_ : known_type Empty_set) : ty.
+  Eval cbv in (_ : known_type unit) : ty.
+  Eval cbv in (_ : known_type bool) : ty.
+  Eval cbv in (_ : known_type Prop) : ty.
+  Eval cbv in (_ : known_type Set) : ty.
+  Eval cbv in (_ : known_type Type) : ty.
+  Local Set Printing All.
+  Check let v := 0%kt in v : ty.
+  Check let v := 1%kt in v : ty.
+  Check let v := 2%kt in v : ty.
+  Check let v := 3%kt in v : ty.
+  Check let v := 4%kt in v : ty.
+  Check let v := 5%kt in v : ty.
+End Test20.
diff --git a/test-suite/output/PatternsInBinders.out b/test-suite/output/PatternsInBinders.out
index 8a6d94c732..2952b6d94b 100644
--- a/test-suite/output/PatternsInBinders.out
+++ b/test-suite/output/PatternsInBinders.out
@@ -15,8 +15,7 @@ swap =
 fun (A B : Type) '(x, y) => (y, x)
      : forall A B : Type, A * B -> B * A
 
-Arguments A, B are implicit and maximally inserted
-Argument scopes are [type_scope type_scope _]
+Arguments swap {A%type_scope} {B%type_scope}
 fun (A B : Type) '(x, y) => swap (x, y) = (y, x)
      : forall A B : Type, A * B -> Prop
 forall (A B : Type) '(x, y), swap (x, y) = (y, x)
@@ -42,6 +41,6 @@ fun (pat : nat) '(x, y) => x + y = pat
 f = fun x : nat => x + x
      : nat -> nat
 
-Argument scope is [nat_scope]
+Arguments f _%nat_scope
 fun x : nat => x + x
      : nat -> nat
diff --git a/test-suite/output/PatternsInBinders.v b/test-suite/output/PatternsInBinders.v
index 0c1b08f5a3..d671053c07 100644
--- a/test-suite/output/PatternsInBinders.v
+++ b/test-suite/output/PatternsInBinders.v
@@ -53,7 +53,7 @@ Module Suboptimal.
 (** This test shows an example which exposes the [let] introduced by
     the pattern notation in binders. *)
 
-#[universes(template)] Inductive Fin (n:nat) := Z : Fin n.
+Inductive Fin (n:nat) := Z : Fin n.
 Definition F '(n,p) : Type := (Fin n * Fin p)%type.
 Definition both_z '(n,p) : F (n,p) := (Z _,Z _).
 Print both_z.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index ab4172711e..7d0d81a3e8 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -1,36 +1,24 @@
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
-existT is template universe polymorphic
-Argument A is implicit
-Argument scopes are [type_scope function_scope _ _]
+existT is template universe polymorphic on sigT.u0 sigT.u1
+Arguments existT [A%type_scope] _%function_scope
 Expands to: Constructor Coq.Init.Specif.existT
 Inductive sigT (A : Type) (P : A -> Type) : Type :=
     existT : forall x : A, P x -> {x : A & P x}
 
-For sigT: Argument A is implicit
-For existT: Argument A is implicit
-For sigT: Argument scopes are [type_scope type_scope]
-For existT: Argument scopes are [type_scope function_scope _ _]
+Arguments sigT [A%type_scope] _%type_scope
+Arguments existT [A%type_scope] _%function_scope
 existT : forall (A : Type) (P : A -> Type) (x : A), P x -> {x : A & P x}
 
 Argument A is implicit
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument A is implicit
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+Arguments eq {A%type_scope}
+Arguments eq_refl {A%type_scope} {x}, [A] _
 eq_refl : forall (A : Type) (x : A), x = x
 
 eq_refl is not universe polymorphic
-When applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-When applied to 1 argument:
-  Argument A is implicit
-Argument scopes are [type_scope _]
+Arguments eq_refl {A%type_scope} {x}, [A] _
 Expands to: Constructor Coq.Init.Logic.eq_refl
 eq_refl : forall (A : Type) (x : A), x = x
 
@@ -46,11 +34,11 @@ fix add (n m : nat) {struct n} : nat :=
   end
      : nat -> nat -> nat
 
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.add _%nat_scope _%nat_scope
 Nat.add : nat -> nat -> nat
 
 Nat.add is not universe polymorphic
-Argument scopes are [nat_scope nat_scope]
+Arguments Nat.add _%nat_scope _%nat_scope
 Nat.add is transparent
 Expands to: Constant Coq.Init.Nat.add
 Nat.add : nat -> nat -> nat
@@ -58,17 +46,15 @@ Nat.add : nat -> nat -> nat
 plus_n_O : forall n : nat, n = n + 0
 
 plus_n_O is not universe polymorphic
-Argument scope is [nat_scope]
+Arguments plus_n_O _%nat_scope
 plus_n_O is opaque
 Expands to: Constant Coq.Init.Peano.plus_n_O
 Inductive le (n : nat) : nat -> Prop :=
     le_n : n <= n | le_S : forall m : nat, n <= m -> n <= S m
 
-For le_S: Argument m is implicit
-For le_S: Argument n is implicit and maximally inserted
-For le: Argument scopes are [nat_scope nat_scope]
-For le_n: Argument scope is [nat_scope]
-For le_S: Argument scopes are [nat_scope nat_scope _]
+Arguments le _%nat_scope _%nat_scope
+Arguments le_n _%nat_scope
+Arguments le_S {n%nat_scope} [m%nat_scope]
 comparison : Set
 
 comparison is not universe polymorphic
@@ -81,26 +67,21 @@ bar is not universe polymorphic
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
-Argument x is implicit and maximally inserted
+Arguments bar {x}
 Expands to: Constant PrintInfos.bar
 *** [ bar : foo ]
 
 Expanded type for implicit arguments
 bar : forall x : nat, x = 0
 
-Argument x is implicit and maximally inserted
+Arguments bar {x}
 Module Coq.Init.Peano
 Notation sym_eq := eq_sym
 Expands to: Notation Coq.Init.Logic.sym_eq
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
-For eq: Argument A is implicit and maximally inserted
-For eq_refl, when applied to no arguments:
-  Arguments A, x are implicit and maximally inserted
-For eq_refl, when applied to 1 argument:
-  Argument A is implicit and maximally inserted
-For eq: Argument scopes are [type_scope _ _]
-For eq_refl: Argument scopes are [type_scope _]
+Arguments eq {A%type_scope}
+Arguments eq_refl {A%type_scope} {x}, {A} _
 n:nat
 
 Hypothesis of the goal context.
diff --git a/test-suite/output/Projections.v b/test-suite/output/Projections.v
index 35f36e87d7..14d63d39c4 100644
--- a/test-suite/output/Projections.v
+++ b/test-suite/output/Projections.v
@@ -6,7 +6,7 @@ Class HostFunction := host_func : Type.
 
 Section store.
   Context `{HostFunction}.
-  #[universes(template)] Record store := { store_funcs : host_func }.
+  Record store := { store_funcs : host_func }.
 End store.
 
 Check (fun (S:@store nat) => S.(store_funcs)).
diff --git a/test-suite/output/Record.v b/test-suite/output/Record.v
index 4fe7b051f8..d9a649fadc 100644
--- a/test-suite/output/Record.v
+++ b/test-suite/output/Record.v
@@ -20,12 +20,12 @@ Check {| field := 5 |}.
 Check build_r 5.
 Check build_c 5.
 
-#[universes(template)] Record N := C { T : Type; _ : True }.
+Record N := C { T : Type; _ : True }.
 Check fun x:N => let 'C _ p := x in p.
 Check fun x:N => let 'C T _ := x in T.
 Check fun x:N => let 'C T p := x in (T,p).
 
-#[universes(template)] Record M := D { U : Type; a := 0; q : True }.
+Record M := D { U : Type; a := 0; q : True }.
 Check fun x:M => let 'D T _ p := x in p.
 Check fun x:M => let 'D T _ p := x in T.
 Check fun x:M => let 'D T p := x in (T,p).
diff --git a/test-suite/output/ShowMatch.v b/test-suite/output/ShowMatch.v
index 99183f2064..9cf6ad35b8 100644
--- a/test-suite/output/ShowMatch.v
+++ b/test-suite/output/ShowMatch.v
@@ -3,12 +3,12 @@
 *)
 
 Module A.
-  #[universes(template)] Inductive foo := f.
+  Inductive foo := f.
   Show Match foo. (* no need to disambiguate *)
 End A. 
 
 Module B.
-  #[universes(template)] Inductive foo := f.
+  Inductive foo := f.
   (* local foo shadows A.foo, so constructor "f" needs disambiguation *)
   Show Match A.foo. 
 End B.
diff --git a/test-suite/output/StringSyntax.out b/test-suite/output/StringSyntax.out
index 9366113c0c..e9cf4282dc 100644
--- a/test-suite/output/StringSyntax.out
+++ b/test-suite/output/StringSyntax.out
@@ -433,7 +433,7 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_rect _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 byte_rec = 
 fun P : byte -> Set => byte_rect P
      : forall P : byte -> Set,
@@ -607,7 +607,7 @@ fun P : byte -> Set => byte_rect P
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_rec _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 byte_ind = 
 fun (P : byte -> Prop) (f : P "000") (f0 : P "001") (f1 : P "002") (f2 : P "003") (f3 : P "004") (f4 : P "005") (f5 : P "006") (f6 : P "007") (f7 : P "008") (f8 : P "009") (f9 : P "010") (f10 : P "011") (f11 : P "012") (f12 : P "013") (f13 : P "014") (f14 : P "015") (f15 : P "016") (f16 : P "017") (f17 : P "018") (f18 : P "019") (f19 : P "020") (f20 : P "021") (f21 : P "022") (f22 : P "023") (f23 : P "024") (f24 : P "025") (f25 : P "026") (f26 : P "027") (f27 : P "028") (f28 : P "029") (f29 : P "030") (f30 : P "031") (f31 : P " ") (f32 : P "!") (f33 : P """") (f34 : P "#") (f35 : P "$") (f36 : P "%") (f37 : P "&") (f38 : P "'") (f39 : P "(") (f40 : P ")") (f41 : P "*") (f42 : P "+") (f43 : P ",") (f44 : P "-") (f45 : P ".") (f46 : P "/") (f47 : P "0") (f48 : P "1") (f49 : P "2") (f50 : P "3") (f51 : P "4") (f52 : P "5") (f53 : P "6") (f54 : P "7") (f55 : P "8") (f56 : P "9") (f57 : P ":") (f58 : P ";") (f59 : P "<") (f60 : P "=") (f61 : P ">") (f62 : P "?") 
   (f63 : P "@") (f64 : P "A") (f65 : P "B") (f66 : P "C") (f67 : P "D") (f68 : P "E") (f69 : P "F") (f70 : P "G") (f71 : P "H") (f72 : P "I") (f73 : P "J") (f74 : P "K") (f75 : P "L") (f76 : P "M") (f77 : P "N") (f78 : P "O") (f79 : P "P") (f80 : P "Q") (f81 : P "R") (f82 : P "S") (f83 : P "T") (f84 : P "U") (f85 : P "V") (f86 : P "W") (f87 : P "X") (f88 : P "Y") (f89 : P "Z") (f90 : P "[") (f91 : P "\") (f92 : P "]") (f93 : P "^") (f94 : P "_") (f95 : P "`") (f96 : P "a") (f97 : P "b") (f98 : P "c") (f99 : P "d") (f100 : P "e") (f101 : P "f") (f102 : P "g") (f103 : P "h") (f104 : P "i") (f105 : P "j") (f106 : P "k") (f107 : P "l") (f108 : P "m") (f109 : P "n") (f110 : P "o") (f111 : P "p") (f112 : P "q") (f113 : P "r") (f114 : P "s") (f115 : P "t") (f116 : P "u") (f117 : P "v") (f118 : P "w") (f119 : P "x") (f120 : P "y") (f121 : P "z") (f122 : P "{") (f123 : P "|") (f124 : P "}") (f125 : P "~") (f126 : P "127") (f127 : P "128") (f128 : P "129") (f129 : P "130") 
@@ -1043,7 +1043,7 @@ end
        P "167" ->
        P "168" -> P "169" -> P "170" -> P "171" -> P "172" -> P "173" -> P "174" -> P "175" -> P "176" -> P "177" -> P "178" -> P "179" -> P "180" -> P "181" -> P "182" -> P "183" -> P "184" -> P "185" -> P "186" -> P "187" -> P "188" -> P "189" -> P "190" -> P "191" -> P "192" -> P "193" -> P "194" -> P "195" -> P "196" -> P "197" -> P "198" -> P "199" -> P "200" -> P "201" -> P "202" -> P "203" -> P "204" -> P "205" -> P "206" -> P "207" -> P "208" -> P "209" -> P "210" -> P "211" -> P "212" -> P "213" -> P "214" -> P "215" -> P "216" -> P "217" -> P "218" -> P "219" -> P "220" -> P "221" -> P "222" -> P "223" -> P "224" -> P "225" -> P "226" -> P "227" -> P "228" -> P "229" -> P "230" -> P "231" -> P "232" -> P "233" -> P "234" -> P "235" -> P "236" -> P "237" -> P "238" -> P "239" -> P "240" -> P "241" -> P "242" -> P "243" -> P "244" -> P "245" -> P "246" -> P "247" -> P "248" -> P "249" -> P "250" -> P "251" -> P "252" -> P "253" -> P "254" -> P "255" -> forall b : byte, P b
 
-Argument scopes are [function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ byte_scope]
+Arguments byte_ind _%function_scope _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _%byte_scope
 "000"
      : byte
 "a"
diff --git a/test-suite/output/Tactics.out b/test-suite/output/Tactics.out
index 19c9fc4423..70427220ed 100644
--- a/test-suite/output/Tactics.out
+++ b/test-suite/output/Tactics.out
@@ -6,3 +6,4 @@ The command has indeed failed with message:
 H is already used.
 The command has indeed failed with message:
 H is already used.
+a
diff --git a/test-suite/output/Tactics.v b/test-suite/output/Tactics.v
index fa12f09a46..96b6d652c9 100644
--- a/test-suite/output/Tactics.v
+++ b/test-suite/output/Tactics.v
@@ -22,3 +22,11 @@ intros H.
 Fail intros [H%myid ?].
 Fail destruct 1 as [H%myid ?].
 Abort.
+
+
+(* Test that assert_succeeds only runs a tactic once *)
+Ltac should_not_loop := idtac + should_not_loop.
+Goal True.
+  assert_succeeds should_not_loop.
+  assert_succeeds (idtac "a" + idtac "b"). (* should only output "a" *)
+Abort.
diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out
index 222a808768..298a0789c4 100644
--- a/test-suite/output/UnivBinders.out
+++ b/test-suite/output/UnivBinders.out
@@ -4,44 +4,43 @@ Record PWrap (A : Type@{u}) : Type@{u} := pwrap { punwrap : A }
 (* u |=  *)
 
 PWrap has primitive projections with eta conversion.
-For PWrap: Argument scope is [type_scope]
-For pwrap: Argument scopes are [type_scope _]
+Arguments PWrap _%type_scope
+Arguments pwrap _%type_scope
 punwrap@{u} = 
 fun (A : Type@{u}) (p : PWrap@{u} A) => punwrap _ p
      : forall A : Type@{u}, PWrap@{u} A -> A
 (* u |=  *)
 
-Argument scopes are [type_scope _]
+Arguments punwrap _%type_scope
 Record RWrap (A : Type@{u}) : Type@{u} := rwrap { runwrap : A }
 (* u |=  *)
 
-For RWrap: Argument scope is [type_scope]
-For rwrap: Argument scopes are [type_scope _]
+Arguments RWrap _%type_scope
+Arguments rwrap _%type_scope
 runwrap@{u} = 
 fun (A : Type@{u}) (r : RWrap@{u} A) => let (runwrap) := r in runwrap
      : forall A : Type@{u}, RWrap@{u} A -> A
 (* u |=  *)
 
-Argument scopes are [type_scope _]
+Arguments runwrap _%type_scope
 Wrap@{u} = fun A : Type@{u} => A
      : Type@{u} -> Type@{u}
 (* u |=  *)
 
-Argument scope is [type_scope]
+Arguments Wrap _%type_scope
 wrap@{u} = 
 fun (A : Type@{u}) (Wrap : Wrap@{u} A) => Wrap
      : forall A : Type@{u}, Wrap@{u} A -> A
 (* u |=  *)
 
-Arguments A, Wrap are implicit and maximally inserted
-Argument scopes are [type_scope _]
+Arguments wrap {A%type_scope} {Wrap}
 bar@{u} = nat
      : Wrap@{u} Set
 (* u |= Set < u *)
-foo@{u UnivBinders.17 v} = 
-Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.17+1,v+1)}
-(* u UnivBinders.17 v |=  *)
+foo@{u UnivBinders.18 v} = 
+Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,UnivBinders.18+1,v+1)}
+(* u UnivBinders.18 v |=  *)
 Type@{i} -> Type@{j}
      : Type@{max(i+1,j+1)}
 (* {j i} |=  *)
@@ -68,32 +67,32 @@ mono
 The command has indeed failed with message:
 Universe u already exists.
 bobmorane = 
-let tt := Type@{UnivBinders.32} in
-let ff := Type@{UnivBinders.34} in tt -> ff
-     : Type@{max(UnivBinders.31,UnivBinders.33)}
+let tt := Type@{UnivBinders.34} in
+let ff := Type@{UnivBinders.36} in tt -> ff
+     : Type@{max(UnivBinders.33,UnivBinders.35)}
 The command has indeed failed with message:
 Universe u already bound.
 foo@{E M N} = 
 Type@{M} -> Type@{N} -> Type@{E}
      : Type@{max(E+1,M+1,N+1)}
 (* E M N |=  *)
-foo@{u UnivBinders.17 v} = 
-Type@{UnivBinders.17} -> Type@{v} -> Type@{u}
-     : Type@{max(u+1,UnivBinders.17+1,v+1)}
-(* u UnivBinders.17 v |=  *)
+foo@{u UnivBinders.18 v} = 
+Type@{UnivBinders.18} -> Type@{v} -> Type@{u}
+     : Type@{max(u+1,UnivBinders.18+1,v+1)}
+(* u UnivBinders.18 v |=  *)
 Inductive Empty@{E} : Type@{E} :=  
 (* E |=  *)
 Record PWrap (A : Type@{E}) : Type@{E} := pwrap { punwrap : A }
 (* E |=  *)
 
 PWrap has primitive projections with eta conversion.
-For PWrap: Argument scope is [type_scope]
-For pwrap: Argument scopes are [type_scope _]
+Arguments PWrap _%type_scope
+Arguments pwrap _%type_scope
 punwrap@{K} : forall A : Type@{K}, PWrap@{K} A -> A
 (* K |=  *)
 
 punwrap is universe polymorphic
-Argument scopes are [type_scope _]
+Arguments punwrap _%type_scope
 punwrap is transparent
 Expands to: Constant UnivBinders.punwrap
 The command has indeed failed with message:
@@ -118,7 +117,7 @@ Inductive insecind@{k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{k}
 (* k |=  *)
 
-For inseccstr: Argument scope is [type_scope]
+Arguments inseccstr _%type_scope
 insec@{u v} = Type@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
@@ -126,7 +125,7 @@ Inductive insecind@{u k} : Type@{k+1} :=
     inseccstr : Type@{k} -> insecind@{u k}
 (* u k |=  *)
 
-For inseccstr: Argument scope is [type_scope]
+Arguments inseccstr _%type_scope
 insec2@{u} = Prop
      : Type@{Set+1}
 (* u |=  *)
@@ -143,29 +142,29 @@ Applied.infunct@{u v} =
 inmod@{u} -> Type@{v}
      : Type@{max(u+1,v+1)}
 (* u v |=  *)
-axfoo@{i UnivBinders.56 UnivBinders.57} :
-Type@{UnivBinders.56} -> Type@{i}
-(* i UnivBinders.56 UnivBinders.57 |=  *)
+axfoo@{i UnivBinders.59 UnivBinders.60} :
+Type@{UnivBinders.59} -> Type@{i}
+(* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axfoo is universe polymorphic
-Argument scope is [type_scope]
+Arguments axfoo _%type_scope
 Expands to: Constant UnivBinders.axfoo
-axbar@{i UnivBinders.56 UnivBinders.57} :
-Type@{UnivBinders.57} -> Type@{i}
-(* i UnivBinders.56 UnivBinders.57 |=  *)
+axbar@{i UnivBinders.59 UnivBinders.60} :
+Type@{UnivBinders.60} -> Type@{i}
+(* i UnivBinders.59 UnivBinders.60 |=  *)
 
 axbar is universe polymorphic
-Argument scope is [type_scope]
+Arguments axbar _%type_scope
 Expands to: Constant UnivBinders.axbar
-axfoo' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axfoo' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axfoo' is not universe polymorphic
-Argument scope is [type_scope]
+Arguments axfoo' _%type_scope
 Expands to: Constant UnivBinders.axfoo'
-axbar' : Type@{axbar'.u0} -> Type@{axbar'.i}
+axbar' : Type@{axfoo'.u0} -> Type@{axfoo'.i}
 
 axbar' is not universe polymorphic
-Argument scope is [type_scope]
+Arguments axbar' _%type_scope
 Expands to: Constant UnivBinders.axbar'
 The command has indeed failed with message:
 When declaring multiple axioms in one command, only the first is allowed a universe binder (which will be shared by the whole block).
diff --git a/test-suite/output/Warnings.v b/test-suite/output/Warnings.v
index 0eb5db1733..7465442cab 100644
--- a/test-suite/output/Warnings.v
+++ b/test-suite/output/Warnings.v
@@ -1,5 +1,5 @@
 (* Term in warning was not printed in the right environment at some time *)
-#[universes(template)] Record A := { B:Type; b:B->B }.
+Record A := { B:Type; b:B->B }.
 Definition a B := {| B:=B; b:=fun x => x |}.
 Canonical Structure a.
 
diff --git a/test-suite/output/auto.out b/test-suite/output/auto.out
index 2761b87b02..5e81b43504 100644
--- a/test-suite/output/auto.out
+++ b/test-suite/output/auto.out
@@ -2,18 +2,18 @@
 simple apply or_intror (in core).
  intro.
  assumption.
-Debug: (* debug auto: *)
-Debug: * assumption. (*fail*)
-Debug: * intro. (*fail*)
-Debug: * simple apply or_intror (in core). (*success*)
-Debug: ** assumption. (*fail*)
-Debug: ** intro. (*success*)
-Debug: ** assumption. (*success*)
+(* debug auto: *)
+* assumption. (*fail*)
+* intro. (*fail*)
+* simple apply or_intror (in core). (*success*)
+** assumption. (*fail*)
+** intro. (*success*)
+** assumption. (*success*)
 (* info eauto: *)
 simple apply or_intror.
  intro.
  exact H.
-Debug: (* debug eauto: *)
+(* debug eauto: *)
 Debug: 1 depth=5 
 Debug: 1.1 depth=4 simple apply or_intror
 Debug: 1.1.1 depth=4 intro
diff --git a/test-suite/output/bug7191.out b/test-suite/output/bug7191.out
new file mode 100644
index 0000000000..005455e30c
--- /dev/null
+++ b/test-suite/output/bug7191.out
@@ -0,0 +1,9 @@
+
+type unit0 =
+| Tt
+
+(** val f : unit0 -> unit0 **)
+
+let f _ =
+  assert false (* absurd case *)
+
diff --git a/test-suite/output/bug7191.v b/test-suite/output/bug7191.v
new file mode 100644
index 0000000000..1aa4625b6c
--- /dev/null
+++ b/test-suite/output/bug7191.v
@@ -0,0 +1,3 @@
+Require Extraction.
+Definition f (x : False) : unit -> unit := match x with end.
+Recursive Extraction f.
diff --git a/test-suite/output/bug7348.out b/test-suite/output/bug7348.out
new file mode 100644
index 0000000000..325ee95ae2
--- /dev/null
+++ b/test-suite/output/bug7348.out
@@ -0,0 +1,45 @@
+Extracted code successfully compiled
+
+type __ = Obj.t
+
+type unit0 =
+| Tt
+
+type bool =
+| True
+| False
+
+module Case1 =
+ struct
+  type coq_rec = { f : bool }
+
+  (** val f : bool -> coq_rec -> bool **)
+
+  let f _ r =
+    r.f
+
+  (** val silly : bool -> coq_rec -> __ **)
+
+  let silly x b =
+    match x with
+    | True -> Obj.magic b.f
+    | False -> Obj.magic Tt
+ end
+
+module Case2 =
+ struct
+  type coq_rec = { f : (bool -> bool) }
+
+  (** val f : bool -> coq_rec -> bool -> bool **)
+
+  let f _ r =
+    r.f
+
+  (** val silly : bool -> coq_rec -> __ **)
+
+  let silly x b =
+    match x with
+    | True -> Obj.magic b.f False
+    | False -> Obj.magic Tt
+ end
+
diff --git a/test-suite/output/bug7348.v b/test-suite/output/bug7348.v
new file mode 100644
index 0000000000..782b27ce96
--- /dev/null
+++ b/test-suite/output/bug7348.v
@@ -0,0 +1,25 @@
+Require Extraction.
+
+Extraction Language OCaml.
+Set Extraction KeepSingleton.
+
+Module Case1.
+
+Record rec (x : bool) := { f : bool }.
+
+Definition silly x (b : rec x) :=
+  if x return (if x then bool else unit) then f x b else tt.
+
+End Case1.
+
+Module Case2.
+
+Record rec (x : bool) := { f : bool -> bool }.
+
+Definition silly x (b : rec x) :=
+  if x return (if x then bool else unit) then f x b false else tt.
+
+End Case2.
+
+Extraction TestCompile Case1.silly Case2.silly.
+Recursive Extraction Case1.silly Case2.silly.
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index 209fedc343..57a4739e9f 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -21,6 +21,6 @@ Print P.
 
 (* Note: exact numbers of evars are not important... *)
 
-#[universes(template)] Inductive T (n:nat) : Type := A : T n.
+Inductive T (n:nat) : Type := A : T n.
 Check fun n (y:=A n:T n) => _ _ : T n.
 Check fun n => _ _ : T n.
diff --git a/test-suite/output/locate.out b/test-suite/output/locate.out
new file mode 100644
index 0000000000..473db2d312
--- /dev/null
+++ b/test-suite/output/locate.out
@@ -0,0 +1,3 @@
+Notation
+"b1 && b2" := if b1 then b2 else false (default interpretation)
+"x && y" := andb x y : bool_scope
diff --git a/test-suite/output/locate.v b/test-suite/output/locate.v
new file mode 100644
index 0000000000..af8b0ee193
--- /dev/null
+++ b/test-suite/output/locate.v
@@ -0,0 +1,3 @@
+Set Printing Width 400.
+Notation "b1 && b2" := (if b1 then b2 else false).
+Locate "&&".
diff --git a/test-suite/prerequisite/ssr_mini_mathcomp.v b/test-suite/prerequisite/ssr_mini_mathcomp.v
index 74f94a9bed..d293dc0533 100644
--- a/test-suite/prerequisite/ssr_mini_mathcomp.v
+++ b/test-suite/prerequisite/ssr_mini_mathcomp.v
@@ -196,7 +196,7 @@ Definition clone_subType U v :=
 
 Variable sT : subType.
 
-CoInductive Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
+Variant Sub_spec : sT -> Type := SubSpec x Px : Sub_spec (Sub x Px).
 
 Lemma SubP u : Sub_spec u.
 Proof. by case: sT Sub_spec SubSpec u => T' _ C rec /= _. Qed.
@@ -209,7 +209,7 @@ Definition insub x :=
 
 Definition insubd u0 x := odflt u0 (insub x).
 
-CoInductive insub_spec x : option sT -> Type :=
+Variant insub_spec x : option sT -> Type :=
   | InsubSome u of P x & val u = x : insub_spec x (Some u)
   | InsubNone   of ~~ P x          : insub_spec x None.
 
@@ -568,7 +568,7 @@ Fixpoint nth s n {struct n} :=
 
 Fixpoint rcons s z := if s is x :: s' then x :: rcons s' z else [:: z].
 
-CoInductive last_spec : seq T -> Type :=
+Variant last_spec : seq T -> Type :=
   | LastNil        : last_spec [::]
   | LastRcons s x  : last_spec (rcons s x).
 
@@ -1292,7 +1292,7 @@ Open Scope big_scope.
 (* packages both in in a term in which i occurs; it also depends on the       *)
 (* iterated <op>, as this can give more information on the expected type of   *)
 (* the <general_term>, thus allowing for the insertion of coercions.          *)
-CoInductive bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
+Variant bigbody R I := BigBody of I & (R -> R -> R) & bool & R.
 
 Definition applybig {R I} (body : bigbody R I) x :=
   let: BigBody _ op b v := body in if b then op v x else x.
diff --git a/test-suite/primitive/float/add.v b/test-suite/primitive/float/add.v
new file mode 100644
index 0000000000..f8c5939d0a
--- /dev/null
+++ b/test-suite/primitive/float/add.v
@@ -0,0 +1,63 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition five := Eval compute in of_int63 5%int63.
+
+Check (eq_refl : two + three = five).
+Check (eq_refl five <: two + three = five).
+Check (eq_refl five <<: two + three = five).
+Definition compute1 := Eval compute in two + three.
+Check (eq_refl compute1 : five = five).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge + tiny = huge).
+Check (eq_refl huge <: huge + tiny = huge).
+Check (eq_refl huge <<: huge + tiny = huge).
+Definition compute2 := Eval compute in huge + tiny.
+Check (eq_refl compute2 : huge = huge).
+
+Check (eq_refl : huge + huge = infinity).
+Check (eq_refl infinity <: huge + huge = infinity).
+Check (eq_refl infinity <<: huge + huge = infinity).
+Definition compute3 := Eval compute in huge + huge.
+Check (eq_refl compute3 : infinity = infinity).
+
+Check (eq_refl : one + nan = nan).
+Check (eq_refl nan <: one + nan = nan).
+Check (eq_refl nan <<: one + nan = nan).
+Definition compute4 := Eval compute in one + nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity + infinity = infinity).
+Check (eq_refl infinity <: infinity + infinity = infinity).
+Check (eq_refl infinity <<: infinity + infinity = infinity).
+Definition compute5 := Eval compute in infinity + infinity.
+Check (eq_refl compute5 : infinity = infinity).
+
+Check (eq_refl : infinity + neg_infinity = nan).
+Check (eq_refl nan <: infinity + neg_infinity = nan).
+Check (eq_refl nan <<: infinity + neg_infinity = nan).
+Definition compute6 := Eval compute in infinity + neg_infinity.
+Check (eq_refl compute6 : nan = nan).
+
+Check (eq_refl : zero + zero = zero).
+Check (eq_refl zero <: zero + zero = zero).
+Check (eq_refl zero <<: zero + zero = zero).
+Check (eq_refl : neg_zero + zero = zero).
+Check (eq_refl zero <: neg_zero + zero = zero).
+Check (eq_refl zero <<: neg_zero + zero = zero).
+Check (eq_refl : neg_zero + neg_zero = neg_zero).
+Check (eq_refl neg_zero <: neg_zero + neg_zero = neg_zero).
+Check (eq_refl neg_zero <<: neg_zero + neg_zero = neg_zero).
+Check (eq_refl : zero + neg_zero = zero).
+Check (eq_refl zero <: zero + neg_zero = zero).
+Check (eq_refl zero <<: zero + neg_zero = zero).
+
+Check (eq_refl : huge + neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <: huge + neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <<: huge + neg_infinity = neg_infinity).
diff --git a/test-suite/primitive/float/classify.v b/test-suite/primitive/float/classify.v
new file mode 100644
index 0000000000..22e3fca844
--- /dev/null
+++ b/test-suite/primitive/float/classify.v
@@ -0,0 +1,33 @@
+Require Import ZArith Floats.
+
+Definition epsilon := Eval compute in ldexp one (-1024)%Z.
+
+Check (eq_refl : classify one = PNormal).
+Check (eq_refl : classify (- one)%float = NNormal).
+Check (eq_refl : classify epsilon = PSubn).
+Check (eq_refl : classify (- epsilon)%float = NSubn).
+Check (eq_refl : classify zero = PZero).
+Check (eq_refl : classify neg_zero = NZero).
+Check (eq_refl : classify infinity = PInf).
+Check (eq_refl : classify neg_infinity = NInf).
+Check (eq_refl : classify nan = NaN).
+
+Check (eq_refl PNormal <: classify one = PNormal).
+Check (eq_refl NNormal <: classify (- one)%float = NNormal).
+Check (eq_refl PSubn <: classify epsilon = PSubn).
+Check (eq_refl NSubn <: classify (- epsilon)%float = NSubn).
+Check (eq_refl PZero <: classify zero = PZero).
+Check (eq_refl NZero <: classify neg_zero = NZero).
+Check (eq_refl PInf <: classify infinity = PInf).
+Check (eq_refl NInf <: classify neg_infinity = NInf).
+Check (eq_refl NaN <: classify nan = NaN).
+
+Check (eq_refl PNormal <<: classify one = PNormal).
+Check (eq_refl NNormal <<: classify (- one)%float = NNormal).
+Check (eq_refl PSubn <<: classify epsilon = PSubn).
+Check (eq_refl NSubn <<: classify (- epsilon)%float = NSubn).
+Check (eq_refl PZero <<: classify zero = PZero).
+Check (eq_refl NZero <<: classify neg_zero = NZero).
+Check (eq_refl PInf <<: classify infinity = PInf).
+Check (eq_refl NInf <<: classify neg_infinity = NInf).
+Check (eq_refl NaN <<: classify nan = NaN).
diff --git a/test-suite/primitive/float/compare.v b/test-suite/primitive/float/compare.v
new file mode 100644
index 0000000000..23d1e5bbae
--- /dev/null
+++ b/test-suite/primitive/float/compare.v
@@ -0,0 +1,385 @@
+(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *)
+Require Import ZArith Floats.
+Local Open Scope float_scope.
+
+Definition min_denorm := Eval compute in ldexp one (-1074)%Z.
+
+Definition min_norm := Eval compute in ldexp one (-1024)%Z.
+
+Check (eq_refl false : nan == nan = false).
+Check (eq_refl false : nan == nan = false).
+Check (eq_refl false : nan < nan = false).
+Check (eq_refl false : nan < nan = false).
+Check (eq_refl false : nan <= nan = false).
+Check (eq_refl false : nan <= nan = false).
+Check (eq_refl FNotComparable : nan ?= nan = FNotComparable).
+Check (eq_refl FNotComparable : nan ?= nan = FNotComparable).
+
+Check (eq_refl false <: nan == nan = false).
+Check (eq_refl false <: nan == nan = false).
+Check (eq_refl false <: nan < nan = false).
+Check (eq_refl false <: nan < nan = false).
+Check (eq_refl false <: nan <= nan = false).
+Check (eq_refl false <: nan <= nan = false).
+Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable).
+Check (eq_refl FNotComparable <: nan ?= nan = FNotComparable).
+
+Check (eq_refl false <<: nan == nan = false).
+Check (eq_refl false <<: nan == nan = false).
+Check (eq_refl false <<: nan < nan = false).
+Check (eq_refl false <<: nan < nan = false).
+Check (eq_refl false <<: nan <= nan = false).
+Check (eq_refl false <<: nan <= nan = false).
+Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable).
+Check (eq_refl FNotComparable <<: nan ?= nan = FNotComparable).
+
+Check (eq_refl false : nan == - nan = false).
+Check (eq_refl false : - nan == nan = false).
+Check (eq_refl false : nan < - nan = false).
+Check (eq_refl false : - nan < nan = false).
+Check (eq_refl false : nan <= - nan = false).
+Check (eq_refl false : - nan <= nan = false).
+Check (eq_refl FNotComparable : nan ?= - nan = FNotComparable).
+Check (eq_refl FNotComparable : - nan ?= nan = FNotComparable).
+
+Check (eq_refl false <: nan == - nan = false).
+Check (eq_refl false <: - nan == nan = false).
+Check (eq_refl false <: nan < - nan = false).
+Check (eq_refl false <: - nan < nan = false).
+Check (eq_refl false <: nan <= - nan = false).
+Check (eq_refl false <: - nan <= nan = false).
+Check (eq_refl FNotComparable <: nan ?= - nan = FNotComparable).
+Check (eq_refl FNotComparable <: - nan ?= nan = FNotComparable).
+
+Check (eq_refl false <<: nan == - nan = false).
+Check (eq_refl false <<: - nan == nan = false).
+Check (eq_refl false <<: nan < - nan = false).
+Check (eq_refl false <<: - nan < nan = false).
+Check (eq_refl false <<: nan <= - nan = false).
+Check (eq_refl false <<: - nan <= nan = false).
+Check (eq_refl FNotComparable <<: nan ?= - nan = FNotComparable).
+Check (eq_refl FNotComparable <<: - nan ?= nan = FNotComparable).
+
+Check (eq_refl true : one == one = true).
+Check (eq_refl true : one == one = true).
+Check (eq_refl false : one < one = false).
+Check (eq_refl false : one < one = false).
+Check (eq_refl true : one <= one = true).
+Check (eq_refl true : one <= one = true).
+Check (eq_refl FEq : one ?= one = FEq).
+Check (eq_refl FEq : one ?= one = FEq).
+
+Check (eq_refl true <: one == one = true).
+Check (eq_refl true <: one == one = true).
+Check (eq_refl false <: one < one = false).
+Check (eq_refl false <: one < one = false).
+Check (eq_refl true <: one <= one = true).
+Check (eq_refl true <: one <= one = true).
+Check (eq_refl FEq <: one ?= one = FEq).
+Check (eq_refl FEq <: one ?= one = FEq).
+
+Check (eq_refl true <<: one == one = true).
+Check (eq_refl true <<: one == one = true).
+Check (eq_refl false <<: one < one = false).
+Check (eq_refl false <<: one < one = false).
+Check (eq_refl true <<: one <= one = true).
+Check (eq_refl true <<: one <= one = true).
+Check (eq_refl FEq <<: one ?= one = FEq).
+Check (eq_refl FEq <<: one ?= one = FEq).
+
+Check (eq_refl true : zero == zero = true).
+Check (eq_refl true : zero == zero = true).
+Check (eq_refl false : zero < zero = false).
+Check (eq_refl false : zero < zero = false).
+Check (eq_refl true : zero <= zero = true).
+Check (eq_refl true : zero <= zero = true).
+Check (eq_refl FEq : zero ?= zero = FEq).
+Check (eq_refl FEq : zero ?= zero = FEq).
+
+Check (eq_refl true <: zero == zero = true).
+Check (eq_refl true <: zero == zero = true).
+Check (eq_refl false <: zero < zero = false).
+Check (eq_refl false <: zero < zero = false).
+Check (eq_refl true <: zero <= zero = true).
+Check (eq_refl true <: zero <= zero = true).
+Check (eq_refl FEq <: zero ?= zero = FEq).
+Check (eq_refl FEq <: zero ?= zero = FEq).
+
+Check (eq_refl true <<: zero == zero = true).
+Check (eq_refl true <<: zero == zero = true).
+Check (eq_refl false <<: zero < zero = false).
+Check (eq_refl false <<: zero < zero = false).
+Check (eq_refl true <<: zero <= zero = true).
+Check (eq_refl true <<: zero <= zero = true).
+Check (eq_refl FEq <<: zero ?= zero = FEq).
+Check (eq_refl FEq <<: zero ?= zero = FEq).
+
+Check (eq_refl true : zero == - zero = true).
+Check (eq_refl true : - zero == zero = true).
+Check (eq_refl false : zero < - zero = false).
+Check (eq_refl false : - zero < zero = false).
+Check (eq_refl true : zero <= - zero = true).
+Check (eq_refl true : - zero <= zero = true).
+Check (eq_refl FEq : zero ?= - zero = FEq).
+Check (eq_refl FEq : - zero ?= zero = FEq).
+
+Check (eq_refl true <: zero == - zero = true).
+Check (eq_refl true <: - zero == zero = true).
+Check (eq_refl false <: zero < - zero = false).
+Check (eq_refl false <: - zero < zero = false).
+Check (eq_refl true <: zero <= - zero = true).
+Check (eq_refl true <: - zero <= zero = true).
+Check (eq_refl FEq <: zero ?= - zero = FEq).
+Check (eq_refl FEq <: - zero ?= zero = FEq).
+
+Check (eq_refl true <<: zero == - zero = true).
+Check (eq_refl true <<: - zero == zero = true).
+Check (eq_refl false <<: zero < - zero = false).
+Check (eq_refl false <<: - zero < zero = false).
+Check (eq_refl true <<: zero <= - zero = true).
+Check (eq_refl true <<: - zero <= zero = true).
+Check (eq_refl FEq <<: zero ?= - zero = FEq).
+Check (eq_refl FEq <<: - zero ?= zero = FEq).
+
+Check (eq_refl true : - zero == - zero = true).
+Check (eq_refl true : - zero == - zero = true).
+Check (eq_refl false : - zero < - zero = false).
+Check (eq_refl false : - zero < - zero = false).
+Check (eq_refl true : - zero <= - zero = true).
+Check (eq_refl true : - zero <= - zero = true).
+Check (eq_refl FEq : - zero ?= - zero = FEq).
+Check (eq_refl FEq : - zero ?= - zero = FEq).
+
+Check (eq_refl true <: - zero == - zero = true).
+Check (eq_refl true <: - zero == - zero = true).
+Check (eq_refl false <: - zero < - zero = false).
+Check (eq_refl false <: - zero < - zero = false).
+Check (eq_refl true <: - zero <= - zero = true).
+Check (eq_refl true <: - zero <= - zero = true).
+Check (eq_refl FEq <: - zero ?= - zero = FEq).
+Check (eq_refl FEq <: - zero ?= - zero = FEq).
+
+Check (eq_refl true <<: - zero == - zero = true).
+Check (eq_refl true <<: - zero == - zero = true).
+Check (eq_refl false <<: - zero < - zero = false).
+Check (eq_refl false <<: - zero < - zero = false).
+Check (eq_refl true <<: - zero <= - zero = true).
+Check (eq_refl true <<: - zero <= - zero = true).
+Check (eq_refl FEq <<: - zero ?= - zero = FEq).
+Check (eq_refl FEq <<: - zero ?= - zero = FEq).
+
+Check (eq_refl true : infinity == infinity = true).
+Check (eq_refl true : infinity == infinity = true).
+Check (eq_refl false : infinity < infinity = false).
+Check (eq_refl false : infinity < infinity = false).
+Check (eq_refl true : infinity <= infinity = true).
+Check (eq_refl true : infinity <= infinity = true).
+Check (eq_refl FEq : infinity ?= infinity = FEq).
+Check (eq_refl FEq : infinity ?= infinity = FEq).
+
+Check (eq_refl true <: infinity == infinity = true).
+Check (eq_refl true <: infinity == infinity = true).
+Check (eq_refl false <: infinity < infinity = false).
+Check (eq_refl false <: infinity < infinity = false).
+Check (eq_refl true <: infinity <= infinity = true).
+Check (eq_refl true <: infinity <= infinity = true).
+Check (eq_refl FEq <: infinity ?= infinity = FEq).
+Check (eq_refl FEq <: infinity ?= infinity = FEq).
+
+Check (eq_refl true <<: infinity == infinity = true).
+Check (eq_refl true <<: infinity == infinity = true).
+Check (eq_refl false <<: infinity < infinity = false).
+Check (eq_refl false <<: infinity < infinity = false).
+Check (eq_refl true <<: infinity <= infinity = true).
+Check (eq_refl true <<: infinity <= infinity = true).
+Check (eq_refl FEq <<: infinity ?= infinity = FEq).
+Check (eq_refl FEq <<: infinity ?= infinity = FEq).
+
+Check (eq_refl true : - infinity == - infinity = true).
+Check (eq_refl true : - infinity == - infinity = true).
+Check (eq_refl false : - infinity < - infinity = false).
+Check (eq_refl false : - infinity < - infinity = false).
+Check (eq_refl true : - infinity <= - infinity = true).
+Check (eq_refl true : - infinity <= - infinity = true).
+Check (eq_refl FEq : - infinity ?= - infinity = FEq).
+Check (eq_refl FEq : - infinity ?= - infinity = FEq).
+
+Check (eq_refl true <: - infinity == - infinity = true).
+Check (eq_refl true <: - infinity == - infinity = true).
+Check (eq_refl false <: - infinity < - infinity = false).
+Check (eq_refl false <: - infinity < - infinity = false).
+Check (eq_refl true <: - infinity <= - infinity = true).
+Check (eq_refl true <: - infinity <= - infinity = true).
+Check (eq_refl FEq <: - infinity ?= - infinity = FEq).
+Check (eq_refl FEq <: - infinity ?= - infinity = FEq).
+
+Check (eq_refl true <<: - infinity == - infinity = true).
+Check (eq_refl true <<: - infinity == - infinity = true).
+Check (eq_refl false <<: - infinity < - infinity = false).
+Check (eq_refl false <<: - infinity < - infinity = false).
+Check (eq_refl true <<: - infinity <= - infinity = true).
+Check (eq_refl true <<: - infinity <= - infinity = true).
+Check (eq_refl FEq <<: - infinity ?= - infinity = FEq).
+Check (eq_refl FEq <<: - infinity ?= - infinity = FEq).
+
+Check (eq_refl false : min_denorm == min_norm = false).
+Check (eq_refl false : min_norm == min_denorm = false).
+Check (eq_refl true : min_denorm < min_norm = true).
+Check (eq_refl false : min_norm < min_denorm = false).
+Check (eq_refl true : min_denorm <= min_norm = true).
+Check (eq_refl false : min_norm <= min_denorm = false).
+Check (eq_refl FLt : min_denorm ?= min_norm = FLt).
+Check (eq_refl FGt : min_norm ?= min_denorm = FGt).
+
+Check (eq_refl false <: min_denorm == min_norm = false).
+Check (eq_refl false <: min_norm == min_denorm = false).
+Check (eq_refl true <: min_denorm < min_norm = true).
+Check (eq_refl false <: min_norm < min_denorm = false).
+Check (eq_refl true <: min_denorm <= min_norm = true).
+Check (eq_refl false <: min_norm <= min_denorm = false).
+Check (eq_refl FLt <: min_denorm ?= min_norm = FLt).
+Check (eq_refl FGt <: min_norm ?= min_denorm = FGt).
+
+Check (eq_refl false <<: min_denorm == min_norm = false).
+Check (eq_refl false <<: min_norm == min_denorm = false).
+Check (eq_refl true <<: min_denorm < min_norm = true).
+Check (eq_refl false <<: min_norm < min_denorm = false).
+Check (eq_refl true <<: min_denorm <= min_norm = true).
+Check (eq_refl false <<: min_norm <= min_denorm = false).
+Check (eq_refl FLt <<: min_denorm ?= min_norm = FLt).
+Check (eq_refl FGt <<: min_norm ?= min_denorm = FGt).
+
+Check (eq_refl false : min_denorm == one = false).
+Check (eq_refl false : one == min_denorm = false).
+Check (eq_refl true : min_denorm < one = true).
+Check (eq_refl false : one < min_denorm = false).
+Check (eq_refl true : min_denorm <= one = true).
+Check (eq_refl false : one <= min_denorm = false).
+Check (eq_refl FLt : min_denorm ?= one = FLt).
+Check (eq_refl FGt : one ?= min_denorm = FGt).
+
+Check (eq_refl false <: min_denorm == one = false).
+Check (eq_refl false <: one == min_denorm = false).
+Check (eq_refl true <: min_denorm < one = true).
+Check (eq_refl false <: one < min_denorm = false).
+Check (eq_refl true <: min_denorm <= one = true).
+Check (eq_refl false <: one <= min_denorm = false).
+Check (eq_refl FLt <: min_denorm ?= one = FLt).
+Check (eq_refl FGt <: one ?= min_denorm = FGt).
+
+Check (eq_refl false <<: min_denorm == one = false).
+Check (eq_refl false <<: one == min_denorm = false).
+Check (eq_refl true <<: min_denorm < one = true).
+Check (eq_refl false <<: one < min_denorm = false).
+Check (eq_refl true <<: min_denorm <= one = true).
+Check (eq_refl false <<: one <= min_denorm = false).
+Check (eq_refl FLt <<: min_denorm ?= one = FLt).
+Check (eq_refl FGt <<: one ?= min_denorm = FGt).
+
+Check (eq_refl false : min_norm == one = false).
+Check (eq_refl false : one == min_norm = false).
+Check (eq_refl true : min_norm < one = true).
+Check (eq_refl false : one < min_norm = false).
+Check (eq_refl true : min_norm <= one = true).
+Check (eq_refl false : one <= min_norm = false).
+Check (eq_refl FLt : min_norm ?= one = FLt).
+Check (eq_refl FGt : one ?= min_norm = FGt).
+
+Check (eq_refl false <: min_norm == one = false).
+Check (eq_refl false <: one == min_norm = false).
+Check (eq_refl true <: min_norm < one = true).
+Check (eq_refl false <: one < min_norm = false).
+Check (eq_refl true <: min_norm <= one = true).
+Check (eq_refl false <: one <= min_norm = false).
+Check (eq_refl FLt <: min_norm ?= one = FLt).
+Check (eq_refl FGt <: one ?= min_norm = FGt).
+
+Check (eq_refl false <<: min_norm == one = false).
+Check (eq_refl false <<: one == min_norm = false).
+Check (eq_refl true <<: min_norm < one = true).
+Check (eq_refl false <<: one < min_norm = false).
+Check (eq_refl true <<: min_norm <= one = true).
+Check (eq_refl false <<: one <= min_norm = false).
+Check (eq_refl FLt <<: min_norm ?= one = FLt).
+Check (eq_refl FGt <<: one ?= min_norm = FGt).
+
+Check (eq_refl false : one == infinity = false).
+Check (eq_refl false : infinity == one = false).
+Check (eq_refl true : one < infinity = true).
+Check (eq_refl false : infinity < one = false).
+Check (eq_refl true : one <= infinity = true).
+Check (eq_refl false : infinity <= one = false).
+Check (eq_refl FLt : one ?= infinity = FLt).
+Check (eq_refl FGt : infinity ?= one = FGt).
+
+Check (eq_refl false <: one == infinity = false).
+Check (eq_refl false <: infinity == one = false).
+Check (eq_refl true <: one < infinity = true).
+Check (eq_refl false <: infinity < one = false).
+Check (eq_refl true <: one <= infinity = true).
+Check (eq_refl false <: infinity <= one = false).
+Check (eq_refl FLt <: one ?= infinity = FLt).
+Check (eq_refl FGt <: infinity ?= one = FGt).
+
+Check (eq_refl false <<: one == infinity = false).
+Check (eq_refl false <<: infinity == one = false).
+Check (eq_refl true <<: one < infinity = true).
+Check (eq_refl false <<: infinity < one = false).
+Check (eq_refl true <<: one <= infinity = true).
+Check (eq_refl false <<: infinity <= one = false).
+Check (eq_refl FLt <<: one ?= infinity = FLt).
+Check (eq_refl FGt <<: infinity ?= one = FGt).
+
+Check (eq_refl false : - infinity == infinity = false).
+Check (eq_refl false : infinity == - infinity = false).
+Check (eq_refl true : - infinity < infinity = true).
+Check (eq_refl false : infinity < - infinity = false).
+Check (eq_refl true : - infinity <= infinity = true).
+Check (eq_refl false : infinity <= - infinity = false).
+Check (eq_refl FLt : - infinity ?= infinity = FLt).
+Check (eq_refl FGt : infinity ?= - infinity = FGt).
+
+Check (eq_refl false <: - infinity == infinity = false).
+Check (eq_refl false <: infinity == - infinity = false).
+Check (eq_refl true <: - infinity < infinity = true).
+Check (eq_refl false <: infinity < - infinity = false).
+Check (eq_refl true <: - infinity <= infinity = true).
+Check (eq_refl false <: infinity <= - infinity = false).
+Check (eq_refl FLt <: - infinity ?= infinity = FLt).
+Check (eq_refl FGt <: infinity ?= - infinity = FGt).
+
+Check (eq_refl false <<: - infinity == infinity = false).
+Check (eq_refl false <<: infinity == - infinity = false).
+Check (eq_refl true <<: - infinity < infinity = true).
+Check (eq_refl false <<: infinity < - infinity = false).
+Check (eq_refl true <<: - infinity <= infinity = true).
+Check (eq_refl false <<: infinity <= - infinity = false).
+Check (eq_refl FLt <<: - infinity ?= infinity = FLt).
+Check (eq_refl FGt <<: infinity ?= - infinity = FGt).
+
+Check (eq_refl false : - infinity == one = false).
+Check (eq_refl false : one == - infinity = false).
+Check (eq_refl true : - infinity < one = true).
+Check (eq_refl false : one < - infinity = false).
+Check (eq_refl true : - infinity <= one = true).
+Check (eq_refl false : one <= - infinity = false).
+Check (eq_refl FLt : - infinity ?= one = FLt).
+Check (eq_refl FGt : one ?= - infinity = FGt).
+
+Check (eq_refl false <: - infinity == one = false).
+Check (eq_refl false <: one == - infinity = false).
+Check (eq_refl true <: - infinity < one = true).
+Check (eq_refl false <: one < - infinity = false).
+Check (eq_refl true <: - infinity <= one = true).
+Check (eq_refl false <: one <= - infinity = false).
+Check (eq_refl FLt <: - infinity ?= one = FLt).
+Check (eq_refl FGt <: one ?= - infinity = FGt).
+
+Check (eq_refl false <<: - infinity == one = false).
+Check (eq_refl false <<: one == - infinity = false).
+Check (eq_refl true <<: - infinity < one = true).
+Check (eq_refl false <<: one < - infinity = false).
+Check (eq_refl true <<: - infinity <= one = true).
+Check (eq_refl false <<: one <= - infinity = false).
+Check (eq_refl FLt <<: - infinity ?= one = FLt).
+Check (eq_refl FGt <<: one ?= - infinity = FGt).
diff --git a/test-suite/primitive/float/coq_env_double_array.v b/test-suite/primitive/float/coq_env_double_array.v
new file mode 100644
index 0000000000..754ccb69aa
--- /dev/null
+++ b/test-suite/primitive/float/coq_env_double_array.v
@@ -0,0 +1,13 @@
+Require Import Floats.
+
+Goal True.
+pose (f := one).
+pose (f' := (-f)%float).
+
+(* this used to segfault when the coq_env array given to the
+   coq_interprete C function was an unboxed OCaml Double_array
+   (created by Array.map in csymtable.ml just before calling
+   eval_tcode) *)
+vm_compute in f'.
+
+Abort.
diff --git a/test-suite/primitive/float/div.v b/test-suite/primitive/float/div.v
new file mode 100644
index 0000000000..8e971f575b
--- /dev/null
+++ b/test-suite/primitive/float/div.v
@@ -0,0 +1,87 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition six := Eval compute in of_int63 6%int63.
+
+Check (eq_refl : six / three = two).
+Check (eq_refl two <: six / three = two).
+Check (eq_refl two <<: six / three = two).
+Definition compute1 := Eval compute in six / three.
+Check (eq_refl compute1 : two = two).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge / tiny = infinity).
+Check (eq_refl infinity <: huge / tiny = infinity).
+Check (eq_refl infinity <<: huge / tiny = infinity).
+Definition compute2 := Eval compute in huge / tiny.
+Check (eq_refl compute2 : infinity = infinity).
+
+Check (eq_refl : huge / huge = one).
+Check (eq_refl one <: huge / huge = one).
+Check (eq_refl one <<: huge / huge = one).
+Definition compute3 := Eval compute in huge / huge.
+Check (eq_refl compute3 : one = one).
+
+Check (eq_refl : one / nan = nan).
+Check (eq_refl nan <: one / nan = nan).
+Check (eq_refl nan <<: one / nan = nan).
+Definition compute4 := Eval compute in one / nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity / infinity = nan).
+Check (eq_refl nan <: infinity / infinity = nan).
+Check (eq_refl nan <<: infinity / infinity = nan).
+Definition compute5 := Eval compute in infinity / infinity.
+Check (eq_refl compute5 : nan = nan).
+
+Check (eq_refl : infinity / neg_infinity = nan).
+Check (eq_refl nan <: infinity / neg_infinity = nan).
+Check (eq_refl nan <<: infinity / neg_infinity = nan).
+Definition compute6 := Eval compute in infinity / neg_infinity.
+Check (eq_refl compute6 : nan = nan).
+
+Check (eq_refl : zero / zero = nan).
+Check (eq_refl nan <: zero / zero = nan).
+Check (eq_refl nan <<: zero / zero = nan).
+Check (eq_refl : neg_zero / zero = nan).
+Check (eq_refl nan <: neg_zero / zero = nan).
+Check (eq_refl nan <<: neg_zero / zero = nan).
+
+Check (eq_refl : huge / neg_infinity = neg_zero).
+Check (eq_refl neg_zero <: huge / neg_infinity = neg_zero).
+Check (eq_refl neg_zero <<: huge / neg_infinity = neg_zero).
+
+Check (eq_refl : one / tiny = huge).
+Check (eq_refl huge <: one / tiny = huge).
+Check (eq_refl huge <<: one / tiny = huge).
+Check (eq_refl : one / huge = tiny).
+Check (eq_refl tiny <: one / huge = tiny).
+Check (eq_refl tiny <<: one / huge = tiny).
+Check (eq_refl : zero / huge = zero).
+Check (eq_refl zero <: zero / huge = zero).
+Check (eq_refl zero <<: zero / huge = zero).
+Check (eq_refl : zero / (-huge) = neg_zero).
+Check (eq_refl neg_zero <: zero / (-huge) = neg_zero).
+Check (eq_refl neg_zero <<: zero / (-huge) = neg_zero).
+
+Check (eq_refl : tiny / one = tiny).
+Check (eq_refl tiny <: tiny / one = tiny).
+Check (eq_refl tiny <<: tiny / one = tiny).
+Check (eq_refl : huge / one = huge).
+Check (eq_refl huge <: huge / one = huge).
+Check (eq_refl huge <<: huge / one = huge).
+Check (eq_refl : infinity / one = infinity).
+Check (eq_refl infinity <: infinity / one = infinity).
+Check (eq_refl infinity <<: infinity / one = infinity).
+
+Check (eq_refl : zero / infinity = zero).
+Check (eq_refl zero <: zero / infinity = zero).
+Check (eq_refl zero <<: zero / infinity = zero).
+Check (eq_refl : infinity / zero = infinity).
+Check (eq_refl infinity <: infinity / zero = infinity).
+Check (eq_refl infinity <<: infinity / zero = infinity).
diff --git a/test-suite/primitive/float/double_rounding.v b/test-suite/primitive/float/double_rounding.v
new file mode 100644
index 0000000000..e2356cdd7b
--- /dev/null
+++ b/test-suite/primitive/float/double_rounding.v
@@ -0,0 +1,38 @@
+Require Import Floats ZArith.
+
+(* This test check that there is no double rounding with 80 bits registers inside float computations *)
+
+Definition big_cbn := Eval cbn in ldexp one (53)%Z.
+Definition small_cbn := Eval cbn in (one + ldexp one (-52)%Z)%float.
+Definition result_cbn := Eval cbn in (big_cbn + small_cbn)%float.
+Definition check_cbn := Eval cbn in (big_cbn + one)%float.
+
+Check (eq_refl : (result_cbn ?= big_cbn)%float = FGt).
+Check (eq_refl : (check_cbn ?= big_cbn)%float = FEq).
+
+
+Definition big_cbv := Eval cbv in ldexp one (53)%Z.
+Definition small_cbv := Eval cbv in (one + ldexp one (-52)%Z)%float.
+Definition result_cbv := Eval cbv in (big_cbv + small_cbv)%float.
+Definition check_cbv := Eval cbv in (big_cbv + one)%float.
+
+Check (eq_refl : (result_cbv ?= big_cbv)%float = FGt).
+Check (eq_refl : (check_cbv ?= big_cbv)%float = FEq).
+
+
+Definition big_vm := Eval vm_compute in ldexp one (53)%Z.
+Definition small_vm := Eval vm_compute in (one + ldexp one (-52)%Z)%float.
+Definition result_vm := Eval vm_compute in (big_vm + small_vm)%float.
+Definition check_vm := Eval vm_compute in (big_vm + one)%float.
+
+Check (eq_refl : (result_vm ?= big_vm)%float = FGt).
+Check (eq_refl : (check_vm ?= big_vm)%float = FEq).
+
+
+Definition big_native := Eval native_compute in ldexp one (53)%Z.
+Definition small_native := Eval native_compute in (one + ldexp one (-52)%Z)%float.
+Definition result_native := Eval native_compute in (big_native + small_native)%float.
+Definition check_native := Eval native_compute in (big_native + one)%float.
+
+Check (eq_refl : (result_native ?= big_native)%float = FGt).
+Check (eq_refl : (check_native ?= big_native)%float = FEq).
diff --git a/test-suite/primitive/float/frexp.v b/test-suite/primitive/float/frexp.v
new file mode 100644
index 0000000000..2a600429b1
--- /dev/null
+++ b/test-suite/primitive/float/frexp.v
@@ -0,0 +1,28 @@
+Require Import ZArith Floats.
+
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+Definition neg_one := Eval compute in (-one)%float.
+
+Check (eq_refl : let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF infinity)) <<: let (m,e) := frexp infinity in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF infinity)).
+
+Check (eq_refl : let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF nan)) <<: let (m,e) := frexp nan in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF nan)).
+
+Check (eq_refl : let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF zero)) <<: let (m,e) := frexp zero in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF zero)).
+
+Check (eq_refl : let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF one)) <<: let (m,e) := frexp one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF one)).
+
+Check (eq_refl : let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <: let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF neg_one)) <<: let (m,e) := frexp neg_one in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF neg_one)).
+
+Check (eq_refl : let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
+Check (eq_refl (SFfrexp prec emax (Prim2SF denorm)) <<: let (m,e) := frexp denorm in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF denorm)).
diff --git a/test-suite/primitive/float/gen_compare.sh b/test-suite/primitive/float/gen_compare.sh
new file mode 100755
index 0000000000..cd87eb4e5b
--- /dev/null
+++ b/test-suite/primitive/float/gen_compare.sh
@@ -0,0 +1,65 @@
+#!/bin/bash
+# -*- compile-command: "mv -f compare.v{,~} && ./gen_compare.sh" -*-
+set -e
+
+exec > compare.v
+
+cat <<EOF
+(* DO NOT EDIT THIS FILE: automatically generated by ./gen_compare.sh *)
+Require Import ZArith Floats.
+Local Open Scope float_scope.
+
+Definition min_denorm := Eval compute in ldexp one (-1074)%Z.
+
+Definition min_norm := Eval compute in ldexp one (-1024)%Z.
+
+EOF
+
+genTest() {
+    if [ $# -ne 10 ]; then
+        echo >&2 "genTest expects 10 arguments"
+    fi
+    TACTICS=(":" "<:" "<<:")
+    OPS=("==" "<" "<=" "?=")
+    x="$1"
+    y="$2"
+    OPS1=("$3" "$4" "$5" "$6")  # for x y
+    OPS2=("$7" "$8" "$9" "${10}") # for y x
+    for tac in "${TACTICS[@]}"; do
+        for i in {0..3}; do
+            op="${OPS[$i]}"
+            op1="${OPS1[$i]}"
+            op2="${OPS2[$i]}"
+            echo "Check (eq_refl $op1 $tac $x $op $y = $op1)."
+            echo "Check (eq_refl $op2 $tac $y $op $x = $op2)."
+        done
+        echo
+    done
+}
+
+genTest nan nan \
+        false false false FNotComparable \
+        false false false FNotComparable
+genTest nan "- nan" \
+        false false false FNotComparable \
+        false false false FNotComparable
+
+EQ=(true false true FEq \
+    true false true FEq)
+
+genTest one one "${EQ[@]}"
+genTest zero zero "${EQ[@]}"
+genTest zero "- zero" "${EQ[@]}"
+genTest "- zero" "- zero" "${EQ[@]}"
+genTest infinity infinity "${EQ[@]}"
+genTest "- infinity" "- infinity" "${EQ[@]}"
+
+LT=(false true true FLt \
+    false false false FGt)
+
+genTest min_denorm min_norm "${LT[@]}"
+genTest min_denorm one "${LT[@]}"
+genTest min_norm one "${LT[@]}"
+genTest one infinity "${LT[@]}"
+genTest "- infinity" infinity "${LT[@]}"
+genTest "- infinity" one "${LT[@]}"
diff --git a/test-suite/primitive/float/ldexp.v b/test-suite/primitive/float/ldexp.v
new file mode 100644
index 0000000000..a725deeeca
--- /dev/null
+++ b/test-suite/primitive/float/ldexp.v
@@ -0,0 +1,21 @@
+Require Import ZArith Int63 Floats.
+
+Check (eq_refl : ldexp one 9223372036854773807%Z = infinity).
+Check (eq_refl infinity <: ldexp one 9223372036854773807%Z = infinity).
+Check (eq_refl infinity <<: ldexp one 9223372036854773807%Z = infinity).
+
+Check (eq_refl : ldshiftexp one 9223372036854775807 = infinity).
+Check (eq_refl infinity <: ldshiftexp one 9223372036854775807 = infinity).
+Check (eq_refl infinity <<: ldshiftexp one 9223372036854775807 = infinity).
+
+Check (eq_refl : ldexp one (-2102) = 0%float).
+Check (eq_refl 0%float <: ldexp one (-2102) = 0%float).
+Check (eq_refl 0%float <<: ldexp one (-2102) = 0%float).
+
+Check (eq_refl : ldexp one (-3) = 0.125%float).
+Check (eq_refl 0.125%float <: ldexp one (-3) = 0.125%float).
+Check (eq_refl 0.125%float <<: ldexp one (-3) = 0.125%float).
+
+Check (eq_refl : ldexp one 3 = 8%float).
+Check (eq_refl 8%float <: ldexp one 3 = 8%float).
+Check (eq_refl 8%float <<: ldexp one 3 = 8%float).
diff --git a/test-suite/primitive/float/mul.v b/test-suite/primitive/float/mul.v
new file mode 100644
index 0000000000..91fe7e9791
--- /dev/null
+++ b/test-suite/primitive/float/mul.v
@@ -0,0 +1,83 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+Definition six := Eval compute in of_int63 6%int63.
+
+Check (eq_refl : three * two = six).
+Check (eq_refl six <: three * two = six).
+Check (eq_refl six <<: three * two = six).
+Definition compute1 := Eval compute in three * two.
+Check (eq_refl compute1 : six = six).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge * tiny = one).
+Check (eq_refl one <: huge * tiny = one).
+Check (eq_refl one <<: huge * tiny = one).
+Definition compute2 := Eval compute in huge * tiny.
+Check (eq_refl compute2 : one = one).
+
+Check (eq_refl : huge * huge = infinity).
+Check (eq_refl infinity <: huge * huge = infinity).
+Check (eq_refl infinity <<: huge * huge = infinity).
+Definition compute3 := Eval compute in huge * huge.
+Check (eq_refl compute3 : infinity = infinity).
+
+Check (eq_refl : one * nan = nan).
+Check (eq_refl nan <: one * nan = nan).
+Check (eq_refl nan <<: one * nan = nan).
+Definition compute4 := Eval compute in one * nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity * infinity = infinity).
+Check (eq_refl infinity <: infinity * infinity = infinity).
+Check (eq_refl infinity <<: infinity * infinity = infinity).
+Definition compute5 := Eval compute in infinity * infinity.
+Check (eq_refl compute5 : infinity = infinity).
+
+Check (eq_refl : infinity * neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <: infinity * neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <<: infinity * neg_infinity = neg_infinity).
+Definition compute6 := Eval compute in infinity * neg_infinity.
+Check (eq_refl compute6 : neg_infinity = neg_infinity).
+
+Check (eq_refl : zero * zero = zero).
+Check (eq_refl zero <: zero * zero = zero).
+Check (eq_refl zero <<: zero * zero = zero).
+Check (eq_refl : neg_zero * zero = neg_zero).
+Check (eq_refl neg_zero <: neg_zero * zero = neg_zero).
+Check (eq_refl neg_zero <<: neg_zero * zero = neg_zero).
+Check (eq_refl : neg_zero * neg_zero = zero).
+Check (eq_refl zero <: neg_zero * neg_zero = zero).
+Check (eq_refl zero <<: neg_zero * neg_zero = zero).
+Check (eq_refl : zero * neg_zero = neg_zero).
+Check (eq_refl neg_zero <: zero * neg_zero = neg_zero).
+Check (eq_refl neg_zero <<: zero * neg_zero = neg_zero).
+
+Check (eq_refl : huge * neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <: huge * neg_infinity = neg_infinity).
+Check (eq_refl neg_infinity <<: huge * neg_infinity = neg_infinity).
+
+Check (eq_refl : one * tiny = tiny).
+Check (eq_refl tiny <: one * tiny = tiny).
+Check (eq_refl tiny <<: one * tiny = tiny).
+Check (eq_refl : one * huge = huge).
+Check (eq_refl huge <: one * huge = huge).
+Check (eq_refl huge <<: one * huge = huge).
+Check (eq_refl : zero * huge = zero).
+Check (eq_refl zero <: zero * huge = zero).
+Check (eq_refl zero <<: zero * huge = zero).
+Check (eq_refl : zero * (-huge) = neg_zero).
+Check (eq_refl neg_zero <: zero * (-huge) = neg_zero).
+Check (eq_refl neg_zero <<: zero * (-huge) = neg_zero).
+
+Check (eq_refl : zero * infinity = nan).
+Check (eq_refl nan <: zero * infinity = nan).
+Check (eq_refl nan <<: zero * infinity = nan).
+Check (eq_refl : neg_infinity * zero = nan).
+Check (eq_refl nan <: neg_infinity * zero = nan).
+Check (eq_refl nan <<: neg_infinity * zero = nan).
diff --git a/test-suite/primitive/float/next_up_down.v b/test-suite/primitive/float/next_up_down.v
new file mode 100644
index 0000000000..4f8427dc5b
--- /dev/null
+++ b/test-suite/primitive/float/next_up_down.v
@@ -0,0 +1,122 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition f0 := zero.
+Definition f1 := neg_zero.
+Definition f2 := Eval compute in ldexp one 0.
+Definition f3 := Eval compute in -f1.
+(* smallest positive float *)
+Definition f4 := Eval compute in ldexp one (-1074).
+Definition f5 := Eval compute in -f3.
+Definition f6 := infinity.
+Definition f7 := neg_infinity.
+Definition f8 := Eval compute in ldexp one (-1).
+Definition f9 := Eval compute in -f8.
+Definition f10 := Eval compute in of_int63 42.
+Definition f11 := Eval compute in -f10.
+(* max float *)
+Definition f12 := Eval compute in ldexp (of_int63 9007199254740991) 1024.
+Definition f13 := Eval compute in -f12.
+(* smallest positive normalized float *)
+Definition f14 := Eval compute in ldexp one (-1022).
+Definition f15 := Eval compute in -f14.
+
+Check (eq_refl : Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
+Check (eq_refl : Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
+Check (eq_refl : Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
+Check (eq_refl : Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
+Check (eq_refl : Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
+Check (eq_refl : Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
+Check (eq_refl : Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
+Check (eq_refl : Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
+Check (eq_refl : Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
+Check (eq_refl : Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
+Check (eq_refl : Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
+Check (eq_refl : Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
+Check (eq_refl : Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
+Check (eq_refl : Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
+Check (eq_refl : Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
+Check (eq_refl : Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
+Check (eq_refl : Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
+Check (eq_refl : Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
+Check (eq_refl : Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
+Check (eq_refl : Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
+Check (eq_refl : Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
+Check (eq_refl : Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
+Check (eq_refl : Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
+Check (eq_refl : Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
+Check (eq_refl : Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
+Check (eq_refl : Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
+Check (eq_refl : Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
+Check (eq_refl : Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
+Check (eq_refl : Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
+Check (eq_refl : Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
+Check (eq_refl : Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
+Check (eq_refl : Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
+
+Check (eq_refl (SF64succ (Prim2SF f0)) <: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
+Check (eq_refl (SF64pred (Prim2SF f0)) <: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
+Check (eq_refl (SF64succ (Prim2SF f1)) <: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
+Check (eq_refl (SF64pred (Prim2SF f1)) <: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
+Check (eq_refl (SF64succ (Prim2SF f2)) <: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
+Check (eq_refl (SF64pred (Prim2SF f2)) <: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
+Check (eq_refl (SF64succ (Prim2SF f3)) <: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
+Check (eq_refl (SF64pred (Prim2SF f3)) <: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
+Check (eq_refl (SF64succ (Prim2SF f4)) <: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
+Check (eq_refl (SF64pred (Prim2SF f4)) <: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
+Check (eq_refl (SF64succ (Prim2SF f5)) <: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
+Check (eq_refl (SF64pred (Prim2SF f5)) <: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
+Check (eq_refl (SF64succ (Prim2SF f6)) <: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
+Check (eq_refl (SF64pred (Prim2SF f6)) <: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
+Check (eq_refl (SF64succ (Prim2SF f7)) <: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
+Check (eq_refl (SF64pred (Prim2SF f7)) <: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
+Check (eq_refl (SF64succ (Prim2SF f8)) <: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
+Check (eq_refl (SF64pred (Prim2SF f8)) <: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
+Check (eq_refl (SF64succ (Prim2SF f9)) <: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
+Check (eq_refl (SF64pred (Prim2SF f9)) <: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
+Check (eq_refl (SF64succ (Prim2SF f10)) <: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
+Check (eq_refl (SF64pred (Prim2SF f10)) <: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
+Check (eq_refl (SF64succ (Prim2SF f11)) <: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
+Check (eq_refl (SF64pred (Prim2SF f11)) <: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
+Check (eq_refl (SF64succ (Prim2SF f12)) <: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
+Check (eq_refl (SF64pred (Prim2SF f12)) <: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
+Check (eq_refl (SF64succ (Prim2SF f13)) <: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
+Check (eq_refl (SF64pred (Prim2SF f13)) <: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
+Check (eq_refl (SF64succ (Prim2SF f14)) <: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
+Check (eq_refl (SF64pred (Prim2SF f14)) <: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
+Check (eq_refl (SF64succ (Prim2SF f15)) <: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
+Check (eq_refl (SF64pred (Prim2SF f15)) <: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
+
+Check (eq_refl (SF64succ (Prim2SF f0)) <<: Prim2SF (next_up f0) = SF64succ (Prim2SF f0)).
+Check (eq_refl (SF64pred (Prim2SF f0)) <<: Prim2SF (next_down f0) = SF64pred (Prim2SF f0)).
+Check (eq_refl (SF64succ (Prim2SF f1)) <<: Prim2SF (next_up f1) = SF64succ (Prim2SF f1)).
+Check (eq_refl (SF64pred (Prim2SF f1)) <<: Prim2SF (next_down f1) = SF64pred (Prim2SF f1)).
+Check (eq_refl (SF64succ (Prim2SF f2)) <<: Prim2SF (next_up f2) = SF64succ (Prim2SF f2)).
+Check (eq_refl (SF64pred (Prim2SF f2)) <<: Prim2SF (next_down f2) = SF64pred (Prim2SF f2)).
+Check (eq_refl (SF64succ (Prim2SF f3)) <<: Prim2SF (next_up f3) = SF64succ (Prim2SF f3)).
+Check (eq_refl (SF64pred (Prim2SF f3)) <<: Prim2SF (next_down f3) = SF64pred (Prim2SF f3)).
+Check (eq_refl (SF64succ (Prim2SF f4)) <<: Prim2SF (next_up f4) = SF64succ (Prim2SF f4)).
+Check (eq_refl (SF64pred (Prim2SF f4)) <<: Prim2SF (next_down f4) = SF64pred (Prim2SF f4)).
+Check (eq_refl (SF64succ (Prim2SF f5)) <<: Prim2SF (next_up f5) = SF64succ (Prim2SF f5)).
+Check (eq_refl (SF64pred (Prim2SF f5)) <<: Prim2SF (next_down f5) = SF64pred (Prim2SF f5)).
+Check (eq_refl (SF64succ (Prim2SF f6)) <<: Prim2SF (next_up f6) = SF64succ (Prim2SF f6)).
+Check (eq_refl (SF64pred (Prim2SF f6)) <<: Prim2SF (next_down f6) = SF64pred (Prim2SF f6)).
+Check (eq_refl (SF64succ (Prim2SF f7)) <<: Prim2SF (next_up f7) = SF64succ (Prim2SF f7)).
+Check (eq_refl (SF64pred (Prim2SF f7)) <<: Prim2SF (next_down f7) = SF64pred (Prim2SF f7)).
+Check (eq_refl (SF64succ (Prim2SF f8)) <<: Prim2SF (next_up f8) = SF64succ (Prim2SF f8)).
+Check (eq_refl (SF64pred (Prim2SF f8)) <<: Prim2SF (next_down f8) = SF64pred (Prim2SF f8)).
+Check (eq_refl (SF64succ (Prim2SF f9)) <<: Prim2SF (next_up f9) = SF64succ (Prim2SF f9)).
+Check (eq_refl (SF64pred (Prim2SF f9)) <<: Prim2SF (next_down f9) = SF64pred (Prim2SF f9)).
+Check (eq_refl (SF64succ (Prim2SF f10)) <<: Prim2SF (next_up f10) = SF64succ (Prim2SF f10)).
+Check (eq_refl (SF64pred (Prim2SF f10)) <<: Prim2SF (next_down f10) = SF64pred (Prim2SF f10)).
+Check (eq_refl (SF64succ (Prim2SF f11)) <<: Prim2SF (next_up f11) = SF64succ (Prim2SF f11)).
+Check (eq_refl (SF64pred (Prim2SF f11)) <<: Prim2SF (next_down f11) = SF64pred (Prim2SF f11)).
+Check (eq_refl (SF64succ (Prim2SF f12)) <<: Prim2SF (next_up f12) = SF64succ (Prim2SF f12)).
+Check (eq_refl (SF64pred (Prim2SF f12)) <<: Prim2SF (next_down f12) = SF64pred (Prim2SF f12)).
+Check (eq_refl (SF64succ (Prim2SF f13)) <<: Prim2SF (next_up f13) = SF64succ (Prim2SF f13)).
+Check (eq_refl (SF64pred (Prim2SF f13)) <<: Prim2SF (next_down f13) = SF64pred (Prim2SF f13)).
+Check (eq_refl (SF64succ (Prim2SF f14)) <<: Prim2SF (next_up f14) = SF64succ (Prim2SF f14)).
+Check (eq_refl (SF64pred (Prim2SF f14)) <<: Prim2SF (next_down f14) = SF64pred (Prim2SF f14)).
+Check (eq_refl (SF64succ (Prim2SF f15)) <<: Prim2SF (next_up f15) = SF64succ (Prim2SF f15)).
+Check (eq_refl (SF64pred (Prim2SF f15)) <<: Prim2SF (next_down f15) = SF64pred (Prim2SF f15)).
diff --git a/test-suite/primitive/float/normfr_mantissa.v b/test-suite/primitive/float/normfr_mantissa.v
new file mode 100644
index 0000000000..28bd1c03f5
--- /dev/null
+++ b/test-suite/primitive/float/normfr_mantissa.v
@@ -0,0 +1,28 @@
+Require Import Int63 ZArith Floats.
+
+Definition half := ldexp one (-1)%Z.
+Definition three_quarters := (half + (ldexp one (-2)%Z))%float.
+
+Check (eq_refl : normfr_mantissa one = 0%int63).
+Check (eq_refl : normfr_mantissa half = (1 << 52)%int63).
+Check (eq_refl : normfr_mantissa (-half) = (1 << 52)%int63).
+Check (eq_refl : normfr_mantissa (-one) = 0%int63).
+Check (eq_refl : normfr_mantissa zero = 0%int63).
+Check (eq_refl : normfr_mantissa nan = 0%int63).
+Check (eq_refl : normfr_mantissa three_quarters = (3 << 51)%int63).
+
+Check (eq_refl 0%int63 <: normfr_mantissa one = 0%int63).
+Check (eq_refl (1 << 52)%int63 <: normfr_mantissa half = (1 << 52)%int63).
+Check (eq_refl (1 << 52)%int63 <: normfr_mantissa (-half) = (1 << 52)%int63).
+Check (eq_refl 0%int63 <: normfr_mantissa (-one) = 0%int63).
+Check (eq_refl 0%int63 <: normfr_mantissa zero = 0%int63).
+Check (eq_refl 0%int63 <: normfr_mantissa nan = 0%int63).
+Check (eq_refl (3 << 51)%int63 <: normfr_mantissa three_quarters = (3 << 51)%int63).
+
+Check (eq_refl 0%int63 <<: normfr_mantissa one = 0%int63).
+Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa half = (1 << 52)%int63).
+Check (eq_refl (1 << 52)%int63 <<: normfr_mantissa (-half) = (1 << 52)%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa (-one) = 0%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa zero = 0%int63).
+Check (eq_refl 0%int63 <<: normfr_mantissa nan = 0%int63).
+Check (eq_refl (3 << 51)%int63 <<: normfr_mantissa three_quarters = (3 << 51)%int63).
diff --git a/test-suite/primitive/float/spec_conv.v b/test-suite/primitive/float/spec_conv.v
new file mode 100644
index 0000000000..a610d39671
--- /dev/null
+++ b/test-suite/primitive/float/spec_conv.v
@@ -0,0 +1,46 @@
+Require Import ZArith Floats.
+
+Definition two := Eval compute in (one + one)%float.
+Definition half := Eval compute in (one / two)%float.
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Check (eq_refl : SF2Prim (Prim2SF zero) = zero).
+Check (eq_refl : SF2Prim (Prim2SF neg_zero) = neg_zero).
+Check (eq_refl : SF2Prim (Prim2SF one) = one).
+Check (eq_refl : SF2Prim (Prim2SF (-one)) = (-one)%float).
+Check (eq_refl : SF2Prim (Prim2SF infinity) = infinity).
+Check (eq_refl : SF2Prim (Prim2SF neg_infinity) = neg_infinity).
+Check (eq_refl : SF2Prim (Prim2SF huge) = huge).
+Check (eq_refl : SF2Prim (Prim2SF tiny) = tiny).
+Check (eq_refl : SF2Prim (Prim2SF denorm) = denorm).
+Check (eq_refl : SF2Prim (Prim2SF nan) = nan).
+Check (eq_refl : SF2Prim (Prim2SF two) = two).
+Check (eq_refl : SF2Prim (Prim2SF half) = half).
+
+Check (eq_refl zero <: SF2Prim (Prim2SF zero) = zero).
+Check (eq_refl neg_zero <: SF2Prim (Prim2SF neg_zero) = neg_zero).
+Check (eq_refl one <: SF2Prim (Prim2SF one) = one).
+Check (eq_refl (-one)%float <: SF2Prim (Prim2SF (-one)) = (-one)%float).
+Check (eq_refl infinity <: SF2Prim (Prim2SF infinity) = infinity).
+Check (eq_refl neg_infinity <: SF2Prim (Prim2SF neg_infinity) = neg_infinity).
+Check (eq_refl huge <: SF2Prim (Prim2SF huge) = huge).
+Check (eq_refl tiny <: SF2Prim (Prim2SF tiny) = tiny).
+Check (eq_refl denorm <: SF2Prim (Prim2SF denorm) = denorm).
+Check (eq_refl nan <: SF2Prim (Prim2SF nan) = nan).
+Check (eq_refl two <: SF2Prim (Prim2SF two) = two).
+Check (eq_refl half <: SF2Prim (Prim2SF half) = half).
+
+Check (eq_refl zero <<: SF2Prim (Prim2SF zero) = zero).
+Check (eq_refl neg_zero <<: SF2Prim (Prim2SF neg_zero) = neg_zero).
+Check (eq_refl one <<: SF2Prim (Prim2SF one) = one).
+Check (eq_refl (-one)%float <<: SF2Prim (Prim2SF (-one)) = (-one)%float).
+Check (eq_refl infinity <<: SF2Prim (Prim2SF infinity) = infinity).
+Check (eq_refl neg_infinity <<: SF2Prim (Prim2SF neg_infinity) = neg_infinity).
+Check (eq_refl huge <<: SF2Prim (Prim2SF huge) = huge).
+Check (eq_refl tiny <<: SF2Prim (Prim2SF tiny) = tiny).
+Check (eq_refl denorm <<: SF2Prim (Prim2SF denorm) = denorm).
+Check (eq_refl nan <<: SF2Prim (Prim2SF nan) = nan).
+Check (eq_refl two <<: SF2Prim (Prim2SF two) = two).
+Check (eq_refl half <<: SF2Prim (Prim2SF half) = half).
diff --git a/test-suite/primitive/float/sqrt.v b/test-suite/primitive/float/sqrt.v
new file mode 100644
index 0000000000..04c8ab035d
--- /dev/null
+++ b/test-suite/primitive/float/sqrt.v
@@ -0,0 +1,49 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition three := Eval compute in of_int63 3%int63.
+Definition nine := Eval compute in of_int63 9%int63.
+
+Check (eq_refl : sqrt nine = three).
+Check (eq_refl three <: sqrt nine = three).
+Definition compute1 := Eval compute in sqrt nine.
+Check (eq_refl : three = three).
+
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Goal (Prim2SF (sqrt huge) = SF64sqrt (Prim2SF huge)).
+  now compute. Undo. now vm_compute.
+Qed.
+
+Goal (Prim2SF (sqrt tiny) = SF64sqrt (Prim2SF tiny)).
+  now compute. Undo. now vm_compute.
+Qed.
+
+Goal (Prim2SF (sqrt denorm) = SF64sqrt (Prim2SF denorm)).
+  now compute. Undo. now vm_compute.
+Qed.
+
+Check (eq_refl : sqrt neg_zero = neg_zero).
+Check (eq_refl neg_zero <: sqrt neg_zero = neg_zero).
+Check (eq_refl neg_zero <<: sqrt neg_zero = neg_zero).
+Check (eq_refl : sqrt zero = zero).
+Check (eq_refl zero <: sqrt zero = zero).
+Check (eq_refl zero <<: sqrt zero = zero).
+Check (eq_refl : sqrt one = one).
+Check (eq_refl one <: sqrt one = one).
+Check (eq_refl one <<: sqrt one = one).
+Check (eq_refl : sqrt (-one) = nan).
+Check (eq_refl nan <: sqrt (-one) = nan).
+Check (eq_refl nan <<: sqrt (-one) = nan).
+Check (eq_refl : sqrt infinity = infinity).
+Check (eq_refl infinity <: sqrt infinity = infinity).
+Check (eq_refl infinity <<: sqrt infinity = infinity).
+Check (eq_refl : sqrt neg_infinity = nan).
+Check (eq_refl nan <: sqrt neg_infinity = nan).
+Check (eq_refl nan <<: sqrt neg_infinity = nan).
+Check (eq_refl : sqrt infinity = infinity).
+Check (eq_refl infinity <: sqrt infinity = infinity).
+Check (eq_refl infinity <<: sqrt infinity = infinity).
diff --git a/test-suite/primitive/float/sub.v b/test-suite/primitive/float/sub.v
new file mode 100644
index 0000000000..fc068cb585
--- /dev/null
+++ b/test-suite/primitive/float/sub.v
@@ -0,0 +1,62 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in of_int63 2%int63.
+Definition three := Eval compute in of_int63 3%int63.
+
+Check (eq_refl : three - two = one).
+Check (eq_refl one <: three - two = one).
+Check (eq_refl one <<: three - two = one).
+Definition compute1 := Eval compute in three - two.
+Check (eq_refl compute1 : one = one).
+
+Definition huge := Eval compute in ldexp one 1023%Z.
+Definition tiny := Eval compute in ldexp one (-1023)%Z.
+
+Check (eq_refl : huge - tiny = huge).
+Check (eq_refl huge <: huge - tiny = huge).
+Check (eq_refl huge <<: huge - tiny = huge).
+Definition compute2 := Eval compute in huge - tiny.
+Check (eq_refl compute2 : huge = huge).
+
+Check (eq_refl : huge - huge = zero).
+Check (eq_refl zero <: huge - huge = zero).
+Check (eq_refl zero <<: huge - huge = zero).
+Definition compute3 := Eval compute in huge - huge.
+Check (eq_refl compute3 : zero = zero).
+
+Check (eq_refl : one - nan = nan).
+Check (eq_refl nan <: one - nan = nan).
+Check (eq_refl nan <<: one - nan = nan).
+Definition compute4 := Eval compute in one - nan.
+Check (eq_refl compute4 : nan = nan).
+
+Check (eq_refl : infinity - infinity = nan).
+Check (eq_refl nan <: infinity - infinity = nan).
+Check (eq_refl nan <<: infinity - infinity = nan).
+Definition compute5 := Eval compute in infinity - infinity.
+Check (eq_refl compute5 : nan = nan).
+
+Check (eq_refl : infinity - neg_infinity = infinity).
+Check (eq_refl infinity <: infinity - neg_infinity = infinity).
+Check (eq_refl infinity <<: infinity - neg_infinity = infinity).
+Definition compute6 := Eval compute in infinity - neg_infinity.
+Check (eq_refl compute6 : infinity = infinity).
+
+Check (eq_refl : zero - zero = zero).
+Check (eq_refl zero <: zero - zero = zero).
+Check (eq_refl zero <<: zero - zero = zero).
+Check (eq_refl : neg_zero - zero = neg_zero).
+Check (eq_refl neg_zero <: neg_zero - zero = neg_zero).
+Check (eq_refl neg_zero <<: neg_zero - zero = neg_zero).
+Check (eq_refl : neg_zero - neg_zero = zero).
+Check (eq_refl zero <: neg_zero - neg_zero = zero).
+Check (eq_refl zero <<: neg_zero - neg_zero = zero).
+Check (eq_refl : zero - neg_zero = zero).
+Check (eq_refl zero <: zero - neg_zero = zero).
+Check (eq_refl zero <<: zero - neg_zero = zero).
+
+Check (eq_refl : huge - neg_infinity = infinity).
+Check (eq_refl infinity <: huge - neg_infinity = infinity).
+Check (eq_refl infinity <<: huge - neg_infinity = infinity).
diff --git a/test-suite/primitive/float/syntax.v b/test-suite/primitive/float/syntax.v
new file mode 100644
index 0000000000..cc0bbcf628
--- /dev/null
+++ b/test-suite/primitive/float/syntax.v
@@ -0,0 +1,13 @@
+Require Import Floats.
+
+Open Scope float_scope.
+
+Definition two := Eval compute in one + one.
+Definition half := Eval compute in one / two.
+
+Check (eq_refl : 1.5 = one + half).
+Check (eq_refl : 15e-1 = one + half).
+Check (eq_refl : 150e-2 = one + half).
+Check (eq_refl : 0.15e+1 = one + half).
+Check (eq_refl : 0.15e1 = one + half).
+Check (eq_refl : 0.0015e3 = one + half).
diff --git a/test-suite/primitive/float/valid_binary_conv.v b/test-suite/primitive/float/valid_binary_conv.v
new file mode 100644
index 0000000000..82e00b8532
--- /dev/null
+++ b/test-suite/primitive/float/valid_binary_conv.v
@@ -0,0 +1,46 @@
+Require Import ZArith Floats.
+
+Definition two := Eval compute in (one + one)%float.
+Definition half := Eval compute in (one / two)%float.
+Definition huge := Eval compute in ldexp one (1023)%Z.
+Definition tiny := Eval compute in ldexp one (-1022)%Z.
+Definition denorm := Eval compute in ldexp one (-1074)%Z.
+
+Check (eq_refl : valid_binary (Prim2SF zero) = true).
+Check (eq_refl : valid_binary (Prim2SF neg_zero) = true).
+Check (eq_refl : valid_binary (Prim2SF one) = true).
+Check (eq_refl : valid_binary (Prim2SF (-one)) = true).
+Check (eq_refl : valid_binary (Prim2SF infinity) = true).
+Check (eq_refl : valid_binary (Prim2SF neg_infinity) = true).
+Check (eq_refl : valid_binary (Prim2SF huge) = true).
+Check (eq_refl : valid_binary (Prim2SF tiny) = true).
+Check (eq_refl : valid_binary (Prim2SF denorm) = true).
+Check (eq_refl : valid_binary (Prim2SF nan) = true).
+Check (eq_refl : valid_binary (Prim2SF two) = true).
+Check (eq_refl : valid_binary (Prim2SF half) = true).
+
+Check (eq_refl true <: valid_binary (Prim2SF zero) = true).
+Check (eq_refl true <: valid_binary (Prim2SF neg_zero) = true).
+Check (eq_refl true <: valid_binary (Prim2SF one) = true).
+Check (eq_refl true <: valid_binary (Prim2SF (-one)) = true).
+Check (eq_refl true <: valid_binary (Prim2SF infinity) = true).
+Check (eq_refl true <: valid_binary (Prim2SF neg_infinity) = true).
+Check (eq_refl true <: valid_binary (Prim2SF huge) = true).
+Check (eq_refl true <: valid_binary (Prim2SF tiny) = true).
+Check (eq_refl true <: valid_binary (Prim2SF denorm) = true).
+Check (eq_refl true <: valid_binary (Prim2SF nan) = true).
+Check (eq_refl true <: valid_binary (Prim2SF two) = true).
+Check (eq_refl true <: valid_binary (Prim2SF half) = true).
+
+Check (eq_refl true <<: valid_binary (Prim2SF zero) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF neg_zero) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF one) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF (-one)) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF infinity) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF neg_infinity) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF huge) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF tiny) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF denorm) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF nan) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF two) = true).
+Check (eq_refl true <<: valid_binary (Prim2SF half) = true).
diff --git a/test-suite/primitive/float/zero.v b/test-suite/primitive/float/zero.v
new file mode 100644
index 0000000000..75348d4657
--- /dev/null
+++ b/test-suite/primitive/float/zero.v
@@ -0,0 +1,7 @@
+Require Import ZArith Int63 Floats.
+
+Open Scope float_scope.
+
+Fail Check (eq_refl : zero = neg_zero).
+Fail Check (eq_refl <: zero = neg_zero).
+Fail Check (eq_refl <<: zero = neg_zero).
diff --git a/test-suite/arithmetic/add.v b/test-suite/primitive/uint63/add.v
index fb7eb1d53c..fb7eb1d53c 100644
--- a/test-suite/arithmetic/add.v
+++ b/test-suite/primitive/uint63/add.v
diff --git a/test-suite/arithmetic/addc.v b/test-suite/primitive/uint63/addc.v
index 432aec0291..432aec0291 100644
--- a/test-suite/arithmetic/addc.v
+++ b/test-suite/primitive/uint63/addc.v
diff --git a/test-suite/arithmetic/addcarryc.v b/test-suite/primitive/uint63/addcarryc.v
index a4430769ca..a4430769ca 100644
--- a/test-suite/arithmetic/addcarryc.v
+++ b/test-suite/primitive/uint63/addcarryc.v
diff --git a/test-suite/arithmetic/addmuldiv.v b/test-suite/primitive/uint63/addmuldiv.v
index 72b0164b49..72b0164b49 100644
--- a/test-suite/arithmetic/addmuldiv.v
+++ b/test-suite/primitive/uint63/addmuldiv.v
diff --git a/test-suite/arithmetic/compare.v b/test-suite/primitive/uint63/compare.v
index a8d1ea1226..a8d1ea1226 100644
--- a/test-suite/arithmetic/compare.v
+++ b/test-suite/primitive/uint63/compare.v
diff --git a/test-suite/arithmetic/div.v b/test-suite/primitive/uint63/div.v
index 0ee0b91580..0ee0b91580 100644
--- a/test-suite/arithmetic/div.v
+++ b/test-suite/primitive/uint63/div.v
diff --git a/test-suite/arithmetic/diveucl.v b/test-suite/primitive/uint63/diveucl.v
index 8f88a0f356..8f88a0f356 100644
--- a/test-suite/arithmetic/diveucl.v
+++ b/test-suite/primitive/uint63/diveucl.v
diff --git a/test-suite/arithmetic/diveucl_21.v b/test-suite/primitive/uint63/diveucl_21.v
index b888c97be3..b12dba429c 100644
--- a/test-suite/arithmetic/diveucl_21.v
+++ b/test-suite/primitive/uint63/diveucl_21.v
@@ -10,11 +10,11 @@ Check (eq_refl (4611686018427387904,1) <<: diveucl_21 1 1 2 = (46116860184273879
 Definition compute1 := Eval compute in diveucl_21 1 1 2.
 Check (eq_refl compute1 : (4611686018427387904,1) = (4611686018427387904,1)).
 
-Check (eq_refl : diveucl_21 3 1 2 = (4611686018427387904, 1)).
-Check (eq_refl (4611686018427387904, 1) <: diveucl_21 3 1 2 = (4611686018427387904, 1)).
-Check (eq_refl (4611686018427387904, 1) <<: diveucl_21 3 1 2 = (4611686018427387904, 1)).
+Check (eq_refl : diveucl_21 3 1 2 = (0, 0)).
+Check (eq_refl (0, 0) <: diveucl_21 3 1 2 = (0, 0)).
+Check (eq_refl (0, 0) <<: diveucl_21 3 1 2 = (0, 0)).
 Definition compute2 := Eval compute in diveucl_21 3 1 2.
-Check (eq_refl compute2 : (4611686018427387904, 1) = (4611686018427387904, 1)).
+Check (eq_refl compute2 : (0, 0) = (0, 0)).
 
 Check (eq_refl : diveucl_21 1 1 0 = (0,0)).
 Check (eq_refl (0,0) <: diveucl_21 1 1 0 = (0,0)).
@@ -23,3 +23,7 @@ Check (eq_refl (0,0) <<: diveucl_21 1 1 0 = (0,0)).
 Check (eq_refl : diveucl_21 9223372036854775807 0 1 = (0,0)).
 Check (eq_refl (0,0) <: diveucl_21 9223372036854775807 0 1 = (0,0)).
 Check (eq_refl (0,0) <<: diveucl_21 9223372036854775807 0 1 = (0,0)).
+
+Check (eq_refl : diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
+Check (eq_refl (17407905077428, 3068214991893055266) <: diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
+Check (eq_refl (17407905077428, 3068214991893055266) <<: diveucl_21 9305446873517 1793572051078448654 4930380657631323783 = (17407905077428, 3068214991893055266)).
diff --git a/test-suite/arithmetic/eqb.v b/test-suite/primitive/uint63/eqb.v
index dcc0b71f6d..dcc0b71f6d 100644
--- a/test-suite/arithmetic/eqb.v
+++ b/test-suite/primitive/uint63/eqb.v
diff --git a/test-suite/arithmetic/head0.v b/test-suite/primitive/uint63/head0.v
index f4234d2605..f4234d2605 100644
--- a/test-suite/arithmetic/head0.v
+++ b/test-suite/primitive/uint63/head0.v
diff --git a/test-suite/arithmetic/isint.v b/test-suite/primitive/uint63/isint.v
index c215caa878..c215caa878 100644
--- a/test-suite/arithmetic/isint.v
+++ b/test-suite/primitive/uint63/isint.v
diff --git a/test-suite/arithmetic/land.v b/test-suite/primitive/uint63/land.v
index 0ea6fd90b6..0ea6fd90b6 100644
--- a/test-suite/arithmetic/land.v
+++ b/test-suite/primitive/uint63/land.v
diff --git a/test-suite/arithmetic/leb.v b/test-suite/primitive/uint63/leb.v
index 5354919978..5354919978 100644
--- a/test-suite/arithmetic/leb.v
+++ b/test-suite/primitive/uint63/leb.v
diff --git a/test-suite/arithmetic/lor.v b/test-suite/primitive/uint63/lor.v
index 9c3b85c054..9c3b85c054 100644
--- a/test-suite/arithmetic/lor.v
+++ b/test-suite/primitive/uint63/lor.v
diff --git a/test-suite/arithmetic/lsl.v b/test-suite/primitive/uint63/lsl.v
index 70f3b90140..70f3b90140 100644
--- a/test-suite/arithmetic/lsl.v
+++ b/test-suite/primitive/uint63/lsl.v
diff --git a/test-suite/arithmetic/lsr.v b/test-suite/primitive/uint63/lsr.v
index c36c24e237..c36c24e237 100644
--- a/test-suite/arithmetic/lsr.v
+++ b/test-suite/primitive/uint63/lsr.v
diff --git a/test-suite/arithmetic/ltb.v b/test-suite/primitive/uint63/ltb.v
index 7ae5ac6493..7ae5ac6493 100644
--- a/test-suite/arithmetic/ltb.v
+++ b/test-suite/primitive/uint63/ltb.v
diff --git a/test-suite/arithmetic/lxor.v b/test-suite/primitive/uint63/lxor.v
index b453fc7697..b453fc7697 100644
--- a/test-suite/arithmetic/lxor.v
+++ b/test-suite/primitive/uint63/lxor.v
diff --git a/test-suite/arithmetic/mod.v b/test-suite/primitive/uint63/mod.v
index 5307eed493..5307eed493 100644
--- a/test-suite/arithmetic/mod.v
+++ b/test-suite/primitive/uint63/mod.v
diff --git a/test-suite/arithmetic/mul.v b/test-suite/primitive/uint63/mul.v
index 9480e8cd46..9480e8cd46 100644
--- a/test-suite/arithmetic/mul.v
+++ b/test-suite/primitive/uint63/mul.v
diff --git a/test-suite/arithmetic/mulc.v b/test-suite/primitive/uint63/mulc.v
index e10855bafa..e10855bafa 100644
--- a/test-suite/arithmetic/mulc.v
+++ b/test-suite/primitive/uint63/mulc.v
diff --git a/test-suite/arithmetic/reduction.v b/test-suite/primitive/uint63/reduction.v
index 00e067ac5a..00e067ac5a 100644
--- a/test-suite/arithmetic/reduction.v
+++ b/test-suite/primitive/uint63/reduction.v
diff --git a/test-suite/arithmetic/sub.v b/test-suite/primitive/uint63/sub.v
index 1606fd2aa1..1606fd2aa1 100644
--- a/test-suite/arithmetic/sub.v
+++ b/test-suite/primitive/uint63/sub.v
diff --git a/test-suite/arithmetic/subc.v b/test-suite/primitive/uint63/subc.v
index fc4067e48b..fc4067e48b 100644
--- a/test-suite/arithmetic/subc.v
+++ b/test-suite/primitive/uint63/subc.v
diff --git a/test-suite/arithmetic/subcarryc.v b/test-suite/primitive/uint63/subcarryc.v
index e81b6536b2..e81b6536b2 100644
--- a/test-suite/arithmetic/subcarryc.v
+++ b/test-suite/primitive/uint63/subcarryc.v
diff --git a/test-suite/arithmetic/tail0.v b/test-suite/primitive/uint63/tail0.v
index c9d426087a..c9d426087a 100644
--- a/test-suite/arithmetic/tail0.v
+++ b/test-suite/primitive/uint63/tail0.v
diff --git a/test-suite/arithmetic/unsigned.v b/test-suite/primitive/uint63/unsigned.v
index 82920bd201..82920bd201 100644
--- a/test-suite/arithmetic/unsigned.v
+++ b/test-suite/primitive/uint63/unsigned.v
diff --git a/test-suite/ssr/bang_rewrite.v b/test-suite/ssr/bang_rewrite.v
new file mode 100644
index 0000000000..30e6d57a7a
--- /dev/null
+++ b/test-suite/ssr/bang_rewrite.v
@@ -0,0 +1,13 @@
+Set Universe Polymorphism.
+
+Require Import ssreflect.
+
+Axiom mult@{i} : nat -> nat -> nat.
+Notation "m * n" := (mult m n).
+
+Axiom multA : forall a b c, (a * b) * c = a * (b * c).
+
+(* Previously the following gave a universe error: *)
+
+Lemma multAA a b c d : ((a * b) * c) * d = a * (b * (c * d)).
+Proof. by rewrite !multA. Qed.
diff --git a/test-suite/ssr/congr.v b/test-suite/ssr/congr.v
index 026f7538e8..f85791b00b 100644
--- a/test-suite/ssr/congr.v
+++ b/test-suite/ssr/congr.v
@@ -32,3 +32,11 @@ Coercion f : nat >-> Equality.sort.
 
 Lemma test4 : forall a b : nat, b = a -> @eq S (b + b) (a + a).
 Proof. move=> a b Eba; congr (_ + _); exact:  Eba. Qed.
+
+Open Scope type_scope.
+
+Lemma test5 : forall (P Q Q' : Type) (h : Q = Q'), P * Q = P * Q'.
+Proof. move=>*; by congr (_ * _). Qed.
+
+Lemma test6 : forall (P Q Q' : Type) (h : Q = Q'), P * Q -> P * Q'.
+Proof. move=> P Q Q' h; by congr (_ * _). Qed.
diff --git a/test-suite/ssr/over.v b/test-suite/ssr/over.v
index 8232741b0d..267d981d05 100644
--- a/test-suite/ssr/over.v
+++ b/test-suite/ssr/over.v
@@ -12,7 +12,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i).
   unfold x2 in *; clear x2;
   unfold R in *; clear R;
   unfold I in *; clear I.
-  apply Under_eq_from_eq.
+  apply Under_rel_from_rel.
   Fail done.
 
   over.
@@ -27,7 +27,7 @@ assert (H : forall i : nat, i + 2 * i - i = x2 i).
   unfold x2 in *; clear x2;
   unfold R in *; clear R;
   unfold I in *; clear I.
-  apply Under_eq_from_eq.
+  apply Under_rel_from_rel.
   Fail done.
 
   by rewrite over.
@@ -45,7 +45,7 @@ assert (H : forall i j, i + 2 * j - i = x2 i j).
   unfold R in *; clear R;
   unfold J in *; clear J;
   unfold I in *; clear I.
-  apply Under_eq_from_eq.
+  apply Under_rel_from_rel.
   Fail done.
 
   over.
@@ -61,7 +61,7 @@ assert (H : forall i j : nat, i + 2 * j - i = x2 i j).
   unfold R in *; clear R;
   unfold J in *; clear J;
   unfold I in *; clear I.
-  apply Under_eq_from_eq.
+  apply Under_rel_from_rel.
   Fail done.
 
   rewrite over.
diff --git a/test-suite/ssr/under.v b/test-suite/ssr/under.v
index f285ad138b..c12491138a 100644
--- a/test-suite/ssr/under.v
+++ b/test-suite/ssr/under.v
@@ -160,7 +160,15 @@ Lemma test_big_occs (F G : nat -> nat) (n : nat) :
   \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0).
 Proof.
 under {2}[in RHS]eq_bigr => i Hi do rewrite muln0.
-by rewrite big_const_nat iter_addn_0.
+by rewrite big_const_nat iter_addn_0 mul0n addn0.
+Qed.
+
+Lemma test_big_occs_inH (F G : nat -> nat) (n : nat) :
+  \sum_(0 <= i < n) (i * 0) = \sum_(0 <= i < n) (i * 0) + \sum_(0 <= i < n) (i * 0) -> True.
+Proof.
+move=> H.
+do [under {2}[in RHS]eq_bigr => i Hi do rewrite muln0] in H.
+by rewrite big_const_nat iter_addn_0 mul0n addn0 in H.
 Qed.
 
 (* Solely used, one such renaming is useless in practice, but it works anyway *)
@@ -218,7 +226,6 @@ under Lub_Rbar_eqset => r.
 by rewrite over.
 Abort.
 
-
 Lemma ex_iff R (P1 P2 : R -> Prop) :
   (forall x : R, P1 x <-> P2 x) -> ((exists x, P1 x) <-> (exists x, P2 x)).
 Proof.
@@ -227,8 +234,149 @@ Qed.
 
 Arguments ex_iff [R P1] P2 iffP12.
 
-Require Import Setoid.
+(** Load the [setoid_rewrite] machinery *)
+Require Setoid.
+
+(** Replay the tactics from [test_Lub_Rbar] in this new environment *)
+Lemma test_Lub_Rbar_again (E : R -> Prop)  :
+  Rbar_le Rbar0 (Lub_Rbar (fun x => x = R0 \/ E x)).
+Proof.
+under Lub_Rbar_eqset => r.
+by rewrite over.
+Abort.
+
 Lemma test_ex_iff (P : nat -> Prop) : (exists x, P x) -> True.
-under ex_iff => n.
+under ex_iff => n. (* this requires [Setoid] *)
 by rewrite over.
+by move=> _.
+Qed.
+
+Section TestGeneric.
+Context {A B : Type} {R : nat -> B -> B -> Prop}
+        `{!forall n : nat, RelationClasses.Equivalence (R n)}.
+Variables (F : (A -> A -> B) -> B).
+Hypothesis ex_gen : forall (n : nat) (P1 P2 : A -> A -> B),
+  (forall x y : A, R n (P1 x y) (P2 x y)) -> (R n (F P1) (F P2)).
+Arguments ex_gen [n P1] P2 relP12.
+Lemma test_ex_gen (P1 P2 : A -> A -> B) (n : nat) :
+  (forall x y : A, P2 x y = P2 y x) ->
+  R n (F P1) (F P2) /\ True -> True.
+Proof.
+move=> P2C.
+under [X in R _ _ X]ex_gen => a b.
+  by rewrite P2C over.
+by move => _.
+Qed.
+End TestGeneric.
+
+Import Setoid.
+(* to expose [Coq.Relations.Relation_Definitions.reflexive],
+   [Coq.Classes.RelationClasses.RewriteRelation], and so on. *)
+
+Section TestGeneric2.
+(* Some toy abstract example with a parameterized setoid type *)
+Record Setoid (m n : nat) : Type :=
+  { car : Type
+  ; Rel : car -> car -> Prop
+  ; refl : reflexive _ Rel
+  ; sym : symmetric _ Rel
+  ; trans : transitive _ Rel
+  }.
+
+Context {m n : nat}.
+Add Parametric Relation (s : Setoid m n) : (car s) (@Rel _ _ s)
+  reflexivity proved by (@refl _ _ s)
+  symmetry proved by (@sym _ _ s)
+  transitivity proved by (@trans _ _ s)
+  as eq_rel.
+
+Context {A : Type} {s1 s2 : Setoid m n}.
+
+Let B := @car m n s1.
+Let C := @car m n s2.
+Variable (F : C -> (A -> A -> B) -> C).
+Hypothesis rel2_gen :
+  forall (c1 c2 : C) (P1 P2 : A -> A -> B),
+    Rel c1 c2 ->
+    (forall a b : A, Rel (P1 a b) (P2 a b)) ->
+    Rel (F c1 P1) (F c2 P2).
+Arguments rel2_gen [c1] c2 [P1] P2 relc12 relP12.
+Lemma test_rel2_gen (c : C) (P : A -> A -> B)
+  (toy_hyp : forall a b, P a b = P b a) :
+  Rel (F c P) (F c (fun a b => P b a)).
+Proof.
+under [here in Rel _ here]rel2_gen.
+- over.
+- by move=> a b; rewrite toy_hyp over.
+- reflexivity.
+Qed.
+End TestGeneric2.
+
+Section TestPreOrder.
+(* inspired by https://github.com/coq/coq/pull/10022#issuecomment-530101950
+   but without needing to do [rewrite UnderE] manually. *)
+
+Require Import Morphisms.
+
+(** Tip to tell rewrite that the LHS of [leq' x y (:= leq x y = true)]
+    is x, not [leq x y] *)
+Definition rel_true {T} (R : rel T) x y := is_true (R x y).
+Definition leq' : nat -> nat -> Prop := rel_true leq.
+
+Parameter leq_add :
+  forall m1 m2 n1 n2 : nat, m1 <= n1 -> m2 <= n2 -> m1 + m2 <= n1 + n2.
+Parameter leq_mul :
+ forall m1 m2 n1 n2 : nat, m1 <= n1 -> m2 <= n2 -> m1 * m2 <= n1 * n2.
+
+Local Notation "+%N" := addn (at level 0, only parsing).
+
+(** Context lemma (could *)
+Lemma leq'_big : forall I (F G : I -> nat) (r : seq I),
+    (forall i : I, leq' (F i) (G i)) ->
+    (leq' (\big[+%N/0%N]_(i <- r) F i) (\big[+%N/0%N]_(i <- r) G i)).
+Proof.
+red=> F G m n HFG.
+apply: (big_ind2 leq _ _ (P := xpredT) (op1 := addn) (op2 := addn)) =>//.
+move=> *; exact: leq_add.
+move=> *; exact: HFG.
+Qed.
+
+(** Instances for [setoid_rewrite] *)
+Instance leq'_rr : RewriteRelation leq' := {}.
+
+Instance leq'_proper_addn : Proper (leq' ==> leq' ==> leq') addn.
+Proof. move=> a1 b1 le1 a2 b2 le2; exact/leq_add. Qed.
+
+Instance leq'_proper_muln : Proper (leq' ==> leq' ==> leq') muln.
+Proof. move=> a1 b1 le1 a2 b2 le2; exact/leq_mul. Qed.
+
+
+Instance leq'_preorder : PreOrder leq'.
+(** encompasses [Reflexive] *)
+Proof. rewrite /leq' /rel_true; split =>// ??? A B; exact: leq_trans A B. Qed.
+
+Instance leq'_reflexive : Reflexive leq'.
+Proof. by rewrite /leq' /rel_true. Qed.
+
+Parameter leq_add2l :
+  forall p m n : nat, (p + m <= p + n) = (m <= n).
+
+Lemma test : forall n : nat,
+  (1 + 2 * (\big[+%N/0]_(i < n) (3 + i)) * 4 + 5 <= 6 + 24 * n + 8 * n * n)%N.
+Proof.
+move=> n; rewrite -[is_true _]/(rel_true _ _ _) -/leq'.
+have lem : forall (i : nat), i < n -> leq' (3 + i) (3 + n).
+{ by move=> i Hi; rewrite /leq' /rel_true leq_add2l; apply/ltnW. }
+
+under leq'_big => i.
+{
+  (* The "magic" is here: instantiate the evar with the bound "3 + n" *)
+  rewrite lem ?ltn_ord //. over.
+}
+cbv beta.
+
+now_show (leq' (1 + 2 * \big[+%N/0]_(i < n) (3 + n) * 4 + 5) (6 + 24 * n + 8 * n * n)).
+(* uninteresting end of proof, omitted *)
 Abort.
+
+End TestPreOrder.
diff --git a/test-suite/success/Compat88.v b/test-suite/success/Compat88.v
deleted file mode 100644
index 1233a4b8f5..0000000000
--- a/test-suite/success/Compat88.v
+++ /dev/null
@@ -1,18 +0,0 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
-(** Check that various syntax usage is available without importing
-    relevant files. *)
-Require Coq.Strings.Ascii Coq.Strings.String.
-Require Coq.ZArith.BinIntDef Coq.PArith.BinPosDef Coq.NArith.BinNatDef.
-Require Coq.Reals.Rdefinitions.
-Require Coq.Numbers.Cyclic.Int63.Cyclic63.
-
-Require Import Coq.Compat.Coq88. (* XXX FIXME Should not need [Require], see https://github.com/coq/coq/issues/8311 *)
-
-Check String.String "a" String.EmptyString.
-Check String.eqb "a" "a".
-Check Nat.eqb 1 1.
-Check BinNat.N.eqb 1 1.
-Check BinInt.Z.eqb 1 1.
-Check BinPos.Pos.eqb 1 1.
-Check Rdefinitions.Rplus 1 1.
-Check Int63.is_zero 1.
diff --git a/test-suite/success/CompatCurrentFlag.v b/test-suite/success/CompatCurrentFlag.v
index 81469d79c3..fd6101bf89 100644
--- a/test-suite/success/CompatCurrentFlag.v
+++ b/test-suite/success/CompatCurrentFlag.v
@@ -1,3 +1,3 @@
-(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.11") -*- *)
 (** Check that the current compatibility flag actually requires the relevant modules. *)
-Import Coq.Compat.Coq810.
+Import Coq.Compat.Coq811.
diff --git a/test-suite/success/CompatOldFlag.v b/test-suite/success/CompatOldFlag.v
index afeb57f9f2..f774cef44f 100644
--- a/test-suite/success/CompatOldFlag.v
+++ b/test-suite/success/CompatOldFlag.v
@@ -1,5 +1,5 @@
-(* -*- coq-prog-args: ("-compat" "8.8") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
 (** Check that the current-minus-two compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq811.
 Import Coq.Compat.Coq810.
 Import Coq.Compat.Coq89.
-Import Coq.Compat.Coq88.
diff --git a/test-suite/success/CompatPreviousFlag.v b/test-suite/success/CompatPreviousFlag.v
index c8f75915c8..1c5ccc1a92 100644
--- a/test-suite/success/CompatPreviousFlag.v
+++ b/test-suite/success/CompatPreviousFlag.v
@@ -1,4 +1,4 @@
-(* -*- coq-prog-args: ("-compat" "8.9") -*- *)
+(* -*- coq-prog-args: ("-compat" "8.10") -*- *)
 (** Check that the current-minus-one compatibility flag actually requires the relevant modules. *)
+Import Coq.Compat.Coq811.
 Import Coq.Compat.Coq810.
-Import Coq.Compat.Coq89.
diff --git a/test-suite/success/Fixpoint.v b/test-suite/success/Fixpoint.v
index 81c9763ccd..6c333121da 100644
--- a/test-suite/success/Fixpoint.v
+++ b/test-suite/success/Fixpoint.v
@@ -96,10 +96,25 @@ Section visibility.
 
   Let Fixpoint by_proof (n:nat) : True.
   Proof. exact I. Defined.
+
+  Let Fixpoint foo (n:nat) : bool with bar (n:nat) : bool.
+  Proof.
+    - destruct n as [|n].
+      + exact true.
+      + exact (bar n).
+    - destruct n as [|n].
+      + exact false.
+      + exact (foo n).
+  Qed.
+
+  Let Fixpoint bla (n:nat) : Type with bli (n:nat) : bool.
+  Admitted.
+
 End visibility.
 
 Fail Check imm.
 Fail Check by_proof.
+Check bla. Check bli.
 
 Module Import mod_local.
   Fixpoint imm_importable (n:nat) : True := I.
diff --git a/test-suite/success/Nia.v b/test-suite/success/Nia.v
index 62ecece792..2eac9660b4 100644
--- a/test-suite/success/Nia.v
+++ b/test-suite/success/Nia.v
@@ -4,7 +4,8 @@ Open Scope Z_scope.
 
 (** Add [Z.to_euclidean_division_equations] to the end of [zify], just for this
     file. *)
-Ltac zify ::= repeat (zify_nat; zify_positive; zify_N); zify_op; Z.to_euclidean_division_equations.
+Require  Zify.
+Ltac Zify.zify_post_hook ::= Z.to_euclidean_division_equations.
 
 Lemma Z_zerop_or x : x = 0 \/ x <> 0. Proof. nia. Qed.
 Lemma Z_eq_dec_or (x y : Z) : x = y \/ x <> y. Proof. nia. Qed.
diff --git a/test-suite/success/NotationDeprecation.v b/test-suite/success/NotationDeprecation.v
index d313ba0aa4..96814a1b97 100644
--- a/test-suite/success/NotationDeprecation.v
+++ b/test-suite/success/NotationDeprecation.v
@@ -1,13 +1,13 @@
 Module Syndefs.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Notation foo := Prop.
 
-Notation bar := Prop (compat "8.8").
+Notation bar := Prop (compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Notation zar := Prop (compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Notation zar := Prop (compat "8.9").
 
 Check foo.
 Check bar.
@@ -21,14 +21,14 @@ End Syndefs.
 
 Module Notations.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Notation "!!" := Prop.
 
-Notation "##" := Prop (compat "8.8").
+Notation "##" := Prop (compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Notation "**" := Prop (compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Notation "**" := Prop (compat "8.9").
 
 Check !!.
 Check ##.
@@ -42,14 +42,14 @@ End Notations.
 
 Module Infix.
 
-#[deprecated(since = "8.8", note = "Do not use.")]
+#[deprecated(since = "8.9", note = "Do not use.")]
 Infix "!!" := plus (at level 1).
 
-Infix "##" := plus (at level 1, compat "8.8").
+Infix "##" := plus (at level 1, compat "8.9").
 
 Fail
-#[deprecated(since = "8.8", note = "Do not use.")]
-Infix "**" := plus (at level 1, compat "8.8").
+#[deprecated(since = "8.9", note = "Do not use.")]
+Infix "**" := plus (at level 1, compat "8.9").
 
 Check (_ !! _).
 Check (_ ## _).
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index e38affd7fa..998f3f7dd1 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -58,8 +58,8 @@ Section Geometry.
    https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr
 *)
 
-Require Import List.
 Require Import Reals.
+Require Import List.
 
 Record point:Type:={
  X:R;
@@ -419,13 +419,13 @@ Qed.
 
 
 
-Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point,
+Lemma Desargues: forall A B C A1 B1 C1 P Q T S:point,
   X S = 0 -> Y S = 0 -> Y A = 0 ->
   collinear A S A1 -> collinear B S B1 -> collinear C S C1 ->
   collinear B1 C1 P -> collinear B C P ->
   collinear A1 C1 Q -> collinear A C Q -> 
-  collinear A1 B1 R -> collinear A B R ->
-  collinear P Q R
+  collinear A1 B1 T -> collinear A B T ->
+  collinear P Q T
   \/ X A = X B \/ X A = X C \/ X B = X C  \/ X A = 0 \/ Y B = 0 \/ Y C = 0
   \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1.
 Proof.
@@ -440,8 +440,8 @@ let lv := rev (X A
              :: Y A1 :: X A1
                 :: Y B1
                    :: Y C1
-                      :: X R
-                         :: Y R
+                      :: X T
+                         :: Y T
                             :: X Q
                                :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in
 nsatz with radicalmax :=1%N strategy:=0%Z
diff --git a/test-suite/success/RefineInstance.v b/test-suite/success/RefineInstance.v
new file mode 100644
index 0000000000..f4d2f07db5
--- /dev/null
+++ b/test-suite/success/RefineInstance.v
@@ -0,0 +1,23 @@
+
+
+Class Foo := foo { a : nat; b : bool }.
+
+Fail Instance bla : Foo := { b:= true }.
+
+#[refine] Instance bla : Foo := { b:= true }.
+Proof.
+exact 0.
+Defined.
+
+Instance bli : Foo := { a:=1; b := false}.
+Check bli.
+
+Fail #[program, refine] Instance bla : Foo := {b := true}.
+
+#[program] Instance blo : Foo := {b := true}.
+Next Obligation. exact 2. Qed.
+Check blo.
+
+#[refine] Instance xbar : Foo := {a:=4; b:=true}.
+Proof. Qed.
+Check xbar.
diff --git a/test-suite/success/RewriteRegisteredElim.v b/test-suite/success/RewriteRegisteredElim.v
new file mode 100644
index 0000000000..39b103747c
--- /dev/null
+++ b/test-suite/success/RewriteRegisteredElim.v
@@ -0,0 +1,35 @@
+
+Set Universe Polymorphism.
+
+Cumulative Inductive EQ {A} (x : A) : A -> Type
+  := EQ_refl : EQ x x.
+
+Register EQ as core.eq.type.
+
+Lemma renamed_EQ_rect {A} (x:A) (P : A -> Type)
+  (c : P x) (y : A) (e : EQ x y) : P y.
+Proof. destruct e. assumption. Qed.
+
+Register renamed_EQ_rect as core.eq.rect.
+Register renamed_EQ_rect as core.eq.ind.
+
+Lemma renamed_EQ_rect_r {A} (x:A) (P : A -> Type)
+  (c : P x) (y : A) (e : EQ y x) : P y.
+Proof. destruct e. assumption. Qed.
+
+Register renamed_EQ_rect_r as core.eq.rect_r.
+Register renamed_EQ_rect_r as core.eq.ind_r.
+
+Lemma EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite e. reflexivity. Qed.
+
+Lemma EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite <- e. reflexivity. Qed.
+
+Require Import ssreflect.
+
+Lemma ssr_EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite e. reflexivity. Qed.
+
+Lemma ssr_EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x.
+Proof. rewrite -e. reflexivity. Qed.
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index cfc25c3346..656362b8fc 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -46,3 +46,129 @@ Module No.
   Definition j_lebox (A:Type@{j}) := Box A.
   Fail Definition box_lti A := Box A : Type@{i}.
 End No.
+
+Module DefaultProp.
+  Inductive identity (A : Type) (a : A) : A -> Type := id_refl : identity A a a.
+
+  (* By default template polymorphism does not interact with inductives
+     which naturally fall in Prop *)
+  Check (identity nat 0 0 : Prop).
+End DefaultProp.
+
+Module ExplicitTemplate.
+  #[universes(template)]
+  Inductive identity@{i} (A : Type@{i}) (a : A) : A -> Type@{i} := id_refl : identity A a a.
+
+  (* Weird interaction of template polymorphism and inductive types
+     which naturally fall in Prop: this one is template polymorphic but not on i:
+     it just lives in any universe *)
+  Check (identity Type nat nat : Prop).
+End ExplicitTemplate.
+
+Polymorphic Definition f@{i} : Type@{i} := nat.
+Polymorphic Definition baz@{i} : Type@{i} -> Type@{i} := fun x => x.
+
+Section Foo.
+  Universe u.
+  Context (A : Type@{u}).
+
+  Inductive Bar :=
+  | bar : A -> Bar.
+
+  Set Universe Minimization ToSet.
+  Inductive Baz :=
+  | cbaz : A -> baz Baz -> Baz.
+
+  Inductive Baz' :=
+  | cbaz' : A -> baz@{Set} nat -> Baz'.
+
+  (* 2 constructors, at least in Set *)
+  Inductive Bazset@{v} :=
+  | cbaz1 : A -> baz@{v} Bazset -> Bazset
+  | cbaz2 : Bazset.
+
+  Eval compute in ltac:(let T := type of A in exact T).
+
+  Inductive Foo : Type :=
+  | foo : A -> f -> Foo.
+
+End Foo.
+
+Set Printing Universes.
+(* Cannot fall back to Prop or Set anymore as baz is no longer template-polymorphic *)
+Fail Check Bar True : Prop.
+Fail Check Bar nat : Set.
+About Baz.
+
+Check cbaz True I.
+
+(** Neither can it be Set *)
+Fail Check Baz nat : Set.
+
+(** No longer possible for Baz' which contains a type in Set *)
+Fail Check Baz' True : Prop.
+Fail Check Baz' nat : Set.
+
+Fail Check Bazset True : Prop.
+Fail Check Bazset True : Set.
+
+(** We can force the universe instantiated in [baz Bazset] to be [u], so Bazset lives in max(Set, u). *)
+Constraint u = Bazset.v.
+(** As u is global it is already > Set, so: *)
+Definition bazsetex@{i | i < u} : Type@{u} := Bazset Type@{i}.
+
+(* Bazset is closed for universes u = u0, cannot be instantiated with Prop *)
+Definition bazseetpar (X : Type@{u}) : Type@{u} := Bazset X.
+
+(** Would otherwise break singleton elimination and extraction. *)
+Fail Check Foo True : Prop.
+Fail Check Foo True : Set.
+
+Definition foo_proj {A} (f : Foo A) : nat :=
+  match f with foo _ _ n => n end.
+
+Definition ex : Foo True := foo _ I 0.
+Check foo_proj ex.
+
+(** See failure/Template.v for a test of the unsafe Unset Template Check usage *)
+
+Module AutoTemplateTest.
+Set Warnings "+auto-template".
+Section Foo.
+  Universe u'.
+  Context (A : Type@{u'}).
+
+  (* Not failing as Bar cannot be made template polymorphic at all *)
+  Inductive Bar :=
+  | bar : A -> Bar.
+End Foo.
+End AutoTemplateTest.
+
+Module TestTemplateAttribute.
+  Section Foo.
+    Universe u.
+    Context (A : Type@{u}).
+
+    (* Failing as Bar cannot be made template polymorphic at all *)
+    Fail #[universes(template)] Inductive Bar :=
+    | bar : A -> Bar.
+
+  End Foo.
+End TestTemplateAttribute.
+
+Module SharingWithoutSection.
+Inductive Foo A (S:= fun _ => Set : ltac:(let ty := type of A in exact ty))
+  := foo : S A -> Foo A.
+Fail Check Foo True : Prop.
+End SharingWithoutSection.
+
+Module OkNotCovered.
+(* Here it happens that box is safe but we don't see it *)
+Section S.
+Universe u.
+Variable A : Type@{u}.
+Inductive box (A:Type@{u}) := Box : A -> box A.
+Definition B := Set : Type@{u}.
+End S.
+Fail Check box True : Prop.
+End OkNotCovered.
diff --git a/test-suite/success/section_poly.v b/test-suite/success/section_poly.v
new file mode 100644
index 0000000000..1e2201f2de
--- /dev/null
+++ b/test-suite/success/section_poly.v
@@ -0,0 +1,74 @@
+
+
+Section Foo.
+
+  Variable X : Type.
+
+  Polymorphic Section Bar.
+
+  Variable A : Type.
+
+  Definition id (a:A) := a.
+
+End Bar.
+Check id@{_}.
+End Foo.
+Check id@{_}.
+
+Polymorphic Section Foo.
+Variable A : Type.
+Section Bar.
+  Variable B : Type.
+
+  Inductive prod := Prod : A -> B -> prod.
+End Bar.
+Check prod@{_}.
+End Foo.
+Check prod@{_ _}.
+
+Section Foo.
+
+  Universe K.
+  Inductive bla := Bla : Type@{K} -> bla.
+
+  Polymorphic Definition bli@{j} := Type@{j} -> bla.
+
+  Definition bloo := bli@{_}.
+
+  Polymorphic Universe i.
+
+  Fail Definition x := Type.
+  Fail Inductive x : Type := .
+  Polymorphic Definition x := Type.
+  Polymorphic Inductive y : x := .
+
+  Variable A : Type. (* adds a mono univ for the Type, which is unrelated to the others *)
+
+  Fail Variable B : (y : Type@{i}).
+  (* not allowed: mono constraint (about a fresh univ for y) regarding
+  poly univ i *)
+
+  Polymorphic Variable B : Type. (* new polymorphic stuff always OK *)
+
+  Variable C : Type@{i}. (* no new univs so no problems *)
+
+  Polymorphic Definition thing := bloo -> y -> A -> B.
+
+End Foo.
+Check bli@{_}.
+Check bloo@{}.
+
+Check thing@{_ _ _}.
+
+Section Foo.
+
+  Polymorphic Universes i k.
+  Universe j.
+  Fail Constraint i < j.
+  Fail Constraint i < k.
+
+  (* referring to mono univs in poly constraints is OK. *)
+  Polymorphic Constraint i < j. Polymorphic Constraint j < k.
+
+  Polymorphic Definition foo := Type@{j}.
+End Foo.
diff --git a/test-suite/success/typing_flags.v b/test-suite/success/typing_flags.v
new file mode 100644
index 0000000000..bd20d9c804
--- /dev/null
+++ b/test-suite/success/typing_flags.v
@@ -0,0 +1,43 @@
+
+Print Typing Flags.
+Unset Guard Checking.
+Fixpoint f' (n : nat) : nat := f' n.
+
+Fixpoint f (n : nat) : nat.
+Proof.
+  exact (f n).
+Defined.
+
+Fixpoint bla (A:Type) (n:nat) := match n with 0 =>0 | S n => n end.
+
+Print Typing Flags.
+
+Set Guard Checking.
+
+Print Assumptions f.
+
+Unset Universe Checking.
+
+Definition T := Type.
+Fixpoint g (n : nat) : T := T.
+
+Print Typing Flags.
+Set Universe Checking.
+
+Fail Definition g2 (n : nat) : T := T.
+
+Fail Definition e := fix e (n : nat) : nat := e n.
+
+Unset Positivity Checking.
+
+Inductive Cor :=
+| Over : Cor
+| Next : ((Cor -> list nat) -> list nat) -> Cor.
+
+Set Positivity Checking.
+Print Assumptions Cor.
+
+Inductive Box :=
+| box : forall n, f n = n -> g 2 -> Box.
+
+Print Assumptions Box.
diff --git a/test-suite/vos/A.v b/test-suite/vos/A.v
new file mode 100644
index 0000000000..11245ba015
--- /dev/null
+++ b/test-suite/vos/A.v
@@ -0,0 +1,4 @@
+Definition x := 3.
+
+Lemma xeq : x = x.
+Proof. auto. Qed.
diff --git a/test-suite/vos/B.v b/test-suite/vos/B.v
new file mode 100644
index 0000000000..735fefd745
--- /dev/null
+++ b/test-suite/vos/B.v
@@ -0,0 +1,34 @@
+Require Import A.
+
+Definition y := x.
+
+Lemma yeq : y = y.
+Proof. pose xeq. auto. Qed.
+
+
+Section Foo.
+
+Variable (HFalse : False).
+
+Lemma yeq' : y = y.
+Proof using HFalse. elimtype False. apply HFalse. Qed.
+
+End Foo.
+
+Module Type E. End E.
+
+Module M.
+  Lemma x : True.
+  Proof. trivial. Qed.
+End M.
+
+
+Module Type T.
+  Lemma x : True.
+  Proof. trivial. Qed.
+End T.
+
+Module F(X:E).
+  Lemma x : True.
+  Proof. trivial. Qed.
+End F.
diff --git a/test-suite/vos/C.v b/test-suite/vos/C.v
new file mode 100644
index 0000000000..5260b7cdaf
--- /dev/null
+++ b/test-suite/vos/C.v
@@ -0,0 +1,13 @@
+Require Import A B.
+
+Definition z := x + y.
+
+Lemma zeq : z = z.
+Proof. pose xeq. pose yeq. auto. Qed.
+
+Lemma yeq'' : y = y.
+Proof. apply yeq'. Admitted.
+
+Module M. Include B.M. End M.
+Module T. Include B.T. End T.
+Module F. Include B.F. End F.
diff --git a/test-suite/vos/run.sh b/test-suite/vos/run.sh
new file mode 100755
index 0000000000..2496fc8602
--- /dev/null
+++ b/test-suite/vos/run.sh
@@ -0,0 +1,23 @@
+#!/bin/bash
+set -e
+set -o pipefail
+export PATH="$COQBIN:$PATH"
+
+# Clean
+rm -f *.vo *.vos *.vok *.glob *.aux Makefile
+
+# Test building all vos, then all vok
+coq_makefile -R . TEST -o Makefile *.v
+make vos
+make vok
+
+# Cleanup
+make clean
+
+# Test using compilation in custom order
+set -x #echo on
+coqc A.v
+coqc -vos B.v
+coqc -vos C.v
+coqc -vok B.v
+coqc -vok C.v