From f7a642bd3f8a5436873d0163114a30dad23ba9c2 Mon Sep 17 00:00:00 2001
From: Kathy Gray
Date: Thu, 17 Dec 2015 16:48:54 +0000
Subject: Remove external functions that the library provides, having added
 them to the type environment finally. (Also small cleaning of the new
 makefile)

---
 src/type_internal.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'src')

diff --git a/src/type_internal.ml b/src/type_internal.ml
index 65727e1b..59a573d9 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -2101,6 +2101,14 @@ let initial_typ_env =
                                            (mk_range n_zero (mk_nv "m"))])
                                   (mk_vector bit_t (Ovar "ord") (mk_nv "n") (mk_nv "m")))),
                 External (Some "bitwise_rotate"),[],pure_e,pure_e,nob));
+    ("EXTS",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]),
+                  (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))
+                     (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")),
+                 External (Some "EXTS"),[],pure_e,pure_e,nob));
+    ("EXTZ",Base((((mk_nat_params ["n";"m";"o";"p"])@["ord",{k=K_Ord}]),
+                  (mk_pure_imp (mk_vector bit_t (Ovar "ord") (mk_nv "o") (mk_nv "n"))
+                     (mk_vector bit_t (Ovar "ord") (mk_nv "p") (mk_nv "m")) "m")),
+                 External (Some "EXTZ"),[],pure_e,pure_e,nob));
   ]
 
 
-- 
cgit v1.2.3