diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-30 13:47:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-01-30 13:47:58 +0000 |
| commit | e53297f0e103f2c79368cf8aa04792884e463089 (patch) | |
| tree | d12d01185ab3b4fea8a35ac31fc6969af712c351 /kernel | |
| parent | 222b8b52058da65a1dd276d191f6d54748a1485f (diff) | |
cosmetique
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2445 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 4 | ||||
| -rw-r--r-- | kernel/closure.mli | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 7cac9e596..fd432d605 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 54c1328b4..1360862c9 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 *) |