diff options
author | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-26 11:24:16 +0200 |
---|---|---|
committer | Arnaud Spiwack <arnaud@spiwack.net> | 2015-06-26 11:24:16 +0200 |
commit | 576d7a815174106f337fca2f19ad7f26a7e87cc4 (patch) | |
tree | 4679e39132853febe84670f5c039fc4608418496 /pretyping/pretyping.ml | |
parent | 42b7e36ddb68f53ada686900e5a98435d9ff7fde (diff) |
Add a flag to deactivate guard checking in the kernel.
Diffstat (limited to 'pretyping/pretyping.ml')
-rw-r--r-- | pretyping/pretyping.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 03fe2122c..d9f490ba5 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -75,7 +75,7 @@ let search_guard loc env possible_indexes fixdefs = if List.for_all is_singleton possible_indexes then let indexes = Array.of_list (List.map List.hd possible_indexes) in let fix = ((indexes, 0),fixdefs) in - (try check_fix env fix + (try check_fix env ~chk:true fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -88,7 +88,7 @@ let search_guard loc env possible_indexes fixdefs = (fun l -> let indexes = Array.of_list l in let fix = ((indexes, 0),fixdefs) in - try check_fix env fix; raise (Found indexes) + try check_fix env ~chk:true fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -537,7 +537,7 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env cofix + (try check_cofix env ~chk:true cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in |