Hi, in coq-dpdgraph there is this code:
let collect_long_names (c:Constr.t) (acc:Data.t) =
let rec add acc c =
let open Constr in
match kind c with
| Var x -> add_identifier x acc
| Sort s -> add_sort s acc
| Const cst -> add_constant (Univ.out_punivs cst) acc
| Ind i -> add_inductive (Univ.out_punivs i) acc
| Construct cnst -> add_constructor (Univ.out_punivs cnst) acc
| Case({ci_ind=i},_,_,_) ->
add_inductive i (Constr.fold add acc c)
| _ -> Constr.fold add acc c
in add acc c
Usually the Case
case takes 5 arguments in < 8.12 and currently 8.13+alpha. But in 8.12 it only takes 4. Is this going to be a permanent change?
Yes, this was introduced to handle SProp + UIP.
Last updated: Dec 05 2023 at 09:01 UTC