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 /pretyping/typing.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 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 0bb2979c2..fa6fd9677 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -184,13 +184,13 @@ let rec execute env evdref cstr = | Fix ((vn,i as vni),recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let fix = (vni,recdef') in - check_fix env ~chk:true fix; + check_fix env ~flags:{Declarations.check_guarded=true} fix; make_judge (mkFix fix) tys.(i) | CoFix (i,recdef) -> let (_,tys,_ as recdef') = execute_recdef env evdref recdef in let cofix = (i,recdef') in - check_cofix env ~chk:true cofix; + check_cofix env ~flags:{Declarations.check_guarded=true} cofix; make_judge (mkCoFix cofix) tys.(i) | Sort (Prop c) -> |