From 0108db19c96e1b46346f032964f2cca3f8149cb3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sat, 23 Jun 2018 15:38:00 +0200
Subject: Projections use index representation

The upper layers still need a mapping constant -> projection, which is
provided by Recordops.
---
 kernel/mod_subst.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'kernel/mod_subst.mli')

diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 76a1d173b9..2e5211c770 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -147,6 +147,9 @@ val subst_con_kn :
 val subst_constant :
   substitution -> Constant.t -> Constant.t
 
+val subst_proj_repr : substitution -> Projection.Repr.t -> Projection.Repr.t
+val subst_proj : substitution -> Projection.t -> Projection.t
+
 (** Here the semantics is completely unclear.
    What does "Hint Unfold t" means when "t" is a parameter?
    Does the user mean "Unfold X.t" or does she mean "Unfold y"
-- 
cgit v1.2.3