diff options
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 *) |