diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 65f5b3fd0..b6a57785a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -72,17 +72,14 @@ open Inductiveops exception Found of int array -(* spiwack: I chose [tflags] rather than [flags], like in the rest of - the code, for the argument name to avoid interference with the - argument for [inference_flags] also used in this module. *) -let search_guard ~tflags loc env possible_indexes fixdefs = +let search_guard loc env possible_indexes fixdefs = (* Standard situation with only one possibility for each fix. *) (* We treat it separately in order to get proper error msg. *) let is_singleton = function [_] -> true | _ -> false in 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 ~flags:tflags fix + (try check_fix env fix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in @@ -101,7 +98,10 @@ let search_guard ~tflags loc env possible_indexes fixdefs = will be chosen). A more robust solution may be to raise an error when totality is assumed but the strutural argument is not specified. *) - try check_fix env ~flags:Declareops.safe_flags fix; raise (Found indexes) + try + let flags = { (typing_flags env) with Declarations.check_guarded = true } in + let env = Environ.set_typing_flags flags env in + check_fix env fix; raise (Found indexes) with TypeError _ -> ()) (List.combinations possible_indexes); let errmsg = "Cannot guess decreasing argument of fix." in @@ -617,13 +617,12 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ let fixdecls = (names,ftys,fdefs) in let indexes = search_guard - ~tflags:Declareops.safe_flags loc env possible_indexes fixdecls in make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i) | GCoFix i -> let cofix = (i,(names,ftys,fdefs)) in - (try check_cofix env ~flags:Declareops.safe_flags cofix + (try check_cofix env cofix with reraise -> let (e, info) = Errors.push reraise in let info = Loc.add_loc info loc in |