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.
---
 pretyping/retyping.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index d4fa2461b4..821c57d033 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -273,8 +273,8 @@ let relevance_of_term env sigma c =
       | Rel n ->
         let len = Range.length rels in
         if n <= len then Range.get rels (n - 1)
-        else Retypeops.relevance_of_rel env (n - len)
-      | Var x -> Retypeops.relevance_of_var env x
+        else Relevanceops.relevance_of_rel env (n - len)
+      | Var x -> Relevanceops.relevance_of_var env x
       | Sort _ -> Sorts.Relevant
       | Cast (c, _, _) -> aux rels c
       | Prod ({binder_relevance=r}, _, codom) ->
@@ -284,13 +284,13 @@ let relevance_of_term env sigma c =
       | LetIn ({binder_relevance=r}, _, _, bdy) ->
         aux (Range.cons r rels) bdy
       | App (c, _) -> aux rels c
-      | Const (c,_) -> Retypeops.relevance_of_constant env c
+      | Const (c,_) -> Relevanceops.relevance_of_constant env c
       | Ind _ -> Sorts.Relevant
-      | Construct (c,_) -> Retypeops.relevance_of_constructor env c
+      | Construct (c,_) -> Relevanceops.relevance_of_constructor env c
       | Case (ci, _, _, _) -> ci.ci_relevance
       | Fix ((_,i),(lna,_,_)) -> (lna.(i)).binder_relevance
       | CoFix (i,(lna,_,_)) -> (lna.(i)).binder_relevance
-      | Proj (p, _) -> Retypeops.relevance_of_projection env p
+      | Proj (p, _) -> Relevanceops.relevance_of_projection env p
       | Int _ | Float _ -> Sorts.Relevant
 
       | Meta _ | Evar _ -> Sorts.Relevant
-- 
cgit v1.2.3