10 files changed, 162 insertions, 123 deletions
diff --git a/test-suite/bugs/closed/3612.v b/test-suite/bugs/closed/3612.v
index a547685070..4b4f81dbce 100644
--- a/test-suite/bugs/closed/3612.v
+++ b/test-suite/bugs/closed/3612.v
@@ -38,8 +38,11 @@ Axiom path_path_sigma : forall {A : Type} (P : A -> Type) (u v : sigT P)
            (s : transport (fun x => transport P x u.2 = v.2) r p..2 = q..2),
 p = q.
 
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
 
+Set Default Proof Mode "Classic".
+
 Goal forall (A : Type) (B : forall _ : A, Type) (x : @sigT A (fun x : A => B x))
             (xx : @paths (@sigT A (fun x0 : A => B x0)) x x),
        @paths (@paths (@sigT A (fun x0 : A => B x0)) x x) xx
diff --git a/test-suite/bugs/closed/3649.v b/test-suite/bugs/closed/3649.v
index fc4c171e2c..8687eaab00 100644
--- a/test-suite/bugs/closed/3649.v
+++ b/test-suite/bugs/closed/3649.v
@@ -2,7 +2,9 @@
 (* File reduced by coq-bug-finder from original input, then from 9518 lines to 404 lines, then from 410 lines to 208 lines, then from 162 lines to 77 lines *)
 (* coqc version trunk (September 2014) compiled on Sep 18 2014 21:0:5 with OCaml 4.01.0
    coqtop version cagnode16:/afs/csail.mit.edu/u/j/jgross/coq-trunk,trunk (07e4438bd758c2ced8caf09a6961ccd77d84e42b) *)
+Declare ML Module "ltac_plugin".
 Declare ML Module "coretactics".
+Set Default Proof Mode "Classic".
 Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
 Reserved Notation "x = y" (at level 70, no associativity).
 Delimit Scope type_scope with type.
diff --git a/test-suite/bugs/closed/4121.v b/test-suite/bugs/closed/4121.v
index d34a2b8b1b..816bc845fd 100644
--- a/test-suite/bugs/closed/4121.v
+++ b/test-suite/bugs/closed/4121.v
@@ -4,6 +4,8 @@ Unset Strict Universe Declaration.
 (* coqc version 8.5beta1 (March 2015) compiled on Mar 11 2015 18:51:36 with OCaml 4.01.0
    coqtop version cagnode15:/afs/csail.mit.edu/u/j/jgross/coq-8.5,v8.5 (8dbfee5c5f897af8186cb1bdfb04fd4f88eca677) *)
 
+Declare ML Module "ltac_plugin".
+
 Set Universe Polymorphism.
 Class Contr_internal (A : Type) := BuildContr { center : A }.
 Arguments center A {_}.
@@ -13,4 +15,4 @@ Definition contr_paths_contr0 {A} `{Contr A} : Contr A := {| center := center A
 Instance contr_paths_contr1 {A} `{Contr A} : Contr A := {| center := center A |}.
 Check @contr_paths_contr0@{i}.
 Check @contr_paths_contr1@{i}. (* Error: Universe instance should have length 2 *)
-(** It should have length 1, just like contr_paths_contr0 *)
-\ No newline at end of file
+(** It should have length 1, just like contr_paths_contr0 *)
diff --git a/test-suite/bugs/closed/4527.v b/test-suite/bugs/closed/4527.v
index 08628377f0..c6fcc24b6b 100644
--- a/test-suite/bugs/closed/4527.v
+++ b/test-suite/bugs/closed/4527.v
@@ -5,6 +5,7 @@ then from 269 lines to 255 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
diff --git a/test-suite/bugs/closed/4533.v b/test-suite/bugs/closed/4533.v
index ae17fb145d..64c7fd8eb1 100644
--- a/test-suite/bugs/closed/4533.v
+++ b/test-suite/bugs/closed/4533.v
@@ -5,6 +5,7 @@ then from 285 lines to 271 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 
 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -223,4 +224,4 @@ v = _) r,
     | [ |- p2 @ p0 @ p1 @ eissect (to O A) (g x) = r ] => idtac "good"
     | [ |- ?G ] => fail 1 "bad" G
     end.
-    Fail rewrite concat_p_pp.
-\ No newline at end of file
+    Fail rewrite concat_p_pp.
diff --git a/test-suite/bugs/closed/4544.v b/test-suite/bugs/closed/4544.v
index da140c9318..64dd8c304f 100644
--- a/test-suite/bugs/closed/4544.v
+++ b/test-suite/bugs/closed/4544.v
@@ -2,6 +2,7 @@
 (* File reduced by coq-bug-finder from original input, then from 2553 lines to 1932 lines, then from 1946 lines to 1932 lines, then from 2467 lines to 1002 lines, then from 1016 lines to 1002 lines *)
 (* coqc version 8.5 (January 2016) compiled on Jan 23 2016 16:15:22 with OCaml 4.01.0
    coqtop version 8.5 (January 2016) *)
+Declare ML Module "ltac_plugin".
 Inductive False := .
 Axiom proof_admitted : False.
 Tactic Notation "admit" := case proof_admitted.
@@ -1004,4 +1005,4 @@ Proof.
   Fail Timeout 1 Time rewrite !loops_functor_group.
   (* 0.004 s in 8.5rc1, 8.677 s in 8.5 *)
   Timeout 1 do 3 rewrite loops_functor_group.
-Abort.
-\ No newline at end of file
+Abort.
diff --git a/test-suite/bugs/closed/5346.v b/test-suite/bugs/closed/5346.v
new file mode 100644
index 0000000000..0118c18704
--- /dev/null
+++ b/test-suite/bugs/closed/5346.v
@@ -0,0 +1,29 @@
+Inductive comp : Type -> Type :=
+| Ret {T} : forall (v:T), comp T
+| Bind {T T'} : forall (p: comp T') (p': T' -> comp T), comp T.
+
+Notation "'do' x .. y <- p1 ; p2" :=
+  (Bind p1 (fun x => .. (fun y => p2) ..))
+    (at level 60, right associativity,
+     x binder, y binder).
+
+Definition Fst1 A B (p: comp (A*B)) : comp A :=
+  do '(a, b) <- p;
+    Ret a.
+
+Definition Fst2 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => Bind p (fun '(a, b) => Ret a)
+  end.
+
+Definition Fst3 A B (p: comp (A*B)) : comp A :=
+  match tt with
+  | _ => do a <- p;
+          Ret (fst a)
+  end.
+
+Definition Fst A B (p: comp (A * B)) : comp A :=
+  match tt with
+  | _ => do '(a, b) <- p;
+          Ret a
+  end.
diff --git a/test-suite/output/Search.out b/test-suite/output/Search.out
index c17b285bc9..81fda176ec 100644
--- a/test-suite/output/Search.out
+++ b/test-suite/output/Search.out
@@ -1,108 +1,108 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
+le_n_S: forall n m : nat, n <= m -> S n <= S m
+le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
+le_S_n: forall n m : nat, S n <= S m -> n <= m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
 le_ind:
   forall (n : nat) (P : nat -> Prop),
   P n ->
   (forall m : nat, n <= m -> P m -> P (S m)) ->
   forall n0 : nat, n <= n0 -> P n0
-le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
-le_n_S: forall n m : nat, n <= m -> S n <= S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
-true: bool
 false: bool
-bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
-bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
-bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
-implb: bool -> bool -> bool
-xorb: bool -> bool -> bool
+true: bool
+is_true: bool -> Prop
 negb: bool -> bool
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-andb_true_intro:
-  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 eq_true: bool -> Prop
-eq_true_rect:
-  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
-eq_true_ind:
-  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
+implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
+xorb: bool -> bool -> bool
+Nat.even: nat -> bool
+Nat.odd: nat -> bool
+BoolSpec: Prop -> Prop -> bool -> Prop
+Nat.eqb: nat -> nat -> bool
+Nat.testbit: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
+bool_ind: forall P : bool -> Prop, P true -> P false -> forall b : bool, P b
+bool_rec: forall P : bool -> Set, P true -> P false -> forall b : bool, P b
 eq_true_rec:
   forall P : bool -> Set, P true -> forall b : bool, eq_true b -> P b
-is_true: bool -> Prop
-eq_true_ind_r:
-  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
-eq_true_rec_r:
-  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_ind:
+  forall P : bool -> Prop, P true -> forall b : bool, eq_true b -> P b
 eq_true_rect_r:
   forall (P : bool -> Type) (b : bool), P b -> eq_true b -> P true
-BoolSpec: Prop -> Prop -> bool -> Prop
+eq_true_rec_r:
+  forall (P : bool -> Set) (b : bool), P b -> eq_true b -> P true
+eq_true_rect:
+  forall P : bool -> Type, P true -> forall b : bool, eq_true b -> P b
+bool_rect: forall P : bool -> Type, P true -> P false -> forall b : bool, P b
+eq_true_ind_r:
+  forall (P : bool -> Prop) (b : bool), P b -> eq_true b -> P true
+andb_true_intro:
+  forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 BoolSpec_ind:
   forall (P Q : Prop) (P0 : bool -> Prop),
   (P -> P0 true) ->
   (Q -> P0 false) -> forall b : bool, BoolSpec P Q b -> P0 b
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
-Nat.even: nat -> bool
-Nat.odd: nat -> bool
-Nat.testbit: nat -> nat -> bool
-Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
+n_Sn: forall n : nat, n <> S n
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+O_S: forall n : nat, 0 <> S n
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+eq_S: forall x y : nat, x = y -> S x = S y
 eq_add_S: forall n m : nat, S n = S m -> n = m
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+plus_n_Sm: forall n m : nat, S (n + m) = n + S m
+f_equal_nat: forall (B : Type) (f : nat -> B) (x y : nat), x = y -> f x = f y
 not_eq_S: forall n m : nat, n <> m -> S n <> S m
-O_S: forall n : nat, 0 <> S n
-n_Sn: forall n : nat, n <> S n
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
 f_equal2_plus:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
+f_equal2_mult:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
 f_equal2_nat:
   forall (B : Type) (f : nat -> nat -> B) (x1 y1 x2 y2 : nat),
   x1 = y1 -> x2 = y2 -> f x1 x2 = f y1 y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
-plus_n_Sm: forall n m : nat, S (n + m) = n + S m
-plus_Sn_m: forall n m : nat, S n + m = S (n + m)
-f_equal2_mult:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 bool_choice:
   forall (S : Set) (R1 R2 : S -> Prop),
   (forall x : S, {R1 x} + {R2 x}) ->
   {f : S -> bool | forall x : S, f x = true /\ R1 x \/ f x = false /\ R2 x}
-andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 andb_true_intro:
   forall b1 b2 : bool, b1 = true /\ b2 = true -> (b1 && b2)%bool = true
 andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
-h': newdef n <> n
+andb_prop: forall a b : bool, (a && b)%bool = true -> a = true /\ b = true
 h: n <> newdef n
 h': newdef n <> n
 h: n <> newdef n
+h': newdef n <> n
 h: n <> newdef n
 h: n <> newdef n
-h': ~ P n
 h: P n
 h': ~ P n
 h: P n
 h': ~ P n
 h: P n
+h': ~ P n
 h: P n
 h: P n
diff --git a/test-suite/output/SearchHead.out b/test-suite/output/SearchHead.out
index 0d5924ec61..7038eac22c 100644
--- a/test-suite/output/SearchHead.out
+++ b/test-suite/output/SearchHead.out
@@ -1,39 +1,39 @@
 le_n: forall n : nat, n <= n
+le_0_n: forall n : nat, 0 <= n
 le_S: forall n m : nat, n <= m -> n <= S m
 le_pred: forall n m : nat, n <= m -> Nat.pred n <= Nat.pred m
-le_S_n: forall n m : nat, S n <= S m -> n <= m
-le_0_n: forall n : nat, 0 <= n
 le_n_S: forall n m : nat, n <= m -> S n <= S m
-true: bool
+le_S_n: forall n m : nat, S n <= S m -> n <= m
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-eq_S: forall x y : nat, x = y -> S x = S y
-f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
+Nat.eqb: nat -> nat -> bool
+mult_n_O: forall n : nat, 0 = n * 0
+plus_O_n: forall n : nat, 0 + n = n
+plus_n_O: forall n : nat, n = n + 0
 pred_Sn: forall n : nat, n = Nat.pred (S n)
+f_equal_pred: forall x y : nat, x = y -> Nat.pred x = Nat.pred y
 eq_add_S: forall n m : nat, S n = S m -> n = m
-f_equal2_plus:
-  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
-plus_n_O: forall n : nat, n = n + 0
-plus_O_n: forall n : nat, 0 + n = n
+eq_S: forall x y : nat, x = y -> S x = S y
+max_r: forall n m : nat, n <= m -> Nat.max n m = m
+max_l: forall n m : nat, m <= n -> Nat.max n m = n
+min_r: forall n m : nat, m <= n -> Nat.min n m = m
+min_l: forall n m : nat, n <= m -> Nat.min n m = n
 plus_n_Sm: forall n m : nat, S (n + m) = n + S m
 plus_Sn_m: forall n m : nat, S n + m = S (n + m)
+mult_n_Sm: forall n m : nat, n * m + n = n * S m
+f_equal2_plus:
+  forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 + x2 = y1 + y2
 f_equal2_mult:
   forall x1 y1 x2 y2 : nat, x1 = y1 -> x2 = y2 -> x1 * x2 = y1 * y2
-mult_n_O: forall n : nat, 0 = n * 0
-mult_n_Sm: forall n m : nat, n * m + n = n * S m
-max_l: forall n m : nat, m <= n -> Nat.max n m = n
-max_r: forall n m : nat, n <= m -> Nat.max n m = m
-min_l: forall n m : nat, n <= m -> Nat.min n m = n
-min_r: forall n m : nat, m <= n -> Nat.min n m = m
 h: newdef n
 h: P n
diff --git a/test-suite/output/SearchPattern.out b/test-suite/output/SearchPattern.out
index f3c12effca..45ff5e73b6 100644
--- a/test-suite/output/SearchPattern.out
+++ b/test-suite/output/SearchPattern.out
@@ -1,77 +1,77 @@
-true: bool
 false: bool
-andb: bool -> bool -> bool
-orb: bool -> bool -> bool
+true: bool
+negb: bool -> bool
 implb: bool -> bool -> bool
+orb: bool -> bool -> bool
+andb: bool -> bool -> bool
 xorb: bool -> bool -> bool
-negb: bool -> bool
-Nat.eqb: nat -> nat -> bool
-Nat.leb: nat -> nat -> bool
-Nat.ltb: nat -> nat -> bool
 Nat.even: nat -> bool
 Nat.odd: nat -> bool
+Nat.leb: nat -> nat -> bool
+Nat.ltb: nat -> nat -> bool
 Nat.testbit: nat -> nat -> bool
-O: nat
-S: nat -> nat
-length: forall A : Type, list A -> nat
+Nat.eqb: nat -> nat -> bool
+Nat.two: nat
 Nat.zero: nat
 Nat.one: nat
-Nat.two: nat
-Nat.succ: nat -> nat
+O: nat
+Nat.double: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.div2: nat -> nat
+Nat.log2: nat -> nat
 Nat.pred: nat -> nat
+Nat.square: nat -> nat
+S: nat -> nat
+Nat.succ: nat -> nat
+Nat.ldiff: nat -> nat -> nat
 Nat.add: nat -> nat -> nat
-Nat.double: nat -> nat
+Nat.lor: nat -> nat -> nat
+Nat.lxor: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
 Nat.sub: nat -> nat -> nat
 Nat.max: nat -> nat -> nat
-Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
 Nat.div: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.min: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
 Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+length: forall A : Type, list A -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
+Nat.div2: nat -> nat
+Nat.sqrt: nat -> nat
+Nat.log2: nat -> nat
+Nat.double: nat -> nat
+Nat.pred: nat -> nat
+Nat.square: nat -> nat
+Nat.succ: nat -> nat
+S: nat -> nat
 Nat.ldiff: nat -> nat -> nat
+Nat.pow: nat -> nat -> nat
+Nat.land: nat -> nat -> nat
 Nat.lxor: nat -> nat -> nat
-S: nat -> nat
-Nat.succ: nat -> nat
-Nat.pred: nat -> nat
-Nat.add: nat -> nat -> nat
-Nat.double: nat -> nat
+Nat.div: nat -> nat -> nat
 Nat.mul: nat -> nat -> nat
-Nat.sub: nat -> nat -> nat
-Nat.max: nat -> nat -> nat
 Nat.min: nat -> nat -> nat
-Nat.pow: nat -> nat -> nat
-Nat.div: nat -> nat -> nat
 Nat.modulo: nat -> nat -> nat
+Nat.sub: nat -> nat -> nat
+Nat.lor: nat -> nat -> nat
 Nat.gcd: nat -> nat -> nat
-Nat.square: nat -> nat
-Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
-Nat.sqrt: nat -> nat
+Nat.max: nat -> nat -> nat
+Nat.add: nat -> nat -> nat
 Nat.log2_iter: nat -> nat -> nat -> nat -> nat
-Nat.log2: nat -> nat
-Nat.div2: nat -> nat
+Nat.sqrt_iter: nat -> nat -> nat -> nat -> nat
 Nat.bitwise: (bool -> bool -> bool) -> nat -> nat -> nat -> nat
-Nat.land: nat -> nat -> nat
-Nat.lor: nat -> nat -> nat
-Nat.ldiff: nat -> nat -> nat
-Nat.lxor: nat -> nat -> nat
 mult_n_Sm: forall n m : nat, n * m + n = n * S m
-identity_refl: forall (A : Type) (a : A), identity a a
 iff_refl: forall A : Prop, A <-> A
+le_n: forall n : nat, n <= n
+identity_refl: forall (A : Type) (a : A), identity a a
 eq_refl: forall (A : Type) (x : A), x = x
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
-le_n: forall n : nat, n <= n
-pair: forall A B : Type, A -> B -> A * B
 conj: forall A B : Prop, A -> B -> A /\ B
+pair: forall A B : Type, A -> B -> A * B
 Nat.divmod: nat -> nat -> nat -> nat -> nat * nat
 h: n <> newdef n
 h: n <> newdef n