From 9bb2338da402e94f1bed606af665c35696736f95 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Fri, 3 Nov 2023 19:37:57 +0100
Subject: [PATCH] Removing superfluous poly flag for try_add_new_coercion and
 declare_axiom.

---
 elpi-builtin.elpi        | 2 +-
 src/coq_elpi_builtins.ml | 7 +++----
 2 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/elpi-builtin.elpi b/elpi-builtin.elpi
index 2b0186ec6..c3dc18f8f 100644
--- a/elpi-builtin.elpi
+++ b/elpi-builtin.elpi
@@ -55,7 +55,7 @@ not _.
 
 % [declare_constraint C Key1 Key2...] declares C blocked
 % on Key1 Key2 ... (variables, or lists thereof).
-external type declare_constraint any -> any -> variadic any prop.
+external type declare_constraint variadic any prop.
 
 external pred print_constraints. % prints all constraints
 
diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml
index a864eea4c..600aa64a0 100644
--- a/src/coq_elpi_builtins.ml
+++ b/src/coq_elpi_builtins.ml
@@ -875,7 +875,7 @@ let add_axiom_or_variable api id ty local options state =
       GlobRef.VarRef(Id.of_string id), Univ.Instance.empty
     end else begin
       Dumpglob.dump_definition variable false "ax";
-      ComAssumption.declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~poly:false ~kind (EConstr.to_constr sigma ty)
+      ComAssumption.declare_axiom Vernacexpr.NoCoercion ~local:Locality.ImportDefaultBehavior ~kind (EConstr.to_constr sigma ty)
         uentry impargs options.inline
         variable
     end
@@ -2750,15 +2750,14 @@ NParams can always be omitted, since it is inferred.
 - @reversible! (default: false)|})),
   (fun (gr, _, source, target) ~depth { options } _ -> grab_global_env "coq.coercion.declare" (fun state ->
      let local = options.local <> Some false in
-     let poly = false in
      let reversible = options.reversible = Some true in
      begin match source, target with
      | B.Given source, B.Given target ->
         let source = ComCoercion.class_of_global source in
-        ComCoercion.try_add_new_coercion_with_target gr ~local ~poly
+        ComCoercion.try_add_new_coercion_with_target gr ~local
           ~reversible ~source ~target
      | _, _ ->
-        ComCoercion.try_add_new_coercion gr ~local ~poly ~reversible
+        ComCoercion.try_add_new_coercion gr ~local ~reversible
      end;
      state, (), []))),
   DocAbove);