Stream: Coq devs & plugin devs

Topic: `Case` constructor taking less arguments in 8.12

view this post on Zulip Ali Caglayan (Aug 04 2020 at 08:59):

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?

view this post on Zulip Pierre-Marie Pédrot (Aug 04 2020 at 09:08):

Yes, this was introduced to handle SProp + UIP.

Last updated: Jun 09 2023 at 04:01 UTC