Add @no-coercion! option and macro

Author: Jan-Oliver Kaiser

builtin-doc/coq-builtin.elpi

@@ -480,6 +480,7 @@ macro @keep-alg-univs! :- get-option "coq:keepalgunivs" tt.
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @reversible! :- get-option "coq:reversible" tt. % coercions
 macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference 
+macro @no-coercion! :- get-option "coq:no_coercion" tt. % ignore coercions during pretyping
 
 macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance
 

elpi/coq-HOAS.elpi

@@ -308,6 +308,7 @@ macro @keep-alg-univs! :- get-option "coq:keepalgunivs" tt.
 macro @primitive! :- get-option "coq:primitive" tt. % primitive records
 macro @reversible! :- get-option "coq:reversible" tt. % coercions
 macro @no-tc! :- get-option "coq:no_tc" tt. % skip typeclass inference 
+macro @no-coercion! :- get-option "coq:no_coercion" tt. % ignore coercions during pretyping
 
 macro @uinstance! I :- get-option "coq:uinstance" I. % universe instance
 

src/rocq_elpi_HOAS.ml

@@ -311,6 +311,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  no_coercion: bool option;
   algunivs : bool option;
 }
 let default_options () = {
@@ -330,15 +331,16 @@ let default_options () = {
   keepunivs = None;
   redflags = None;
   no_tc = None;
+  no_coercion = None;
   algunivs = None;
 }
 let make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
   ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs
-  ~redflags ~no_tc ~algunivs =
+  ~redflags ~no_tc ~no_coercion ~algunivs =
   let user_warns = Some UserWarn.{ depr; warn } in
   { hoas_holes; local; user_warns; primitive; failsafe; ppwidth; pp;
     pplevel; using; inline; uinstance; universe_decl; reversible; keepunivs;
-    redflags; no_tc; algunivs; }
+    redflags; no_tc; no_coercion; algunivs; }
 let make_warn = UserWarn.make_warn
 
 type 'a coq_context = {
@@ -1314,12 +1316,13 @@ let get_options ~depth hyps state =
     let universe_decl = get_universe_decl () in
     let reversible = get_bool_option "coq:reversible" in
     let no_tc = get_bool_option "coq:no_tc" in
+    let no_coercion = get_bool_option "coq:no_coercion" in
     let keepunivs = get_bool_option "coq:keepunivs" in
     let redflags = get_redflags_option () in
     let algunivs = get_bool_option "coq:keepalgunivs" in
     make_options ~hoas_holes ~local ~warn ~depr ~primitive ~failsafe ~ppwidth
       ~pp ~pplevel ~using ~inline ~uinstance ~universe_decl ~reversible ~keepunivs
-      ~redflags ~no_tc ~algunivs
+      ~redflags ~no_tc ~no_coercion ~algunivs
 let mk_coq_context ~options state =
   let env = get_global_env state in
   let section = section_ids env in

src/rocq_elpi_HOAS.mli

@@ -48,6 +48,7 @@ type options = {
   keepunivs : bool option;
   redflags : RedFlags.reds option;
   no_tc: bool option;
+  no_coercion: bool option;
   algunivs : bool option;
 }
 

src/rocq_elpi_builtins.ml

@@ -3608,7 +3608,9 @@ Supported attributes:
 - @keepunivs! (default false, do not disregard universe levels)
 - @no-tc! (default false, do not infer typeclasses) |}))))),
   (fun gt ety _ diag ~depth proof_context _ state ->
-    let flags = if proof_context.options.no_tc = Some true then {(Pretyping.default_inference_flags false) with  use_typeclasses = NoUseTC} else Pretyping.default_inference_flags false in
+    let flags = Pretyping.default_inference_flags false in
+    let flags = if proof_context.options.no_tc = Some true then {flags with use_typeclasses = NoUseTC} else flags in
+    let flags = if proof_context.options.no_coercion = Some true then {flags with use_coercions = false} else flags in
     try
       let sigma = get_sigma state in
       let ety_given, expected_type =
@@ -3655,7 +3657,9 @@ Supported attributes:
   (fun gt es _ diag ~depth proof_context _ state ->
     try
       let sigma = get_sigma state in
-      let flags = if proof_context.options.no_tc = Some true then {(Pretyping.default_inference_flags false) with  use_typeclasses = NoUseTC} else Pretyping.default_inference_flags false in
+      let flags = Pretyping.default_inference_flags false in
+      let flags = if proof_context.options.no_tc = Some true then {flags with use_typeclasses = NoUseTC} else flags in
+      let flags = if proof_context.options.no_coercion = Some true then {flags with use_coercions = false} else flags in
       let expected_type = Pretyping.IsType in
       let sigma = Evd.push_future_goals sigma in
       let sigma, uj_val, uj_type =