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.ml  | 5 ++++-
 pretyping/detyping.mli | 3 +++
 2 files changed, 7 insertions(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index ab43880478..fd20f199c8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -32,6 +32,9 @@ open Decl_kinds
 
 let dl = dummy_loc
 
+(** Should we keep details of universes during detyping ? *)
+let print_universes = ref false
+
 (****************************************************************************)
 (* Tools for printing of Cases                                              *)
 
@@ -367,7 +370,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
 let detype_sort = function
   | Prop Null -> GProp
   | Prop Pos -> GSet
-  | Type u -> GType (Some u)
+  | Type u -> GType (if !print_universes then Some (Univ.pr_uni u) else None)
 
 type binder_kind = BProd | BLambda | BLetIn
 
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