diff options
| author | Arnaud Spiwack | 2016-06-07 09:52:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2016-06-14 20:01:37 +0200 |
| commit | d4f3a1a807d474050a4e91e16ff7813f1db7f537 (patch) | |
| tree | 68c91e818fd7d35789c514b3db06f77ed54b8968 /kernel/fast_typeops.mli | |
| parent | 64e94267cb80adc1b4df782cc83a579ee521b59b (diff) | |
Assume totality: dedicated type rather than bool
The rational is that
1. further typing flags may be available in the future
2. it makes it easier to trace and document the argument
Diffstat (limited to 'kernel/fast_typeops.mli')
| -rw-r--r-- | kernel/fast_typeops.mli | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/kernel/fast_typeops.mli b/kernel/fast_typeops.mli index 98dbefad13..1c0146baea 100644 --- a/kernel/fast_typeops.mli +++ b/kernel/fast_typeops.mli @@ -8,6 +8,7 @@ open Term open Environ +open Declarations (** {6 Typing functions (not yet tagged as safe) } @@ -18,6 +19,6 @@ open Environ *) -val infer : chkguard:bool -> env -> constr -> unsafe_judgment -val infer_v : chkguard:bool -> env -> constr array -> unsafe_judgment array -val infer_type : chkguard:bool -> env -> types -> unsafe_type_judgment +val infer : flags:typing_flags -> env -> constr -> unsafe_judgment +val infer_v : flags:typing_flags -> env -> constr array -> unsafe_judgment array +val infer_type : flags:typing_flags -> env -> types -> unsafe_type_judgment |