Moving the typing_flags to the environment.

4 files changed, 12 insertions, 13 deletions

diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index 1d77204543..403dcfd1a3 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -592,9 +592,9 @@ let type_of_projection_knowing_arg env sigma p c ty =
 let control_only_guard env c =
   let check_fix_cofix e c = match kind_of_term c with
     | CoFix (_,(_,_,_) as cofix) ->
-      Inductive.check_cofix ~flags:Declareops.safe_flags e cofix
+      Inductive.check_cofix e cofix
     | Fix (_,(_,_,_) as fix) ->
-      Inductive.check_fix ~flags:Declareops.safe_flags e fix
+      Inductive.check_fix e fix
     | _ -> ()
   in
   let rec iter env c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 65f5b3fd0f..b6a57785a1 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
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 2c02b4a217..824bb11aa4 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -22,7 +22,7 @@ open Misctypes
 
 (** An auxiliary function for searching for fixpoint guard indexes *)
 
-val search_guard : tflags:Declarations.typing_flags ->
+val search_guard :
   Loc.t -> env -> int list list -> rec_declaration -> int array
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index f03e6c6e96..52afa7f83a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -189,13 +189,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 ~flags:Declareops.safe_flags fix;
+        check_fix env 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 ~flags:Declareops.safe_flags cofix;
+        check_cofix env cofix;
 	make_judge (mkCoFix cofix) tys.(i)
 
     | Sort (Prop c) ->