UIP in SProp

2 files changed, 31 insertions, 2 deletions

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 f14edec639..5becd03bbd 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -294,7 +294,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)) ->
@@ -406,7 +406,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";