From 421d846d80c19226ba0922ff3c3b0006c98c21b6 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Mon, 12 Dec 2016 14:49:01 +0100
Subject: Replace Typeops by Fast_typeops

This is really [mv fast_typeops.ml{,i} typeops.ml{,i}] plus trivial
changes in the other files, the real changes are in the parent commit.
---
 kernel/term_typing.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index d8774944e4..3a0d1a2a5e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -20,7 +20,6 @@ open Declarations
 open Environ
 open Entries
 open Typeops
-open Fast_typeops
 
 module RelDecl = Context.Rel.Declaration
 module NamedDecl = Context.Named.Declaration
-- 
cgit v1.2.3