From 1f0f1ae93f757be8101d598f8aaf5b564bde9dcd Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 26 Nov 2020 21:32:37 +0100
Subject: [attributes] [typing] Rename `typing` to `bypass_check`

As discussed in the Coq meeting.
---
 vernac/attributes.ml | 15 ++++++++-------
 1 file changed, 8 insertions(+), 7 deletions(-)

(limited to 'vernac')

diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index 05d96a1165..37895d22f5 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -339,24 +339,25 @@ let uses_parser : string key_parser = fun orig args ->
 
 let using = attribute_of_list ["using",uses_parser]
 
-let process_typing_att ~typing_flags att enable =
+let process_typing_att ~typing_flags att disable =
+  let enable = not disable in
   match att with
   | "universes" ->
     { typing_flags with
       Declarations.check_universes = enable
     }
-  | "guarded" ->
+  | "guard" ->
     { typing_flags with
       Declarations.check_guarded = enable
     }
-  | "positive" ->
+  | "positivity" ->
     { typing_flags with
       Declarations.check_positive = enable
     }
   | att ->
     CErrors.user_err Pp.(str "Unknown “typing” attribute: " ++ str att)
 
-let process_typing_enable ~key = function
+let process_typing_disable ~key = function
   | VernacFlagEmpty | VernacFlagLeaf (FlagIdent "yes") ->
     true
   | VernacFlagLeaf (FlagIdent "no") ->
@@ -368,8 +369,8 @@ let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args -
   let rec flag_parser typing_flags = function
     | [] -> typing_flags
     | (typing_att, enable) :: rest ->
-      let enable = process_typing_enable ~key:typing_att enable in
-      let typing_flags = process_typing_att ~typing_flags typing_att enable in
+      let disable = process_typing_disable ~key:typing_att enable in
+      let typing_flags = process_typing_att ~typing_flags typing_att disable in
       flag_parser typing_flags rest
   in
   match args with
@@ -380,4 +381,4 @@ let typing_flags_parser : Declarations.typing_flags key_parser = fun orig args -
     CErrors.user_err Pp.(str "Ill-formed “typing” attribute: " ++ pr_vernac_flag_value att)
 
 let typing_flags =
-  attribute_of_list ["typing", typing_flags_parser]
+  attribute_of_list ["bypass_check", typing_flags_parser]
-- 
cgit v1.2.3