[Regression] Anomaly: grounding a non evar-free term

[cpitclaudel]

In 8.12.0+0.12.0, the following input raises an anomaly:

("query0"("Add"()"Class Countable T :=\n  inj_countable {\n      encode: T -> nat;\n      decode: nat -> T;\n      encode_decode_ok : forall x, decode (encode x) = x;\n    }.\n\nInductive bin_op :=\n  | PlusOp.\n\nGlobal Instance bin_op_countable : Countable bin_op.\nProof.\n  refine (inj_countable bin_op\n            (fun op => match op with | PlusOp => 0  end)\n            (fun n => match n with | 0 => _ | _ => PlusOp end) _).\n  destruct x; auto.\nQed."))
("query12"("Exec""6"))
("query13"("Query"(("sid""6"))"EGoals"))

Output:

(Answer query13 Ack)
(Answer query13(CoqExn((loc())(stm_ids())(backtrace(Backtrace()))(exn("\"Anomaly: grounding a non evar-free term\""))(pp(Pp_glue((Pp_box(Pp_hovbox 0)(Pp_glue((Pp_string Anomaly)(Pp_print_break 1 0)(Pp_box(Pp_hbox 0)(Pp_glue((Pp_string"\"")(Pp_string"grounding a non evar-free term")(Pp_string"\"")))))))(Pp_print_break 1 0)(Pp_box(Pp_hovbox 0)(Pp_glue((Pp_string"Please report at ")(Pp_string http://coq.inria.fr/bugs/)(Pp_string .)))))))(str"Anomaly \"grounding a non evar-free term\"\nPlease report at http://coq.inria.fr/bugs/."))))

Original report: https://github.com/cpitclaudel/alectryon/issues/18

[ejgallego]

Ups, I thought this was fixed, let me have a look.

[corwin-of-amber]

Cheers @ejgallego, @cpitclaudel I just stumbled on it in jsCoq. I think we should just add ~abort_on_undefined_evars:false here? https://github.com/ejgallego/coq-serapi/blob/3ba346eecd5eb0a43937ab09686b74e0b41278d8/serapi/serapi_goals.ml#L58