Fix all FIXME comments in src/

[Copilot]

Addresses a collection of FIXME markers across the codebase — removing dead parameters, replacing assert false/failwith crashes with proper errors, and implementing missing cases.

Remove unused parameters

• ecCoreGoal.ml/mli: Drop ?who:string from tc_error, tc_error_exn, tc_error_lazy, tc_lookup_error — was accepted and immediately ignored. All 14 call sites updated.
• ecUnify.ml/mli: Drop ?hidden:bool from select_op — same issue. Updated the one call site in ecPrinting.ml.

Replace crashes with proper errors

File	Location	Fix
ecIo.ml	parseall	assert false → ParseError for P_Undo/P_Exit
ecScope.ml	add_instance	failwith "unsupported" → hierror with instance name
ecPhlInline.ml	inline_i	assert false → tc_error "code pattern doesn't match instruction type"
ecPhlInline.ml	pat_of_occs	bare assert (Sint.is_empty !occs) → tc_error reporting the invalid occurrence numbers (also threads tc into pat_of_occs)
ecPhlSkip.ml	t_bdhoare_skip_r_low	empty string error → "skip requires comparison to be = or >=, got <="
ecEnv.ml	actmem_body	assert false for FBabs/FBalias → invalid_arg
ecTyping.ml	i_inuse	assert false for Sabstract → invalid_arg
ecPV.ml	add_glob	three bare assert false → invalid_arg with messages
ecPV.ml	i_eqobs_in_refl, eqobs_inF_refl	assert false → invalid_arg
ecProofTerm.ml	apply_pterm_to_local	assert false for LD_abs_st → invalid_arg

Implement missing cases

• ecPhlFel.ml callable_oracles_i: Handle Sabstract by folding callable_oracles_f over aus_calls from the abstract statement's use set.
• ecEnv.ml ld_subst: Implement LD_abs_st substitution — apply ty_subst/pv_subst/x_subst to aus_reads, aus_writes, and aus_calls.

---

🔒 GitHub Advanced Security automatically protects Copilot coding agent pull requests. You can protect all pull requests by enabling Advanced Security for your repositories. Learn more about Advanced Security.