diff options
| author | herbelin | 2002-01-30 13:47:58 +0000 |
|---|---|---|
| committer | herbelin | 2002-01-30 13:47:58 +0000 |
| commit | e53297f0e103f2c79368cf8aa04792884e463089 (patch) | |
| tree | d12d01185ab3b4fea8a35ac31fc6969af712c351 /kernel/closure.mli | |
| 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/closure.mli')
| -rw-r--r-- | kernel/closure.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 *) |