From 32d372f83a7797244b4e4d4f0d5791145bc615d1 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 29 May 2012 11:09:19 +0000
Subject: No more Univ in grammar.cma

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15385 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/detyping.mli | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'pretyping/detyping.mli')

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 439609b020..10f23b1b2c 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -17,6 +17,9 @@ open Termops
 open Mod_subst
 open Misctypes
 
+(** Should we keep details of universes during detyping ? *)
+val print_universes : bool ref
+
 val subst_cases_pattern : substitution -> cases_pattern -> cases_pattern
 
 val subst_glob_constr : substitution -> glob_constr -> glob_constr
-- 
cgit v1.2.3