From 99944c675dc1cd79b0f6263536c57b536f2249a7 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 3 Nov 2023 19:37:57 +0100 Subject: [PATCH] Removing superfluous poly flag for coercions. --- src/coq_elpi_builtins.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/coq_elpi_builtins.ml b/src/coq_elpi_builtins.ml index a864eea4c..fc1f6d253 100644 --- a/src/coq_elpi_builtins.ml +++ b/src/coq_elpi_builtins.ml @@ -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);