From 6aeea41c8a94233cb8b3ae15db1b20c75397610e Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 20 Sep 2001 16:31:09 +0000
Subject: Nettoyage des commentaires

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/univ.mli | 15 +--------------
 1 file changed, 1 insertion(+), 14 deletions(-)

(limited to 'kernel/univ.mli')

diff --git a/kernel/univ.mli b/kernel/univ.mli
index e677b765c..da66f4aed 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -16,15 +16,9 @@ open Names
 
 type universe
 
-(*
-val dummy_univ : universe
-*)
 val implicit_univ : universe
 
 val prop_univ : universe
-(*
-val prop_univ_univ : universe
-*)
 
 val set_module : dir_path -> unit
 
@@ -38,11 +32,7 @@ val initial_universes : universes
 
 (*s Constraints. *)
 
-(*
-type constraint_type = Gt | Geq | Eq
-*)
-
-type univ_constraint (* = universe * constraint_type * universe *)
+type univ_constraint
 
 module Constraint : Set.S with type elt = univ_constraint
 
@@ -50,9 +40,6 @@ type constraints = Constraint.t
 
 type constraint_function = universe -> universe -> constraints -> constraints
 
-(*
-val enforce_gt : constraint_function
-*)
 val enforce_geq : constraint_function
 val enforce_eq : constraint_function
 
-- 
cgit v1.2.3