From 46099edde62abacd5829cc4e715ec06542c0a351 Mon Sep 17 00:00:00 2001
From: Pierre-Yves Strub <pierre-yves.strub@pqshield.com>
Date: Sat, 18 Jan 2025 10:27:45 +0100
Subject: [PATCH] Revert subtype theory + syntactic sugar for cloning it

The previous Subtype theory forces the definition of the type sT for
the subtype carrier, having multiple `sT` types when one has multiple
subtype instances. This commits reverts this (i.e. the subtype carrier
can be substituted by a user type) but add a command to carefully
clone it.
---
 examples/ChaChaPoly/chacha_poly.ec |  377 ++++----
 examples/MEE-CBC/FunctionalSpec.ec |    1 -
 examples/ehoare/adversary.ec       |    2 +-
 src/ecCommands.ml                  |    8 +
 src/ecCoreLib.ml                   |    2 +-
 src/ecLexer.mll                    |    1 +
 src/ecParser.mly                   |   17 +
 src/ecParsetree.ml                 |   10 +
 src/ecScope.ml                     | 1332 +++++++++++++++-------------
 src/ecScope.mli                    |    1 +
 src/ecThCloning.ml                 |   30 +-
 src/ecThCloning.mli                |   18 +-
 src/ecTheoryReplay.ml              |  100 ++-
 tests/subtype-clone-sugar.ec       |    7 +
 theories/algebra/Poly.ec           |   15 +-
 theories/algebra/ZModP.ec          |   11 +-
 theories/datatypes/Word.eca        |   11 +-
 theories/datatypes/Xreal.ec        |   73 +-
 theories/structure/Quotient.ec     |   18 +-
 theories/structure/Subtype.eca     |   99 +--
 20 files changed, 1142 insertions(+), 991 deletions(-)
 create mode 100644 tests/subtype-clone-sugar.ec

diff --git a/examples/ChaChaPoly/chacha_poly.ec b/examples/ChaChaPoly/chacha_poly.ec
index da96991394..bc6db7b880 100644
--- a/examples/ChaChaPoly/chacha_poly.ec
+++ b/examples/ChaChaPoly/chacha_poly.ec
@@ -80,28 +80,26 @@ theory C.
 
   axiom gt0_max_counter : 0 < max_counter.
 
-  clone include Subtype with 
-    type T <- int,
-    op P <- fun (i:int) => 0 <= i < max_counter + 1
-    rename (* [type] "sT" as "counter" *) (* Gives error. *)
-           [op] "insubd" as "ofint"
-  proof *.
-  realize inhabited. exists 0. smt(gt0_max_counter). qed.
-  type counter = sT.
+  subtype counter =
+    { i : int | 0 <= i < max_counter + 1 }
+    rename "ofint", "toint".
+
+  realize inhabited.
+  proof. by exists 0; smt(gt0_max_counter). qed.
 
   clone FinType with 
     type t  = counter,
-    op enum = List.map ofint (iota_ 0 (max_counter + 1))
+    op enum = List.map ofintd (iota_ 0 (max_counter + 1))
     proof *.
   realize enum_spec.  
   proof.
     move=> c; rewrite count_uniq_mem.
     + apply map_inj_in_uniq; last by apply iota_uniq.
       move=> x y /mema_iota hx /mema_iota hy heq.
-      by rewrite -(insubdK x) 1:// -(insubdK y) 1:// heq.
+      by rewrite -(ofintdK x) 1:// -(ofintdK y) 1:// heq.
     have -> // : c \in enum.  
-    rewrite /enum mapP; exists (val c).
-    by rewrite mema_iota /= valP valKd.
+    rewrite /enum mapP; exists (toint c).
+    by rewrite mema_iota /= tointP tointKd.
   qed.
 
 end C.
@@ -116,18 +114,16 @@ abstract theory GenBlock.
   op block_size : int.
   axiom ge0_block_size : 0 <= block_size.
 
-  clone include Subtype with
-    type T <- bytes, 
-    op P <- fun (l:bytes) => size l = block_size
-    rename [op] "val" as "bytes_of_block"
-  proof *.
+  subtype block = { l : bytes | size l = block_size }
+    rename "block_of_bytes", "bytes_of_block".
+
   realize inhabited.
+  proof.
     exists (nseq block_size witness).
     smt(size_nseq ge0_block_size).
   qed.
-  type block = sT.
 
-  op dblock =  dmap (dlist dbyte block_size) insubd.
+  op dblock =  dmap (dlist dbyte block_size) block_of_bytesd.
 
   lemma dblock_ll : is_lossless dblock.
   proof. apply dmap_ll; apply dlist_ll; apply dbyte_ll. qed.
@@ -136,37 +132,37 @@ abstract theory GenBlock.
   proof. 
     apply dmap_uni_in_inj.
     + move=> x y hx hy heq.
-      rewrite -(insubdK x) 1:(supp_dlist_size _ _ _ ge0_block_size hx) //.
-      by rewrite -(insubdK y) 1:(supp_dlist_size _ _ _ ge0_block_size hy) // heq.
+      rewrite -(block_of_bytesdK x) 1:(supp_dlist_size _ _ _ ge0_block_size hx) //.
+      by rewrite -(block_of_bytesdK y) 1:(supp_dlist_size _ _ _ ge0_block_size hy) // heq.
     by apply dlist_uni; apply dbyte_uni.
   qed.
 
   lemma dblock_fu: is_full dblock.
   proof.
    move=> x; rewrite supp_dmap; exists (bytes_of_block x).
-   rewrite valKd /= -(valP x); apply dlist_fu => ??; apply dbyte_fu.
+   rewrite bytes_of_blockKd /= -(bytes_of_blockP x); apply dlist_fu => ??; apply dbyte_fu.
   qed.
  
   lemma dblock_funi: is_funiform dblock.
   proof. apply is_full_funiform; [apply dblock_fu | apply dblock_uni]. qed.
 
-  op zero = insubd (mkseq (fun _ => Byte.zero) block_size).
+  op zero = block_of_bytesd (mkseq (fun _ => Byte.zero) block_size).
 
   op (+^) (b1 b2:block) =
-     insubd (map2 (+^) (bytes_of_block b1) (bytes_of_block b2)).
+     block_of_bytesd (map2 (+^) (bytes_of_block b1) (bytes_of_block b2)).
  
   lemma nth_xor x y i :
      0 <= i < block_size =>
      nth Byte.zero (bytes_of_block (x +^ y)) i =
      nth Byte.zero (bytes_of_block x) i +^ nth Byte.zero (bytes_of_block y) i.
   proof. 
-    move=> hi; rewrite /(+^) !insubdK ?size_map2 ?valP //.
-    rewrite !(nth_map2 Byte.zero Byte.zero) ?valP //.
+    move=> hi; rewrite /(+^) !block_of_bytesdK ?size_map2 ?bytes_of_blockP //.
+    rewrite !(nth_map2 Byte.zero Byte.zero) ?bytes_of_blockP //.
   qed.
 
   lemma nth_zero i : nth Byte.zero (bytes_of_block zero) i = Byte.zero. 
   proof.
-    rewrite /zero insubdK ?size_mkseq; 1:smt (ge0_block_size).
+    rewrite /zero block_of_bytesdK ?size_mkseq; 1:smt (ge0_block_size).
     smt (nth_mkseq nth_neg nth_default size_mkseq).
   qed.
 
@@ -177,23 +173,27 @@ abstract theory GenBlock.
     proof *.
   realize Axioms.addmA.
   proof.
-    move=> x y z; apply val_inj; apply (eq_from_nth Byte.zero); rewrite !valP //.
+    move=> x y z; apply bytes_of_block_inj.
+    apply (eq_from_nth Byte.zero); rewrite !bytes_of_blockP //.
     by move=> i hi; rewrite !nth_xor // Byte.MB.addmA. 
   qed.
   realize Axioms.addmC.
   proof.
-    move=> x y; apply val_inj; apply (eq_from_nth Byte.zero); rewrite !valP //.
+    move=> x y; apply bytes_of_block_inj.
+    apply (eq_from_nth Byte.zero); rewrite !bytes_of_blockP //.
     by move=> i hi; rewrite !nth_xor // Byte.MB.addmC.
   qed.
   realize Axioms.add0m.
   proof.
-    move=> x; apply val_inj; apply (eq_from_nth Byte.zero); rewrite !valP //.
+    move=> x; apply bytes_of_block_inj.
+    apply (eq_from_nth Byte.zero); rewrite !bytes_of_blockP //.
     by move=> i hi; rewrite !nth_xor // nth_zero Byte.MB.add0m.
   qed.
 
   lemma addK b : b +^ b = zero.
   proof.
-    apply val_inj; apply (eq_from_nth Byte.zero); rewrite !valP //.
+    apply bytes_of_block_inj; apply (eq_from_nth Byte.zero);
+      rewrite !bytes_of_blockP //.
     by move=> i hi; rewrite nth_xor // Byte.addK nth_zero.
   qed.
 
@@ -229,13 +229,15 @@ hint solve 0 random : dblock_ll dblock_funi dblock_fu.
 axiom gt0_block_size : 0 < block_size.
 
 op extend (bs:bytes) : block = 
-  Block.insubd (take block_size bs ++ mkseq (fun _ => Byte.zero) (block_size - size bs)).
+  Block.block_of_bytesd
+    (take block_size bs ++ mkseq (fun _ => Byte.zero)
+    (block_size - size bs)).
 
 lemma nth_extend m i : 0 <= i < block_size => 
   nth Byte.zero (bytes_of_block (extend m)) i = 
     if i < size m then  nth Byte.zero m i else Byte.zero.
 proof.
-  move=> [h0i hi]; rewrite /extend Block.insubdK.
+  move=> [h0i hi]; rewrite /extend Block.block_of_bytesdK.
   + by rewrite size_cat size_mkseq size_take 1:ge0_block_size /#.
   rewrite nth_cat size_take 1:ge0_block_size; smt (nth_take nth_mkseq).
 qed.
@@ -248,7 +250,7 @@ op chacha20_block : key -> nonce -> C.counter -> block.
 
 op gen_ctr_round (merge: bytes -> block -> bytes) genblock (k:key) (n:nonce) (round_st : bytes * bytes * int) =
   let (cph,m,c) = round_st in
-  let stream = genblock k n (C.ofint c) in
+  let stream = genblock k n (C.ofintd c) in
   (cph ++ merge m stream, drop block_size m, c + 1).
 
 op gen_CTR_encrypt_bytes merge genblock key nonce counter m =
@@ -270,9 +272,10 @@ op chacha20_CTR_encrypt_bytes key nonce counter m =
 lemma take_xor_map2_xor m str: map2_xor m str = take_xor m str.
 proof.
   apply (eq_from_nth Byte.zero).
-  + by rewrite size_map2 Block.valP size_take 1:size_ge0 Block.valP.
-  rewrite size_map2 Block.valP => j hj.
-  rewrite (nth_map2 Byte.zero Byte.zero) ?Block.valP 1://.
+  + rewrite size_map2 Block.bytes_of_blockP.
+    by rewrite size_take 1:size_ge0 Block.bytes_of_blockP.
+  rewrite size_map2 Block.bytes_of_blockP => j hj.
+  rewrite (nth_map2 Byte.zero Byte.zero) ?Block.bytes_of_blockP 1://.
   rewrite nth_take 1:size_ge0 1:/# Block.nth_xor 1:/#; congr.
   smt (nth_extend).
 qed.
@@ -294,7 +297,7 @@ lemma iter_gen_ctr_round_S merge genblock k n c m i j:
   0 <= i =>
   iter (i + 1) round (c, m, j) = 
     let (c', m', j') = iter i round ([], drop block_size m, j + 1) in 
-    (c ++ merge m (genblock k n (C.ofint j)) ++ c', m', j').
+    (c ++ merge m (genblock k n (C.ofintd j)) ++ c', m', j').
 proof.  
   by move=> round hi; rewrite iterSr // {2}/round /gen_ctr_round /= iter_gen_ctr_round_nil_cat.
 qed.
@@ -319,7 +322,7 @@ qed.
 lemma gen_CTR_encrypt_bytes_cons merge genblock k n c m:
   (forall str, merge [] str = []) =>
   gen_CTR_encrypt_bytes merge genblock k n c m = 
-  merge m (genblock k n (C.ofint c)) ++ 
+  merge m (genblock k n (C.ofintd c)) ++ 
     gen_CTR_encrypt_bytes merge genblock k n (c+1) (drop block_size m).
 proof.
   move=> hm; rewrite /gen_CTR_encrypt_bytes /=; have h0s := size_ge0 m.
@@ -362,10 +365,13 @@ op poly1305 (r:poly_in) (s:poly_out) (p:polynomial) = s + poly1305_eval r p.
 
 op mk_rs (b:block) = 
   let b = take (poly_in_size + poly_out_size) (bytes_of_block b) in
-  (Poly_in.insubd (take poly_in_size b), Poly_out.insubd (drop poly_in_size b)).
+  (
+    Poly_in.poly_in_of_bytesd (take poly_in_size b),
+    Poly_out.poly_out_of_bytesd (drop poly_in_size b)
+  ).
 
 op genpoly1305 genblock (k:key) (n:nonce) (p:polynomial) = 
-  let (r,s) = mk_rs (genblock k n (C.ofint 0)) in
+  let (r,s) = mk_rs (genblock k n (C.ofintd 0)) in
   poly1305 r s p.
   
 axiom poly_out_sub_add (p1 p2: poly_out) : p1 = p1 - p2 + p2.
@@ -432,7 +438,7 @@ module ChaCha(CC:CC) = {
     c     <- [];
     i     <- 1;
     while (p <> []) {
-      z <@ CC.cc(k, n, C.ofint i);
+      z <@ CC.cc(k, n, C.ofintd i);
       c <- c ++ take (size p) (bytes_of_block (extend p +^ z));
       p <- drop block_size p;
       i <- i + 1;
@@ -444,7 +450,7 @@ module ChaCha(CC:CC) = {
 module Poly(CC:CC) = {
   proc mac(k:key, n: nonce, a: associated_data, c: message) : tag = {
     var b, r, s;
-    b     <@ CC.cc(k, n, C.ofint 0);
+    b     <@ CC.cc(k, n, C.ofintd 0);
     (r,s) <- mk_rs b; 
     return poly1305 r s (topol a c);
   }
@@ -659,7 +665,7 @@ module D(A:CCA_Adv, RO: Indist.Oracle) = {
         c     <- [];
         i     <- 1;
         while (p <> []) {
-          z <@ RO.f(n, C.ofint i);
+          z <@ RO.f(n, C.ofintd i);
           c <- c ++ take (size p) (bytes_of_block (extend p +^ z));
           p <- drop block_size p;
           i <- i + 1;
@@ -671,7 +677,7 @@ module D(A:CCA_Adv, RO: Indist.Oracle) = {
     module Poly = {
       proc mac(n: nonce, a: associated_data, c: message) : tag = {
         var b, r, s;
-        b     <@ RO.f(n, C.ofint 0);
+        b     <@ RO.f(n, C.ofintd 0);
         (r,s) <- mk_rs b; 
         return poly1305 r s (topol a c);
       }
@@ -727,7 +733,7 @@ module UFCMA_poly(A:CCA_Adv, RO:RO) = {
     i <- 0;
     while (i < size ns) {
       n  <- List.nth witness ns i;
-      bl <@ RO.get(n,C.ofint 0);
+      bl <@ RO.get(n,C.ofintd 0);
       (r,s) <- mk_rs bl; 
       forged <- forged || test_poly n Mem.lc r s;
       i <- i + 1;
@@ -789,23 +795,29 @@ proof.
   move=> hs; rewrite (gen_CTR_encrypt_bytes_cons _ _ _ _ _ p) 1:// gen_CTR_encrypt_bytes_cons 1://.
   case: (size p < block_size) => hsz.
   + rewrite drop_oversize 1:/# gen_CTR_encrypt_bytes0 1:// cats0 drop_oversize.
-    + by rewrite size_take // Block.valP /#.
+    + by rewrite size_take // Block.bytes_of_blockP /#.
     rewrite gen_CTR_encrypt_bytes0 1:// cats0. 
     rewrite -!take_xor_map2_xor; apply (eq_from_nth Byte.zero).
-    + by rewrite !size_map2 Block.valP /#.
-    move=> j; rewrite !size_map2 Block.valP => hj.
-    by rewrite !(nth_map2 Byte.zero Byte.zero) ?size_map2 ?Block.valP 1,2:/# -Byte.xorK1.
-  rewrite drop_size_cat;1: by rewrite size_take 1:// Block.valP /#.
+    + by rewrite !size_map2 Block.bytes_of_blockP /#.
+    move=> j; rewrite !size_map2 Block.bytes_of_blockP => hj.
+    by rewrite
+         !(nth_map2 Byte.zero Byte.zero) ?size_map2
+         ?Block.bytes_of_blockP 1,2:/# -Byte.xorK1.
+  rewrite drop_size_cat;1: by rewrite size_take 1:// Block.bytes_of_blockP /#.
   rewrite (hrec (size (drop block_size p))) 2://; 1: smt(size_drop gt0_block_size).
   rewrite -{4}(cat_take_drop block_size p); congr.
   rewrite -!take_xor_map2_xor; apply (eq_from_nth Byte.zero).
-  + smt (size_map2 Block.valP size_cat size_take gt0_block_size size_ge0).
+  + smt (size_map2 Block.bytes_of_blockP size_cat size_take gt0_block_size size_ge0).
   move=> j hj.
   have [hj1 hj2] : j < block_size /\ j < size p.
-  + smt (size_map2 Block.valP size_cat size_take gt0_block_size size_ge0).
-  rewrite (nth_map2 Byte.zero Byte.zero) ?(size_cat, size_map2, Block.valP) 1:#smt:(size_ge0).
-  rewrite nth_cat ?(size_cat, size_map2, Block.valP) /min hsz /= hj1.
-  by rewrite (nth_map2 Byte.zero Byte.zero) ?Block.valP 1:/# /= -Byte.xorK1 nth_take 1:ge0_block_size.
+  + smt (size_map2 Block.bytes_of_blockP size_cat size_take gt0_block_size size_ge0).
+  rewrite
+    (nth_map2 Byte.zero Byte.zero)
+    ?(size_cat, size_map2, Block.bytes_of_blockP) 1:#smt:(size_ge0).
+  rewrite nth_cat ?(size_cat, size_map2, Block.bytes_of_blockP) /min hsz /= hj1.
+  by rewrite
+       (nth_map2 Byte.zero Byte.zero)
+       ?Block.bytes_of_blockP 1:/# /= -Byte.xorK1 nth_take 1:ge0_block_size.
 qed.
 
 module St = {
@@ -825,38 +837,43 @@ clone Split as Split0 with
   proof *.
 
 clone import Split0.SplitDom as SplitD with
-  op test = fun p:nonce * C.counter => C.val p.`2 = 0.
+  op test = fun p:nonce * C.counter => C.toint p.`2 = 0.
 
 clone import Split0.SplitCodom as SplitC1 with
   type to1 <- poly,
   type to2 <- extra_block,
   op topair = fun (b:block) => 
      let bs = bytes_of_block b in
-     (TPoly.insubd (take poly_size bs), Extra_block.insubd (drop poly_size bs)),
+     (
+       TPoly.poly_of_bytesd (take poly_size bs),
+       Extra_block.extra_block_of_bytesd (drop poly_size bs)
+     ),
   op ofpair = fun (p:poly * extra_block) =>
-     Block.insubd (bytes_of_poly p.`1 ++ bytes_of_extra_block p.`2),
+     Block.block_of_bytesd (bytes_of_poly p.`1 ++ bytes_of_extra_block p.`2),
   op sampleto1 <- fun _ => dpoly,
   op sampleto2 <- fun _ => dextra_block
   proof *.
 realize topairK.
 proof.
   move=> x; rewrite /topair /ofpair /=.
-  rewrite -{3}(Block.valKd x); congr.
-  rewrite TPoly.insubdK. 
-  + rewrite size_take 1:ge0_poly_size Block.valP.
+  rewrite -{3}(Block.bytes_of_blockKd x); congr.
+  rewrite TPoly.poly_of_bytesdK. 
+  + rewrite size_take 1:ge0_poly_size Block.bytes_of_blockP.
     smt (ge0_poly_in_size ge0_poly_out_size ge0_extra_block_size).
-  rewrite Extra_block.insubdK 2:cat_take_drop 2://.
-  rewrite size_drop 1:ge0_poly_size Block.valP.
+  rewrite Extra_block.extra_block_of_bytesdK 2:cat_take_drop 2://.
+  rewrite size_drop 1:ge0_poly_size Block.bytes_of_blockP.
   smt (ge0_poly_in_size ge0_poly_out_size ge0_extra_block_size).
 qed.
 
 realize ofpairK.
 proof.
   move=> [x1 x2]; rewrite /topair /ofpair /=.
-  rewrite Block.insubdK.
-  + by rewrite size_cat TPoly.valP Extra_block.valP.
-  by rewrite take_size_cat 1:TPoly.valP 1:// drop_size_cat 1:TPoly.valP 1://
-     TPoly.valKd Extra_block.valKd.
+  rewrite Block.block_of_bytesdK.
+  + by rewrite size_cat TPoly.bytes_of_polyP Extra_block.bytes_of_extra_blockP.
+  by rewrite
+       take_size_cat 1:TPoly.bytes_of_polyP 1:// drop_size_cat
+       1:TPoly.bytes_of_polyP 1:// TPoly.bytes_of_polyKd
+       Extra_block.bytes_of_extra_blockKd.
 qed.
 
 realize sample_spec.
@@ -871,17 +888,17 @@ proof.
   have s1 := supp_dlist_size dbyte _ _ ge0_poly_size h1.
   have s2 := supp_dlist_size dbyte _ _ ge0_extra_block_size h2.
   rewrite eq_iff /pred1 /topair //=; split=> />.
-  + rewrite insubdK 1:size_cat 1:s1 1:s2 //.
+  + rewrite block_of_bytesdK 1:size_cat 1:s1 1:s2 //.
     by rewrite take_size_cat // drop_size_cat.
-  move=> /(congr1 bytes_of_poly); rewrite insubdK=> // ->.
-  move=> /(congr1 bytes_of_extra_block); rewrite insubdK=> // ->.
-  rewrite insubdK.
-  + rewrite size_drop 1:ge0_poly_size valP /block_size /poly_size.
+  move=> /(congr1 bytes_of_poly); rewrite poly_of_bytesdK=> // ->.
+  move=> /(congr1 bytes_of_extra_block); rewrite extra_block_of_bytesdK=> // ->.
+  rewrite extra_block_of_bytesdK.
+  + rewrite size_drop 1:ge0_poly_size bytes_of_blockP /block_size /poly_size.
     smt(ge0_poly_in_size ge0_poly_out_size ge0_extra_block_size).
-  rewrite insubdK.
-  + rewrite size_take 1:ge0_poly_size valP /poly_size /block_size.
+  rewrite poly_of_bytesdK.
+  + rewrite size_take 1:ge0_poly_size bytes_of_blockP /poly_size /block_size.
     smt(ge0_poly_in_size ge0_poly_out_size ge0_extra_block_size).
-  by rewrite cat_take_drop valKd.
+  by rewrite cat_take_drop bytes_of_blockKd.
 qed.
 
 clone Split as Split1 with 
@@ -898,31 +915,36 @@ clone import Split1.SplitCodom as SplitC2 with
   type to2 <- poly_out,
   op topair = fun (b:poly) => 
      let bs = bytes_of_poly b in
-     (Poly_in.insubd (take poly_in_size bs), Poly_out.insubd (drop poly_in_size bs)),
+     (
+       Poly_in.poly_in_of_bytesd (take poly_in_size bs),
+       Poly_out.poly_out_of_bytesd (drop poly_in_size bs)
+     ),
   op ofpair = fun (p:poly_in * poly_out) =>
-     TPoly.insubd (bytes_of_poly_in p.`1 ++ bytes_of_poly_out p.`2),
+     TPoly.poly_of_bytesd (bytes_of_poly_in p.`1 ++ bytes_of_poly_out p.`2),
   op sampleto1 <- fun _ => dpoly_in,
   op sampleto2 <- fun _ => dpoly_out
   proof *.
 realize topairK.
 proof.
   move=> x; rewrite /topair /ofpair /=.
-  rewrite -{3}(TPoly.valKd x); congr.
-  rewrite Poly_in.insubdK. 
-  + rewrite size_take 1:ge0_poly_in_size TPoly.valP.
+  rewrite -{3}(TPoly.bytes_of_polyKd x); congr.
+  rewrite Poly_in.poly_in_of_bytesdK. 
+  + rewrite size_take 1:ge0_poly_in_size TPoly.bytes_of_polyP.
     smt (ge0_poly_in_size ge0_poly_out_size).
-  rewrite Poly_out.insubdK 2:cat_take_drop 2://.
-  rewrite size_drop 1:ge0_poly_in_size TPoly.valP.
+  rewrite Poly_out.poly_out_of_bytesdK 2:cat_take_drop 2://.
+  rewrite size_drop 1:ge0_poly_in_size TPoly.bytes_of_polyP.
   smt (ge0_poly_in_size ge0_poly_out_size).
 qed.
 
 realize ofpairK.
 proof.
   move=> [x1 x2]; rewrite /topair /ofpair /=.
-  rewrite TPoly.insubdK.
-  + by rewrite size_cat Poly_in.valP Poly_out.valP.
-  by rewrite take_size_cat 1:Poly_in.valP 1:// drop_size_cat 1:Poly_in.valP 1://
-     Poly_in.valKd Poly_out.valKd.
+  rewrite TPoly.poly_of_bytesdK.
+  + by rewrite size_cat Poly_in.bytes_of_poly_inP Poly_out.bytes_of_poly_outP.
+  by rewrite
+       take_size_cat 1:Poly_in.bytes_of_poly_inP 1:// drop_size_cat
+       1:Poly_in.bytes_of_poly_inP 1:// Poly_in.bytes_of_poly_inKd
+       Poly_out.bytes_of_poly_outKd.
 qed.
 
 realize sample_spec.
@@ -937,17 +959,17 @@ proof.
   have s1 := supp_dlist_size dbyte _ _ ge0_poly_in_size h1.
   have s2 := supp_dlist_size dbyte _ _ ge0_poly_out_size h2.
   rewrite eq_iff /pred1 /topair //=; split=> />.
-  + rewrite insubdK 1:size_cat 1:s1 1:s2 //.
+  + rewrite poly_of_bytesdK 1:size_cat 1:s1 1:s2 //.
     by rewrite take_size_cat // drop_size_cat.
-  move=> /(congr1 bytes_of_poly_in); rewrite insubdK=> // ->.
-  move=> /(congr1 bytes_of_poly_out); rewrite insubdK=> // ->.
-  rewrite insubdK.
-  + rewrite size_drop 1:ge0_poly_in_size valP /poly_size.
+  move=> /(congr1 bytes_of_poly_in); rewrite poly_in_of_bytesdK=> // ->.
+  move=> /(congr1 bytes_of_poly_out); rewrite poly_out_of_bytesdK=> // ->.
+  rewrite poly_out_of_bytesdK.
+  + rewrite size_drop 1:ge0_poly_in_size bytes_of_polyP /poly_size.
     smt(ge0_poly_in_size ge0_poly_out_size ge0_extra_block_size).
-  rewrite insubdK.
-  + rewrite size_take 1:ge0_poly_in_size valP /poly_size.
+  rewrite poly_in_of_bytesdK.
+  + rewrite size_take 1:ge0_poly_in_size bytes_of_polyP /poly_size.
     smt(ge0_poly_in_size ge0_poly_out_size ge0_extra_block_size).
-  by rewrite cat_take_drop valKd.
+  by rewrite cat_take_drop bytes_of_polyKd.
 qed.
 
 module G4 (A:CCA_Adv, RO:RO) = {
@@ -967,7 +989,7 @@ module G5_end(RO:RO) = {
     i <- 0;
     while (i < size ns) {
       n  <- List.nth witness ns i;
-      bl <@ RO.get(n,C.ofint 0);
+      bl <@ RO.get(n,C.ofintd 0);
       (r,s) <- mk_rs bl; 
       forged <- forged || test_poly n Mem.lc r s;
       i <- i + 1;
@@ -1147,7 +1169,7 @@ section PROOFS.
     wp;while{2} (0 <= i <= size ns /\ 
               forged = exists j, 0 <= j < i /\
                         let n = nth witness ns j in
-                        let bl = oget RO.m.[(n,C.ofint 0)] in
+                        let bl = oget RO.m.[(n,C.ofintd 0)] in
                         let (r,s) = mk_rs bl in
                         test_poly n Mem.lc r s){2} (size ns - i){2}.
     + by move=> _ z; inline *; auto => /> /#.
@@ -1160,7 +1182,7 @@ section PROOFS.
     have in_ns : n \in ns.
     + by rewrite mem_undup; apply (map_f _ _ (n,a,c,t)).
     move: hdec; rewrite in_ns /dec /genpoly1305 /test_poly /= /get nth_index 1://.
-    case: (mk_rs (oget RO.m{2}.[(n, C.ofint 0)])) => r s /=.
+    case: (mk_rs (oget RO.m{2}.[(n, C.ofintd 0)])) => r s /=.
     case: (t = poly1305 r s (topol a c)) => // heq _.
     apply List.hasP; exists (topol a c, t) => /=;split; 2:by rewrite heq.
     by apply mapP; exists (n, a, c, t) => /=; apply List.mem_filter.
@@ -1376,12 +1398,13 @@ section PROOFS.
   local lemma mk_rs_ofpair r s e : 
     mk_rs (SplitC1.ofpair (SplitC2.ofpair (r, s), e)) = (r, s).
   proof.
-    rewrite /mk_rs /SplitC1.ofpair /SplitC2.ofpair /= insubdK.
-    + by rewrite size_cat TPoly.valP Extra_block.valP.
+    rewrite /mk_rs /SplitC1.ofpair /SplitC2.ofpair /= block_of_bytesdK.
+    + by rewrite size_cat TPoly.bytes_of_polyP Extra_block.bytes_of_extra_blockP.
     have h1 : size (bytes_of_poly_in r ++ bytes_of_poly_out s) = poly_size.
-    + by rewrite size_cat Poly_in.valP Poly_out.valP.
-    rewrite TPoly.insubdK 1:// take_size_cat 1:// take_size_cat 2:drop_size_cat ?Poly_in.valP //.
-    by rewrite Poly_in.valKd Poly_out.valKd.
+    + by rewrite size_cat Poly_in.bytes_of_poly_inP Poly_out.bytes_of_poly_outP.
+    rewrite TPoly.poly_of_bytesdK 1:// take_size_cat 1://.
+    rewrite take_size_cat 2:drop_size_cat ?Poly_in.bytes_of_poly_inP //.
+    by rewrite Poly_in.bytes_of_poly_inKd Poly_out.bytes_of_poly_outKd.
   qed.
 
   op inv_cpa (mr1 : (nonce*C.counter, poly_in) fmap) 
@@ -1415,7 +1438,7 @@ section PROOFS.
            size p{1} <= (C.max_counter - (i{1} - 1)) * block_size /\
            mr0 = ROin.m{1} /\ ms0 = ROout.m{1}  /\
            (forall n' c, (n',c) \in ROF.m => 
-                  if n{2} = n' then 1 <= C.val c < i else n' \in BNR.lenc){1}).
+                  if n{2} = n' then 1 <= C.toint c < i else n' \in BNR.lenc){1}).
     + inline{1} 1; inline{1} 4; wp.
       conseq (_ : (={i, c, n} /\ size c{1} + size p{1} = sz /\
                   size p{1} = size p{2} /\
@@ -1424,21 +1447,21 @@ section PROOFS.
                   mr0 = ROin.m{1} /\ ms0 = ROout.m{1}  /\
                   (forall (n' : nonce) (c1 : C.counter),
                     (n', c1) \in ROF.m{1} => 
-                    if n{2} = n' then 1 <= C.val c1 < i{1} else n' \in BNR.lenc{1})) /\
+                    if n{2} = n' then 1 <= C.toint c1 < i{1} else n' \in BNR.lenc{1})) /\
                   p{1} <> [] /\ p{2} <> [] /\
                   i{1} <= C.max_counter ==> _) => //.
       + move=> /> &1 &2 -> *.
         have h1 : 0 < size p{2} by smt (size_ge0 size_eq0).
         have : 0 < (C.max_counter - (i{2} - 1)) * block_size by smt().
         by rewrite (StdOrder.IntOrder.pmulr_lgt0 _ _ gt0_block_size) /#.
-      rcondf{1} ^if; 1: by auto; smt (C.insubdK).
-      inline{1} 5; rcondt{1} ^if; 1: by auto; smt (C.insubdK).
+      rcondf{1} ^if; 1: by auto; smt (C.ofintdK).
+      inline{1} 5; rcondt{1} ^if; 1: by auto; smt (C.ofintdK).
       wp; rnd (fun z => z +^ extend p{1}); auto => &1 &2 [#] 3!-> heq hs /= *;split.
       + move=> ??;apply xorK1.
       move=> h1 b ?; rewrite -h1 //= get_setE /= Block.MB.addmC /=.
       rewrite -!size_eq0 !size_drop 1,2:ge0_block_size hs /= 
-        size_cat size_take 1:size_ge0 -heq Block.valP; split;1: smt(); split; 1: smt().
-      split; 2: smt(mem_set C.insubdK).
+        size_cat size_take 1:size_ge0 -heq Block.bytes_of_blockP; split;1: smt(); split; 1: smt().
+      split; 2: smt(mem_set C.ofintdK).
       have := StdOrder.IntOrder.mulr_ge0 (C.max_counter - i{2}) block_size.
       smt (ge0_block_size).
     wp; skip=> &1 &2 [#] //= 4!->> h1 h2 h3 2!<<- //=.
@@ -1469,7 +1492,7 @@ section PROOFS.
       + by ecall (equ_cc n{1} ROin.m{1} ROout.m{1}); rewrite /check_plaintext; auto => /> /#.
       move=> {&m};inline{1} 5; inline{1} 8.
       rcondt{1} ^if.
-      + move=> &m; auto => />; rewrite /SplitD.test /= C.insubdK //=.
+      + move=> &m; auto => />; rewrite /SplitD.test /= C.ofintdK //=.
         smt(C.gt0_max_counter).
       inline{1} 9; wp.
       call{1} (_: true ==> true); 1: by islossless; apply dextra_block_ll.
@@ -1525,8 +1548,8 @@ section PROOFS.
         c <@ EncRnd.cc(n,p);   
         (* t <$ dp *)
         t <@ set_bad1(map (fun c:ciphertext => c.`4) (filter (fun (c:ciphertext) => c.`1 = n) Mem.lc));
-        ROin.sample(n,C.ofint 0);
-        ROout.set((n,C.ofint 0), witness); 
+        ROin.sample(n,C.ofintd 0);
+        ROout.set((n,C.ofintd 0), witness); 
         log.[n] <- (a,c,t);
         return (n,a,c,t);
       }
@@ -1552,15 +1575,15 @@ section PROOFS.
         i <- 0;
         while (i < size ns) {
           n  <- List.nth witness ns i;
-          if ((n,C.ofint 0) \in ROout.m) {
-            r <@ ROin.get(n,C.ofint 0);
+          if ((n,C.ofintd 0) \in ROout.m) {
+            r <@ ROin.get(n,C.ofintd 0);
             forged <- forged || test_poly_in n Mem.lc r (oget log.[n]);
           } else { 
-            r <@ ROin.get(n,C.ofint 0);
+            r <@ ROin.get(n,C.ofintd 0);
             t <@ set_bad2((map 
                 (fun c:ciphertext => c.`4 - poly1305_eval r (topol c.`2 c.`3)) 
                 (filter (fun c:ciphertext => c.`1 = n) Mem.lc)));
-            ROout.set((n,C.ofint 0), witness); 
+            ROout.set((n,C.ofintd 0), witness); 
           }
           i <- i + 1;
         }
@@ -1597,8 +1620,8 @@ section PROOFS.
      (forall n a c t, (n,a,c,t) \in lc1 => n \in nlog => nlog.[n] <> Some (a, c, t)) /\
      (forall n, n \in lenc1 => 
         let (a,c,t) = oget nlog.[n] in
-        let r = oget mr1.[(n,C.ofint 0)] in
-        let s = oget ms1.[(n,C.ofint 0)] in
+        let r = oget mr1.[(n,C.ofintd 0)] in
+        let s = oget ms1.[(n,C.ofintd 0)] in
         s = t - poly1305_eval r (topol a c)).
 
   local lemma step4_1 &m:
@@ -1646,7 +1669,7 @@ section PROOFS.
         + by ecall (equ_cc n{1} ROin.m{1} ROout.m{1}); rewrite /check_plaintext; auto => /> /#.
         inline{1} 5; inline{1} 8.
         rcondt{1} ^if.
-        + by move=> &m; auto => />; rewrite /SplitD.test /= C.insubdK //=; smt(C.gt0_max_counter).
+        + by move=> &m; auto => />; rewrite /SplitD.test /= C.ofintdK //=; smt(C.gt0_max_counter).
         inline{1} 9; wp.
         call{1} (_: true ==> true); 1: by islossless; apply dextra_block_ll.
         inline *.
@@ -1729,11 +1752,11 @@ section PROOFS.
             (forall j, 
               i{1} <= j < size ns{1} =>
               let n = nth witness ns{1} j in
-              (n, C.ofint 0) \in ROout.m{1} =>
+              (n, C.ofintd 0) \in ROout.m{1} =>
               let (a, c, t) = oget UFCMA.log{2}.[n] in
               !(n,a,c,t) \in Mem.lc{1} /\ valid_topol a c /\
-              let r = oget ROin.m{1}.[(n, C.ofint 0)] in 
-              let s = oget ROout.m{1}.[(n, C.ofint 0)] in 
+              let r = oget ROin.m{1}.[(n, C.ofintd 0)] in 
+              let s = oget ROout.m{1}.[(n, C.ofintd 0)] in 
               s = t - poly1305_eval r (topol a c))); last first.
     + auto => /> ; smt (undup_uniq size_undup size_map).
 
@@ -1761,7 +1784,7 @@ section PROOFS.
     (*     smt (undup_uniq size_undup size_map). *)
 
     inline{1} 2; rcondt{1} 3. 
-    + by move=> *;auto => />;rewrite /test /= C.insubdK; smt (C.gt0_max_counter).
+    + by move=> *;auto => />;rewrite /test /= C.ofintdK; smt (C.gt0_max_counter).
     inline{1} 3; inline{1} 4; sp 0 1; wp.
     call{1} (_: true ==> true); 1: by islossless.
     wp; inline *; if{2}.
@@ -1805,10 +1828,10 @@ section PROOFS.
     proof *.
 
   op sub_map (m1 : (nonce * C.counter, 'a) fmap) (m2 : (nonce * C.counter, 'a) fmap) i l =
-    (forall n, (n, C.ofint 0) \in m2 => (n,C.ofint 0) \in m1) /\
-    (forall n, (n, C.ofint 0) \in m2 => m1.[(n,C.ofint 0)] = m2.[(n,C.ofint 0)]) /\
-    (forall j, 0 <= j < i => (nth witness l j, C.ofint 0) \in m1) /\
-    (forall n, (n, C.ofint 0) \in m1 => (n, C.ofint 0) \in m2 \/ exists j, 0 <= j < i /\ n = nth witness l j).
+    (forall n, (n, C.ofintd 0) \in m2 => (n,C.ofintd 0) \in m1) /\
+    (forall n, (n, C.ofintd 0) \in m2 => m1.[(n,C.ofintd 0)] = m2.[(n,C.ofintd 0)]) /\
+    (forall j, 0 <= j < i => (nth witness l j, C.ofintd 0) \in m1) /\
+    (forall n, (n, C.ofintd 0) \in m1 => (n, C.ofintd 0) \in m2 \/ exists j, 0 <= j < i /\ n = nth witness l j).
 
 
   local module UF = {
@@ -1818,15 +1841,15 @@ section PROOFS.
   local module Orcl : Orcl = {
     proc f (n : nonce) : unit = {
       var r, t;
-      if ((n,C.ofint 0) \in ROout.m) {
-        r <@ ROIN.RO.get(n,C.ofint 0);
+      if ((n,C.ofintd 0) \in ROout.m) {
+        r <@ ROIN.RO.get(n,C.ofintd 0);
         UF.forged <- UF.forged || test_poly_in n Mem.lc r (oget UFCMA.log.[n]);
       } else { 
-        r <@ ROIN.RO.get(n,C.ofint 0);
+        r <@ ROIN.RO.get(n,C.ofintd 0);
         t <@ UFCMA(ROIN.RO).set_bad2((map 
                 (fun c:ciphertext => c.`4 - poly1305_eval r (topol c.`2 c.`3)) 
                 (filter (fun c:ciphertext => c.`1 = n) Mem.lc)));
-        ROout.set((n,C.ofint 0), witness); 
+        ROout.set((n,C.ofintd 0), witness); 
       }
     }
   }.
@@ -1850,8 +1873,8 @@ section PROOFS.
       UF.forged <- false;
       if (size Mem.lc <= qdec) {
         ns <- undup (List.map (fun (p:ciphertext) => p.`1) Mem.lc);
-        ns1 <- filter (fun n => (n,C.ofint 0) \in ROout.m) ns;
-        ns2 <- filter (fun n => (n,C.ofint 0) \notin ROout.m) ns;
+        ns1 <- filter (fun n => (n,C.ofintd 0) \in ROout.m) ns;
+        ns2 <- filter (fun n => (n,C.ofintd 0) \notin ROout.m) ns;
         Iter(Orcl).iter(ns1++ns2);
       }
       return UF.forged;
@@ -1878,19 +1901,19 @@ section PROOFS.
       UF.forged <- false;
       if (size Mem.lc <= qdec) {
         ns <- undup (List.map (fun (p:ciphertext) => p.`1) Mem.lc);
-        ns1 <- filter (fun n => (n,C.ofint 0) \in ROout.m) ns;
-        ns2 <- filter (fun n => (n,C.ofint 0) \notin ROout.m) ns;
+        ns1 <- filter (fun n => (n,C.ofintd 0) \in ROout.m) ns;
+        ns2 <- filter (fun n => (n,C.ofintd 0) \notin ROout.m) ns;
         i <- 0;
         while (i < size ns1) {
           n <- nth witness ns1 i;
-          r <@ ROin.get(n,C.ofint 0);
+          r <@ ROin.get(n,C.ofintd 0);
           UF.forged <- UF.forged || test_poly_in n Mem.lc r (oget UFCMA.log.[n]);
           i <- i + 1;
         }
         i <- 0;
         while (i < size ns2) {
           n <- nth witness ns2 i;
-          r <@ ROin.get(n,C.ofint 0);
+          r <@ ROin.get(n,C.ofintd 0);
           t <@ UFCMA(ROin).set_bad2((map 
                 (fun c:ciphertext => c.`4 - poly1305_eval r (topol c.`2 c.`3)) 
                 (filter (fun c:ciphertext => c.`1 = n) Mem.lc)));
@@ -1979,7 +2002,7 @@ section PROOFS.
       rewrite set_setE //= (eq_sym t2{2}) h /= => /> *. 
       by rewrite set_setE //= (eq_sym t2{2}) h /= => /> *; smt().
     move=> /> &2 *; pose l := undup _.
-    by have:=perm_filterC (fun n => (n,C.ofint 0) \in ROout.m{2}) l; rewrite /predC perm_eq_sym.
+    by have:=perm_filterC (fun n => (n,C.ofintd 0) \in ROout.m{2}) l; rewrite /predC perm_eq_sym.
   proc; sp.
   seq 2 2 : (={glob UFCMA2,RO.m}); 1: by sim.
   inline*; if; auto; sp.
@@ -1987,17 +2010,17 @@ section PROOFS.
   seq 1 1 : (={glob UFCMA2,RO.m,ns,ns1,ns2} /\
                l{1} = ns2{2} /\
                ns{2} = undup (map (fun (p : ciphertext) => p.`1) Mem.lc{2}) /\
-               ns1{2} = filter (fun (n0 : nonce) => (n0, C.ofint 0) \in ROout.m{2}) ns{2} /\
-               ns2{2} = filter (fun (n0 : nonce) => (n0, C.ofint 0) \notin ROout.m{2}) ns{2}).
+               ns1{2} = filter (fun (n0 : nonce) => (n0, C.ofintd 0) \in ROout.m{2}) ns{2} /\
+               ns2{2} = filter (fun (n0 : nonce) => (n0, C.ofintd 0) \notin ROout.m{2}) ns{2}).
   + move=> />.
     while(={glob UFCMA2, RO.m, ns, ns1, ns2} /\
         ns{2} = undup (map (fun (p : ciphertext) => p.`1) Mem.lc{2}) /\
-        ns1{2} = filter (fun (n0 : nonce) => (n0, (C.ofint 0)%C) \in ROout.m{2}) ns{2} /\
-        ns2{2} = filter (fun (n0 : nonce) => (n0, (C.ofint 0)%C) \notin ROout.m{2}) ns{2} /\
+        ns1{2} = filter (fun (n0 : nonce) => (n0, (C.ofintd 0)%C) \in ROout.m{2}) ns{2} /\
+        ns2{2} = filter (fun (n0 : nonce) => (n0, (C.ofintd 0)%C) \notin ROout.m{2}) ns{2} /\
         l{1} = drop i{2} ns1{2} ++ ns2{2} /\ 0 <= i{2});
       2: by auto=>/>; smt(drop0 size_eq0 size_ge0 size_cat drop_oversize).    
     sp=> />.
-    conseq(: n{2} = nth witness ns1{2} i{2} /\ x{2} = (n{2}, (C.ofint 0)%C) /\
+    conseq(: n{2} = nth witness ns1{2} i{2} /\ x{2} = (n{2}, (C.ofintd 0)%C) /\
              n{1} = head witness l{1} /\
              (((UF.forged{1}, UFCMA.bad2{1}, UFCMA.cbad2{1}, UFCMA.bad1{1}, UFCMA.cbad1{1}, RO.m{1}, UFCMA.log{1}, SplitC2.I2.RO.m{1},
                 SplitD.ROF.RO.m{1}, BNR.ndec{1}, BNR.lenc{1}, Mem.lc{1}, Mem.log{1}, (glob A){1}) =
@@ -2007,18 +2030,18 @@ section PROOFS.
                 (glob A){2}) /\
              ={RO.m, ns, ns1, ns2}) /\
              ns{2} = undup (map (fun (p : ciphertext) => p.`1) Mem.lc{2}) /\
-             ns1{2} = filter (fun (n0 : nonce) => (n0, (C.ofint 0)%C) \in ROout.m{2}) ns{2} /\
-             ns2{2} = filter (fun (n0 : nonce) => (n0, (C.ofint 0)%C) \notin ROout.m{2}) ns{2} /\
+             ns1{2} = filter (fun (n0 : nonce) => (n0, (C.ofintd 0)%C) \in ROout.m{2}) ns{2} /\
+             ns2{2} = filter (fun (n0 : nonce) => (n0, (C.ofintd 0)%C) \notin ROout.m{2}) ns{2} /\
              l{1} = drop i{2} ns1{2} ++ ns2{2} /\ 0 <= i{2}) /\
              (l{1} <> [] /\ size ns2{1} < size l{1}) /\ i{2} < size ns1{2} /\
-             ={n} /\ (forall j, 0 <= j < size ns1{2} => (nth witness ns1{2} j, C.ofint 0) \in ROout.m{2}) ==> _).
+             ={n} /\ (forall j, 0 <= j < size ns1{2} => (nth witness ns1{2} j, C.ofintd 0) \in ROout.m{2}) ==> _).
     - move=> /> &2.
       pose l := undup _; pose l1 := List.filter _ _; pose l2 := List.filter _ _.
       move=> H H0 H1 *.
       have:= H1; rewrite size_cat ltz_addr => h. 
       rewrite -nth0_head  nth_cat //= h /= nth_drop //= => *.
-      have:=allP (fun (n0 : nonce) => (n0, (C.ofint 0)%C) \in SplitC2.I2.RO.m{2}) l1.
-      have->//=->//=:=filter_all (fun (n0 : nonce) => (n0, (C.ofint 0)%C) \in SplitC2.I2.RO.m{2}) l.
+      have:=allP (fun (n0 : nonce) => (n0, (C.ofintd 0)%C) \in SplitC2.I2.RO.m{2}) l1.
+      have->//=->//=:=filter_all (fun (n0 : nonce) => (n0, (C.ofintd 0)%C) \in SplitC2.I2.RO.m{2}) l.
       by apply mem_nth.
     rcondt{1} 1; 1: by auto=> /#.
     wp 5 4.
@@ -2032,16 +2055,16 @@ section PROOFS.
   while(={UF.forged,UFCMA.bad2,UFCMA.cbad2,UFCMA.log,Mem.lc,Mem.log,RO.m,ns,ns1,ns2} /\
         l{1} = drop i{2} ns2{2} /\ 0 <= i{2} /\
         ns{2} = undup (map (fun (p : ciphertext) => p.`1) Mem.lc{2}) /\
-        ns1{2} = filter (fun (n0 : nonce) => (n0, C.ofint 0) \in ROout.m{2}) ns{2} /\
-        ns2{2} = filter (fun (n0 : nonce) => (n0, C.ofint 0) \notin ROout.m{2}) ns{2} /\
+        ns1{2} = filter (fun (n0 : nonce) => (n0, C.ofintd 0) \in ROout.m{2}) ns{2} /\
+        ns2{2} = filter (fun (n0 : nonce) => (n0, C.ofintd 0) \notin ROout.m{2}) ns{2} /\
         sub_map ROout.m{1} ROout.m{2} i{2} ns2{2}); 2: by auto; smt(drop0 size_eq0 size_ge0).
   sp.
-  conseq(: n{2} = nth witness ns2{2} i{2} /\ x0{2} = (n{2}, C.ofint 0) /\
+  conseq(: n{2} = nth witness ns2{2} i{2} /\ x0{2} = (n{2}, C.ofintd 0) /\
       n{1} = head witness l{1} /\
       (={UF.forged, UFCMA.bad2, UFCMA.cbad2, UFCMA.log, Mem.lc, Mem.log, RO.m, ns, ns1, ns2} /\
       l{1} = drop i{2} ns2{2} /\ 0 <= i{2} /\ ns{2} = undup (map (fun (p : ciphertext) => p.`1) Mem.lc{2}) /\
-      ns1{2} = filter (fun (n0 : nonce) => (n0, (C.ofint 0)%C) \in ROout.m{2}) ns{2} /\
-      ns2{2} = filter (fun (n0 : nonce) => (n0, (C.ofint 0)%C) \notin ROout.m{2}) ns{2} /\
+      ns1{2} = filter (fun (n0 : nonce) => (n0, (C.ofintd 0)%C) \in ROout.m{2}) ns{2} /\
+      ns2{2} = filter (fun (n0 : nonce) => (n0, (C.ofintd 0)%C) \notin ROout.m{2}) ns{2} /\
       sub_map ROout.m{1} ROout.m{2} i{2} ns2{2}) /\ l{1} <> [] /\ i{2} < size ns2{2} /\ ={n} ==> _).
   + by move=> /> *; rewrite (drop_nth witness) //=.
   rcondf{1} 1; 1: auto=> />.
@@ -2052,8 +2075,8 @@ section PROOFS.
     have/=:=H3 (nth witness l2 i{m}).
     apply absurd=> /= -> /=.
     rewrite negb_or negb_exists/=; split=> />.
-    - have:=allP (fun (n0 : nonce) => (n0, C.ofint 0) \notin SplitC2.I2.RO.m{m}) l2.
-      have-> /= -> //=:=filter_all (fun (n0 : nonce) => (n0, C.ofint 0) \notin SplitC2.I2.RO.m{m}) l.
+    - have:=allP (fun (n0 : nonce) => (n0, C.ofintd 0) \notin SplitC2.I2.RO.m{m}) l2.
+      have-> /= -> //=:=filter_all (fun (n0 : nonce) => (n0, C.ofintd 0) \notin SplitC2.I2.RO.m{m}) l.
       by rewrite mem_nth //=.
     move=> a; case: (0 <= a < i{m})=> //= [#]*.
     have := before_index witness (nth witness l2 i{m}) l2 a.
@@ -2064,10 +2087,10 @@ section PROOFS.
   pose l := undup _.
   pose l2 := List.filter _ _.
   move=> *.
-  have h1: forall j, 0 <= j < size l2 => (nth witness l2 j, C.ofint 0) \notin ROout.m{2}.
+  have h1: forall j, 0 <= j < size l2 => (nth witness l2 j, C.ofintd 0) \notin ROout.m{2}.
   + move=> j [#] *.
-    - have:=allP (fun (n0 : nonce) => (n0, C.ofint 0) \notin ROout.m{2}) l2.
-      have-> /= -> //=:=filter_all (fun (n0 : nonce) => (n0, C.ofint 0) \notin SplitC2.I2.RO.m{2}) l.
+    - have:=allP (fun (n0 : nonce) => (n0, C.ofintd 0) \notin ROout.m{2}) l2.
+      have-> /= -> //=:=filter_all (fun (n0 : nonce) => (n0, C.ofintd 0) \notin SplitC2.I2.RO.m{2}) l.
       by rewrite mem_nth //=.
   rewrite (drop_nth witness i{2} l2) //= drop0 //=; do ! split=> /> *.
   + smt().
@@ -2091,11 +2114,11 @@ section PROOFS.
       var n, r, ns, ns1;
 
       ns <- undup (List.map (fun (p:ciphertext) => p.`1) Mem.lc);
-      ns1 <- filter (fun n => (n,C.ofint 0) \in ROout.m) ns;
+      ns1 <- filter (fun n => (n,C.ofintd 0) \in ROout.m) ns;
       if (cforged < size ns1) {
         n <- nth witness ns1 cforged;
         r <$ dpoly_in;
-        ROin.set((n,C.ofint 0), r);
+        ROin.set((n,C.ofintd 0), r);
         UF.forged <- UF.forged ||
             test_poly_in n Mem.lc r (oget UFCMA.log.[n]);
         cforged <- cforged + 1;
@@ -2106,10 +2129,10 @@ section PROOFS.
       var n, r, ns, ns2, t;
 
       ns <- undup (List.map (fun (p:ciphertext) => p.`1) Mem.lc);
-      ns2 <- filter (fun n => (n,C.ofint 0) \notin ROout.m) ns;
+      ns2 <- filter (fun n => (n,C.ofintd 0) \notin ROout.m) ns;
       if (UFCMA.cbad2 < size ns2) {
         n <- nth witness ns2 UFCMA.cbad2;
-        r <@ ROin.get(n,C.ofint 0);
+        r <@ ROin.get(n,C.ofintd 0);
         t <$ dpoly_out;
         UFCMA.bad2 <- UFCMA.bad2 || 
               t \in (map (fun c:ciphertext => c.`4 - poly1305_eval r (topol c.`2 c.`3)) 
@@ -2124,7 +2147,7 @@ section PROOFS.
       UF.forged <- false;
       cforged <- 0;
       ns <- undup (List.map (fun (p:ciphertext) => p.`1) Mem.lc);
-      ns1 <- filter (fun n => (n,C.ofint 0) \in ROout.m) ns;
+      ns1 <- filter (fun n => (n,C.ofintd 0) \in ROout.m) ns;
 
       while (cforged < size ns1) {
         set_forged();
@@ -2137,7 +2160,7 @@ section PROOFS.
       UFCMA.bad2 <- false;
       UFCMA.cbad2 <- 0;
       ns <- undup (List.map (fun (p:ciphertext) => p.`1) Mem.lc);
-      ns2 <- filter (fun n => (n,C.ofint 0) \notin ROout.m) ns;
+      ns2 <- filter (fun n => (n,C.ofintd 0) \notin ROout.m) ns;
 
       while (UFCMA.cbad2 < size ns2) {
         set_bad2();
@@ -2182,7 +2205,7 @@ section PROOFS.
     if; auto; sp.
     while(={ns2, Mem.lc, RO.m, UFCMA.bad2, UF.forged, ROout.m} /\ i{1} = UFCMA.cbad2{2} /\ 
            ns{1} = undup (map (fun (p : ciphertext) => p.`1) Mem.lc{1}) /\
-           ns2{1} = filter (fun (n1 : nonce) => (n1, (C.ofint 0)%C) \notin ROout.m{1}) ns{1} /\
+           ns2{1} = filter (fun (n1 : nonce) => (n1, (C.ofintd 0)%C) \notin ROout.m{1}) ns{1} /\
            size Mem.lc{2} <= qdec).
     + sp; rcondt{2} 1; 1: auto=> />.
       sp; conseq(:_==> ={RO.m, UFCMA.bad2} /\ i{1} = UFCMA.cbad2{2})=>/>.
@@ -2191,9 +2214,9 @@ section PROOFS.
     conseq(:_==> ={Mem.lc,RO.m,UF.forged,ROout.m})=> />.
     while(={Mem.lc,RO.m,UF.forged,ROout.m, ns1, UFCMA.log} /\ i{1} = UFCMA4.cforged{2} /\ 
            size Mem.lc{2} <= qdec /\ 0 <= i{1} /\
-           (forall j, i{1} <= j < size ns1{1} => (nth witness ns1{1} j, C.ofint 0) \notin RO.m{1}) /\
+           (forall j, i{1} <= j < size ns1{1} => (nth witness ns1{1} j, C.ofintd 0) \notin RO.m{1}) /\
            ns{1} = undup (map (fun (p : ciphertext) => p.`1) Mem.lc{1}) /\
-           ns1{1} = filter (fun (n1 : nonce) => (n1, (C.ofint 0)%C) \in ROout.m{1}) ns{1}).
+           ns1{1} = filter (fun (n1 : nonce) => (n1, (C.ofintd 0)%C) \in ROout.m{1}) ns{1}).
     + sp; rcondt{2} 1; 1: by auto.
       rcondt{1} 2; 1: by auto=> /#.
       wp; auto=> /> &h.
@@ -2214,10 +2237,10 @@ section PROOFS.
     by hoare; auto; smt(ge0_qdec ge0_pr_zeropol).
   exists * Mem.lc, ROout.m; elim * => l roout.
   pose undupl := undup (map (fun (c:ciphertext) => c.`1) l).
-  pose l1 := filter (fun n => (n, C.ofint 0) \in roout) undupl. 
-  pose l2 := filter (fun n => (n, C.ofint 0) \notin roout) undupl.
-  pose n1 := size (filter (fun (c:ciphertext) => (c.`1, C.ofint 0) \in roout) l).
-  pose n2 := size (filter (fun (c:ciphertext) => (c.`1, C.ofint 0) \notin roout) l).
+  pose l1 := filter (fun n => (n, C.ofintd 0) \in roout) undupl. 
+  pose l2 := filter (fun n => (n, C.ofintd 0) \notin roout) undupl.
+  pose n1 := size (filter (fun (c:ciphertext) => (c.`1, C.ofintd 0) \in roout) l).
+  pose n2 := size (filter (fun (c:ciphertext) => (c.`1, C.ofintd 0) \notin roout) l).
   seq 1 : UF.forged (n1%r * pr_zeropol) 1%r 1%r (n2%r * pr1_poly_out)
     (l = Mem.lc /\ roout = ROout.m /\ 0 < size Mem.lc <= qdec); auto.
   + by inline*; auto=> />; while(true); auto.
@@ -2247,7 +2270,7 @@ section PROOFS.
     + by move=> c; proc; sp; inline*; sp; if; auto=> /#.
     + by move=> b c; proc; inline*; sp; rcondf 1; auto. 
     + (* compute sum of probabilities *)
-      have hn1: n1 = size (filter (fun n => (n, C.ofint 0) \in roout) (map (fun (c:ciphertext) => c.`1) l)).
+      have hn1: n1 = size (filter (fun n => (n, C.ofintd 0) \in roout) (map (fun (c:ciphertext) => c.`1) l)).
       + by rewrite /n1 !size_filter count_map /preim.
       rewrite -BRA.mulr_suml ler_wpmul2r 1:ge0_pr_zeropol -sumr_ofint le_fromint IntOrder.lerr_eq.
       rewrite hn1 eq_sym  -big_count -BIA.big_filter /= /l1 //= (BIA.big_nth witness); apply BIA.congr_big_seq=> />.
@@ -2282,7 +2305,7 @@ section PROOFS.
     + move=> c; proc; inline*; sp; rcondt 1; 1: auto=> />.
       by wp -1=> />; conseq(:_==> true); auto; smt().
     + by move=> b c; proc; inline*; sp; rcondf 1; auto=> />.
-    + have hn2: n2 = size (filter (fun n => (n, C.ofint 0) \notin roout) (map (fun (c:ciphertext) => c.`1) l)).
+    + have hn2: n2 = size (filter (fun n => (n, C.ofintd 0) \notin roout) (map (fun (c:ciphertext) => c.`1) l)).
       + by rewrite /n2 !size_filter count_map /preim.
       rewrite -BRA.mulr_suml ler_wpmul2r; 1:smt(mu_bounded).
       rewrite -sumr_ofint le_fromint IntOrder.lerr_eq.
@@ -2326,8 +2349,8 @@ section PROOFS.
         c <@ EncRnd.cc(n,p);   
         (* t <$ dp *)
         t <@ set_bad1(map (fun c:ciphertext => c.`4) (filter (fun (c:ciphertext) => c.`1 = n) Mem.lc));
-        ROIN.RO.sample(n,C.ofint 0);
-        ROout.set((n,C.ofint 0), witness); 
+        ROIN.RO.sample(n,C.ofintd 0);
+        ROout.set((n,C.ofintd 0), witness); 
         UFCMA.log.[n] <- (a,c,t);
         return (n,a,c,t);
       }
@@ -2574,8 +2597,8 @@ section PROOFS.
         c <@ EncRnd.cc(n,p);   
         (* t <$ dp *)
         t <@ set_bad1(map (fun c:ciphertext => c.`4) (filter (fun (c:ciphertext) => c.`1 = n) Mem.lc));
-        ROIN.RO.sample(n,C.ofint 0);
-        ROout.set((n,C.ofint 0), witness); 
+        ROIN.RO.sample(n,C.ofintd 0);
+        ROout.set((n,C.ofintd 0), witness); 
         UFCMA.log.[n] <- (a,c,t);
         return (n,a,c,t);
       }
diff --git a/examples/MEE-CBC/FunctionalSpec.ec b/examples/MEE-CBC/FunctionalSpec.ec
index 29acabb5d9..5e05aa9f81 100644
--- a/examples/MEE-CBC/FunctionalSpec.ec
+++ b/examples/MEE-CBC/FunctionalSpec.ec
@@ -492,7 +492,6 @@ proof.
                       (size (pad _p (hmac_sha256 _mk _p)))
                       (nth witness (iv :: mee_enc AES hmac_sha256 _ek _mk iv _p)
                                    (size (pad _p (hmac_sha256 _mk _p)))).
-        smt().
       split=> //=.
       split; 1:by rewrite /mee_enc /= size_cbc_enc addzC.
       by rewrite take_size.
diff --git a/examples/ehoare/adversary.ec b/examples/ehoare/adversary.ec
index 1f22debbc2..6117ad1639 100644
--- a/examples/ehoare/adversary.ec
+++ b/examples/ehoare/adversary.ec
@@ -74,7 +74,7 @@ proof.
     rewrite (eq_Ep _ _
        ((fun r => (inv p)%xr * (! test r)%xr) + (fun r => (1 + size log)%xr))).
     + move => x xx /=. rewrite of_realM; 1,2:smt(of_realM invr_ge0 ge0_mu). smt().
-    rewrite EpD EpC EpZ /=; 1: smt(invr_gt0 dr_mu_test of_realK).
+    rewrite EpD EpC EpZ /=; 1: smt(invr_gt0 dr_mu_test of_realdK).
     rewrite Ep_mu mu_not dr_ll /= -/p.
     rewrite !to_pos_pos; 1,2,3,4:smt(mu_bounded dr_mu_test size_ge0).
   by auto.
diff --git a/src/ecCommands.ml b/src/ecCommands.ml
index 8114cbac50..1f86a41b4a 100644
--- a/src/ecCommands.ml
+++ b/src/ecCommands.ml
@@ -411,6 +411,13 @@ let rec process_type (scope : EcScope.scope) (tyd : ptydecl located) =
 and process_types (scope : EcScope.scope) tyds =
   List.fold_left process_type scope tyds
 
+(* -------------------------------------------------------------------- *)
+and process_subtype (scope : EcScope.scope) (subtype : psubtype located) =
+  EcScope.check_state `InTop "subtype" scope;
+  let scope = EcScope.Ty.add_subtype scope subtype in
+  EcScope.notify scope `Info "added subtype: `%s'" (unloc subtype.pl_desc.pst_name);
+  scope
+
 (* -------------------------------------------------------------------- *)
 and process_typeclass (scope : EcScope.scope) (tcd : ptypeclass located) =
   EcScope.check_state `InTop "type class" scope;
@@ -743,6 +750,7 @@ and process (ld : Loader.loader) (scope : EcScope.scope) g =
     match
       match g.pl_desc with
       | Gtype        t    -> `Fct   (fun scope -> process_types      scope  (List.map (mk_loc loc) t))
+      | Gsubtype     t    -> `Fct   (fun scope -> process_subtype    scope  (mk_loc loc t))
       | Gtypeclass   t    -> `Fct   (fun scope -> process_typeclass  scope  (mk_loc loc t))
       | Gtycinstance t    -> `Fct   (fun scope -> process_tycinst    scope  (mk_loc loc t))
       | Gmodule      m    -> `Fct   (fun scope -> process_module     scope  m)
diff --git a/src/ecCoreLib.ml b/src/ecCoreLib.ml
index 365213fe54..6e884a4e8c 100644
--- a/src/ecCoreLib.ml
+++ b/src/ecCoreLib.ml
@@ -116,7 +116,7 @@ module CI_Xreal = struct
   let mk_Rpbar = fun x -> EcPath.pqname p_Rpbar x
 
   let p_realp   = mk_Rp "realp"
-  let p_of_real = mk_Rp "of_real"
+  let p_of_real = mk_Rp "of_reald"
 
   let p_xreal   = mk_Rpbar "xreal"
   let p_rp      = mk_Rpbar "rp"
diff --git a/src/ecLexer.mll b/src/ecLexer.mll
index c1225b0720..f3552cb5ca 100644
--- a/src/ecLexer.mll
+++ b/src/ecLexer.mll
@@ -195,6 +195,7 @@
     "theory"      , THEORY     ;        (* KW: global *)
     "abstract"    , ABSTRACT   ;        (* KW: global *)
     "section"     , SECTION    ;        (* KW: global *)
+    "subtype"     , SUBTYPE    ;        (* KW: global *)
     "type"        , TYPE       ;        (* KW: global *)
     "class"       , CLASS      ;        (* KW: global *)
     "instance"    , INSTANCE   ;        (* KW: global *)
diff --git a/src/ecParser.mly b/src/ecParser.mly
index 2ac2421d97..82f1ef1452 100644
--- a/src/ecParser.mly
+++ b/src/ecParser.mly
@@ -558,6 +558,7 @@
 %token SPLITWHILE
 %token STAR
 %token SUBST
+%token SUBTYPE
 %token SUFF
 %token SWAP
 %token SYMMETRY
@@ -1644,6 +1645,21 @@ typedecl:
 | locality=locality TYPE td=tyd_name EQ te=datatype_def
     { [mk_tydecl ~locality td (PTYD_Datatype te)] }
 
+(* -------------------------------------------------------------------- *)
+(* Subtypes                                                             *)
+subtype:
+| SUBTYPE name=lident cname=prefix(AS, uident)? EQ LBRACE
+    x=lident COLON carrier=loc(type_exp) PIPE pred=form
+  RBRACE rename=subtype_rename?
+  { { pst_name    = name;
+      pst_cname   = cname;
+      pst_carrier = carrier;
+      pst_pred    = (x, pred);
+      pst_rename  = rename; } }
+
+subtype_rename:
+| RENAME x=STRING COMMA y=STRING { (x, y) }
+
 (* -------------------------------------------------------------------- *)
 (* Type classes                                                         *)
 typeclass:
@@ -3764,6 +3780,7 @@ global_action:
 | mod_def_or_decl  { Gmodule      $1 }
 | sig_def          { Ginterface   $1 }
 | typedecl         { Gtype        $1 }
+| subtype          { Gsubtype     $1 }
 | typeclass        { Gtypeclass   $1 }
 | tycinstance      { Gtycinstance $1 }
 | operator         { Goperator    $1 }
diff --git a/src/ecParsetree.ml b/src/ecParsetree.ml
index 936aa147a6..19909d4e3f 100644
--- a/src/ecParsetree.ml
+++ b/src/ecParsetree.ml
@@ -385,6 +385,15 @@ let rec pf_ident ?(raw = false) f =
   | PFtuple [f] when not raw -> pf_ident ~raw f
   | _ -> None
 
+(* -------------------------------------------------------------------- *)
+type psubtype = {
+  pst_name    : psymbol;
+  pst_cname   : psymbol option;
+  pst_carrier : pty;
+  pst_pred    : (psymbol * pformula);
+  pst_rename  : (string * string) option;
+}
+
 (* -------------------------------------------------------------------- *)
 type ptyvardecls =
   (psymbol * pqsymbol list) list
@@ -1262,6 +1271,7 @@ type global_action =
   | Gabbrev      of pabbrev
   | Gaxiom       of paxiom
   | Gtype        of ptydecl list
+  | Gsubtype     of psubtype
   | Gtypeclass   of ptypeclass
   | Gtycinstance of ptycinstance
   | Gaddrw       of (is_local * pqsymbol * pqsymbol list)
diff --git a/src/ecScope.ml b/src/ecScope.ml
index ac291529da..17e1b1a4a4 100644
--- a/src/ecScope.ml
+++ b/src/ecScope.ml
@@ -1548,760 +1548,838 @@ module ModType = struct
 end
 
 (* -------------------------------------------------------------------- *)
-module Ty = struct
-  open EcDecl
-  open EcTyping
+module Theory = struct
+  open EcTheory
 
-  module TT  = EcTyping
-  module ELI = EcInductive
-  module EHI = EcHiInductive
+  exception TopScope
 
   (* ------------------------------------------------------------------ *)
-  let check_name_available scope x =
-    let pname = EcPath.pqname (EcEnv.root (env scope)) x.pl_desc in
-
-    if    EcEnv.Ty       .by_path_opt pname (env scope) <> None
-       || EcEnv.TypeClass.by_path_opt pname (env scope) <> None then
-      hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc
+  let bind (scope : scope) (cth : thloaded) =
+    assert (scope.sc_pr_uc = None);
+    { scope with
+        sc_env = EcSection.add_th ~import:EcTheory.import0 cth scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
-  let bind ?(import = EcTheory.import0) (scope : scope) ((x, tydecl) : (_ * tydecl)) =
+  let required (scope : scope) (name : required_info) =
     assert (scope.sc_pr_uc = None);
-    let item = EcTheory.mkitem import (EcTheory.Th_type (x, tydecl)) in
-    { scope with sc_env = EcSection.add_item item scope.sc_env }
+    List.exists (fun x ->
+        if x.rqd_name = name.rqd_name then (
+          (* FIXME: raise an error message *)
+          assert (x.rqd_digest = name.rqd_digest);
+          true)
+        else false)
+      scope.sc_required
 
   (* ------------------------------------------------------------------ *)
-  let add scope (tyd : ptydecl located) =
-    let loc = loc tyd in
+  let mark_as_direct (scope : scope) (name : symbol) =
+    let for1 rq =
+      if   rq.rqd_name = name
+      then { rq with rqd_direct = true }
+      else rq
+    in { scope with sc_required = List.map for1 scope.sc_required }
 
-    let { pty_name = name; pty_tyvars = args;
-          pty_body = body; pty_locality = tyd_loca } = unloc tyd in
+  (* ------------------------------------------------------------------ *)
+  let enter (scope : scope) (mode : thmode) (name : symbol) =
+    assert (scope.sc_pr_uc = None);
+    subscope scope mode name
 
-    check_name_available scope name;
-    let env = env scope in
-    let tyd_params, tyd_type =
-      match body with
-      | PTYD_Abstract tcs ->
-        let tcs =
-          List.map
-            (fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) env))
-            tcs  in
-        let ue = TT.transtyvars env (loc, Some args) in
-        EcUnify.UniEnv.tparams ue, `Abstract (Sp.of_list tcs)
+  (* ------------------------------------------------------------------ *)
+  let rec require_loaded (id : required_info) scope =
+    if required scope id then
+      scope
+    else
+      match Msym.find_opt id.rqd_name scope.sc_loaded with
+      | Some (rth, ids) ->
+          let scope = List.fold_right require_loaded ids scope in
+          let env   = EcSection.require rth scope.sc_env in
+            { scope with
+                sc_env      = env;
+                sc_required = id :: scope.sc_required; }
 
-      | PTYD_Alias    bd ->
-        let ue     = TT.transtyvars env (loc, Some args) in
-        let body   = transty tp_tydecl env ue bd in
-        EcUnify.UniEnv.tparams ue, `Concrete body
+      | None -> assert false
 
-      | PTYD_Datatype dt ->
-        let datatype = EHI.trans_datatype env (mk_loc loc (args,name)) dt in
-        let tparams, tydt =
-          try ELI.datatype_as_ty_dtype datatype
-          with ELI.NonPositive -> EHI.dterror loc env EHI.DTE_NonPositive
-        in
-        tparams, `Datatype tydt
+  (* ------------------------------------------------------------------ *)
+  let update_with_required ~(dst : scope) ~(src : scope) =
+    let dst =
+      let sc_loaded =
+        Msym.union
+          (fun _ x y -> assert (x ==(*phy*) y); Some x)
+          dst.sc_loaded src.sc_loaded
+      in { dst with sc_loaded }
+    in List.fold_right require_loaded src.sc_required dst
 
-      | PTYD_Record rt ->
-        let record  = EHI.trans_record env (mk_loc loc (args,name)) rt in
-        let scheme  = ELI.indsc_of_record record in
-        record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields)
-    in
+  (* ------------------------------------------------------------------ *)
+  let add_clears clears scope =
+    let clears =
+      let for1 = function
+        | None -> EcEnv.root (env scope)
+        | Some { pl_loc = loc; pl_desc = (xs, x) as q } ->
+          let xp = EcEnv.root (env scope) in
+          let xp = EcPath.pqname (EcPath.extend xp xs) x in
+          if is_none (EcEnv.Theory.by_path_opt xp (env scope)) then
+            hierror ~loc "unknown theory: `%s`" (string_of_qsymbol q);
+          xp
+      in List.map for1 clears
+    in { scope with sc_clears = scope.sc_clears @ clears }
 
-    bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; })
+  (* -------------------------------------------------------------------- *)
+  let exit_r ?pempty (scope : scope) =
+    match scope.sc_top with
+    | None     -> raise TopScope
+    | Some sup ->
+      let clears   = scope.sc_clears in
+      let _, cth, _ = EcSection.exit_theory ?pempty ~clears scope.sc_env in
+      let loaded   = scope.sc_loaded in
+      let required = scope.sc_required in
+      let sup = { sup with sc_loaded = loaded; } in
+      ((cth, required), scope.sc_name, sup)
 
   (* ------------------------------------------------------------------ *)
-  let bindclass ?(import = EcTheory.import0) (scope : scope) (x, tc) =
+  let exit ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) =
     assert (scope.sc_pr_uc = None);
-    let item = EcTheory.mkitem import (EcTheory.Th_typeclass(x, tc)) in
-    { scope with sc_env = EcSection.add_item item scope.sc_env }
+
+    let cth = exit_r ~pempty (add_clears clears scope) in
+    let ((cth, required), (name, _), scope) = cth in
+    let scope = List.fold_right require_loaded required scope in
+    let scope = ofold (fun cth scope -> bind scope cth) scope cth in
+    (name, scope)
 
   (* ------------------------------------------------------------------ *)
-  let add_class (scope : scope) { pl_desc = tcd } =
-    assert (scope.sc_pr_uc = None);
-    let lc = tcd.ptc_loca in
-    let name  = unloc tcd.ptc_name in
-    let scenv = (env scope) in
+  let bump_prelude (scope : scope) =
+    match scope.sc_prelude with
+    | `InPrelude, _ ->
+         { scope with sc_prelude = (`InPrelude,
+             { pr_env      = env scope;
+               pr_required = scope.sc_required; }) }
+    | _ -> scope
 
-    check_name_available scope tcd.ptc_name;
+  (* ------------------------------------------------------------------ *)
+  let import (scope : scope) (name : qsymbol) =
+    assert (scope.sc_pr_uc = None);
 
-    let tclass =
-      let uptc =
-        tcd.ptc_inth |> omap
-          (fun { pl_loc = uploc; pl_desc = uptc } ->
-            match EcEnv.TypeClass.lookup_opt uptc scenv with
-            | None -> hierror ~loc:uploc "unknown type-class: `%s'"
-                        (string_of_qsymbol uptc)
-            | Some (tcp, _) -> tcp)
-      in
+    match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with
+    | None ->
+        hierror
+          "cannot import the non-existent theory `%s'"
+          (string_of_qsymbol name)
 
-      let asty  =
-        let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in
-          { tyd_params  = [];
-            tyd_type    = `Abstract body;
-            tyd_loca    = (lc :> locality);
-            tyd_resolve = true;  } in
-      let scenv = EcEnv.Ty.bind name asty scenv in
+    | Some (path, cth) ->
+      if cth.cth_mode = `Abstract then
+        hierror "cannot import an abstract theory";
+      bump_prelude
+        { scope with
+          sc_env = EcSection.import path scope.sc_env }
 
-      (* Check for duplicated field names *)
-      Msym.odup unloc (List.map fst tcd.ptc_ops)
-        |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc
-                    "duplicated operator name: `%s'" x.pl_desc);
-      Msym.odup unloc (List.map fst tcd.ptc_axs)
-        |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc
-                    "duplicated axiom name: `%s'" x.pl_desc);
+  (* ------------------------------------------------------------------ *)
+  let export_p scope (p, lc) =
+    let item = mkitem EcTheory.import0 (EcTheory.Th_export (p, lc)) in
+    { scope with sc_env = EcSection.add_item item scope.sc_env }
 
-      (* Check operators types *)
-      let operators =
-        let check1 (x, ty) =
-          let ue = EcUnify.UniEnv.create (Some []) in
-          let ty = transty tp_tydecl scenv ue ty in
-          let uidmap = EcUnify.UniEnv.close ue in
-          let ty = ty_subst (Tuni.subst uidmap) ty in
-            (EcIdent.create (unloc x), ty)
-        in
-          tcd.ptc_ops |> List.map check1 in
+  let export (scope : scope) (name : qsymbol) =
+    assert (scope.sc_pr_uc = None);
 
-      (* Check axioms *)
-      let axioms =
-        let scenv = EcEnv.Var.bind_locals operators scenv in
-        let check1 (x, ax) =
-          let ue = EcUnify.UniEnv.create (Some []) in
-          let ax = trans_prop scenv ue ax in
-          let uidmap = EcUnify.UniEnv.close ue in
-          let fs = Tuni.subst uidmap in
-          let ax = Fsubst.f_subst fs ax in
-            (unloc x, ax)
-        in
-          tcd.ptc_axs |> List.map check1 in
+    match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with
+    | None ->
+        hierror
+          "cannot export the non-existent theory `%s'"
+          (string_of_qsymbol name)
 
-      (* Construct actual type-class *)
-      { tc_prt = uptc; tc_ops = operators; tc_axs = axioms; tc_loca = lc}
-    in
-      bindclass scope (name, tclass)
+    | Some (path, cth) ->
+      if cth.cth_mode = `Abstract then
+        hierror "cannot export an abstract theory";
+      (* The section will fix the locality *)
+      bump_prelude (export_p scope (path, `Global))
 
   (* ------------------------------------------------------------------ *)
-  let check_tci_operators env tcty ops reqs =
-    let ue   = EcUnify.UniEnv.create (Some (fst tcty)) in
-    let rmap = Mstr.of_list reqs in
+  let check_end_required scope thname =
+    if fst scope.sc_name <> thname then
+      hierror "end-of-file while processing external theory %s %s"
+        (fst scope.sc_name) thname;
+    if scope.sc_pr_uc <> None then
+      hierror
+        "end-of-file while processing proof %s" (fst scope.sc_name)
 
-    let ops =
-      let tt1 m (x, (tvi, op)) =
-        if not (Mstr.mem (unloc x) rmap) then
-          hierror ~loc:x.pl_loc "invalid operator name: `%s'" (unloc x);
+  (* -------------------------------------------------------------------- *)
+  let require (scope : scope) ((name, mode) : required_info * thmode) loader =
+    assert (scope.sc_pr_uc = None);
 
-        let tvi = List.map (TT.transty tp_tydecl env ue) tvi in
-        let selected =
-          EcUnify.select_op ~filter:(fun _ -> EcDecl.is_oper)
-            (Some (EcUnify.TVIunamed tvi)) env (unloc op) ue ([], None)
-        in
-        let op =
-          match selected with
-          | [] -> hierror ~loc:op.pl_loc "unknown operator"
-          | op1::op2::_ ->
-              hierror ~loc:op.pl_loc
-                "ambiguous operator (%s / %s)"
-                (EcPath.tostring (fst (proj4_1 op1)))
-                (EcPath.tostring (fst (proj4_1 op2)))
-          | [((p, _), _, _, _)] ->
-              let op   = EcEnv.Op.by_path p env in
-              let opty =
-                Tvar.subst
-                  (Tvar.init (List.map fst op.op_tparams) tvi)
-                  op.op_ty
-              in
-                (p, opty)
-
-        in
-          Mstr.change
-            (function
-            | None   -> Some (x.pl_loc, op)
-            | Some _ -> hierror ~loc:(x.pl_loc)
-              "duplicated operator name: `%s'" (unloc x))
-            (unloc x) m
-      in
-        List.fold_left tt1 Mstr.empty ops
-    in
-      List.iter
-        (fun (x, (req, _)) ->
-           if req && not (Mstr.mem x ops) then
-             hierror "no definition for operator `%s'" x)
-        reqs;
-      List.fold_left
-        (fun m (x, (_, ty)) ->
-           match Mstr.find_opt x ops with
-           | None -> m
-           | Some (loc, (p, opty)) ->
-               if not (EcReduction.EqTest.for_type env ty opty) then
-                 hierror ~loc "invalid type for operator `%s'" x;
-               Mstr.add x p m)
-        Mstr.empty reqs
+    if required scope name then begin
+      if   name.rqd_direct
+      then mark_as_direct scope name.rqd_name
+      else scope
+    end else
+      match Msym.find_opt name.rqd_name scope.sc_loaded with
+      | Some _ -> require_loaded name scope
 
-  (* ------------------------------------------------------------------ *)
-  let check_tci_axioms scope mode axs reqs lc =
-    let rmap = Mstr.of_list reqs in
-    let symbs, axs =
-      List.map_fold
-        (fun m (x, t) ->
-          if not (Mstr.mem (unloc x) rmap) then
-            hierror ~loc:x.pl_loc "invalid axiom name: `%s'" (unloc x);
-          if Sstr.mem (unloc x) m then
-            hierror ~loc:(x.pl_loc) "duplicated axiom name: `%s'" (unloc x);
-          (Sstr.add (unloc x) m, (unloc x, t, Mstr.find (unloc x) rmap)))
-        Sstr.empty axs in
+      | None ->
+        try
+          let imported = enter (for_loading scope) mode name.rqd_name `Global in
+          let imported = { imported with sc_env = EcSection.astop imported.sc_env } in
+          let thname   = fst imported.sc_name in
+          let imported = loader imported in
 
-    let interactive =
-      List.pmap
-        (fun (x, req) ->
-           if not (Mstr.mem x symbs) then
-             let ax = {
-               ax_tparams    = [];
-               ax_spec       = req;
-               ax_kind       = `Lemma;
-               ax_loca       = lc;
-               ax_visibility = `NoSmt;
-             } in Some ((None, ax), EcPath.psymbol x, scope.sc_env)
-           else None)
-        reqs in
-      List.iter
-        (fun (x, pt, f) ->
-          let x  = "$" ^ x in
-          let t  = { pt_core = pt; pt_intros = []; } in
-          let t  = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]) } in
-          let t  = { pt_core = t; pt_intros = []; } in
-          let ax = {
-              ax_tparams    = [];
-              ax_spec       = f;
-              ax_kind       = `Lemma;
-              ax_visibility = `NoSmt;
-              ax_loca       = lc;
-          } in
+          check_end_required imported thname;
 
-          let pucflags = { puc_visibility = `Visible; puc_local = false; } in
-          let pucflags = (([], None), pucflags) in
-          let check    = Check_mode.check scope.sc_options in
+          let cth = exit_r ~pempty:`No imported in
+          let (cth, rqs), (name1, _), imported = cth in
+          assert (name.rqd_name = name1);
+          let scope = { scope with sc_loaded =
+            Msym.add name.rqd_name (oget cth, rqs) imported.sc_loaded; } in
 
-          let escope = scope in
-          let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in
-          let escope = Tactics.proof escope in
-          let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in
-            ignore (Ax.save_r escope))
-        axs;
-      interactive
+          bump_prelude (require_loaded name scope)
 
-  (* ------------------------------------------------------------------ *)
-  (* FIXME section: those path does not exists ...
-     futhermode Ring.ZModule is an abstract theory *)
-  let p_zmod    = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ZModule"], "zmodule")
-  let p_ring    = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ComRing"], "ring"   )
-  let p_idomain = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "IDomain"], "idomain")
-  let p_field   = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "Field"  ], "field"  )
+        with e -> begin
+          match toperror_of_exn_r e with
+          | Some (l, e) when not (EcLocation.isdummy l) ->
+              raise (ImportError (Some l, name.rqd_name, e))
+          | _ ->
+              raise (ImportError (None, name.rqd_name, e))
+        end
 
-  (* ------------------------------------------------------------------ *)
-  let ring_of_symmap env ty kind symbols =
-    { r_type  = ty;
-      r_zero  = oget (Mstr.find_opt "rzero" symbols);
-      r_one   = oget (Mstr.find_opt "rone"  symbols);
-      r_add   = oget (Mstr.find_opt "add"   symbols);
-      r_opp   =      (Mstr.find_opt "opp"   symbols);
-      r_mul   = oget (Mstr.find_opt "mul"   symbols);
-      r_exp   =      (Mstr.find_opt "expr"  symbols);
-      r_sub   =      (Mstr.find_opt "sub"   symbols);
-      r_kind  = kind;
-      r_embed =
-        (match Mstr.find_opt "ofint" symbols with
-         | None when EcReduction.EqTest.for_type env ty tint -> `Direct
-         | None -> `Default | Some p -> `Embed p); }
+  let required scope = scope.sc_required
+end
 
-  let addring ~import (scope : scope) mode (kind, { pl_desc = tci; pl_loc = loc }) =
-    let env = env scope in
-    if not (EcAlgTactic.is_module_loaded env) then
-      hierror "load AlgTactic/Ring first";
+(* -------------------------------------------------------------------- *)
+module Section = struct
+  module T = EcTheory
 
-    let ty =
-      let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in
-      let ty = transty tp_tydecl env ue (snd tci.pti_type) in
-      assert (EcUnify.UniEnv.closed ue);
-      let uidmap = EcUnify.UniEnv.close ue in
-        (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty)
-    in
-    if not (List.is_empty (fst ty)) then
-      hierror "ring instances cannot be polymorphic";
+  let enter (scope : scope) (name : psymbol option) =
+    assert (scope.sc_pr_uc = None);
+    { scope with
+      sc_env = EcSection.enter_section (omap unloc name) scope.sc_env }
 
-    let symbols = EcAlgTactic.ring_symbols env kind (snd ty) in
-    let symbols = check_tci_operators env ty tci.pti_ops symbols in
-    let cr      = ring_of_symmap env (snd ty) kind symbols in
-    let axioms  = EcAlgTactic.ring_axioms env cr in
-    let lc      = (tci.pti_loca :> locality) in
-    let inter   = check_tci_axioms scope mode tci.pti_axs axioms lc in
-    let add env p =
-      let item = EcTheory.Th_instance (ty,`General p, tci.pti_loca) in
-      let item = EcTheory.mkitem import item in
-      EcSection.add_item item env in
+  let exit (scope : scope) (name : psymbol option) =
+    let sc_env = EcSection.exit_section (omap unloc name) scope.sc_env in
+    { scope with sc_env }
+end
 
-    let scope   =
-      { scope with sc_env =
-          List.fold_left add
-            (let item =
-               EcTheory.Th_instance (([], snd ty), `Ring cr, tci.pti_loca) in
-             let item = EcTheory.mkitem import item in
-             EcSection.add_item item scope.sc_env)
-            [p_zmod; p_ring; p_idomain] }
+(* -------------------------------------------------------------------- *)
+module Reduction = struct
+  (* FIXME: section -> allow "local" flag *)
+  let add_reduction scope (opts, reds) =
+    check_state `InTop "hint simplify" scope;
 
-    in Ax.add_defer scope inter
+    let rules =
+      let for1 idx name =
+        let idx  = odfl 0 idx in
+        let ax_p = EcEnv.Ax.lookup_path (unloc name) (env scope) in
+        let opts = EcTheory.{
+          ur_delta  = List.mem `Delta  opts;
+          ur_eqtrue = List.mem `EqTrue opts;
+        } in
 
-  (* ------------------------------------------------------------------ *)
-  let field_of_symmap env ty symbols =
-    { f_ring = ring_of_symmap env ty `Integer symbols;
-      f_inv  = oget (Mstr.find_opt "inv" symbols);
-      f_div  = Mstr.find_opt "div" symbols; }
+        let red_info =
+          EcReduction.User.compile ~opts ~prio:idx (env scope) ax_p in
+        (ax_p, opts, Some red_info) in
 
-  let addfield ~import (scope : scope) mode { pl_desc = tci; pl_loc = loc; } =
-    let env = env scope in
-    if not (EcAlgTactic.is_module_loaded env) then
-      hierror "load AlgTactic/Ring first";
+      let rules = List.map (fun (xs, idx) -> List.map (for1 idx) xs) reds in
+      List.flatten rules
 
-    let ty =
-      let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in
-      let ty = transty tp_tydecl env ue (snd tci.pti_type) in
-      assert (EcUnify.UniEnv.closed ue);
-      let uidmap = EcUnify.UniEnv.close ue in
-        (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty)
     in
-    if not (List.is_empty (fst ty)) then
-      hierror "field instances cannot be polymorphic";
-    let symbols = EcAlgTactic.field_symbols env (snd ty) in
-    let symbols = check_tci_operators env ty tci.pti_ops symbols in
-    let cr      = field_of_symmap env (snd ty) symbols in
-    let axioms  = EcAlgTactic.field_axioms env cr in
-    let lc      = (tci.pti_loca :> locality) in
-    let inter   = check_tci_axioms scope mode tci.pti_axs axioms lc; in
-    let add env p =
-      let item = EcTheory.Th_instance(ty,`General p, tci.pti_loca) in
-      let item = EcTheory.mkitem import item in
-      EcSection.add_item item env in
-    let scope   =
-      { scope with
-        sc_env =
-          List.fold_left add
-            (let item =
-               EcTheory.Th_instance (([], snd ty), `Field cr, tci.pti_loca) in
-             let item = EcTheory.mkitem import item in
-              EcSection.add_item item scope.sc_env)
-            [p_zmod; p_ring; p_idomain; p_field] }
 
-    in Ax.add_defer scope inter
+    let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_reduction rules) in
+    { scope with sc_env = EcSection.add_item item scope.sc_env }
+end
 
+(* -------------------------------------------------------------------- *)
+module Cloning = struct
   (* ------------------------------------------------------------------ *)
-  let symbols_of_tc (_env : EcEnv.env) ty (tcp, tc) =
-    let subst = EcSubst.add_tydef EcSubst.empty tcp ([], ty) in
-      List.map (fun (x, opty) ->
-        (EcIdent.name x, (true, EcSubst.subst_ty subst opty)))
-        tc.tc_ops
+  open EcTheory
+  open EcThCloning
+
+  module C = EcThCloning
+  module R = EcTheoryReplay
 
-(*
   (* ------------------------------------------------------------------ *)
-  let add_generic_tc (scope : scope) _mode { pl_desc = tci; pl_loc = loc; } =
-    let ty =
-      let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
-      let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
-        assert (EcUnify.UniEnv.closed ue);
-        (EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
-    in
+  let hooks : scope R.ovrhooks =
+    let thexit sc pempty = snd (Theory.exit ?clears:None ~pempty sc) in
+    let add_item scope import item =
+      let item = EcTheory.mkitem import item in
+      { scope with sc_env = EcSection.add_item item scope.sc_env } in
+    { R.henv      = (fun scope -> scope.sc_env);
+      R.hadd_item = add_item;
+      R.hthenter  = Theory.enter;
+      R.hthexit   = thexit;
+      R.herr      = (fun ?loc -> hierror ?loc "%s"); }
 
-    let (tcp, tc) =
-      match EcEnv.TypeClass.lookup_opt (unloc tci.pti_name) (env scope) with
+  (* ------------------------------------------------------------------ *)
+  module Options = struct
+    open EcTheoryReplay
+
+    let default = { clo_abstract = false; }
+
+    let merge1 opts (b, (x : theory_cloning_option)) =
+      match x with
+      | `Abstract -> { opts with clo_abstract = b; }
+
+    let merge opts (specs : theory_cloning_options) =
+      List.fold_left merge1 opts specs
+  end
+
+
+  (* ------------------------------------------------------------------ *)
+  let replay_proofs (scope : scope) (mode : Tactics.proofmode) (proofs : _) =
+    proofs |> List.pmap (fun axc ->
+      match axc.C.axc_tac with
       | None ->
-          hierror ~loc:tci.pti_name.pl_loc
-            "unknown type-class: %s" (string_of_qsymbol (unloc tci.pti_name))
-      | Some tc -> tc
-    in
+          Some (fst_map some axc.C.axc_axiom, axc.C.axc_path, axc.C.axc_env)
 
-    let  symbols = symbols_of_tc scope.sc_env (snd ty) (tcp, tc) in
-    let _symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in
+      | Some pt ->
+          let t = { pt_core = pt; pt_intros = []; } in
+          let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in
+          let t = { pt_core = t; pt_intros = []; } in
+          let (x, ax) = axc.C.axc_axiom in
 
-    { scope with
-        sc_env = EcEnv.TypeClass.add_instance ty (`General tcp) scope.sc_env }
+          let pucflags = { puc_visibility = `Visible; puc_local = false; } in
+          let pucflags = (([], None), pucflags) in
+          let check    = Check_mode.check scope.sc_options in
 
-(*
-          let ue = EcUnify.UniEnv.create (Some []) in
-          let ty = fst (EcUnify.UniEnv.openty ue (fst ty) None (snd ty)) in
-            try  EcUnify.hastc scope.sc_env ue ty (Sp.singleton (fst tc)); tc
-            with EcUnify.UnificationFailure _ ->
-              hierror "type must be an instance of `%s'" (EcPath.tostring (fst tc))
-*)
-*)
+          let escope = { scope with sc_env = axc.C.axc_env; } in
+          let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in
+          let escope = Tactics.proof escope in
+          let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in
+          ignore (Ax.save_r escope); None
+    )
 
   (* ------------------------------------------------------------------ *)
-  let add_instance
-    ?(import = EcTheory.import0) (scope : scope) mode ({ pl_desc = tci } as toptci)
-  =
-    match unloc tci.pti_name with
-    | ([], "bring") -> begin
-        if EcUtils.is_some tci.pti_args then
-          hierror "unsupported-option";
-        addring ~import scope mode (`Boolean, toptci)
-    end
+  let clone (scope : scope) mode (thcl : theory_cloning) =
+    assert (scope.sc_pr_uc = None);
 
-    | ([], "ring") -> begin
-      let kind =
-        match tci.pti_args with
-        | None -> `Integer
-        | Some (`Ring (c, p)) ->
-            if odfl false (c |> omap (fun c -> c <^ BI.of_int 2)) then
-              hierror "invalid coefficient modulus";
-            if odfl false (p |> omap (fun p -> p <^ BI.of_int 2)) then
-              hierror "invalid power modulus";
-            if      opt_equal BI.equal c (Some (BI.of_int 2))
-                 && opt_equal BI.equal p (Some (BI.of_int 2))
-            then `Boolean
-            else `Modulus (c, p)
-      in addring ~import scope mode (kind, toptci)
-    end
+    let { cl_name   = name;
+          cl_theory = (opath, oth);
+          cl_clone  = ovrds;
+          cl_rename = rnms;
+          cl_ntclr  = ntclr; }
 
-    | ([], "field") -> addfield ~import scope mode toptci
+        = C.clone scope.sc_env thcl in
+
+    let incl  = thcl.pthc_import = Some `Include in
+    let opts  = Options.merge Options.default thcl.pthc_opts in
+
+    if thcl.pthc_import = Some `Include && opts.R.clo_abstract then
+      hierror "cannot include an abstract theory";
+    if thcl.pthc_import = Some `Include && EcUtils.is_some thcl.pthc_name then
+      hierror "cannot give an alias to an included clone";
+
+    let cpath = EcEnv.root (env scope) in
+    let npath = if incl then cpath else EcPath.pqname cpath name in
+
+    let (proofs, scope) =
+      EcTheoryReplay.replay hooks
+        ~abstract:opts.R.clo_abstract ~local:thcl.pthc_local ~incl
+        ~clears:ntclr ~renames:rnms ~opath ~npath ovrds
+        scope (name, oth.cth_items)
+    in
+
+    let proofs = replay_proofs scope mode proofs in
+
+    let scope =
+      thcl.pthc_import |> ofold (fun flag scope ->
+        match flag with
+        | `Import  ->
+          { scope with sc_env = EcSection.import npath scope.sc_env; }
+        | `Export  ->
+          let item = EcTheory.mkitem EcTheory.import0 (Th_export (npath, `Global)) in
+          { scope with sc_env = EcSection.add_item item scope.sc_env; }
+        | `Include -> scope)
+        scope
+
+    in Ax.add_defer scope proofs
 
-    | _ ->
-        if EcUtils.is_some tci.pti_args then
-          hierror "unsupported-option";
-        failwith "unsupported"          (* FIXME *)
 end
 
 (* -------------------------------------------------------------------- *)
-module Theory = struct
-  open EcTheory
-
-  exception TopScope
+module Ty = struct
+  open EcDecl
+  open EcTyping
 
-  (* ------------------------------------------------------------------ *)
-  let bind (scope : scope) (cth : thloaded) =
-    assert (scope.sc_pr_uc = None);
-    { scope with
-        sc_env = EcSection.add_th ~import:EcTheory.import0 cth scope.sc_env }
+  module TT  = EcTyping
+  module ELI = EcInductive
+  module EHI = EcHiInductive
 
   (* ------------------------------------------------------------------ *)
-  let required (scope : scope) (name : required_info) =
-    assert (scope.sc_pr_uc = None);
-    List.exists (fun x ->
-        if x.rqd_name = name.rqd_name then (
-          (* FIXME: raise an error message *)
-          assert (x.rqd_digest = name.rqd_digest);
-          true)
-        else false)
-      scope.sc_required
+  let check_name_available scope x =
+    let pname = EcPath.pqname (EcEnv.root (env scope)) x.pl_desc in
 
-  (* ------------------------------------------------------------------ *)
-  let mark_as_direct (scope : scope) (name : symbol) =
-    let for1 rq =
-      if   rq.rqd_name = name
-      then { rq with rqd_direct = true }
-      else rq
-    in { scope with sc_required = List.map for1 scope.sc_required }
+    if    EcEnv.Ty       .by_path_opt pname (env scope) <> None
+       || EcEnv.TypeClass.by_path_opt pname (env scope) <> None then
+      hierror ~loc:x.pl_loc "duplicated type/type-class name `%s'" x.pl_desc
 
   (* ------------------------------------------------------------------ *)
-  let enter (scope : scope) (mode : thmode) (name : symbol) =
+  let bind ?(import = EcTheory.import0) (scope : scope) ((x, tydecl) : (_ * tydecl)) =
     assert (scope.sc_pr_uc = None);
-    subscope scope mode name
+    let item = EcTheory.mkitem import (EcTheory.Th_type (x, tydecl)) in
+    { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
-  let rec require_loaded (id : required_info) scope =
-    if required scope id then
-      scope
-    else
-      match Msym.find_opt id.rqd_name scope.sc_loaded with
-      | Some (rth, ids) ->
-          let scope = List.fold_right require_loaded ids scope in
-          let env   = EcSection.require rth scope.sc_env in
-            { scope with
-                sc_env      = env;
-                sc_required = id :: scope.sc_required; }
-
-      | None -> assert false
+  let add scope (tyd : ptydecl located) =
+    let loc = loc tyd in
 
-  (* ------------------------------------------------------------------ *)
-  let update_with_required ~(dst : scope) ~(src : scope) =
-    let dst =
-      let sc_loaded =
-        Msym.union
-          (fun _ x y -> assert (x ==(*phy*) y); Some x)
-          dst.sc_loaded src.sc_loaded
-      in { dst with sc_loaded }
-    in List.fold_right require_loaded src.sc_required dst
+    let { pty_name = name; pty_tyvars = args;
+          pty_body = body; pty_locality = tyd_loca } = unloc tyd in
 
-  (* ------------------------------------------------------------------ *)
-  let add_clears clears scope =
-    let clears =
-      let for1 = function
-        | None -> EcEnv.root (env scope)
-        | Some { pl_loc = loc; pl_desc = (xs, x) as q } ->
-          let xp = EcEnv.root (env scope) in
-          let xp = EcPath.pqname (EcPath.extend xp xs) x in
-          if is_none (EcEnv.Theory.by_path_opt xp (env scope)) then
-            hierror ~loc "unknown theory: `%s`" (string_of_qsymbol q);
-          xp
-      in List.map for1 clears
-    in { scope with sc_clears = scope.sc_clears @ clears }
+    check_name_available scope name;
+    let env = env scope in
+    let tyd_params, tyd_type =
+      match body with
+      | PTYD_Abstract tcs ->
+        let tcs =
+          List.map
+            (fun tc -> fst (EcEnv.TypeClass.lookup (unloc tc) env))
+            tcs  in
+        let ue = TT.transtyvars env (loc, Some args) in
+        EcUnify.UniEnv.tparams ue, `Abstract (Sp.of_list tcs)
 
-  (* -------------------------------------------------------------------- *)
-  let exit_r ?pempty (scope : scope) =
-    match scope.sc_top with
-    | None     -> raise TopScope
-    | Some sup ->
-      let clears   = scope.sc_clears in
-      let _, cth, _ = EcSection.exit_theory ?pempty ~clears scope.sc_env in
-      let loaded   = scope.sc_loaded in
-      let required = scope.sc_required in
-      let sup = { sup with sc_loaded = loaded; } in
-      ((cth, required), scope.sc_name, sup)
+      | PTYD_Alias    bd ->
+        let ue     = TT.transtyvars env (loc, Some args) in
+        let body   = transty tp_tydecl env ue bd in
+        EcUnify.UniEnv.tparams ue, `Concrete body
 
-  (* ------------------------------------------------------------------ *)
-  let exit ?(pempty = `ClearOnly) ?(clears =[]) (scope : scope) =
-    assert (scope.sc_pr_uc = None);
+      | PTYD_Datatype dt ->
+        let datatype = EHI.trans_datatype env (mk_loc loc (args,name)) dt in
+        let tparams, tydt =
+          try ELI.datatype_as_ty_dtype datatype
+          with ELI.NonPositive -> EHI.dterror loc env EHI.DTE_NonPositive
+        in
+        tparams, `Datatype tydt
 
-    let cth = exit_r ~pempty (add_clears clears scope) in
-    let ((cth, required), (name, _), scope) = cth in
-    let scope = List.fold_right require_loaded required scope in
-    let scope = ofold (fun cth scope -> bind scope cth) scope cth in
-    (name, scope)
+      | PTYD_Record rt ->
+        let record  = EHI.trans_record env (mk_loc loc (args,name)) rt in
+        let scheme  = ELI.indsc_of_record record in
+        record.ELI.rc_tparams, `Record (scheme, record.ELI.rc_fields)
+    in
 
-  (* ------------------------------------------------------------------ *)
-  let bump_prelude (scope : scope) =
-    match scope.sc_prelude with
-    | `InPrelude, _ ->
-         { scope with sc_prelude = (`InPrelude,
-             { pr_env      = env scope;
-               pr_required = scope.sc_required; }) }
-    | _ -> scope
+    bind scope (unloc name, { tyd_params; tyd_type; tyd_loca; tyd_resolve = true; })
 
   (* ------------------------------------------------------------------ *)
-  let import (scope : scope) (name : qsymbol) =
-    assert (scope.sc_pr_uc = None);
+  let add_subtype (scope : scope) ({ pl_desc = subtype } : psubtype located) =
+    let loced x = mk_loc _dummy x in
+    let env = env scope in
 
-    match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with
-    | None ->
-        hierror
-          "cannot import the non-existent theory `%s'"
-          (string_of_qsymbol name)
+    let scope =
+      let decl = EcDecl.{
+        tyd_params  = [];
+        tyd_type    = `Abstract Sp.empty;
+        tyd_loca    = `Global; (* FIXME:SUBTYPE *)
+        tyd_resolve = true;
+      } in bind scope (unloc subtype.pst_name, decl) in
+
+    let carrier =
+      let ue = EcUnify.UniEnv.create None in
+      transty tp_tydecl env ue subtype.pst_carrier in
+    
+    let pred =
+      let x = EcIdent.create (fst subtype.pst_pred).pl_desc in
+      let env = EcEnv.Var.bind_local x carrier env in
+      let ue = EcUnify.UniEnv.create None in
+      let pred = EcTyping.trans_prop env ue (snd subtype.pst_pred) in
+      if not (EcUnify.UniEnv.closed ue) then
+        hierror ~loc:(snd subtype.pst_pred).pl_loc 
+          "the predicate contains free type variables";
+      let uidmap = EcUnify.UniEnv.close ue in
+      let fs = Tuni.subst uidmap in
+      f_lambda [(x, GTty carrier)] (Fsubst.f_subst fs pred) in
+
+    let evclone =
+      { EcThCloning.evc_empty with
+          evc_types = Msym.of_list [
+            "T", loced (`Direct carrier, `Inline `Clear);
+            "sT", loced (
+              `ByPath (EcPath.pqname (EcEnv.root env) (unloc subtype.pst_name)),
+              `Inline `Clear
+            );
+          ];
+          evc_ops = Msym.of_list [
+            "P", loced (`Direct pred, `Inline `Clear)
+          ];
+          evc_lemmas = {
+            ev_bynames = Msym.empty;
+            ev_global  =  [ (None, Some [`Include, "prove"]) ]
+          } } in
+ 
+    let cname = Option.map unloc subtype.pst_cname in
+    let npath = ofold ((^~) EcPath.pqname) (EcEnv.root env) cname in
+    let cpath = EcPath.fromqsymbol ([EcCoreLib.i_top], "Subtype") in
+    let theory = EcEnv.Theory.by_path ~mode:`Abstract cpath env in
+      
+    let renames =
+      match subtype.pst_rename with
+      | None -> []
+
+      | Some (insub, val_) -> [
+        (`All, (EcRegexp.regexp "val", EcRegexp.subst val_));
+        (`All, (EcRegexp.regexp "insub", EcRegexp.subst insub));
+      ] in
 
-    | Some (path, cth) ->
-      if cth.cth_mode = `Abstract then
-        hierror "cannot import an abstract theory";
-      bump_prelude
-        { scope with
-          sc_env = EcSection.import path scope.sc_env }
+    let (proofs, scope) =
+      EcTheoryReplay.replay Cloning.hooks
+        ~abstract:false ~local:`Global ~incl:(Option.is_none cname)
+        ~clears:Sp.empty ~renames ~opath:cpath ~npath
+        evclone scope
+        (
+          Option.value ~default:(EcPath.basename cpath) cname,
+          theory.cth_items
+        ) in
+
+    let proofs = Cloning.replay_proofs scope `Check proofs in
+    
+    Ax.add_defer scope proofs
 
   (* ------------------------------------------------------------------ *)
-  let export_p scope (p, lc) =
-    let item = mkitem EcTheory.import0 (EcTheory.Th_export (p, lc)) in
-    { scope with sc_env = EcSection.add_item item scope.sc_env }
-
-  let export (scope : scope) (name : qsymbol) =
+  let bindclass ?(import = EcTheory.import0) (scope : scope) (x, tc) =
     assert (scope.sc_pr_uc = None);
-
-    match EcEnv.Theory.lookup_opt ~mode:`All name (env scope) with
-    | None ->
-        hierror
-          "cannot export the non-existent theory `%s'"
-          (string_of_qsymbol name)
-
-    | Some (path, cth) ->
-      if cth.cth_mode = `Abstract then
-        hierror "cannot export an abstract theory";
-      (* The section will fix the locality *)
-      bump_prelude (export_p scope (path, `Global))
+    let item = EcTheory.mkitem import (EcTheory.Th_typeclass(x, tc)) in
+    { scope with sc_env = EcSection.add_item item scope.sc_env }
 
   (* ------------------------------------------------------------------ *)
-  let check_end_required scope thname =
-    if fst scope.sc_name <> thname then
-      hierror "end-of-file while processing external theory %s %s"
-        (fst scope.sc_name) thname;
-    if scope.sc_pr_uc <> None then
-      hierror
-        "end-of-file while processing proof %s" (fst scope.sc_name)
-
-  (* -------------------------------------------------------------------- *)
-  let require (scope : scope) ((name, mode) : required_info * thmode) loader =
+  let add_class (scope : scope) { pl_desc = tcd } =
     assert (scope.sc_pr_uc = None);
+    let lc = tcd.ptc_loca in
+    let name  = unloc tcd.ptc_name in
+    let scenv = (env scope) in
 
-    if required scope name then begin
-      if   name.rqd_direct
-      then mark_as_direct scope name.rqd_name
-      else scope
-    end else
-      match Msym.find_opt name.rqd_name scope.sc_loaded with
-      | Some _ -> require_loaded name scope
-
-      | None ->
-        try
-          let imported = enter (for_loading scope) mode name.rqd_name `Global in
-          let imported = { imported with sc_env = EcSection.astop imported.sc_env } in
-          let thname   = fst imported.sc_name in
-          let imported = loader imported in
+    check_name_available scope tcd.ptc_name;
 
-          check_end_required imported thname;
+    let tclass =
+      let uptc =
+        tcd.ptc_inth |> omap
+          (fun { pl_loc = uploc; pl_desc = uptc } ->
+            match EcEnv.TypeClass.lookup_opt uptc scenv with
+            | None -> hierror ~loc:uploc "unknown type-class: `%s'"
+                        (string_of_qsymbol uptc)
+            | Some (tcp, _) -> tcp)
+      in
 
-          let cth = exit_r ~pempty:`No imported in
-          let (cth, rqs), (name1, _), imported = cth in
-          assert (name.rqd_name = name1);
-          let scope = { scope with sc_loaded =
-            Msym.add name.rqd_name (oget cth, rqs) imported.sc_loaded; } in
+      let asty  =
+        let body = ofold (fun p tc -> Sp.add p tc) Sp.empty uptc in
+          { tyd_params  = [];
+            tyd_type    = `Abstract body;
+            tyd_loca    = (lc :> locality);
+            tyd_resolve = true;  } in
+      let scenv = EcEnv.Ty.bind name asty scenv in
 
-          bump_prelude (require_loaded name scope)
+      (* Check for duplicated field names *)
+      Msym.odup unloc (List.map fst tcd.ptc_ops)
+        |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc
+                    "duplicated operator name: `%s'" x.pl_desc);
+      Msym.odup unloc (List.map fst tcd.ptc_axs)
+        |> oiter (fun (x, y) -> hierror ~loc:y.pl_loc
+                    "duplicated axiom name: `%s'" x.pl_desc);
 
-        with e -> begin
-          match toperror_of_exn_r e with
-          | Some (l, e) when not (EcLocation.isdummy l) ->
-              raise (ImportError (Some l, name.rqd_name, e))
-          | _ ->
-              raise (ImportError (None, name.rqd_name, e))
-        end
+      (* Check operators types *)
+      let operators =
+        let check1 (x, ty) =
+          let ue = EcUnify.UniEnv.create (Some []) in
+          let ty = transty tp_tydecl scenv ue ty in
+          let uidmap = EcUnify.UniEnv.close ue in
+          let ty = ty_subst (Tuni.subst uidmap) ty in
+            (EcIdent.create (unloc x), ty)
+        in
+          tcd.ptc_ops |> List.map check1 in
 
-  let required scope = scope.sc_required
-end
+      (* Check axioms *)
+      let axioms =
+        let scenv = EcEnv.Var.bind_locals operators scenv in
+        let check1 (x, ax) =
+          let ue = EcUnify.UniEnv.create (Some []) in
+          let ax = trans_prop scenv ue ax in
+          let uidmap = EcUnify.UniEnv.close ue in
+          let fs = Tuni.subst uidmap in
+          let ax = Fsubst.f_subst fs ax in
+            (unloc x, ax)
+        in
+          tcd.ptc_axs |> List.map check1 in
 
-(* -------------------------------------------------------------------- *)
-module Section = struct
-  module T = EcTheory
+      (* Construct actual type-class *)
+      { tc_prt = uptc; tc_ops = operators; tc_axs = axioms; tc_loca = lc}
+    in
+      bindclass scope (name, tclass)
 
-  let enter (scope : scope) (name : psymbol option) =
-    assert (scope.sc_pr_uc = None);
-    { scope with
-      sc_env = EcSection.enter_section (omap unloc name) scope.sc_env }
+  (* ------------------------------------------------------------------ *)
+  let check_tci_operators env tcty ops reqs =
+    let ue   = EcUnify.UniEnv.create (Some (fst tcty)) in
+    let rmap = Mstr.of_list reqs in
 
-  let exit (scope : scope) (name : psymbol option) =
-    let sc_env = EcSection.exit_section (omap unloc name) scope.sc_env in
-    { scope with sc_env }
-end
+    let ops =
+      let tt1 m (x, (tvi, op)) =
+        if not (Mstr.mem (unloc x) rmap) then
+          hierror ~loc:x.pl_loc "invalid operator name: `%s'" (unloc x);
 
-(* -------------------------------------------------------------------- *)
-module Reduction = struct
-  (* FIXME: section -> allow "local" flag *)
-  let add_reduction scope (opts, reds) =
-    check_state `InTop "hint simplify" scope;
+        let tvi = List.map (TT.transty tp_tydecl env ue) tvi in
+        let selected =
+          EcUnify.select_op ~filter:(fun _ -> EcDecl.is_oper)
+            (Some (EcUnify.TVIunamed tvi)) env (unloc op) ue ([], None)
+        in
+        let op =
+          match selected with
+          | [] -> hierror ~loc:op.pl_loc "unknown operator"
+          | op1::op2::_ ->
+              hierror ~loc:op.pl_loc
+                "ambiguous operator (%s / %s)"
+                (EcPath.tostring (fst (proj4_1 op1)))
+                (EcPath.tostring (fst (proj4_1 op2)))
+          | [((p, _), _, _, _)] ->
+              let op   = EcEnv.Op.by_path p env in
+              let opty =
+                Tvar.subst
+                  (Tvar.init (List.map fst op.op_tparams) tvi)
+                  op.op_ty
+              in
+                (p, opty)
 
-    let rules =
-      let for1 idx name =
-        let idx  = odfl 0 idx in
-        let ax_p = EcEnv.Ax.lookup_path (unloc name) (env scope) in
-        let opts = EcTheory.{
-          ur_delta  = List.mem `Delta  opts;
-          ur_eqtrue = List.mem `EqTrue opts;
-        } in
+        in
+          Mstr.change
+            (function
+            | None   -> Some (x.pl_loc, op)
+            | Some _ -> hierror ~loc:(x.pl_loc)
+              "duplicated operator name: `%s'" (unloc x))
+            (unloc x) m
+      in
+        List.fold_left tt1 Mstr.empty ops
+    in
+      List.iter
+        (fun (x, (req, _)) ->
+           if req && not (Mstr.mem x ops) then
+             hierror "no definition for operator `%s'" x)
+        reqs;
+      List.fold_left
+        (fun m (x, (_, ty)) ->
+           match Mstr.find_opt x ops with
+           | None -> m
+           | Some (loc, (p, opty)) ->
+               if not (EcReduction.EqTest.for_type env ty opty) then
+                 hierror ~loc "invalid type for operator `%s'" x;
+               Mstr.add x p m)
+        Mstr.empty reqs
 
-        let red_info =
-          EcReduction.User.compile ~opts ~prio:idx (env scope) ax_p in
-        (ax_p, opts, Some red_info) in
+  (* ------------------------------------------------------------------ *)
+  let check_tci_axioms scope mode axs reqs lc =
+    let rmap = Mstr.of_list reqs in
+    let symbs, axs =
+      List.map_fold
+        (fun m (x, t) ->
+          if not (Mstr.mem (unloc x) rmap) then
+            hierror ~loc:x.pl_loc "invalid axiom name: `%s'" (unloc x);
+          if Sstr.mem (unloc x) m then
+            hierror ~loc:(x.pl_loc) "duplicated axiom name: `%s'" (unloc x);
+          (Sstr.add (unloc x) m, (unloc x, t, Mstr.find (unloc x) rmap)))
+        Sstr.empty axs in
 
-      let rules = List.map (fun (xs, idx) -> List.map (for1 idx) xs) reds in
-      List.flatten rules
+    let interactive =
+      List.pmap
+        (fun (x, req) ->
+           if not (Mstr.mem x symbs) then
+             let ax = {
+               ax_tparams    = [];
+               ax_spec       = req;
+               ax_kind       = `Lemma;
+               ax_loca       = lc;
+               ax_visibility = `NoSmt;
+             } in Some ((None, ax), EcPath.psymbol x, scope.sc_env)
+           else None)
+        reqs in
+      List.iter
+        (fun (x, pt, f) ->
+          let x  = "$" ^ x in
+          let t  = { pt_core = pt; pt_intros = []; } in
+          let t  = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]) } in
+          let t  = { pt_core = t; pt_intros = []; } in
+          let ax = {
+              ax_tparams    = [];
+              ax_spec       = f;
+              ax_kind       = `Lemma;
+              ax_visibility = `NoSmt;
+              ax_loca       = lc;
+          } in
 
-    in
+          let pucflags = { puc_visibility = `Visible; puc_local = false; } in
+          let pucflags = (([], None), pucflags) in
+          let check    = Check_mode.check scope.sc_options in
 
-    let item = EcTheory.mkitem EcTheory.import0 (EcTheory.Th_reduction rules) in
-    { scope with sc_env = EcSection.add_item item scope.sc_env }
-end
+          let escope = scope in
+          let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in
+          let escope = Tactics.proof escope in
+          let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in
+            ignore (Ax.save_r escope))
+        axs;
+      interactive
 
-(* -------------------------------------------------------------------- *)
-module Cloning = struct
   (* ------------------------------------------------------------------ *)
-  open EcTheory
-  open EcThCloning
-
-  module C = EcThCloning
-  module R = EcTheoryReplay
+  (* FIXME section: those path does not exists ...
+     futhermode Ring.ZModule is an abstract theory *)
+  let p_zmod    = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ZModule"], "zmodule")
+  let p_ring    = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "ComRing"], "ring"   )
+  let p_idomain = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "IDomain"], "idomain")
+  let p_field   = EcPath.fromqsymbol ([EcCoreLib.i_top; "Ring"; "Field"  ], "field"  )
 
   (* ------------------------------------------------------------------ *)
-  let hooks : scope R.ovrhooks =
-    let thexit sc pempty = snd (Theory.exit ?clears:None ~pempty sc) in
-    let add_item scope import item =
-      let item = EcTheory.mkitem import item in
-      { scope with sc_env = EcSection.add_item item scope.sc_env } in
-    { R.henv      = (fun scope -> scope.sc_env);
-      R.hadd_item = add_item;
-      R.hthenter  = Theory.enter;
-      R.hthexit   = thexit;
-      R.herr      = (fun ?loc -> hierror ?loc "%s"); }
+  let ring_of_symmap env ty kind symbols =
+    { r_type  = ty;
+      r_zero  = oget (Mstr.find_opt "rzero" symbols);
+      r_one   = oget (Mstr.find_opt "rone"  symbols);
+      r_add   = oget (Mstr.find_opt "add"   symbols);
+      r_opp   =      (Mstr.find_opt "opp"   symbols);
+      r_mul   = oget (Mstr.find_opt "mul"   symbols);
+      r_exp   =      (Mstr.find_opt "expr"  symbols);
+      r_sub   =      (Mstr.find_opt "sub"   symbols);
+      r_kind  = kind;
+      r_embed =
+        (match Mstr.find_opt "ofint" symbols with
+         | None when EcReduction.EqTest.for_type env ty tint -> `Direct
+         | None -> `Default | Some p -> `Embed p); }
 
-  (* ------------------------------------------------------------------ *)
-  module Options = struct
-    open EcTheoryReplay
+  let addring ~import (scope : scope) mode (kind, { pl_desc = tci; pl_loc = loc }) =
+    let env = env scope in
+    if not (EcAlgTactic.is_module_loaded env) then
+      hierror "load AlgTactic/Ring first";
 
-    let default = { clo_abstract = false; }
+    let ty =
+      let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in
+      let ty = transty tp_tydecl env ue (snd tci.pti_type) in
+      assert (EcUnify.UniEnv.closed ue);
+      let uidmap = EcUnify.UniEnv.close ue in
+        (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty)
+    in
+    if not (List.is_empty (fst ty)) then
+      hierror "ring instances cannot be polymorphic";
 
-    let merge1 opts (b, (x : theory_cloning_option)) =
-      match x with
-      | `Abstract -> { opts with clo_abstract = b; }
+    let symbols = EcAlgTactic.ring_symbols env kind (snd ty) in
+    let symbols = check_tci_operators env ty tci.pti_ops symbols in
+    let cr      = ring_of_symmap env (snd ty) kind symbols in
+    let axioms  = EcAlgTactic.ring_axioms env cr in
+    let lc      = (tci.pti_loca :> locality) in
+    let inter   = check_tci_axioms scope mode tci.pti_axs axioms lc in
+    let add env p =
+      let item = EcTheory.Th_instance (ty,`General p, tci.pti_loca) in
+      let item = EcTheory.mkitem import item in
+      EcSection.add_item item env in
 
-    let merge opts (specs : theory_cloning_options) =
-      List.fold_left merge1 opts specs
-  end
+    let scope   =
+      { scope with sc_env =
+          List.fold_left add
+            (let item =
+               EcTheory.Th_instance (([], snd ty), `Ring cr, tci.pti_loca) in
+             let item = EcTheory.mkitem import item in
+             EcSection.add_item item scope.sc_env)
+            [p_zmod; p_ring; p_idomain] }
 
-  (* ------------------------------------------------------------------ *)
-  let clone (scope : scope) mode (thcl : theory_cloning) =
-    assert (scope.sc_pr_uc = None);
+    in Ax.add_defer scope inter
 
-    let { cl_name   = name;
-          cl_theory = (opath, oth);
-          cl_clone  = ovrds;
-          cl_rename = rnms;
-          cl_ntclr  = ntclr; }
+  (* ------------------------------------------------------------------ *)
+  let field_of_symmap env ty symbols =
+    { f_ring = ring_of_symmap env ty `Integer symbols;
+      f_inv  = oget (Mstr.find_opt "inv" symbols);
+      f_div  = Mstr.find_opt "div" symbols; }
 
-        = C.clone scope.sc_env thcl in
+  let addfield ~import (scope : scope) mode { pl_desc = tci; pl_loc = loc; } =
+    let env = env scope in
+    if not (EcAlgTactic.is_module_loaded env) then
+      hierror "load AlgTactic/Ring first";
 
-    let incl  = thcl.pthc_import = Some `Include in
-    let opts  = Options.merge Options.default thcl.pthc_opts in
+    let ty =
+      let ue = TT.transtyvars env (loc, Some (fst tci.pti_type)) in
+      let ty = transty tp_tydecl env ue (snd tci.pti_type) in
+      assert (EcUnify.UniEnv.closed ue);
+      let uidmap = EcUnify.UniEnv.close ue in
+        (EcUnify.UniEnv.tparams ue, ty_subst (Tuni.subst uidmap) ty)
+    in
+    if not (List.is_empty (fst ty)) then
+      hierror "field instances cannot be polymorphic";
+    let symbols = EcAlgTactic.field_symbols env (snd ty) in
+    let symbols = check_tci_operators env ty tci.pti_ops symbols in
+    let cr      = field_of_symmap env (snd ty) symbols in
+    let axioms  = EcAlgTactic.field_axioms env cr in
+    let lc      = (tci.pti_loca :> locality) in
+    let inter   = check_tci_axioms scope mode tci.pti_axs axioms lc; in
+    let add env p =
+      let item = EcTheory.Th_instance(ty,`General p, tci.pti_loca) in
+      let item = EcTheory.mkitem import item in
+      EcSection.add_item item env in
+    let scope   =
+      { scope with
+        sc_env =
+          List.fold_left add
+            (let item =
+               EcTheory.Th_instance (([], snd ty), `Field cr, tci.pti_loca) in
+             let item = EcTheory.mkitem import item in
+              EcSection.add_item item scope.sc_env)
+            [p_zmod; p_ring; p_idomain; p_field] }
 
-    if thcl.pthc_import = Some `Include && opts.R.clo_abstract then
-      hierror "cannot include an abstract theory";
-    if thcl.pthc_import = Some `Include && EcUtils.is_some thcl.pthc_name then
-      hierror "cannot give an alias to an included clone";
+    in Ax.add_defer scope inter
 
-    let cpath = EcEnv.root (env scope) in
-    let npath = if incl then cpath else EcPath.pqname cpath name in
+  (* ------------------------------------------------------------------ *)
+  let symbols_of_tc (_env : EcEnv.env) ty (tcp, tc) =
+    let subst = EcSubst.add_tydef EcSubst.empty tcp ([], ty) in
+      List.map (fun (x, opty) ->
+        (EcIdent.name x, (true, EcSubst.subst_ty subst opty)))
+        tc.tc_ops
 
-    let (proofs, scope) =
-      EcTheoryReplay.replay hooks
-        ~abstract:opts.R.clo_abstract ~local:thcl.pthc_local ~incl
-        ~clears:ntclr ~renames:rnms ~opath ~npath ovrds
-        scope (name, oth.cth_items)
+(*
+  (* ------------------------------------------------------------------ *)
+  let add_generic_tc (scope : scope) _mode { pl_desc = tci; pl_loc = loc; } =
+    let ty =
+      let ue = TT.transtyvars scope.sc_env (loc, Some (fst tci.pti_type)) in
+      let ty = transty tp_tydecl scope.sc_env ue (snd tci.pti_type) in
+        assert (EcUnify.UniEnv.closed ue);
+        (EcUnify.UniEnv.tparams ue, Tuni.offun (EcUnify.UniEnv.close ue) ty)
     in
 
-    let proofs = List.pmap (fun axc ->
-      match axc.C.axc_tac with
+    let (tcp, tc) =
+      match EcEnv.TypeClass.lookup_opt (unloc tci.pti_name) (env scope) with
       | None ->
-          Some (fst_map some axc.C.axc_axiom, axc.C.axc_path, axc.C.axc_env)
+          hierror ~loc:tci.pti_name.pl_loc
+            "unknown type-class: %s" (string_of_qsymbol (unloc tci.pti_name))
+      | Some tc -> tc
+    in
 
-      | Some pt ->
-          let t = { pt_core = pt; pt_intros = []; } in
-          let t = { pl_loc = pt.pl_loc; pl_desc = Pby (Some [t]); } in
-          let t = { pt_core = t; pt_intros = []; } in
-          let (x, ax) = axc.C.axc_axiom in
+    let  symbols = symbols_of_tc scope.sc_env (snd ty) (tcp, tc) in
+    let _symbols = check_tci_operators scope.sc_env ty tci.pti_ops symbols in
 
-          let pucflags = { puc_visibility = `Visible; puc_local = false; } in
-          let pucflags = (([], None), pucflags) in
-          let check    = Check_mode.check scope.sc_options in
+    { scope with
+        sc_env = EcEnv.TypeClass.add_instance ty (`General tcp) scope.sc_env }
 
-          let escope = { scope with sc_env = axc.C.axc_env; } in
-          let escope = Ax.start_lemma escope pucflags check ~name:x (ax, None) in
-          let escope = Tactics.proof escope in
-          let escope = snd (Tactics.process_r ~reloc:x false mode escope [t]) in
-            ignore (Ax.save_r escope); None)
-      proofs
-    in
+(*
+          let ue = EcUnify.UniEnv.create (Some []) in
+          let ty = fst (EcUnify.UniEnv.openty ue (fst ty) None (snd ty)) in
+            try  EcUnify.hastc scope.sc_env ue ty (Sp.singleton (fst tc)); tc
+            with EcUnify.UnificationFailure _ ->
+              hierror "type must be an instance of `%s'" (EcPath.tostring (fst tc))
+*)
+*)
 
-    let scope =
-      thcl.pthc_import |> ofold (fun flag scope ->
-        match flag with
-        | `Import  ->
-          { scope with sc_env = EcSection.import npath scope.sc_env; }
-        | `Export  ->
-          let item = EcTheory.mkitem EcTheory.import0 (Th_export (npath, `Global)) in
-          { scope with sc_env = EcSection.add_item item scope.sc_env; }
-        | `Include -> scope)
-        scope
+  (* ------------------------------------------------------------------ *)
+  let add_instance
+    ?(import = EcTheory.import0) (scope : scope) mode ({ pl_desc = tci } as toptci)
+  =
+    match unloc tci.pti_name with
+    | ([], "bring") -> begin
+        if EcUtils.is_some tci.pti_args then
+          hierror "unsupported-option";
+        addring ~import scope mode (`Boolean, toptci)
+    end
 
-    in Ax.add_defer scope proofs
+    | ([], "ring") -> begin
+      let kind =
+        match tci.pti_args with
+        | None -> `Integer
+        | Some (`Ring (c, p)) ->
+            if odfl false (c |> omap (fun c -> c <^ BI.of_int 2)) then
+              hierror "invalid coefficient modulus";
+            if odfl false (p |> omap (fun p -> p <^ BI.of_int 2)) then
+              hierror "invalid power modulus";
+            if      opt_equal BI.equal c (Some (BI.of_int 2))
+                 && opt_equal BI.equal p (Some (BI.of_int 2))
+            then `Boolean
+            else `Modulus (c, p)
+      in addring ~import scope mode (kind, toptci)
+    end
+
+    | ([], "field") -> addfield ~import scope mode toptci
 
+    | _ ->
+        if EcUtils.is_some tci.pti_args then
+          hierror "unsupported-option";
+        failwith "unsupported"          (* FIXME *)
 end
 
 (* -------------------------------------------------------------------- *)
diff --git a/src/ecScope.mli b/src/ecScope.mli
index f04f9595aa..7b1abcbace 100644
--- a/src/ecScope.mli
+++ b/src/ecScope.mli
@@ -118,6 +118,7 @@ end
 module Ty : sig
   val add : scope -> ptydecl located -> scope
 
+  val add_subtype : scope -> psubtype located -> scope
   val add_class    : scope -> ptypeclass located -> scope
   val add_instance : ?import:EcTheory.import -> scope -> Ax.proofmode -> ptycinstance located -> scope
 end
diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml
index 5ed2df1d2c..603b52914a 100644
--- a/src/ecThCloning.ml
+++ b/src/ecThCloning.ml
@@ -53,11 +53,23 @@ type axclone = {
   axc_tac   : EcParsetree.ptactic_core option;
 }
 
+(* ------------------------------------------------------------------ *)
+type xty_override =
+  [ty_override_def genoverride | `Direct of EcAst.ty] * clmode
+
+(* ------------------------------------------------------------------ *)
+type xop_override =
+  [op_override_def genoverride | `Direct of EcAst.form] * clmode
+
+(* ------------------------------------------------------------------ *)
+type xpr_override =
+  [pr_override_def genoverride | `Direct of EcAst.form] * clmode
+
 (* ------------------------------------------------------------------ *)
 type evclone = {
-  evc_types    : (ty_override located) Msym.t;
-  evc_ops      : (op_override located) Msym.t;
-  evc_preds    : (pr_override located) Msym.t;
+  evc_types    : (xty_override located) Msym.t;
+  evc_ops      : (xop_override located) Msym.t;
+  evc_preds    : (xpr_override located) Msym.t;
   evc_abbrevs  : (nt_override located) Msym.t;
   evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
@@ -65,6 +77,7 @@ type evclone = {
   evc_ths      : evclone Msym.t;
 }
 
+
 and evlemma = {
   ev_global  : (ptactic_core option * evtags option) list;
   ev_bynames : evinfo Msym.t;
@@ -271,7 +284,8 @@ end = struct
         (fun evc ->
           if Msym.mem x evc.evc_types then
             clone_error oc.oc_env (CE_DupOverride (OVK_Type, name));
-          { evc with evc_types = Msym.add x (mk_loc lc tyd) evc.evc_types })
+          { evc with evc_types =
+              Msym.add x (mk_loc lc tyd :> xty_override located) evc.evc_types })
         nm evc
 
     in (proofs, evc)
@@ -288,13 +302,14 @@ end = struct
         (fun evc ->
          if Msym.mem x evc.evc_ops then
            clone_error oc.oc_env (CE_DupOverride (OVK_Operator, name));
-         { evc with evc_ops = Msym.add x (mk_loc lc opd) evc.evc_ops })
+         { evc with evc_ops = 
+            Msym.add x (mk_loc lc opd :> xop_override located) evc.evc_ops })
         nm evc
 
     in (proofs, evc)
 
   (* ------------------------------------------------------------------ *)
-  let pr_ovrd oc ((proofs, evc) : state) name (prd : pr_override) =
+  let pr_ovrd oc ((proofs, evc) : state) name (prd : EcParsetree.pr_override) =
     let { pl_loc = lc; pl_desc = ((nm, x) as name) } = name in
 
     if find_pr oc.oc_oth name = None then
@@ -305,7 +320,8 @@ end = struct
         (fun evc ->
          if Msym.mem x evc.evc_preds then
            clone_error oc.oc_env (CE_DupOverride (OVK_Predicate, name));
-         { evc with evc_preds = Msym.add x (mk_loc lc prd) evc.evc_preds })
+         { evc with evc_preds =
+            Msym.add x (mk_loc lc prd :> xpr_override located) evc.evc_preds })
         nm evc
 
     in (proofs, evc)
diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli
index b4206554d6..26806f6c14 100644
--- a/src/ecThCloning.mli
+++ b/src/ecThCloning.mli
@@ -39,11 +39,23 @@ exception CloneError of EcEnv.env * clone_error
 
 val clone_error : EcEnv.env -> clone_error -> 'a
 
+(* ------------------------------------------------------------------ *)
+type xty_override =
+  [ty_override_def genoverride | `Direct of EcAst.ty] * clmode
+
+(* ------------------------------------------------------------------ *)
+type xop_override =
+  [op_override_def genoverride | `Direct of EcAst.form] * clmode
+
+(* ------------------------------------------------------------------ *)
+type xpr_override =
+  [pr_override_def genoverride | `Direct of EcAst.form] * clmode
+
 (* -------------------------------------------------------------------- *)
 type evclone = {
-  evc_types    : (ty_override located) Msym.t;
-  evc_ops      : (op_override located) Msym.t;
-  evc_preds    : (pr_override located) Msym.t;
+  evc_types    : (xty_override located) Msym.t;
+  evc_ops      : (xop_override located) Msym.t;
+  evc_preds    : (xpr_override located) Msym.t;
   evc_abbrevs  : (nt_override located) Msym.t;
   evc_modexprs : (me_override located) Msym.t;
   evc_modtypes : (mt_override located) Msym.t;
diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml
index 060368a248..283fca0c26 100644
--- a/src/ecTheoryReplay.ml
+++ b/src/ecTheoryReplay.ml
@@ -246,22 +246,33 @@ let operator_compatible env oper1 oper2 =
   | _                 , _                  -> raise exn
 
 (* -------------------------------------------------------------------- *)
-let check_evtags (tags : evtags) (src : symbol list) =
-  let module E = struct exception Reject end in
+let check_evtags ?(tags : evtags option) (src : symbol list) =
+  let exception Reject in
+
+  let explicit = "explicit" in
 
   try
-    let dfl = not (List.exists (fun (mode, _) -> mode = `Include) tags) in
-    let stt =
-      List.map (fun src ->
-        let do1 status (mode, dst) =
-          match mode with
-          | `Exclude -> if sym_equal src dst then raise E.Reject; status
-          | `Include -> status || (sym_equal src dst)
-        in List.fold_left do1 dfl tags)
-        src
-    in List.mem true stt
-
-  with E.Reject -> false
+    match tags with
+    | None ->
+      if List.mem explicit src then
+        raise Reject;
+      true
+
+    | Some tags ->
+      let dfl =
+        not (List.mem explicit src) &&
+        not (List.exists (fun (mode, _) -> mode = `Include) tags) in
+      let stt =
+        List.map (fun src ->
+          let do1 status (mode, dst) =
+            match mode with
+            | `Exclude -> if sym_equal src dst then raise Reject; status
+            | `Include -> status || (sym_equal src dst)
+          in List.fold_left do1 dfl tags)
+          src
+      in List.mem true stt
+
+  with Reject -> false
 
 (* -------------------------------------------------------------------- *)
 let xpath ove x =
@@ -284,12 +295,23 @@ let string_of_renaming_kind = function
   | `Theory  -> "theory"
 
 (* -------------------------------------------------------------------- *)
-let rename ove subst (kind, name) =
+let rename ?(fold = true) ove subst (kind, name) =
   try
     let newname =
-      List.find_map
-        (fun rnm -> EcThCloning.rename rnm (kind, name))
-        ove.ovre_rnms in
+      match fold with
+      | false ->
+        List.find_map
+          (fun rnm -> EcThCloning.rename rnm (kind, name))
+          ove.ovre_rnms
+      | _ ->
+        let newname =
+          List.fold_left (* FIXME:parallel substitution *)
+            (fun name rnm ->
+              Option.value ~default:name (EcThCloning.rename rnm (kind, name)))
+            name ove.ovre_rnms in
+        if newname = name then raise Not_found;
+        newname
+    in
 
     let nameok =
       match kind with
@@ -355,6 +377,17 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd
 
             | _ -> assert false
           end
+
+        | `Direct ty -> begin
+          assert (List.is_empty otyd.tyd_params);
+          let decl  =
+            { tyd_params  = [];
+              tyd_type    = `Concrete ty;
+              tyd_resolve = otyd.tyd_resolve && (mode = `Alias);
+              tyd_loca    = otyd.tyd_loca; }
+
+          in (decl, ty)
+    end
       in
 
       let subst, x =
@@ -487,6 +520,15 @@ and replay_opd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopd) =
 
             | _ -> clone_error env (CE_UnkOverride(OVK_Operator, EcPath.toqsymbol p))
           end
+
+          | `Direct body ->
+            assert (List.is_empty refop.op_tparams);
+            let newop =
+              mk_op
+                ~opaque:optransparent ~clinline:(opmode <> `Alias)
+                [] body.f_ty (Some (OP_Plain body)) refop.op_loca in
+            (newop, body)
+  
         in
           match opmode with
           | `Alias ->
@@ -605,6 +647,18 @@ and replay_prd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, oopr) =
 
           | _ -> clone_error env (CE_UnkOverride(OVK_Predicate, EcPath.toqsymbol p))
         end
+
+        | `Direct body ->
+          assert (List.is_empty refpr.op_tparams);
+          let newpr   =
+            { op_tparams  = [];
+              op_ty       = body.f_ty;
+              op_kind     = OB_pred (Some (PR_Plain body));
+              op_opaque   = oopr.op_opaque;
+              op_clinline = prmode <> `Alias;
+              op_loca     = refpr.op_loca;
+              op_unfold   = refpr.op_unfold; } in
+          (newpr, body)
       in
 
         match prmode with
@@ -682,9 +736,13 @@ and replay_axd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, ax) =
       match Msym.find_opt x (ove.ovre_ovrd.evc_lemmas.ev_bynames) with
       | Some (pt, hide, explicit) -> Some (pt, hide, explicit)
       | None when is_axiom ax.ax_kind ->
-          List.Exceptionless.find_map
-            (function (pt, None) -> Some (pt, `Alias, false) | (pt, Some pttags) ->
-               if check_evtags pttags (Ssym.elements tags) then
+          List.Exceptionless.find_map (function
+            | (pt, None) ->
+              if check_evtags (Ssym.elements tags) then
+                Some (pt, `Alias, false)
+              else None
+            | (pt, Some pttags) ->
+               if check_evtags ~tags:pttags (Ssym.elements tags) then
                  Some (pt, `Alias, false)
                else None)
             ove.ovre_glproof
diff --git a/tests/subtype-clone-sugar.ec b/tests/subtype-clone-sugar.ec
new file mode 100644
index 0000000000..94bc894913
--- /dev/null
+++ b/tests/subtype-clone-sugar.ec
@@ -0,0 +1,7 @@
+require import AllCore.
+require Subtype.
+
+subtype zmod3 =
+  { x : int | 0 <= x < 3 }.
+
+realize inhabited. by exists 0. qed.
diff --git a/theories/algebra/Poly.ec b/theories/algebra/Poly.ec
index d2633cd5d7..a58e61ab4b 100644
--- a/theories/algebra/Poly.ec
+++ b/theories/algebra/Poly.ec
@@ -23,18 +23,11 @@ op ispoly (p : prepoly) =
       (forall c, c < 0 => p c = zeror)
     /\ (exists d, forall c, (d < c)%Int => p c = zeror).
 
-clone include Subtype
-  with type T   <- prepoly,
-       op P   <- ispoly
-  rename "insub" as "to_poly"
-  rename "val"   as "of_poly"
-proof *.
+subtype poly = { p : prepoly | ispoly p }
+  rename "to_poly", "of_poly".
+
 realize inhabited.
-  exists (fun _, zeror).
-  rewrite /ispoly.
-  auto.
-qed.
-type poly = sT.
+proof. by exists (fun _ => zeror). qed.
 
 op "_.[_]" (p : poly) (i : int) = (of_poly p) i.
 
diff --git a/theories/algebra/ZModP.ec b/theories/algebra/ZModP.ec
index 3d68db5ce2..df0e3127f9 100644
--- a/theories/algebra/ZModP.ec
+++ b/theories/algebra/ZModP.ec
@@ -11,15 +11,10 @@ abstract theory ZModRing.
 const p : { int | 2 <= p } as ge2_p.
 
 (* -------------------------------------------------------------------- *)
-clone Subtype as Sub with
-  type T <- int,
-  op P (x : int) <- 0 <= x < p
-proof *.
-realize inhabited.
-exists 0. smt(ge2_p).
-qed.
+subtype zmod as Sub = { x : int | 0 <= x < p }.
 
-type zmod = Sub.sT.
+realize inhabited.
+proof. by exists 0; smt(ge2_p). qed.
 
 (* -------------------------------------------------------------------- *)
 op inzmod (z : int)  = Sub.insubd (z %% p).
diff --git a/theories/datatypes/Word.eca b/theories/datatypes/Word.eca
index ee7dcfaa11..07582d5a47 100644
--- a/theories/datatypes/Word.eca
+++ b/theories/datatypes/Word.eca
@@ -14,19 +14,16 @@ op wordw : t list = mkseq (fun _ => dchar) n.
 lemma size_wordw: size wordw = n.
 proof. by rewrite size_mkseq ler_maxr ?ge0_n. qed.
 
-clone include Subtype
-  with type T   <- t list,
-       op P   <- fun w => size w = n
-proof *.
-realize inhabited by exists wordw; exact size_wordw.
+subtype word = { w : t list | size w = n }.
+
+realize inhabited.
+proof. by exists wordw; exact: size_wordw. qed.
 
-type word = sT.
 (* default value chosen for backward compatibility *)
 op mkword x = odflt (insubd wordw) (insub x).
 op ofword = val.
 
 (* -------------------------------------------------------------------- *)
-
 lemma mkwordK : cancel ofword mkword.
 proof. smt(valK). qed.
 
diff --git a/theories/datatypes/Xreal.ec b/theories/datatypes/Xreal.ec
index e84ca54d2e..e2fac68d6d 100644
--- a/theories/datatypes/Xreal.ec
+++ b/theories/datatypes/Xreal.ec
@@ -62,18 +62,13 @@ end MonoidDI.
 
 theory Rp.
 
-clone include Subtype
-  with type T <- real,
-       op P <- fun x => 0.0 <= x
-   rename "insubd" as "of_real"
-   rename "val" as "to_real"
-proof*.
-realize inhabited by exists 0%r.
+subtype realp = { x : real | 0.0 <= x }
+  rename "of_real", "to_real".
 
-type realp = sT.
+realize inhabited by exists 0%r.
 
 abbrev (%r) = to_real.
-abbrev (%rp) = of_real.
+abbrev (%rp) = of_reald.
 
 theory IntNotation.
   abbrev (%rp) (n:int) = n%r%rp.
@@ -82,13 +77,13 @@ end IntNotation. export IntNotation.
 axiom witness_0 : witness = 0%rp.
 
 lemma of_real_neg x : x < 0.0 =>  x%rp = 0%rp.
-proof. smt(to_realK val_of_real witness_0). qed.
+proof. smt(to_realK to_real_of_reald witness_0). qed.
 
 lemma of_real_le0 x : x <= 0%r => x%rp = 0%rp.
 proof. by rewrite ler_eqVlt; case => [->// | /of_real_neg]. qed.
 
 lemma to_realK_simpl (x:realp) : x%r%rp = x by apply: to_realKd.
-hint simplify to_realK_simpl, of_realK.
+hint simplify to_realK_simpl, of_realdK.
 
 lemma to_realP_simpl x : (0.0 <= x%r) = true by rewrite to_realP. 
 hint simplify to_realP_simpl.
@@ -106,33 +101,33 @@ abbrev (<) (x y : realp)  = x%r < y%r.
 
 clone include MonoidDI with
    type t  <- realp,
-   op zero <- of_real 0.0,
-   op MulMonoid.one  <- of_real 1.0,
+   op zero <- of_reald 0.0,
+   op MulMonoid.one  <- of_reald 1.0,
    op ( + ) <- Rp.( + ),
    op ( * ) <- Rp.( * )
-proof * by smt(of_realK to_realP to_real_inj).
+proof * by smt(of_realdK to_realP to_real_inj).
 
 lemma to_realD (x y:realp) : (x + y)%r = x%r + y%r.
-proof. smt (of_realK to_realP). qed.
+proof. smt (of_realdK to_realP). qed.
 
 lemma to_realM (x y:realp) : (x * y)%r = x%r * y%r.
-proof. smt (of_realK to_realP). qed.
+proof. smt (of_realdK to_realP). qed.
 
 lemma to_realI x : (inv x)%r = inv x%r.
-proof. smt (of_realK to_realP Real.invr0). qed.
+proof. smt (of_realdK to_realP Real.invr0). qed.
 
 hint simplify to_realD, to_realM, to_realI.
 
 lemma of_realD x y : 0.0 <= x => 0.0 <= y => 
    (x + y)%rp = x%rp + y%rp.
-proof. smt (of_realK to_realP). qed.
+proof. smt (of_realdK to_realP). qed.
 
 lemma of_realM x y : 0.0 <= x => 0.0 <= y => 
    (x * y)%rp = x%rp * y%rp.
-proof. smt (of_realK to_realP). qed.
+proof. smt (of_realdK to_realP). qed.
 
 lemma of_realI (x:real) : (inv x)%rp = inv x%rp.
-proof. smt (of_realK to_realP  of_real_neg divr0). qed.
+proof. smt (of_realdK to_realP  of_real_neg divr0). qed.
 hint simplify of_realI.
 
 op (%pos) (x:real) = if 0.0 <= x then x else 0.0.
@@ -148,7 +143,7 @@ lemma inv_pos x : inv x%pos = (inv x)%pos
 by smt(divr0).
 
 lemma to_real_of_real (x:real) : x%rp%r = x%pos.
-proof. by rewrite val_of_real witness_0. qed.
+proof. by rewrite to_real_of_reald witness_0. qed.
 hint simplify to_real_of_real.
 
 lemma to_pos_mu ['a] (d : 'a distr) (e: 'a -> bool) : 
@@ -283,19 +278,19 @@ proof. by rewrite /( ** ) one_neq0. qed.
 hint simplify smul0m, smul1m.
 
 lemma smulmDr x y z: x ** (y + z) = x ** y + x ** z. 
-proof. by rewrite /( ** ); case: (x = of_real 0%r) => //= ?; apply mulmDr. qed.
+proof. by rewrite /( ** ); case: (x = of_reald 0%r) => //= ?; apply mulmDr. qed.
 
 lemma smulmCA d x y : d ** (rp x * y) = rp x * (d ** y).
-proof. by rewrite /( ** ); case: (d = of_real 0.0) => //=; rewrite mulmCA. qed.
+proof. by rewrite /( ** ); case: (d = of_reald 0.0) => //=; rewrite mulmCA. qed.
 
 lemma smulmA d x y : d ** (x * rp y) = (d ** x) * rp y.
-proof. by rewrite /( ** ); case: (d = of_real 0.0) => //=;rewrite mulmA. qed.
+proof. by rewrite /( ** ); case: (d = of_reald 0.0) => //=;rewrite mulmA. qed.
 
 lemma smulmAC d x y : d ** (x * rp y) = rp y * (d ** x) .
 proof. by rewrite mulmC smulmCA. qed.
 
 lemma smulrp x y : x ** rp y =  rp (x * y).
-proof. by rewrite /( ** ); case: (x = of_real 0.0). qed.
+proof. by rewrite /( ** ); case: (x = of_reald 0.0). qed.
 hint simplify smulrp.
 
 (* -------------------------------------------------------------- *)
@@ -355,7 +350,7 @@ lemma xler_pmul2l (x:realp) : 0%rp < x =>
   forall (y z : xreal),
   rp x * y <= rp x * z <=> y <= z.
 proof.
-rewrite (of_realK 0%r) //.
+rewrite (of_realdK 0%r) //.
 move=> hx y z; case: z => // z; case: y => // y.
 by rewrite /= -!to_realM !to_realM ler_pmul2l.
 qed.
@@ -368,7 +363,7 @@ lemma xler_pmul2r (x:realp) : 0%rp < x =>
   forall (y z : xreal),
   y * rp x <= z * rp x <=> y <= z.
 proof.
-rewrite (of_realK 0%r) //.
+rewrite (of_realdK 0%r) //.
 move=> hx y z; case: z => // z; case: y => // y.
 by rewrite /= -!to_realM !to_realM ler_pmul2r.
 qed.
@@ -390,7 +385,7 @@ lemma xler_md x y c : ((0%r < c) => x <= y) => c ** x <= c ** y.
 proof.
   move=> h; rewrite /( **).
   case: (0%r < c ) => hc.
-  + have -> /=: (c%rp <> 0%rp) by smt(to_realP of_realK to_realK_simpl).
+  + have -> /=: (c%rp <> 0%rp) by smt(to_realP of_realdK to_realK_simpl).
     by apply/xler_mull/h.
   by have -> : (c%rp = 0%rp) by smt(of_real_neg).
 qed.
@@ -452,7 +447,7 @@ theory Lift.
     fun (x : 'a) => f1 x * f2 x.
 
   abbrev ( ** ) (d : 'a distr) (f : 'a -> xreal) =
-    fun (x : 'a) => of_real (mu1 d x) ** f x.
+    fun (x : 'a) => of_reald (mu1 d x) ** f x.
 
   op is_real ['a] (f : 'a -> xreal) = 
     forall x, is_real (f x).
@@ -542,7 +537,7 @@ theory Lift.
     is_real (d ** f1) <=> is_real (d ** f2).
   proof.
     move=> h; split => h1 x; have := h1 x; rewrite /( ** );
-    case: (of_real (mu1 d x) = of_real 0.0) => // ?; rewrite !is_realM h //; smt(mu_bounded).
+    case: (of_reald (mu1 d x) = of_reald 0.0) => // ?; rewrite !is_realM h //; smt(mu_bounded).
   qed.
 
   lemma is_real_rp ['a] (f:'a -> realp) : is_real (fun x => rp (f x)).
@@ -641,7 +636,7 @@ op Ep ['a] (d : 'a distr) (f : 'a -> xreal) =
   if is_real g then psuminf g else oo.
 
 lemma psuminfZ ['a] (c:realp) (f: 'a -> xreal) :
-  is_real f => c <> of_real 0.0 =>
+  is_real f => c <> of_reald 0.0 =>
   psuminf (fun x => rp c * f x) = rp c * psuminf f.
 proof.
   move=> hf hc; have heq := summableZ_iff (to_real f) (to_real c) _; 1:smt(@Rp).
@@ -709,26 +704,26 @@ proof.
   have -> : !is_real (fun (x : 'a) => if (mu1 d x)%rp = 0%rp then 0%xr else oo).
   + apply/negP => his.
     move/neq0_mu : hw => -[x [hx _]].
-    by have := his x; smt(of_realK to_realP ge0_weight).
-  by have -> : (weight d)%rp <> 0%rp by smt(of_realK to_realP ge0_weight).
+    by have := his x; smt(of_realdK to_realP ge0_weight).
+  by have -> : (weight d)%rp <> 0%rp by smt(of_realdK to_realP ge0_weight).
 qed.
 
 lemma EpZ ['a] (d: 'a distr) (c:realp) (f: 'a -> xreal) :
-  c <> of_real 0.0 => 
+  c <> of_reald 0.0 => 
   Ep d (fun x => rp c * f x) = rp c * Ep d f.
 proof. 
   move=> hc; rewrite /Ep /= (is_realMd f); 1: by move=> x _ /=; rewrite is_realM. 
   case: (is_real (d ** f)) => // hr; rewrite /psuminf.
   rewrite mdCA /= to_realM /=.
   rewrite -summableZ_iff 1:#smt:(@Rp); rewrite /to_real.
-  case: (summable (fun (x : 'a) => to_real (of_real (mu1 d x) ** f x))) => // ?.
+  case: (summable (fun (x : 'a) => to_real (of_reald (mu1 d x) ** f x))) => // ?.
   rewrite sumZ /= of_realM // ge0_sum => /= ?; apply to_realP.
 qed.
 
 lemma EpsZ ['a] (d: 'a distr) (c:realp) (f: 'a -> xreal) :
   Ep d (fun x => c ** f x) = c ** Ep d f.
 proof. 
-  rewrite /( ** ); case: (c = of_real 0%r) => ?; last by apply EpZ.
+  rewrite /( ** ); case: (c = of_reald 0%r) => ?; last by apply EpZ.
   by rewrite EpC.
 qed.
 
@@ -737,7 +732,7 @@ lemma EpD ['a] (d : 'a distr) (f1 f2 : 'a -> xreal) :
 proof.
   rewrite /Ep /= mdDr.
   have /= := is_realD (d ** f1) (d ** f2).
-  case: (is_real (fun x => of_real (mu1 d x) ** f1 x + of_real (mu1 d x) ** f2 x)) => h />.
+  case: (is_real (fun x => of_reald (mu1 d x) ** f1 x + of_reald (mu1 d x) ** f2 x)) => h />.
   + by move=> h1 h2; rewrite -psumifD.
   by case: (is_real (d ** f1)) => />.
 qed.
@@ -883,7 +878,7 @@ proof. rewrite /dmap Ep_dlet; apply eq_Ep => x _ /=; apply Ep_dunit. qed.
 (* -------------------------------------------------------------------- *)
 lemma Ep_duniform ['a] (s : 'a list) (f : 'a -> xreal) :
   Ep (duniform s) f =
-    of_real (1%r / (size ((undup s)))%r) ** big predT f (undup s).
+    of_reald (1%r / (size ((undup s)))%r) ** big predT f (undup s).
 proof.
   rewrite (Ep_fin (undup s)) 1:undup_uniq.
   + move=> x hx; rewrite mem_undup -supp_duniform; smt(ge0_mu).
@@ -893,7 +888,7 @@ qed.
 
 (* -------------------------------------------------------------------- *)
 lemma Ep_dbool (f : bool -> xreal) :
-  Ep {0,1} f = of_real 0.5 ** f true + of_real 0.5 ** f false.
+  Ep {0,1} f = of_reald 0.5 ** f true + of_reald 0.5 ** f false.
 proof.
   rewrite (Ep_fin [true; false]) 1://; 1: smt(supp_dbool).
   by rewrite big_consT big_seq1 /= !dbool1E.
diff --git a/theories/structure/Quotient.ec b/theories/structure/Quotient.ec
index 1e61798741..6626fd19a2 100644
--- a/theories/structure/Quotient.ec
+++ b/theories/structure/Quotient.ec
@@ -87,24 +87,22 @@ apply/(eqv_trans (canon x)); first by apply/eqv_canon.
 by rewrite eq &(eqv_refl).
 qed.
 
-clone import Subtype with
-  type T  <- T,
-  op P  <- iscanon
-proof *.
+subtype qT as QSub = { x : T | iscanon x }.
+
 realize inhabited.
-smt(canonK).
-qed.
-    
-type qT = sT.
+proof. smt(canonK). qed.
+
+import QSub.
 
 clone include CoreQuotient with
   type T     <- T,
   type qT    <- qT,
-  op   pi    =  fun x => Subtype.insubd (canon x),
-  op   repr  =  fun x => Subtype.val x
+  op   pi    =  fun x => QSub.insubd (canon x),
+  op   repr  =  fun x => QSub.val x
 
   proof *.
 
+
 realize reprK. proof.
 by move=> q; rewrite /pi /repr /insubd canon_iscanon 1:valP valK.
 qed.
diff --git a/theories/structure/Subtype.eca b/theories/structure/Subtype.eca
index 7e01521967..6276df116c 100644
--- a/theories/structure/Subtype.eca
+++ b/theories/structure/Subtype.eca
@@ -1,7 +1,5 @@
-pragma +implicits.
-
-
 (* -------------------------------------------------------------------- *)
+pragma +implicits.
 
 (* -------------------------------------------------------------------- *)
 (* This theory defines the subtype [sT] of [T] defined as {x : T | P x} *)
@@ -21,89 +19,34 @@ pragma +implicits.
 
 require import AllCore.
 
-(* These three parameters are to be instantiated by the user. *)
-type T.
-op P : T -> bool.
-axiom inhabited: exists x, P x.
-
-(* This parameter must never be instantiated upon cloning, otherwise
-   unsoundness may ensure. Hence the name. *)
-type do_not_instantiate_this_type.
-(* TODO: we want a tag to make abstract types uninstantiable *)
-
-(* The lemma below is justified by the axiom [inhabited] and the fact
-  that the type [do_not_instantiate_this_type] is unspecified. It says
-  that there is an injective function [f] with range [P]
-
-  The proof is admitted, essentially turning it into a global axiom
-  asserting the existence of subtypes. We cannot use [axiom] here,
-  because this would make the lemma a parameter of the theory *)
-
-lemma subtype_injection:
-  exists (f : do_not_instantiate_this_type -> T),
-    injective f /\ (forall x, P x <=> exists y, x = f y).
-admitted.
-(* TODO: together with uninstantiable abstract types, we also want
-   global axioms in (abstract) theories.that do not show up in [proof*] *)
-
-(* This is the subtype that the user sees. By making it a type-copy of
-   [do_not_instantiate_this_type], we make sure that the user cannot
-   do `type sT <- ...` when cloning. *)
-type sT = do_not_instantiate_this_type wrapped.
-
-(* We define `val` in two steps so that `print val` does not show the
-   ugly internal stuff *)
-op [opaque] internal_val = choiceb
-   (fun (f : do_not_instantiate_this_type -> T),
-     injective f /\ (forall (x:T), ((P x) <=> exists y, x = f y))) witness.
+type T, sT.
 
-(* -------------------------------------------------------------------- *)
+op P : T -> bool.
 
-(* Injection from [sT] to [T] *)
-op [opaque] val (x : sT) : T = with x = Wrap x' => internal_val x'.
+op insub : T  -> sT option.
+op val   : sT -> T.
 
-lemma val_range x: P x <=> exists y, x = val y.
-proof.
-have /= := choicebP _ witness subtype_injection; rewrite -/internal_val.
-move => [ival_inj ival_range].
-split => [Px|[[y] ->]]; 2: smt().
-have := ival_range x; rewrite Px /= => -[z ?].
-by exists (Wrap z); smt().
-qed.
+axiom [prove] inhabited : exists x, P x.
 
-lemma val_inj: injective val.
-proof.
-have /= := choicebP _ witness subtype_injection; rewrite -/internal_val.
-by move => [ival_inj _] [x] [y] /#.
-qed.
+axiom [explicit] insubN (x : T): !P x => insub x = None.
+axiom [explicit] insubT (x : T):  P x => omap val (insub x) = Some x.
 
-lemma valP (x : sT): P (val x) by smt (val_range).
+axiom [explicit] valP (x : sT): P (val x).
+axiom [explicit] valK: pcancel val insub.
 
 (* -------------------------------------------------------------------- *)
-
-op [opaque] insub : T -> sT option = pinv val.
-
-lemma insubN (x : T): !P x => insub x = None.
-proof. by rewrite /insub => not; apply pinvN; smt(val_range). qed.
-
-lemma valK: pcancel val insub.
-proof. by rewrite /insub; apply/pcancel_pinv/val_inj. qed.
-
-lemma insubT (x : T):  P x => omap val (insub x) = Some x.
-proof. by move => Px @/insub; apply pinv_inv; smt(val_range). qed.
+op insubd (x : T) = odflt witness (insub x).
 
 (* -------------------------------------------------------------------- *)
-
-(* TODO: Maybe this could be removed, it seems relatively
-pointless. It's here for compatibility with the previous Subtype
-implementation *)
-op wsT = val witness.
-
-lemma insubW: insub wsT = Some witness<:sT>.
-proof. by rewrite /wsT; smt (valK). qed.
+lemma val_range x: P x <=> exists y, x = val y.
+proof. split.
+- by move/insubT; case (insub x) => // [y] /= <-; exists y.
+- by case=> y ->; apply/valP.
+qed.
 
 (* -------------------------------------------------------------------- *)
-op insubd (x : T) = odflt witness (insub x).
+lemma val_inj: injective val.
+proof. by apply/(pcan_inj _ _ valK). qed.
 
 (* -------------------------------------------------------------------- *)
 lemma valKd: cancel val insubd.
@@ -113,9 +56,9 @@ lemma insubP (x : T):           (* We need inductive predicates *)
      (exists u, P x /\ insub x = Some u /\ val u = x)
   \/ (!P x /\ insub x = None).
 proof.                          (* this proof script is awful *)
-  case (P x)=> [Px | /insubN -> //]; left.
-  move: Px => /insubT; case {-2}(insub x) (eq_refl (insub x))=> //.
-  by move=> /= u eq_insub eqx; exists u => /=; move: eqx => ->.
+case (P x)=> [Px | /insubN -> //]; left.
+move: Px => /insubT; case {-2}(insub x) (eq_refl (insub x))=> //.
+by move=> /= u eq_insub eqx; exists u => /=; move: eqx => ->.
 qed.
 
 lemma val_insubd x: val (insubd x) = if P x then x else val witness.