Merge pull request #1060 from Yann-Leray/rewrite-rules-adapt

Adapt to coq/coq#18038 (rewrite rules)
MetaCoq · Feb 21, 2024 · be825a7 · be825a7
2 parents 25effb8 + 61e75d2
commit be825a7
Show file tree

Hide file tree

Showing 3 changed files with 10 additions and 0 deletions.
diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml
@@ -195,6 +195,7 @@ let quote_module ~(include_functor : bool) ~(include_submodule : bool) ~(include
           match field with
           | SFBconst _ -> [GlobRef.ConstRef (Constant.make2 mp label)]
           | SFBmind _ -> [GlobRef.IndRef (MutInd.make2 mp label, 0)]
+          | SFBrules _ -> failwith "Rewrite rules are not supported by TemplateCoq"
           | SFBmodule mb -> if include_submodule then aux mb.mod_type mb.mod_mp else []
           | SFBmodtype mtb -> if include_submodtype then aux mtb.mod_type mtb.mod_mp else []
         in

diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
@@ -30,6 +30,10 @@ let make_warning_if_not_exist w =
 let warn_primitive_turned_into_axiom =
   CWarnings.create_in (make_warning_if_not_exist "primitive-turned-into-axiom")
           Pp.(fun prim -> str "Quoting primitive " ++ str prim ++ str " into an axiom.")
+
+let warn_symbol_turned_into_axiom =
+  CWarnings.create_in (make_warning_if_not_exist "symbol-turned-into-axiom")
+          Pp.(fun prim -> str "Quoting symbol " ++ str prim ++ str " into an axiom.")
 let warn_ignoring_private_polymorphic_universes =
   CWarnings.create_in (make_warning_if_not_exist "private-polymorphic-universes-ignored")
           Pp.(fun () -> str "Ignoring private polymorphic universes.")
@@ -522,6 +526,9 @@ struct
               | Primitive t ->
                   warn_primitive_turned_into_axiom (CPrimitives.to_string t);
                   None
+              | Symbol _ ->
+                  warn_symbol_turned_into_axiom (Constant.debug_to_string c);
+                  None
               | Def cs -> Some cs
               | OpaqueDef lc ->
                 if bypass then
@@ -651,6 +658,7 @@ since  [absrt_info] is a private type *)
         then Some (quote_term env evm (fst (Global.force_proof Library.indirect_accessor cs)))
         else None
       | Primitive _ -> failwith "Primitive types not supported by TemplateCoq"
+      | Symbol _ -> failwith "Symbols are not supported by TemplateCoq"
     in
     (ty, body)
 

diff --git a/template-coq/src/run_extractable.ml b/template-coq/src/run_extractable.ml
@@ -125,6 +125,7 @@ let get_constant_body b =
     (* FIXME delayed univs skipped *)
     Some proof
   | Primitive _ -> failwith "Primitives not supported by TemplateCoq"
+  | Symbol _ -> failwith "Symbols are not supported by TemplateCoq"
 
 (* note(gmm): code taken from quoter.ml (quote_entry_aux) *)
 let of_constant_body (env : Environ.env) (cd : Plugin_core.constant_body) : Ast0.Env.constant_body =