Merge PR #10390: UIP in SProp

Reviewed-by: Zimmi48
Ack-by: ejgallego
Reviewed-by: maximedenes

3 files changed, 61 insertions, 2 deletions

diff --git a/dev/ci/user-overlays/10390-SkySkimmer-uip.sh b/dev/ci/user-overlays/10390-SkySkimmer-uip.sh
new file mode 100644
index 0000000000..80107ac9c5
--- /dev/null
+++ b/dev/ci/user-overlays/10390-SkySkimmer-uip.sh
@@ -0,0 +1,30 @@
+if [ "$CI_PULL_REQUEST" = "10390" ] || [ "$CI_BRANCH" = "uip" ]; then
+
+    unicoq_CI_REF=uip
+    unicoq_CI_GITURL=https://github.com/SkySkimmer/unicoq
+
+    mtac2_CI_REF=uip
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/Mtac2
+
+    elpi_CI_REF=uip
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=uip
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    paramcoq_CI_REF=uip
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+
+    relation_algebra_CI_REF=uip
+    relation_algebra_CI_GITURL=https://github.com/SkySkimmer/relation-algebra
+
+    coq_dpdgraph_CI_REF=uip
+    coq_dpdgraph_CI_GITURL=https://github.com/SkySkimmer/coq-dpdgraph
+
+    coqhammer_CI_REF=uip
+    coqhammer_CI_GITURL=https://github.com/SkySkimmer/coqhammer
+
+    metacoq_CI_REF=uip
+    metacoq_CI_GITURL=https://github.com/SkySkimmer/metacoq
+
+fi
diff --git a/dev/doc/SProp.md b/dev/doc/SProp.md
index f263dbb867..d517983046 100644
--- a/dev/doc/SProp.md
+++ b/dev/doc/SProp.md
@@ -39,3 +39,32 @@ Relevance can be inferred from a well-typed term using functions in
 term, note the difference between its relevance as a term (is `x :
 (_ : SProp)`) and as a type (is `x : SProp`), there are functions for
 both kinds.
+
+## Case inversion
+
+Inductives in SProp with 1 constructor which has no arguments have a
+special reduction rule for matches. To implement it the Case
+constructor is extended with a `case_invert` field.
+
+If you are constructing a match on a normal (non-special reduction)
+inductive you must fill the new field with `NoInvert`. Otherwise you
+must fill it with `CaseInvert {univs ; args}` where `univs` is the
+universe instance of the type you are matching and `args` the
+parameters and indices.
+
+For instance, in
+
+~~~coq
+Inductive seq {A} (a:A) : A -> SProp :=
+  srefl : seq a a.
+
+Definition seq_to_eq {A x y} (e:seq x y) : x = y :> A
+  := match e with srefl => eq_refl end.
+~~~
+
+the `match e with ...` has `CaseInvert {univs = Instance.empty; args = [|A x y|]}`.
+(empty instance since we defined a universe monomorphic `seq`).
+
+In practice, you should use `Inductiveops.make_case_or_project` which
+will take care of this for you (and also handles primitive records
+correctly etc).
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 34110f96cf..3df6f986ce 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -296,7 +296,7 @@ let constr_display csr =
       "MutConstruct(("^(MutInd.to_string sp)^","^(string_of_int i)^"),"
       ^","^(universes_display u)^(string_of_int j)^")"
   | Proj (p, c) -> "Proj("^(Constant.to_string (Projection.constant p))^","^term_display c ^")"
-  | Case (ci,p,c,bl) ->
+  | Case (ci,p,iv,c,bl) ->
       "MutCase(<abs>,"^(term_display p)^","^(term_display c)^","
       ^(array_display bl)^")"
   | Fix ((t,i),(lna,tl,bl)) ->
@@ -408,7 +408,7 @@ let print_pure_constr csr =
       print_int i; print_string ","; print_int j;
       print_string ","; universes_display u;
       print_string ")"
-  | Case (ci,p,c,bl) ->
+  | Case (ci,p,iv,c,bl) ->
       open_vbox 0;
       print_string "<"; box_display p; print_string ">";
       print_cut(); print_string "Case";