From cb9413483bcd2a6bc91fb439343550bb6f425e5b Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 18 Mar 2020 17:57:12 +0100
Subject: Rename Retypeops -> Relevanceops

This module used to do retyping for the kernel in prototypes of SProp,
but was switched to only relevance inference before the merge.
---
 kernel/term_typing.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term_typing.ml')

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 0c89d51033..c8c2301171 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -143,7 +143,7 @@ let infer_declaration env (dcl : constant_entry) =
         Cooking.cook_body = def;
         cook_type = typ;
         cook_universes = univs;
-        cook_relevance = Retypeops.relevance_of_term env j.uj_val;
+        cook_relevance = Relevanceops.relevance_of_term env j.uj_val;
         cook_inline = c.const_entry_inline_code;
         cook_context = c.const_entry_secctx;
       }
-- 
cgit v1.2.3