adapt to coq/coq#19300

gares · Jul 5, 2024 · cea331c · cea331c
1 parent 55e6039
commit cea331c
Show file tree

Hide file tree

Showing 3 changed files with 19 additions and 3 deletions.
diff --git a/src/coq_elpi_arg_syntax.mlg b/src/coq_elpi_arg_syntax.mlg
@@ -220,6 +220,16 @@ GRAMMAR EXTEND Gram
     [ [ any_kwd -> { !the_kwd }] ];
 END
 
+{
+
+[%%if coq = "8.19" || coq = "8.20"]
+let mkAttributesFlagQualid q = Attributes.FlagIdent (Names.Id.to_string (Libnames.qualid_basename q)) 
+[%%else]
+let mkAttributesFlagQualid q = Attributes.FlagQualid q
+[%%endif]
+
+}
+
 ARGUMENT EXTEND attributes
   PRINTED BY { pr_attributes } 
 END
@@ -236,7 +246,7 @@ GRAMMAR EXTEND Gram GLOBAL: attributes;
   ;
   my_attr_value:
     [ [ "=" ; v = string -> { Attributes.VernacFlagLeaf (Attributes.FlagString v) }
-      | "=" ; v = IDENT -> { Attributes.VernacFlagLeaf (Attributes.FlagIdent v) }
+      | "=" ; v = qualid -> { Attributes.VernacFlagLeaf (mkAttributesFlagQualid v) }
       | "(" ; a = my_attribute_list ; ")" -> { Attributes.VernacFlagList a }
       | -> { Attributes.VernacFlagEmpty } ]
     ]

diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
@@ -931,9 +931,13 @@ let eval_of_constant c =
 let eval_to_oeval = Evaluable.to_kevaluable
 let mkCLocalAssum x y z = Constrexpr.CLocalAssum(x,None,y,z)
 let pattern_of_glob_constr env g = Patternops.pattern_of_glob_constr env g
-let warns_of_options options = options.user_warns
 [%%endif]
 
+[%%if coq = "8.20"]
+let warns_of_options options = options.user_warns
+[%%elif coq <> "8.19"]
+let warns_of_options options = options.user_warns |> Option.map UserWarn.with_empty_qf
+[%%endif]
 let add_axiom_or_variable api id ty local options state =
   let state, poly, cumul, udecl, _ = poly_cumul_udecl_variance_of_options state options in
   let used = universes_of_term state ty in

diff --git a/src/coq_elpi_vernacular.ml b/src/coq_elpi_vernacular.ml
@@ -33,7 +33,9 @@ let atts2impl loc phase ~depth state atts q =
   and convert_att att = convert_att_r att.CAst.v
   and convert_atts l = List.map convert_att l
   and convert_att_value = function
-    Attributes.FlagIdent s | Attributes.FlagString s -> AttributeString s
+    | Attributes.FlagIdent s [@if coq = "8.19" || coq = "8.20"] -> AttributeString s
+    | Attributes.FlagQualid q [@if coq <> "8.19" && coq <> "8.20"] -> AttributeString (Libnames.string_of_qualid q)
+    | Attributes.FlagString s -> AttributeString s
   in
   let phase = match phase with Summary.Stage.Interp -> "interp" | Summary.Stage.Synterp -> "synterp" in
   let atts =