Skip to content

Commit f8985dc

Browse files
authored
Merge pull request #66 from SkySkimmer/uip
Adapt to rocq-prover/rocq#10390 (UIP in SProp)
2 parents acd7c15 + ef099e6 commit f8985dc

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

searchdepend.mlg

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ let collect_long_names (c:Constr.t) (acc:Data.t) =
5151
| Const cst -> add_constant (Univ.out_punivs cst) acc
5252
| Ind i -> add_inductive (Univ.out_punivs i) acc
5353
| Construct cnst -> add_constructor (Univ.out_punivs cnst) acc
54-
| Case({ci_ind=i},_,_,_) ->
54+
| Case({ci_ind=i},_,_,_,_) ->
5555
add_inductive i (Constr.fold add acc c)
5656
| _ -> Constr.fold add acc c
5757
in add acc c

0 commit comments

Comments
 (0)