From e53297f0e103f2c79368cf8aa04792884e463089 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 30 Jan 2002 13:47:58 +0000
Subject: cosmetique

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2445 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/closure.ml  | 4 ++--
 kernel/closure.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel')

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 7cac9e5969..fd432d6058 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -54,7 +54,7 @@ let with_stats c =
 
 type evaluable_global_reference =
   | EvalVarRef of identifier
-  | EvalConstRef of section_path
+  | EvalConstRef of constant
 
 type transparent_state = Idpred.t * Sppred.t
 
@@ -68,7 +68,7 @@ module type RedFlagsSig = sig
   val fDELTA : red_kind
   val fIOTA : red_kind
   val fZETA : red_kind
-  val fCONST : section_path -> red_kind
+  val fCONST : constant -> red_kind
   val fVAR : identifier -> red_kind
   val no_red : reds
   val red_add : reds -> red_kind -> reds
diff --git a/kernel/closure.mli b/kernel/closure.mli
index 54c1328b48..1360862c9c 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -50,7 +50,7 @@ module type RedFlagsSig = sig
   val fDELTA : red_kind
   val fIOTA : red_kind
   val fZETA : red_kind
-  val fCONST : section_path -> red_kind
+  val fCONST : constant -> red_kind
   val fVAR : identifier -> red_kind
 
   (* No reduction at all *)
-- 
cgit v1.2.3