diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2016-06-07 09:52:43 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2016-06-14 20:01:37 +0200 |
| commit | d4f3a1a807d474050a4e91e16ff7813f1db7f537 (patch) | |
| tree | 68c91e818fd7d35789c514b3db06f77ed54b8968 /kernel/typeops.ml | |
| 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/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 9e9f18aaa..1c3117725 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -494,13 +494,13 @@ let rec execute env cstr = | Fix ((vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in - check_fix ~chk:true env fix; + check_fix ~flags:{check_guarded=true} env fix; make_judge (mkFix fix) fix_ty | CoFix (i,recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let cofix = (i,recdef') in - check_cofix ~chk:true env cofix; + check_cofix ~flags:{check_guarded=true} env cofix; (make_judge (mkCoFix cofix) fix_ty) (* Partial proofs: unsupported by the kernel *) |