diff options
| author | Emilio Jesus Gallego Arias | 2019-06-22 01:53:08 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-06-24 20:55:38 +0200 |
| commit | c2abcaefd796b7f430f056884349b9d959525eec (patch) | |
| tree | e73aa6302fdb07bbb10af3de7de0254c3f1d4d35 /vernac | |
| parent | 5f190f9e12f42a0ff6b5275c8087852a87aff47b (diff) | |
[proof] Remove last case of optional `?poly` arguments.
As noted in GitHub discussion, it is a good idea to make `poly` always
explicit, this PR does remove last case of `?(poly=false)` in the
codebase.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 6 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 2 |
2 files changed, 4 insertions, 4 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 38852992e4..8b98408c5e 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -694,7 +694,7 @@ let make_bl_scheme mode mind = let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let bl_goal = EConstr.of_constr bl_goal in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx bl_goal + let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal (compute_bl_tact mode (!bl_scheme_kind_aux()) (ind, EConstr.EInstance.empty) lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -824,7 +824,7 @@ let make_lb_scheme mode mind = let ctx = UState.make (Global.universes ()) in let side_eff = side_effect_of_mode mode in let lb_goal = EConstr.of_constr lb_goal in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx lb_goal + let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal (compute_lb_tact mode (!lb_scheme_kind_aux()) ind lnamesparrec nparrec) in ([|ans|], ctx), eff @@ -1001,7 +1001,7 @@ let make_eq_decidability mode mind = let lnonparrec,lnamesparrec = context_chop (nparams-nparrec) mib.mind_params_ctxt in let side_eff = side_effect_of_mode mode in - let (ans, _, ctx) = Pfedit.build_by_tactic ~side_eff (Global.env()) ctx + let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx (EConstr.of_constr (compute_dec_goal (ind,u) lnamesparrec nparrec)) (compute_dec_tact ind lnamesparrec nparrec) in diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 55fff432d5..dc46aad8af 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -574,7 +574,7 @@ let start_proof_and_print ~program_mode ~poly ?hook ~scope ~kind l = Evarutil.is_ground_term sigma concl) then raise Exit; let c, _, ctx = - Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) concl tac + Pfedit.build_by_tactic ~poly:false env (Evd.evar_universe_context sigma) concl tac in Evd.set_universe_context sigma ctx, EConstr.of_constr c with Logic_monad.TacticFailure e when Logic.catchable_exception e -> user_err Pp.(str "The statement obligations could not be resolved \ |