Skip to content

Commit

Permalink
Removing superfluous poly flag for coercions.
Browse files Browse the repository at this point in the history
  • Loading branch information
herbelin committed Nov 3, 2023
1 parent 7075a45 commit 99944c6
Showing 1 changed file with 2 additions and 3 deletions.
5 changes: 2 additions & 3 deletions src/coq_elpi_builtins.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down

0 comments on commit 99944c6

Please sign in to comment.