8 files changed, 208 insertions, 50 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index d4bafe773f..7adae148bd 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -846,7 +846,7 @@ struct
      match env with
       | [] -> ([v],n)
       | e::l ->
-         if EConstr.eq_constr sigma e v
+         if EConstr.eq_constr_nounivs sigma e v
          then (env,n)
          else
           let (env,n) = _add l ( n+1) v in
diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index c5a09d677e..a964febf9c 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -452,6 +452,7 @@ constructor;red;intros;subst;trivial.
 Qed.
 
 Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
+Defined.
 
 Instance Rri : (Ring (Ro:=Rops)).
 constructor;
@@ -468,6 +469,7 @@ Class can_compute_Z (z : Z) := dummy_can_compute_Z : True.
 Hint Extern 0 (can_compute_Z ?v) =>
   match isZcst v with true => exact I end : typeclass_instances.
 Instance reify_IZR z lvar {_ : can_compute_Z z} : reify (PEc z) lvar (IZR z).
+Defined.
 
 Lemma R_one_zero: 1%R <> 0%R.
 discrR.
@@ -484,6 +486,7 @@ exact Rmult_integral. exact R_one_zero. Defined.
 Require Import QArith.
 
 Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
+Defined.
 
 Instance Qri : (Ring (Ro:=Qops)).
 constructor.
diff --git a/plugins/omega/PreOmega.v b/plugins/omega/PreOmega.v
index 94a3d40441..695f000cb1 100644
--- a/plugins/omega/PreOmega.v
+++ b/plugins/omega/PreOmega.v
@@ -12,6 +12,120 @@ Require Import Arith Max Min BinInt BinNat Znat Nnat.
 
 Local Open Scope Z_scope.
 
+(** * [Z.div_mod_to_equations], [Z.quot_rem_to_equations], [Z.to_euclidean_division_equations]: the tactics for preprocessing [Z.div] and [Z.modulo], [Z.quot] and [Z.rem] *)
+
+(** These tactic use the complete specification of [Z.div] and
+    [Z.modulo] ([Z.quot] and [Z.rem], respectively) to remove these
+    functions from the goal without losing information.  The
+    [Z.euclidean_division_equations_cleanup] tactic removes needless
+    hypotheses, which makes tactics like [nia] run faster.  The tactic
+    [Z.to_euclidean_division_equations] combines the handling of both variants
+    of division/quotient and modulo/remainder. *)
+
+Module Z.
+  Lemma mod_0_r_ext x y : y = 0 -> x mod y = 0.
+  Proof. intro; subst; destruct x; reflexivity. Qed.
+  Lemma div_0_r_ext x y : y = 0 -> x / y = 0.
+  Proof. intro; subst; destruct x; reflexivity. Qed.
+
+  Lemma rem_0_r_ext x y : y = 0 -> Z.rem x y = x.
+  Proof. intro; subst; destruct x; reflexivity. Qed.
+  Lemma quot_0_r_ext x y : y = 0 -> Z.quot x y = 0.
+  Proof. intro; subst; destruct x; reflexivity. Qed.
+
+  Lemma rem_bound_pos_pos x y : 0 < y -> 0 <= x -> 0 <= Z.rem x y < y.
+  Proof. intros; apply Z.rem_bound_pos; assumption. Qed.
+  Lemma rem_bound_neg_pos x y : y < 0 -> 0 <= x -> 0 <= Z.rem x y < -y.
+  Proof. rewrite <- Z.rem_opp_r'; intros; apply Z.rem_bound_pos; rewrite ?Z.opp_pos_neg; assumption. Qed.
+  Lemma rem_bound_pos_neg x y : 0 < y -> x <= 0 -> -y < Z.rem x y <= 0.
+  Proof. rewrite <- (Z.opp_involutive x), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg; apply rem_bound_pos_pos. Qed.
+  Lemma rem_bound_neg_neg x y : y < 0 -> x <= 0 -> y < Z.rem x y <= 0.
+  Proof. rewrite <- (Z.opp_involutive x), <- (Z.opp_involutive y), Z.rem_opp_l', <- Z.opp_lt_mono, and_comm, !Z.opp_nonpos_nonneg, Z.opp_involutive; apply rem_bound_neg_pos. Qed.
+
+  Ltac div_mod_to_equations_generalize x y :=
+    pose proof (Z.div_mod x y);
+    pose proof (Z.mod_pos_bound x y);
+    pose proof (Z.mod_neg_bound x y);
+    pose proof (div_0_r_ext x y);
+    pose proof (mod_0_r_ext x y);
+    let q := fresh "q" in
+    let r := fresh "r" in
+    set (q := x / y) in *;
+    set (r := x mod y) in *;
+    clearbody q r.
+  Ltac quot_rem_to_equations_generalize x y :=
+    pose proof (Z.quot_rem' x y);
+    pose proof (rem_bound_pos_pos x y);
+    pose proof (rem_bound_pos_neg x y);
+    pose proof (rem_bound_neg_pos x y);
+    pose proof (rem_bound_neg_neg x y);
+    pose proof (quot_0_r_ext x y);
+    pose proof (rem_0_r_ext x y);
+    let q := fresh "q" in
+    let r := fresh "r" in
+    set (q := Z.quot x y) in *;
+    set (r := Z.rem x y) in *;
+    clearbody q r.
+
+  Ltac div_mod_to_equations_step :=
+    match goal with
+    | [ |- context[?x / ?y] ] => div_mod_to_equations_generalize x y
+    | [ |- context[?x mod ?y] ] => div_mod_to_equations_generalize x y
+    | [ H : context[?x / ?y] |- _ ] => div_mod_to_equations_generalize x y
+    | [ H : context[?x mod ?y] |- _ ] => div_mod_to_equations_generalize x y
+    end.
+  Ltac quot_rem_to_equations_step :=
+    match goal with
+    | [ |- context[Z.quot ?x ?y] ] => quot_rem_to_equations_generalize x y
+    | [ |- context[Z.rem ?x ?y] ] => quot_rem_to_equations_generalize x y
+    | [ H : context[Z.quot ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
+    | [ H : context[Z.rem ?x ?y] |- _ ] => quot_rem_to_equations_generalize x y
+    end.
+  Ltac div_mod_to_equations' := repeat div_mod_to_equations_step.
+  Ltac quot_rem_to_equations' := repeat quot_rem_to_equations_step.
+  Ltac euclidean_division_equations_cleanup :=
+    repeat match goal with
+           | [ H : ?x = ?x -> _ |- _ ] => specialize (H eq_refl)
+           | [ H : ?x <> ?x -> _ |- _ ] => clear H
+           | [ H : ?x < ?x -> _ |- _ ] => clear H
+           | [ H : ?T -> _, H' : ?T |- _ ] => specialize (H H')
+           | [ H : ?T -> _, H' : ~?T |- _ ] => clear H
+           | [ H : ~?T -> _, H' : ?T |- _ ] => clear H
+           | [ H : ?A -> ?x = ?x -> _ |- _ ] => specialize (fun a => H a eq_refl)
+           | [ H : ?A -> ?x <> ?x -> _ |- _ ] => clear H
+           | [ H : ?A -> ?x < ?x -> _ |- _ ] => clear H
+           | [ H : ?A -> ?B -> _, H' : ?B |- _ ] => specialize (fun a => H a H')
+           | [ H : ?A -> ?B -> _, H' : ~?B |- _ ] => clear H
+           | [ H : ?A -> ~?B -> _, H' : ?B |- _ ] => clear H
+           | [ H : 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           | [ H : ?A -> 0 < ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?A -> ?x < 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           | [ H : 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           | [ H : ?A -> 0 <= ?x -> _, H' : ?x < 0 |- _ ] => clear H
+           | [ H : ?A -> ?x <= 0 -> _, H' : 0 < ?x |- _ ] => clear H
+           | [ H : 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
+           | [ H : ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
+           | [ H : ?A -> 0 < ?x -> _, H' : ?x <= 0 |- _ ] => clear H
+           | [ H : ?A -> ?x < 0 -> _, H' : 0 <= ?x |- _ ] => clear H
+           | [ H : 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x (eq_sym pf)))
+           | [ H : ?A -> 0 <= ?x -> _, H' : ?x <= 0 |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl 0 x (eq_sym pf)))
+           | [ H : ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun pf => H (@Z.eq_le_incl 0 x pf))
+           | [ H : ?A -> ?x <= 0 -> _, H' : 0 <= ?x |- _ ] => specialize (fun a pf => H a (@Z.eq_le_incl x 0 pf))
+           | [ H : ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
+           | [ H : ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
+           | [ H : ?A -> ?x < ?y -> _, H' : ?x = ?y |- _ ] => clear H
+           | [ H : ?A -> ?x < ?y -> _, H' : ?y = ?x |- _ ] => clear H
+           | [ H : ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
+           | [ H : ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
+           | [ H : ?A -> ?x = ?y -> _, H' : ?x < ?y |- _ ] => clear H
+           | [ H : ?A -> ?x = ?y -> _, H' : ?y < ?x |- _ ] => clear H
+           end.
+  Ltac div_mod_to_equations := div_mod_to_equations'; euclidean_division_equations_cleanup.
+  Ltac quot_rem_to_equations := quot_rem_to_equations'; euclidean_division_equations_cleanup.
+  Ltac to_euclidean_division_equations := div_mod_to_equations'; quot_rem_to_equations'; euclidean_division_equations_cleanup.
+End Z.
 
 (** * zify: the Z-ification tactic *)
 
@@ -411,6 +525,24 @@ Ltac zify_N_op :=
   | |- context [ Z.of_N  (N.mul ?a ?b) ] =>
         pose proof (N2Z.is_nonneg (N.mul a b)); rewrite (N2Z.inj_mul a b) in *
 
+  (* N.div -> Z.div and a positivity hypothesis *)
+  | H : context [ Z.of_N (N.div ?a ?b) ] |- _ =>
+        pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in *
+  | |- context [ Z.of_N  (N.div ?a ?b) ] =>
+        pose proof (N2Z.is_nonneg (N.div a b)); rewrite (N2Z.inj_div a b) in *
+
+  (* N.modulo -> Z.rem / Z.modulo and a positivity hypothesis (N.modulo agrees with Z.modulo on everything except 0; so we pose both the non-zero proof for this agreement, but also replace things with [Z.rem]) *)
+  | H : context [ Z.of_N (N.modulo ?a ?b) ] |- _ =>
+    pose proof (N2Z.is_nonneg (N.modulo a b));
+    pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+    pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+    rewrite (N2Z.inj_rem a b) in *
+  | |- context [ Z.of_N  (N.div ?a ?b) ] =>
+    pose proof (N2Z.is_nonneg (N.modulo a b));
+    pose proof (@Z.quot_div_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+    pose proof (@Z.rem_mod_nonneg (Z.of_N a) (Z.of_N b) (N2Z.is_nonneg a));
+    rewrite (N2Z.inj_rem a b) in *
+
   (* atoms of type N : we add a positivity condition (if not already there) *)
   | _ : 0 <= Z.of_N ?a |- _ => hide_Z_of_N a
   | _ : context [ Z.of_N ?a ] |- _ => pose proof (N2Z.is_nonneg a); hide_Z_of_N a
diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v
index 1ca6227f25..aa0370b2ac 100644
--- a/plugins/setoid_ring/Ncring_initial.v
+++ b/plugins/setoid_ring/Ncring_initial.v
@@ -32,6 +32,7 @@ Lemma Zsth : Equivalence (@eq Z).
 Proof. exact Z.eq_equiv. Qed.
 
 Instance Zops:@Ring_ops Z 0%Z 1%Z Z.add Z.mul Z.sub Z.opp (@eq Z).
+Defined.
 
 Instance Zr: (@Ring _ _ _ _ _ _ _ _ Zops).
 Proof.
diff --git a/plugins/setoid_ring/Ncring_tac.v b/plugins/setoid_ring/Ncring_tac.v
index 7958507819..c8d560cfe9 100644
--- a/plugins/setoid_ring/Ncring_tac.v
+++ b/plugins/setoid_ring/Ncring_tac.v
@@ -27,41 +27,50 @@ Class nth (R:Type) (t:R) (l:list R) (i:nat).
 
 Instance  Ifind0 (R:Type) (t:R) l
  : nth t(t::l) 0.
+Defined.
 
 Instance  IfindS (R:Type) (t2 t1:R) l i 
  {_:nth t1 l i} 
  : nth t1 (t2::l) (S i) | 1.
+Defined.
 
 Class closed (T:Type) (l:list T).
 
 Instance Iclosed_nil T 
  : closed (T:=T) nil.
+Defined.
 
 Instance Iclosed_cons T t (l:list T) 
  {_:closed l} 
  : closed (t::l).
+Defined.
 
 Class reify (R:Type)`{Rr:Ring (T:=R)} (e:PExpr Z) (lvar:list R) (t:R).
 
 Instance  reify_zero (R:Type)  lvar op
  `{Ring (T:=R)(ring0:=op)}
  : reify (ring0:=op)(PEc 0%Z) lvar op.
+Defined.
 
 Instance  reify_one (R:Type)  lvar op
  `{Ring (T:=R)(ring1:=op)}
  : reify (ring1:=op) (PEc 1%Z) lvar op.
+Defined.
 
 Instance  reifyZ0 (R:Type)  lvar 
  `{Ring (T:=R)}
  : reify (PEc Z0) lvar Z0|11.
+Defined.
 
 Instance  reifyZpos (R:Type)  lvar (p:positive)
  `{Ring (T:=R)}
  : reify (PEc (Zpos p)) lvar (Zpos p)|11.
+Defined.
 
 Instance  reifyZneg (R:Type)  lvar (p:positive)
  `{Ring (T:=R)}
  : reify (PEc (Zneg p)) lvar (Zneg p)|11.
+Defined.
 
 Instance  reify_add (R:Type)
   e1 lvar t1 e2 t2 op 
@@ -69,6 +78,7 @@ Instance  reify_add (R:Type)
  {_:reify (add:=op) e1 lvar t1}
  {_:reify (add:=op) e2 lvar t2}
  : reify (add:=op) (PEadd e1 e2) lvar (op t1 t2).
+Defined.
 
 Instance  reify_mul (R:Type) 
   e1 lvar t1 e2 t2 op 
@@ -76,6 +86,7 @@ Instance  reify_mul (R:Type)
  {_:reify (mul:=op) e1 lvar t1}
  {_:reify (mul:=op) e2 lvar t2}
  : reify (mul:=op) (PEmul e1 e2) lvar (op t1 t2)|10.
+Defined.
 
 Instance  reify_mul_ext (R:Type) `{Ring R}
   lvar (z:Z) e2 t2 
@@ -83,6 +94,7 @@ Instance  reify_mul_ext (R:Type) `{Ring R}
  {_:reify e2 lvar t2}
  : reify (PEmul (PEc z) e2) lvar
       (@multiplication Z _ _ z t2)|9.
+Defined.
 
 Instance  reify_sub (R:Type)
  e1 lvar t1 e2 t2 op
@@ -90,24 +102,28 @@ Instance  reify_sub (R:Type)
  {_:reify (sub:=op) e1 lvar t1}
  {_:reify (sub:=op) e2 lvar t2}
  : reify (sub:=op) (PEsub e1 e2) lvar (op t1 t2).
+Defined.
 
 Instance  reify_opp (R:Type)
  e1 lvar t1  op
  `{Ring (T:=R)(opp:=op)}
  {_:reify (opp:=op) e1 lvar t1}
  : reify (opp:=op) (PEopp e1) lvar (op t1).
+Defined.
 
 Instance  reify_pow (R:Type) `{Ring R}
  e1 lvar t1 n 
  `{Ring (T:=R)}
  {_:reify e1 lvar t1}
  : reify (PEpow e1 n) lvar (pow_N t1 n)|1.
+Defined.
 
 Instance  reify_var (R:Type) t lvar i 
  `{nth R t lvar i}
  `{Rr: Ring (T:=R)}
  : reify (Rr:= Rr) (PEX Z (Pos.of_succ_nat i))lvar t
  | 100.
+Defined.
 
 Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R) 
   (lterm:list R).
@@ -115,12 +131,14 @@ Class reifylist (R:Type)`{Rr:Ring (T:=R)} (lexpr:list (PExpr Z)) (lvar:list R)
 Instance reify_nil (R:Type) lvar 
  `{Rr: Ring (T:=R)}
  : reifylist (Rr:= Rr) nil lvar (@nil R).
+Defined.
 
 Instance reify_cons (R:Type) e1 lvar t1 lexpr2 lterm2
  `{Rr: Ring (T:=R)}
  {_:reify (Rr:= Rr) e1 lvar t1}
  {_:reifylist (Rr:= Rr) lexpr2 lvar lterm2} 
  : reifylist (Rr:= Rr) (e1::lexpr2) lvar (t1::lterm2).
+Defined.
 
 Definition list_reifyl (R:Type) lexpr lvar lterm 
  `{Rr: Ring (T:=R)}
diff --git a/plugins/setoid_ring/Rings_Q.v b/plugins/setoid_ring/Rings_Q.v
index ae91ee1664..df3677e1c3 100644
--- a/plugins/setoid_ring/Rings_Q.v
+++ b/plugins/setoid_ring/Rings_Q.v
@@ -15,6 +15,7 @@ Require Export Integral_domain.
 Require Import QArith.
 
 Instance Qops: (@Ring_ops Q 0%Q 1%Q Qplus Qmult Qminus Qopp Qeq).
+Defined.
 
 Instance Qri : (Ring (Ro:=Qops)).
 constructor.
diff --git a/plugins/setoid_ring/Rings_R.v b/plugins/setoid_ring/Rings_R.v
index 901b36ed3b..fe7558845d 100644
--- a/plugins/setoid_ring/Rings_R.v
+++ b/plugins/setoid_ring/Rings_R.v
@@ -20,6 +20,7 @@ constructor;red;intros;subst;trivial.
 Qed.
 
 Instance Rops: (@Ring_ops R 0%R 1%R Rplus Rmult Rminus Ropp (@eq R)).
+Defined.
 
 Instance Rri : (Ring (Ro:=Rops)).
 constructor;
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index 470deb4a60..ea564ae2ba 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -33,30 +33,41 @@ let get_constructors ind =
   Array.to_list
     (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc)
 
-let q_z = qualid_of_string "Coq.Numbers.BinNums.Z"
-let q_positive = qualid_of_string "Coq.Numbers.BinNums.positive"
-let q_int = qualid_of_string "Coq.Init.Decimal.int"
-let q_uint = qualid_of_string "Coq.Init.Decimal.uint"
-let q_option = qualid_of_string "Coq.Init.Datatypes.option"
+let qualid_of_ref n =
+  n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty
+
+let q_option () = qualid_of_ref "core.option.type"
 
 let unsafe_locate_ind q =
   match Nametab.locate q with
   | IndRef i -> i
   | _ -> raise Not_found
 
-let locate_ind q =
-  try unsafe_locate_ind q
-  with Not_found -> Nametab.error_global_not_found q
-
 let locate_z () =
-  try
-    Some { z_ty = unsafe_locate_ind q_z;
-           pos_ty = unsafe_locate_ind q_positive }
-  with Not_found -> None
+  let zn = "num.Z.type" in
+  let pn = "num.pos.type" in
+  if Coqlib.has_ref zn && Coqlib.has_ref pn
+  then
+    let q_z = qualid_of_ref zn in
+    let q_pos = qualid_of_ref pn in
+    Some ({
+        z_ty = unsafe_locate_ind q_z;
+        pos_ty = unsafe_locate_ind q_pos;
+    }, mkRefC q_z)
+  else None
 
 let locate_int () =
-  { uint = locate_ind q_uint;
-    int = locate_ind q_int }
+  let int = "num.int.type" in
+  let uint = "num.uint.type" in
+  if Coqlib.has_ref int && Coqlib.has_ref uint
+  then
+    let q_int = qualid_of_ref int in
+    let q_uint = qualid_of_ref uint in
+    Some ({
+        int = unsafe_locate_ind q_int;
+        uint = unsafe_locate_ind q_uint;
+    }, mkRefC q_int, mkRefC q_uint)
+  else None
 
 let has_type f ty =
   let (sigma, env) = Pfedit.get_current_context () in
@@ -64,19 +75,17 @@ let has_type f ty =
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
 
-let type_error_to f ty loadZ =
+let type_error_to f ty =
   CErrors.user_err
     (pr_qualid f ++ str " should go from Decimal.int to " ++
      pr_qualid ty ++ str " or (option " ++ pr_qualid ty ++ str ")." ++
-     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
-     (if loadZ then str " (require BinNums first)." else str "."))
+     fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).")
 
-let type_error_of g ty loadZ =
+let type_error_of g ty =
   CErrors.user_err
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
      str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
-     str "Instead of Decimal.int, the types Decimal.uint or Z could be used" ++
-     (if loadZ then str " (require BinNums first)." else str "."))
+     str "Instead of Decimal.int, the types Decimal.uint or Z could be used (you may need to require BinNums or Decimal first).")
 
 let vernac_numeral_notation local ty f g scope opts =
   let int_ty = locate_int () in
@@ -86,43 +95,36 @@ let vernac_numeral_notation local ty f g scope opts =
   let of_ty = Smartlocate.global_with_alias g in
   let cty = mkRefC ty in
   let app x y = mkAppC (x,[y]) in
-  let cref q = mkRefC q in
   let arrow x y =
     mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y)
   in
-  let cZ = cref q_z in
-  let cint = cref q_int in
-  let cuint = cref q_uint in
-  let coption = cref q_option in
-  let opt r = app coption r in
+  let opt r = app (mkRefC (q_option ())) r in
   let constructors = get_constructors tyc in
   (* Check the type of f *)
   let to_kind =
-    if has_type f (arrow cint cty) then Int int_ty, Direct
-    else if has_type f (arrow cint (opt cty)) then Int int_ty, Option
-    else if has_type f (arrow cuint cty) then UInt int_ty.uint, Direct
-    else if has_type f (arrow cuint (opt cty)) then UInt int_ty.uint, Option
-    else
-      match z_pos_ty with
-      | Some z_pos_ty ->
-         if has_type f (arrow cZ cty) then Z z_pos_ty, Direct
-         else if has_type f (arrow cZ (opt cty)) then Z z_pos_ty, Option
-         else type_error_to f ty false
-      | None -> type_error_to f ty true
+    match int_ty with
+    | Some (int_ty, cint, _) when has_type f (arrow cint cty) -> Int int_ty, Direct
+    | Some (int_ty, cint, _) when has_type f (arrow cint (opt cty)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint) when has_type f (arrow cuint cty) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint) when has_type f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+    | _ ->
+    match z_pos_ty with
+    | Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct
+    | Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
+    | _ -> type_error_to f ty
   in
   (* Check the type of g *)
   let of_kind =
-    if has_type g (arrow cty cint) then Int int_ty, Direct
-    else if has_type g (arrow cty (opt cint)) then Int int_ty, Option
-    else if has_type g (arrow cty cuint) then UInt int_ty.uint, Direct
-    else if has_type g (arrow cty (opt cuint)) then UInt int_ty.uint, Option
-    else
-      match z_pos_ty with
-      | Some z_pos_ty ->
-         if has_type g (arrow cty cZ) then Z z_pos_ty, Direct
-         else if has_type g (arrow cty (opt cZ)) then Z z_pos_ty, Option
-         else type_error_of g ty false
-      | None -> type_error_of g ty true
+    match int_ty with
+    | Some (int_ty, cint, _) when has_type g (arrow cty cint) -> Int int_ty, Direct
+    | Some (int_ty, cint, _) when has_type g (arrow cty (opt cint)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint) when has_type g (arrow cty cuint) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint) when has_type g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+    | _ ->
+    match z_pos_ty with
+    | Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct
+    | Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
+    | _ -> type_error_of g ty
   in
   let o = { to_kind; to_ty; of_kind; of_ty;
             ty_name = ty;