Add a flag in `VernacFixpoint` and `VernacCoFixpoint` to control assuming guardedness.

10 files changed, 42 insertions, 27 deletions

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 5fff21e27..ba9ac16b6 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -307,8 +307,10 @@ type vernac_expr =
       bool (*[false] => assume positive*) *
       private_flag * inductive_flag * (inductive_expr * decl_notation list) list
   | VernacFixpoint of
+      bool * (* [false] => assume guarded *)
       locality option * (fixpoint_expr * decl_notation list) list
   | VernacCoFixpoint of
+      bool * (* [false] => assume guarded *)
       locality option * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 25e679ba8..b71028942 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -214,13 +214,13 @@ GEXTEND Gram
 	  let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
           VernacInductive (check_positivity a,priv,f,indl)
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (None, recs)
+          VernacFixpoint (true,None, recs)
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
-          VernacFixpoint (Some Discharge, recs)
+          VernacFixpoint (true,Some Discharge, recs)
       | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (None, corecs)
+          VernacCoFixpoint (true,None, corecs)
       | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" ->
-          VernacCoFixpoint (Some Discharge, corecs)
+          VernacCoFixpoint (true,Some Discharge, corecs)
       | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l
       | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from";
 	      l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 61f03d6f2..53ec304cc 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function
            | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
          match
            Vernac_classifier.classify_vernac
-             (Vernacexpr.VernacFixpoint(None, List.map snd recsl))
+             (Vernacexpr.VernacFixpoint(true,None, List.map snd recsl))
          with
          | Vernacexpr.VtSideff ids, _ when hard ->
              Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 5dcb0c043..5c849ba41 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -399,7 +399,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
        in
        evd,List.rev rev_pconstants
     | _ ->
-       Command.do_fixpoint Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
+       Command.do_fixpoint ~chkguard:true Global (Flags.is_universe_polymorphism ()) fixpoint_exprl;
        let evd,rev_pconstants =
 	 List.fold_left
 	   (fun (evd,l) (((_,fname),_,_,_,_),_) ->
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index a65bfd44d..93cd35472 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -399,6 +399,15 @@ module Make
     | None -> mt ()
     | Some i -> spc () ++ str "|" ++ spc () ++ int i
 
+  let pr_assume ?(positive=false) ?(guarded=false) () =
+    let assumed =
+      (if guarded then [str"Guarded"] else []) @
+      (if positive then [str"Positive"] else [])
+    in
+    match assumed with
+    | [] -> mt ()
+    | l -> keyword"Assume" ++ spc() ++ str"[" ++ prlist (fun x->x) l ++ str"]" ++ spc()
+
 (**************************************)
 (* Pretty printer for vernac commands *)
 (**************************************)
@@ -797,7 +806,7 @@ module Make
               (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
           )
 
-        | VernacFixpoint (local, recs) ->
+        | VernacFixpoint (chkguard,local, recs) ->
           let local = match local with
             | Some Discharge -> "Let "
             | Some Local -> "Local "
@@ -812,11 +821,11 @@ module Make
                 prlist (pr_decl_notation pr_constr) ntn
           in
           return (
-            hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++
+            hov 0 (pr_assume ~guarded:chkguard ()++str local ++ keyword "Fixpoint" ++ spc () ++
                      prlist_with_sep (fun _ -> fnl () ++ keyword "with" ++ spc ()) pr_onerec recs)
           )
 
-        | VernacCoFixpoint (local, corecs) ->
+        | VernacCoFixpoint (chkguard,local, corecs) ->
           let local = match local with
             | Some Discharge -> keyword "Let" ++ spc ()
             | Some Local -> keyword "Local" ++ spc ()
@@ -829,7 +838,7 @@ module Make
               prlist (pr_decl_notation pr_constr) ntn
           in
           return (
-            hov 0 (local ++ keyword "CoFixpoint" ++ spc() ++
+            hov 0 (pr_assume ~guarded:chkguard ()++local ++ keyword "CoFixpoint" ++ spc() ++
                      prlist_with_sep (fun _ -> fnl() ++ keyword "with" ++ spc ()) pr_onecorec corecs)
           )
         | VernacScheme l ->
diff --git a/stm/texmacspp.ml b/stm/texmacspp.ml
index 4cc362dda..4f014be2d 100644
--- a/stm/texmacspp.ml
+++ b/stm/texmacspp.ml
@@ -598,14 +598,14 @@ let rec tmpp v loc =
             (fun (ie, dnl) -> (pp_inductive_expr ie) @
                               (List.map pp_decl_notation dnl)) iednll) in
       xmlInductive kind loc exprs
-  | VernacFixpoint (_, fednll) ->
+  | VernacFixpoint (_,_, fednll) ->
       let exprs =
         List.flatten (* should probably not be flattened *)
           (List.map
             (fun (fe, dnl) -> (pp_fixpoint_expr fe) @
                               (List.map pp_decl_notation dnl)) fednll) in
       xmlFixpoint exprs
-  | VernacCoFixpoint (_, cfednll) ->
+  | VernacCoFixpoint (_,_, cfednll) ->
       (* Nota: it is like VernacFixpoint without so could be merged *)
       let exprs =
         List.flatten (* should probably not be flattened *)
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 03ade646b..574cc0044 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -125,14 +125,14 @@ let rec classify_vernac e =
           CList.map_filter (function (Some(_,i), _) -> Some i | _ -> None) l in
         VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
     | VernacGoal _ -> VtStartProof ("Classic",GuaranteesOpacity,[]), VtLater
-    | VernacFixpoint (_,l) ->
+    | VernacFixpoint (_,_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
         if open_proof
         then VtStartProof ("Classic",GuaranteesOpacity,ids), VtLater
         else VtSideff ids, VtLater
-    | VernacCoFixpoint (_,l) ->
+    | VernacCoFixpoint (_,_,l) ->
         let ids, open_proof =
           List.fold_left (fun (l,b) (((_,id),_,_,p),_) ->
             id::l, b || p = None) ([],false) l in
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 06d7c629a..14a1efe4d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1044,7 +1044,7 @@ let interp_cofixpoint l ntns =
   check_recursive false  env evd fix;
   fix,Evd.evar_universe_context evd,info
     
-let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
+let declare_fixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexes ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1080,7 +1080,7 @@ let declare_fixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) indexe
   (* Declare notations *)
   List.iter Metasyntax.add_notation_interpretation ntns
 
-let declare_cofixpoint local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
+let declare_cofixpoint ~chkguard local poly ((fixnames,fixdefs,fixtypes),ctx,fiximps) ntns =
   if List.exists Option.is_empty fixdefs then
     (* Some bodies to define by proof *)
     let thms =
@@ -1202,19 +1202,19 @@ let do_program_fixpoint local poly l =
 	errorlabstrm "do_program_fixpoint"
 	  (str "Well-founded fixpoints not allowed in mutually recursive blocks")
 
-let do_fixpoint local poly l =
+let do_fixpoint ~chkguard local poly l =
   if Flags.is_program_mode () then do_program_fixpoint local poly l
   else
     let fixl, ntns = extract_fixpoint_components true l in
     let fix = interp_fixpoint fixl ntns in
     let possible_indexes =
       List.map compute_possible_guardness_evidences (pi3 fix) in
-    declare_fixpoint local poly fix possible_indexes ntns
+    declare_fixpoint ~chkguard local poly fix possible_indexes ntns
 
-let do_cofixpoint local poly l =
+let do_cofixpoint ~chkguard local poly l =
   let fixl,ntns = extract_cofixpoint_components l in
     if Flags.is_program_mode () then
       do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns
     else
       let cofix = interp_cofixpoint fixl ntns in
-	declare_cofixpoint local poly cofix ntns
+	declare_cofixpoint ~chkguard local poly cofix ntns
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 3ec65b487..7112591fe 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -146,12 +146,14 @@ val interp_cofixpoint :
 (** Registering fixpoints and cofixpoints in the environment *)
 
 val declare_fixpoint :
+  chkguard:bool ->
   locality -> polymorphic ->
   recursive_preentry * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   lemma_possible_guards -> decl_notation list -> unit
 
-val declare_cofixpoint : locality -> polymorphic -> 
+val declare_cofixpoint :
+  chkguard:bool -> locality -> polymorphic ->
   recursive_preentry * Evd.evar_universe_context * 
   (Name.t list * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
@@ -159,9 +161,11 @@ val declare_cofixpoint : locality -> polymorphic ->
 (** Entry points for the vernacular commands Fixpoint and CoFixpoint *)
 
 val do_fixpoint :
+  chkguard:bool -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (fixpoint_expr * decl_notation list) list -> unit
 
 val do_cofixpoint :
+  chkguard:bool -> (* When [false], assume guarded. *)
   locality -> polymorphic -> (cofixpoint_expr * decl_notation list) list -> unit
 
 (** Utils *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index c925719fb..a0af1d573 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -578,17 +578,17 @@ let vernac_inductive chk poly lo finite indl =
     let indl = List.map unpack indl in
     do_mutual_inductive chk indl poly lo finite
 
-let vernac_fixpoint locality poly local l =
+let vernac_fixpoint ~chkguard locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_fixpoint local poly l
+  do_fixpoint ~chkguard local poly l
 
-let vernac_cofixpoint locality poly local l =
+let vernac_cofixpoint ~chkguard locality poly local l =
   let local = enforce_locality_exp locality local in
   if Dumpglob.dump () then
     List.iter (fun ((lid, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l;
-  do_cofixpoint local poly l
+  do_cofixpoint ~chkguard local poly l
 
 let vernac_scheme l =
   if Dumpglob.dump () then
@@ -1895,8 +1895,8 @@ let interp ?proof locality poly c =
   | VernacExactProof c -> vernac_exact_proof c
   | VernacAssumption (stre,nl,l) -> vernac_assumption locality poly stre l nl
   | VernacInductive (chk,priv,finite,l) -> vernac_inductive chk poly priv finite l
-  | VernacFixpoint (local, l) -> vernac_fixpoint locality poly local l
-  | VernacCoFixpoint (local, l) -> vernac_cofixpoint locality poly local l
+  | VernacFixpoint (chkguard,local, l) -> vernac_fixpoint ~chkguard locality poly local l
+  | VernacCoFixpoint (chkguard,local, l) -> vernac_cofixpoint ~chkguard locality poly local l
   | VernacScheme l -> vernac_scheme l
   | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l
   | VernacUniverse l -> vernac_universe l