Allow `Pretyping.search_guard` to not check guard

This is a minimal modification to the pretyping interface which allows
for toplevel fixed points to be accepted by the pretyper.

Toplevel co-fixed points are accepted without this. However (co-)fixed
point _nested_ inside a `Definition` or a `Fixpoint` are always checked
for guardedness by the pretyper.

2 files changed, 18 insertions, 5 deletions

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8fbcc8e5e7..c86a4e3e48 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -68,14 +68,17 @@ open Inductiveops
 
 exception Found of int array
 
-let search_guard loc env possible_indexes fixdefs =
+(* 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 =
   (* 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:{Declarations.check_guarded=true} fix
+    (try check_fix env ~flags:tflags fix
      with reraise ->
        let (e, info) = Errors.push reraise in
        let info = Loc.add_loc info loc in
@@ -87,7 +90,13 @@ let search_guard loc env possible_indexes fixdefs =
        List.iter
 	 (fun l ->
 	    let indexes = Array.of_list l in
-	    let fix = ((indexes, 0),fixdefs) in
+            let fix = ((indexes, 0),fixdefs) in
+            (* spiwack: We search for a unspecified structural
+               argument under the assumption that we need to check the
+               guardedness condition (otherwise the first inductive argument
+               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:{Declarations.check_guarded=true} fix; raise (Found indexes)
 	    with TypeError _ -> ())
 	 (List.combinations possible_indexes);
@@ -533,7 +542,11 @@ let rec pretype resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_var
 			     vn)
 	  in
 	  let fixdecls = (names,ftys,fdefs) in
-	  let indexes = search_guard loc env possible_indexes fixdecls in
+          let indexes =
+            search_guard
+              ~tflags:{Declarations.check_guarded=true}
+              loc env possible_indexes fixdecls
+          in
 	    make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	| GCoFix i ->
 	  let cofix = (i,(names,ftys,fdefs)) in
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 142b54513e..1ef3da1509 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 :
+val search_guard : tflags:Declarations.typing_flags ->
   Loc.t -> env -> int list list -> rec_declaration -> int array
 
 type typing_constraint = OfType of types | IsType | WithoutTypeConstraint