Jason Gross (Sep 23 2022 at 11:26): Jason Gross (Sep 23 2022 at 11:26):How suspicious is this backtrace if I'm messing around with Constr.Unsafe?
Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.
Raised at Environ.lookup_rel in file "kernel/environ.ml", line 152, characters 29-44
Called from EConstr.lookup_rel in file "engine/eConstr.ml" (inlined), line 850, characters 51-67
Called from Tacred.unsafe_reference_opt_value in file "pretyping/tacred.ml", line 139, characters 6-25
Called from Tacred.compute_consteval_direct in file "pretyping/tacred.ml", line 307, characters 8-48
Called from Tacred.compute_consteval in file "pretyping/tacred.ml", line 344, characters 8-46
Called from Tacred.red_elim_const in file "pretyping/tacred.ml", line 697, characters 12-40
Called from Tacred.whd_simpl_stack.redrec in file "pretyping/tacred.ml", line 814, characters 32-68
Called from Tacred.whd_simpl_orelse_delta_but_fix.redrec in file "pretyping/tacred.ml", line 1024, characters 32-59
Called from Tacred.whd_simpl_orelse_delta_but_fix in file "pretyping/tacred.ml", line 1042, characters 19-29
Called from Redexpr.e_red in file "tactics/redexpr.ml" (inlined), line 204, characters 29-40
Called from Redexpr.reduction_of_red_expr_val in file "tactics/redexpr.ml", line 245, characters 12-28
Called from Ltac2_plugin__Tac2tactics.eval_fun.(fun) in file "plugins/ltac2/tac2tactics.ml", line 280, characters 21-39
Called from Logic_monad.BackState.(>>=).(fun) in file "engine/logic_monad.ml", line 192, characters 38-43
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.refine_by_tactic in file "proofs/proof.ml", line 524, characters 8-30
Called from Ltac_plugin__Tacinterp.eval in file "plugins/ltac/tacinterp.ml", line 2204, characters 21-94
Called from Pretyping.Default.pretype_hole in file "pretyping/pretyping.ml", line 661, characters 21-78
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1370, characters 21-79
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 43-86
Called from Ltac_plugin__Tacinterp.catch_error_with_trace_loc in file "plugins/ltac/tacinterp.ml", line 192, characters 6-9
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 6-91
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.lifts.(fun) in file "plugins/ltac/tacinterp.ml", line 2114, characters 19-36
Called from Proofview.V82.wrap_exceptions in file "engine/proofview.ml", line 1274, characters 8-12
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Proof.run_tactic in file "proofs/proof.ml", line 381, characters 4-49
Called from Proof.refine_by_tactic in file "proofs/proof.ml", line 524, characters 8-30
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Proof.refine_by_tactic in file "proofs/proof.ml", line 528, characters 6-30
[...]
[...]
Called from Ltac_plugin__Tacinterp.eval in file "plugins/ltac/tacinterp.ml", line 2204, characters 21-94
Called from Pretyping.Default.pretype_hole in file "pretyping/pretyping.ml", line 661, characters 21-78
Called from Cases.build_leaf in file "pretyping/cases.ml", line 1298, characters 17-79
Called from Cases.compile.shift_problem in file "pretyping/cases.ml", line 1503, characters 25-41
Called from Cases.compile.shift_problem in file "pretyping/cases.ml", line 1503, characters 25-41
Called from Cases.compile_cases.compile_for_one_predicate in file "pretyping/cases.ml", line 2770, characters 25-55
Called from Cases.list_try_compile.aux in file "pretyping/cases.ml", line 82, characters 10-13
Called from Cases.compile_cases in file "pretyping/cases.ml", line 2779, characters 23-71
Called from Pretyping.Default.pretype_lambda in file "pretyping/pretyping.ml", line 958, characters 20-87
Called from Cases.build_leaf in file "pretyping/cases.ml", line 1298, characters 17-79
Called from Cases.compile.shift_problem in file "pretyping/cases.ml", line 1503, characters 25-41
Called from Cases.compile_cases.compile_for_one_predicate in file "pretyping/cases.ml", line 2770, characters 25-55
Called from Cases.list_try_compile.aux in file "pretyping/cases.ml", line 82, characters 10-13
Called from Cases.compile_cases in file "pretyping/cases.ml", line 2779, characters 23-71
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1370, characters 21-79
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 43-86
Called from Ltac_plugin__Tacinterp.catch_error_with_trace_loc in file "plugins/ltac/tacinterp.ml", line 192, characters 6-9
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 6-91
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.lifts.(fun) in file "plugins/ltac/tacinterp.ml", line 2114, characters 19-36
Called from Proofview.V82.wrap_exceptions in file "engine/proofview.ml", line 1274, characters 8-12
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Proof.run_tactic in file "proofs/proof.ml", line 381, characters 4-49
Called from Proof.refine_by_tactic in file "proofs/proof.ml", line 524, characters 8-30
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Proof.refine_by_tactic in file "proofs/proof.ml", line 528, characters 6-30
Called from Ltac_plugin__Tacinterp.eval in file "plugins/ltac/tacinterp.ml", line 2204, characters 21-94
Called from Pretyping.Default.pretype_hole in file "pretyping/pretyping.ml", line 661, characters 21-78
Called from Cases.build_leaf in file "pretyping/cases.ml", line 1298, characters 17-79
Called from Cases.compile.shift_problem in file "pretyping/cases.ml", line 1503, characters 25-41
Called from Cases.compile.shift_problem in file "pretyping/cases.ml", line 1503, characters 25-41
Called from Cases.compile_cases.compile_for_one_predicate in file "pretyping/cases.ml", line 2770, characters 25-55
Called from Cases.list_try_compile.aux in file "pretyping/cases.ml", line 82, characters 10-13
Called from Cases.compile_cases in file "pretyping/cases.ml", line 2779, characters 23-71
Called from Pretyping.Default.pretype_lambda in file "pretyping/pretyping.ml", line 958, characters 20-87
Called from Cases.build_leaf in file "pretyping/cases.ml", line 1298, characters 17-79
Called from Cases.compile.shift_problem in file "pretyping/cases.ml", line 1503, characters 25-41
Called from Cases.compile_cases.compile_for_one_predicate in file "pretyping/cases.ml", line 2770, characters 25-55
Called from Cases.list_try_compile.aux in file "pretyping/cases.ml", line 82, characters 10-13
Called from Cases.compile_cases in file "pretyping/cases.ml", line 2779, characters 23-71
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1370, characters 21-79
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 43-86
Called from Ltac_plugin__Tacinterp.catch_error_with_trace_loc in file "plugins/ltac/tacinterp.ml", line 192, characters 6-9
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 6-91
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.lifts.(fun) in file "plugins/ltac/tacinterp.ml", line 2114, characters 19-36
Called from Proofview.V82.wrap_exceptions in file "engine/proofview.ml", line 1274, characters 8-12
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Proof.run_tactic in file "proofs/proof.ml", line 381, characters 4-49
Called from Proof.refine_by_tactic in file "proofs/proof.ml", line 524, characters 8-30
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Proof.refine_by_tactic in file "proofs/proof.ml", line 528, characters 6-30
Called from Ltac_plugin__Tacinterp.eval in file "plugins/ltac/tacinterp.ml", line 2204, characters 21-94
Called from Pretyping.Default.pretype_hole in file "pretyping/pretyping.ml", line 661, characters 21-78
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1370, characters 21-79
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 43-86
Called from Ltac_plugin__Tacinterp.catch_error_with_trace_loc in file "plugins/ltac/tacinterp.ml", line 192, characters 6-9
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 6-91
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.lifts.(fun) in file "plugins/ltac/tacinterp.ml", line 2114, characters 19-36
Called from Proofview.V82.wrap_exceptions in file "engine/proofview.ml", line 1274, characters 8-12
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Proof.run_tactic in file "proofs/proof.ml", line 381, characters 4-49
Called from Proof.refine_by_tactic in file "proofs/proof.ml", line 524, characters 8-30
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Proof.refine_by_tactic in file "proofs/proof.ml", line 528, characters 6-30
Called from Ltac_plugin__Tacinterp.eval in file "plugins/ltac/tacinterp.ml", line 2204, characters 21-94
Called from Pretyping.Default.pretype_hole in file "pretyping/pretyping.ml", line 661, characters 21-78
Called from Pretyping.Default.pretype_lambda in file "pretyping/pretyping.ml", line 958, characters 20-87
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1370, characters 21-79
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 43-86
Called from Ltac_plugin__Tacinterp.catch_error_with_trace_loc in file "plugins/ltac/tacinterp.ml", line 192, characters 6-9
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 6-91
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.lifts.(fun) in file "plugins/ltac/tacinterp.ml", line 2114, characters 19-36
Called from Proofview.V82.wrap_exceptions in file "engine/proofview.ml", line 1274, characters 8-12
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
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 ComTactic.solve_core.(fun) in file "vernac/comTactic.ml", line 46, characters 23-59
Called from Declare.Proof.map_fold_endline in file "vernac/declare.ml", line 1457, characters 20-33
Called from ComTactic.solve_core in file "vernac/comTactic.ml", line 43, characters 23-442
Called from Vernacextend.vtmodifyproof.(fun) in file "vernac/vernacextend.ml", line 163, characters 32-47
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 203, 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 253, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 251, 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 2169, characters 20-47
Called from Stm.Reach.known_state.resilient_tactic in file "stm/stm.ml", line 2111, characters 10-14
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
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 Vernac.interp_vernac in file "toplevel/vernac.ml", line 68, characters 31-52
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
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 Flags.silently in file "lib/flags.ml" (inlined), line 64, characters 19-40
Called from Vernac.load_vernac_core.loop in file "toplevel/vernac.ml", line 112, characters 8-69
Called from Vernac.load_vernac_core in file "toplevel/vernac.ml", line 116, characters 6-19
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.load_vernac in file "toplevel/vernac.ml", line 172, characters 30-94
Called from Ccompile.compile in file "toplevel/ccompile.ml", line 146, characters 18-95
Called from Ccompile.compile in file "toplevel/ccompile.ml" (inlined), line 210, characters 2-59
Called from Ccompile.compile_file in file "toplevel/ccompile.ml", line 219, characters 4-61
Called from Coqc.coqc_main in file "toplevel/coqc.ml", line 48, characters 2-100
Called from Coqc.coqc_run in file "toplevel/coqc.ml", line 67, characters 4-36
This is with Coq 8.15.0
Pierre-Marie Pédrot (Sep 23 2022 at 11:54):looks normal to me, you wrote a term with an unbound rel
Jason Gross (Sep 23 2022 at 12:45):Hm, I tried very hard to not invoke any operations that relied on having all the rels be bound. Is there a way to figure out what line of code (presumably Ltac2?) is invoking the problematic reduction(?)
Janno (Sep 23 2022 at 13:17):I am not sure but whd_simpl_orelse_delta_but_fix reminds me of hnf. Are you using that? I don't think Ltac2 calls any reduction automatically anywhere so it would have to be in your code somewhere.
Janno (Sep 23 2022 at 13:22):If you need reduction that is fine with unbound rels then I think the only option is the kernel's weak head reduction.
Jason Gross (Sep 23 2022 at 14:53):I do call reduction with unbound rels, cbv beta and delta seem to work perfectly fine in most cases with unbound rels. I am calling hnf, but not on this term, I think. Does unification call hnf? This issue only happens when I leave an evar in the term (one that eventually gets unified with something boring like nat). I'm trying to minimize it, and have run into a bunch of other strange issues. Like when I define the terms this one depends on by transparent_abstract instead of Definition, I get an evar not declared anomaly (without even invoking Ltac2). And if I define them by tactics with transparent_abstract rather than giving the definitions explicitly with exact, then they all go through but instead of a not found anomaly, I get a different anomaly:
Jason Gross (Sep 23 2022 at 14:53):Error:
Anomaly
"File "pretyping/evarsolve.ml", line 103, characters 9-15: Assertion failed."
Please report at http://coq.inria.fr/bugs/.
Raised at Evarsolve.normalize_evar in file "pretyping/evarsolve.ml", line 103, characters 9-21
Called from Evarsolve.invert_definition.imitate in file "pretyping/evarsolve.ml", line 1645, characters 36-58
Called from Stdlib__array.map in file "array.ml", line 106, characters 21-40
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 711, characters 16-34
Called from Stdlib__array.map in file "array.ml", line 108, characters 21-40
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 711, characters 16-34
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 698, characters 15-53
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 698, characters 15-53
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 698, characters 15-53
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 698, characters 15-53
Called from Termops.Internal.map_constr_with_full_binders in file "engine/termops.ml", line 697, characters 15-20
Called from Evarsolve.invert_definition in file "pretyping/evarsolve.ml", line 1716, characters 15-34
Called from Evarsolve.evar_define in file "pretyping/evarsolve.ml", line 1743, characters 22-91
Called from Evarsolve.solve_simple_eqn in file "pretyping/evarsolve.ml", line 1823, characters 14-79
Called from Evarconv.evar_conv_x in file "pretyping/evarconv.ml", line 578, characters 19-125
Called from Evarconv.unify_leq_delay in file "pretyping/evarconv.ml", line 1817, characters 8-45
Called from Coercion.inh_conv_coerce_to_fail in file "pretyping/coercion.ml", line 622, characters 7-44
Called from Coercion.inh_conv_coerce_to_gen in file "pretyping/coercion.ml", line 658, characters 33-111
Called from Pretyping.Default.pretype_var in file "pretyping/pretyping.ml", line 627, characters 21-96
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1373, characters 21-85
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.type_uconstr in file "plugins/ltac/tacinterp.ml", line 1093, characters 2-57
Called from Ltac_plugin__Internals.exact.(fun) in file "plugins/ltac/internals.ml", line 377, characters 17-85
Called from Proofview.Goal.enter.f in file "engine/proofview.ml", line 1120, characters 40-46
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.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.refine_by_tactic in file "proofs/proof.ml", line 524, characters 8-30
Called from Ltac_plugin__Tacinterp.eval in file "plugins/ltac/tacinterp.ml", line 2204, characters 21-94
Called from Pretyping.Default.pretype_hole in file "pretyping/pretyping.ml", line 661, characters 21-78
Called from Cases.build_leaf in file "pretyping/cases.ml", line 1298, characters 17-79
Called from Cases.compile.shift_problem in file "pretyping/cases.ml", line 1503, characters 25-41
Called from Cases.compile_cases.compile_for_one_predicate in file "pretyping/cases.ml", line 2770, characters 25-55
Called from Cases.list_try_compile.aux in file "pretyping/cases.ml", line 82, characters 10-13
Called from Cases.compile_cases in file "pretyping/cases.ml", line 2779, characters 23-71
Called from Pretyping.Default.pretype_lambda in file "pretyping/pretyping.ml", line 958, characters 20-87
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1370, characters 21-79
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 43-86
Called from Ltac_plugin__Tacinterp.catch_error_with_trace_loc in file "plugins/ltac/tacinterp.ml", line 192, characters 6-9
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 6-91
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.lifts.(fun) in file "plugins/ltac/tacinterp.ml", line 2114, characters 19-36
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.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.(>>=).(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.(>>=).(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.(>>=).(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.(>>=).(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.refine_by_tactic in file "proofs/proof.ml", line 524, characters 8-30
Called from Ltac_plugin__Tacinterp.eval in file "plugins/ltac/tacinterp.ml", line 2204, characters 21-94
Called from Pretyping.Default.pretype_hole in file "pretyping/pretyping.ml", line 661, characters 21-78
[...]
[...]
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1370, characters 21-79
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 43-86
Called from Ltac_plugin__Tacinterp.catch_error_with_trace_loc in file "plugins/ltac/tacinterp.ml", line 192, characters 6-9
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 6-91
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.lifts.(fun) in file "plugins/ltac/tacinterp.ml", line 2114, characters 19-36
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.(>>=).(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.(>>=).(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.(>>=).(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.(>>=).(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.(>>=).(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.(>>=).(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.(>>=).(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.refine_by_tactic in file "proofs/proof.ml", line 524, characters 8-30
Called from Ltac_plugin__Tacinterp.eval in file "plugins/ltac/tacinterp.ml", line 2204, characters 21-94
Called from Pretyping.Default.pretype_hole in file "pretyping/pretyping.ml", line 661, characters 21-78
Called from Pretyping.Default.pretype_lambda in file "pretyping/pretyping.ml", line 958, characters 20-87
Called from Pretyping.pretype in file "pretyping/pretyping.ml" (inlined), line 1352, characters 2-81
Called from Pretyping.ise_pretype_gen in file "pretyping/pretyping.ml", line 1370, characters 21-79
Called from Pretyping.understand_ltac in file "pretyping/pretyping.ml" (inlined), line 1422, characters 22-65
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 43-86
Called from Ltac_plugin__Tacinterp.catch_error_with_trace_loc in file "plugins/ltac/tacinterp.ml", line 192, characters 6-9
Called from Ltac_plugin__Tacinterp.interp_gen in file "plugins/ltac/tacinterp.ml", line 610, characters 6-91
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Ltac_plugin__Tacinterp.lifts.(fun) in file "plugins/ltac/tacinterp.ml", line 2114, characters 19-36
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.(>>=).(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.(>>=).(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 ComTactic.solve_core.(fun) in file "vernac/comTactic.ml", line 46, characters 23-59
Called from Declare.Proof.map_fold_endline in file "vernac/declare.ml", line 1457, characters 20-33
Called from ComTactic.solve_core in file "vernac/comTactic.ml", line 43, characters 23-442
Called from Vernacextend.vtmodifyproof.(fun) in file "vernac/vernacextend.ml", line 163, characters 32-47
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 203, 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 253, characters 18-43
Called from Vernacinterp.interp_gen in file "vernac/vernacinterp.ml", line 251, 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 2169, characters 20-47
Called from Stm.Reach.known_state.resilient_tactic in file "stm/stm.ml", line 2111, characters 10-14
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 Vernac.interp_vernac in file "toplevel/vernac.ml", line 68, characters 31-52
Re-raised at Exninfo.iraise in file "clib/exninfo.ml", line 81, characters 4-38
Called from Vernac.process_expr in file "toplevel/vernac.ml" (inlined), line 123, characters 2-60
Called from Coqloop.process_toplevel_command in file "toplevel/coqloop.ml", line 415, characters 17-62
Called from Coqloop.read_and_execute_base in file "toplevel/coqloop.ml", line 452, characters 4-39
Called from Coqloop.read_and_execute in file "toplevel/coqloop.ml", line 458, characters 6-34
The evar not declared anomaly: https://github.com/coq/coq/issues/16534
Jason Gross (Sep 24 2022 at 10:24):What about getting an assertion failure on
let normalize_evar evd ev =
match EConstr.kind evd (mkEvar ev) with
| Evar (evk,args) -> (evk,args)
| _ -> assert false
?
Is this expected from messing with unbound rels?
Reported at https://github.com/coq/coq/issues/16540
Last updated: Apr 18 2024 at 21:01 UTC