From 0ade32f84b28d2190360ec79520788142755b5b7 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 11 Mar 2018 20:29:16 +0100
Subject: [api] Deprecate a couple of aliases that we missed.

---
 kernel/term.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'kernel/term.ml')

diff --git a/kernel/term.ml b/kernel/term.ml
index 403ed881c5..e1affb1c07 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term =
   | Case      of case_info * 'constr * 'constr * 'constr array
   | Fix       of ('constr, 'types) pfixpoint
   | CoFix     of ('constr, 'types) pcofixpoint
-  | Proj      of projection * 'constr
+  | Proj      of Projection.t * 'constr
 
 type values = Vmvalues.values
 
-- 
cgit v1.2.3