Alizter
commented
2 years ago Note that the following variations work:
Require Import Coq.Program.Tactics.
Class Progression : Type := {
next: Set;
}.
#[export, program]
Instance item_loaded_progression : Progression.Require Import Coq.Program.Tactics.
Record Progression : Type := {
next: Set;
}.
Existing Class Progression.
#[export]
Instance item_loaded_progression : Progression.So it seems to be a bad interaction with program and Existing Class.
Here is a backtrace:
item_loaded_progression has type-checked, generating 1 obligation
Solving obligations automatically...
Anomaly "Unable to handle arbitrary u+k <= v constraints."
Please report at http://coq.inria.fr/bugs/.
Raised at Exninfo.iraise in file "clib/exninfo.ml", line 79, characters 4-11
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Stdlib__list.fold_left in file "list.ml", line 121, characters 24-34
Called from Stdlib__set.Make.fold in file "set.ml", line 383, characters 34-55
Called from UState.process_universe_constraints in file "engine/uState.ml", line 296, characters 4-64
Called from UState.add_universe_constraints in file "engine/uState.ml", line 322, characters 27-66
Called from Evd.add_universe_constraints in file "engine/evd.ml", line 787, characters 23-68
Called from Evarsolve.refresh_universes.refresh_sort in file "pretyping/evarsolve.ml", line 125, characters 11-40
Called from Evarsolve.refresh_universes in file "pretyping/evarsolve.ml", line 198, characters 26-62
Called from Ltac_plugin__Tacinterp.interp_may_eval in file "plugins/ltac/tacinterp.ml", line 790, characters 23-70
Called from Ltac_plugin__Tacinterp.interp_constr_may_eval in file "plugins/ltac/tacinterp.ml", line 808, characters 6-51
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.interp_constr_may_eval in file "plugins/ltac/tacinterp.ml", line 815, characters 6-28
Called from Ltac_plugin__Tacinterp.interp_tacarg.(fun) in file "plugins/ltac/tacinterp.ml", line 1303, characters 31-69
Called from Proofview.V82.wrap_exceptions in file "engine/proofview.ml", line 1274, characters 8-12
Called from Logic_monad.BackState.(>>=).(fun) in file "engine/logic_monad.ml", line 192, characters 38-43
Called from Logic_monad.BackState.split.(fun) in file "engine/logic_monad.ml", line 260, characters 6-27
Called from Logic_monad.NonLogical.(>>=).(fun) in file "engine/logic_monad.ml", line 67, characters 36-42
Called from Logic_monad.NonLogical.(>>=).(fun) in file "engine/logic_monad.ml", line 67, characters 36-42
Called from Logic_monad.NonLogical.run in file "engine/logic_monad.ml", line 117, characters 8-12
Called from Proofview.apply in file "engine/proofview.ml", line 234, characters 12-42
Called from Proof.run_tactic in file "proofs/proof.ml", line 381, characters 4-49
Called from Proof.solve in file "proofs/proof.ml", line 500, characters 31-52
Called from Declare.Proof.map_fold in file "vernac/declare.ml", line 1443, characters 37-46
Called from Declare.Proof.build_constant_by_tactic in file "vernac/declare.ml", line 1797, characters 19-28
Called from Declare.Proof.build_by_tactic in file "vernac/declare.ml", line 1809, characters 25-81
Called from Declare.Obls.solve_by_tac in file "vernac/declare.ml", line 2273, characters 6-61
Called from Declare.Obls.solve_and_declare_by_tac in file "vernac/declare.ml", line 2291, characters 8-35
Called from Declare.Obls.solve_prg_obligations.(fun) in file "vernac/declare.ml", line 2367, characters 16-55
Called from CArray.fold_left_i.fold in file "clib/cArray.ml", line 233, characters 56-74
Called from Declare.Obls.solve_prg_obligations in file "vernac/declare.ml", line 2364, characters 4-337
Called from Declare.Obls.add_definition in file "vernac/declare.ml", line 2484, characters 18-63
Called from Classes.declare_instance_program in file "vernac/classes.ml", line 405, characters 4-65
Called from Classes.do_instance_program in file "vernac/classes.ml", line 565, characters 4-88
Called from Classes.new_instance_program in file "vernac/classes.ml", line 621, characters 4-120
Called from Vernacentries.vernac_instance_program in file "vernac/vernacentries.ml", line 1385, characters 16-85
Called from Vernacextend.vtmodifyprogram.(fun) in file "vernac/vernacextend.ml", line 191, characters 29-34
Called from Vernacinterp.interp_typed_vernac in file "vernac/vernacinterp.ml", line 20, characters 20-113
Called from Vernacinterp.interp_control.(fun) in file "vernac/vernacinterp.ml", line 201, characters 24-69
Called from Flags.with_modified_ref in file "lib/flags.ml", line 17, characters 14-17
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernacinterp.interp_gen.(fun) in file "vernac/vernacinterp.ml", line 251, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 249, characters 6-279
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach.(fun) in file "stm/stm.ml", line 2178, characters 16-43
Called from Stm.State.define in file "stm/stm.ml", line 964, characters 6-10
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.Reach.known_state.reach in file "stm/stm.ml", line 2320, characters 4-105
Called from Stm.observe in file "stm/stm.ml", line 2421, characters 4-60
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Stm.finish in file "stm/stm.ml", line 2432, characters 12-50
Called from Dune__exe__Idetop.goals in file "ide/coqide/idetop.ml", line 216, characters 13-28
Called from Dune__exe__Idetop.eval_call.interruptible in file "ide/coqide/idetop.ml", line 471, characters 12-15
Called from Xmlprotocol.abstract_eval_call in file "ide/coqide/protocol/xmlprotocol.ml", line 759, characters 29-46
Description of the problem
Coq Version