diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index fb308fd3163b..1e95d5c68bfd 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -161,6 +161,8 @@ let () = let open Goptions in
 let program =
   enable_attribute ~key:"program" ~default:(fun () -> !program_mode)
 
+let guard_check = bool_attribute ~name:"Guard Checking" ~on:"guard" ~off:"unguard"
+
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
 let option_locality =
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 51bab79938bb..010fb1a91d0c 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -45,6 +45,7 @@ end
 
 val polymorphic : bool attribute
 val program : bool attribute
+val guard_check : bool option attribute
 val template : bool option attribute
 val locality : bool option attribute
 val option_locality : Goptions.option_locality attribute
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 9a1d935928d9..dede4334d17c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1997,12 +1997,22 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
   | VernacInductive (finite, l) ->
     VtDefault(fun () -> vernac_inductive ~atts finite l)
   | VernacFixpoint (discharge, l) ->
+    let (atts, guard) = parse_with_extra guard_check atts in
+    let with_guard_check f _ =
+      match guard with
+      | Some b ->
+        let before = (Global.typing_flags ()).Declarations.check_guarded in
+        Global.set_check_guarded b;
+        let res = f () in
+        Global.set_check_guarded before;
+        res
+      | _ -> f () in
     let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
     if opens then
-      VtOpenProof (fun () ->
+      VtOpenProof (with_guard_check @@ fun _ ->
         with_def_attributes ~atts vernac_fixpoint_interactive discharge l)
     else
-      VtDefault (fun () ->
+      VtDefault (with_guard_check @@ fun _ ->
         with_def_attributes ~atts vernac_fixpoint discharge l)
   | VernacCoFixpoint (discharge, l) ->
     let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in