From 45352e43db4c67eab23517f13e94ba1b5cc11808 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 13 Nov 2018 15:42:02 +0100
Subject: Towards unifying parsing/printing for universe instances and Type's
 argument.

We consistently use:
- UUnknown: to mean a rigid anonymous universe
  (written Type in instances and Type as a sort)
  [was formerly encoded as [] in Type's argument]
- UAnonymous: to mean a flexible anonymous universe
  (written _ in instances and Type@{_} as a sort)
  [was formerly encoded as [None] in Type's argument]
- UNamed: to mean a named universe or universe expression
  (written id or qualid in instances and Type@{id} or Type@{qualid} or more
   generally Type@{id+n}, Type@{qualid+n}, Type@{max(...)} as a sort)

There is a little change of syntax: "_" in a "max" list of universes
(e.g. "Type@{max(_,id+1)}" is not anymore allowed. But it was
trivially satisfiable by unifying the flexible universe with a
neighbor of the list and the syntax is anyway not documented.

There is a little change of semantics: if I do id@{Type} for an
abbreviation "id := Type", it will consider a rigid variable rather
than a flexible variable as before.
---
 plugins/funind/glob_term_to_relation.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 4c67d65816..889a2d7359 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1302,7 +1302,7 @@ let rec rebuild_return_type rt =
 	CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
     | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
                                        Constrexpr.Default Decl_kinds.Explicit, rt)],
-			    CAst.make @@ Constrexpr.CSort(GType []))
+                            CAst.make @@ Constrexpr.CSort(GType UUnknown))
 
 let do_build_inductive
       evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
-- 
cgit v1.2.3


From 460bf801123d13e8c82503a2fc491892f8eed6d5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 14 Nov 2018 10:10:39 +0100
Subject: Allowing Set to be part of universe expressions.

Conversely, Type existential variables now (explicitly) cover the Set
case.

Similarly for Prop and SProp.
---
 plugins/funind/glob_term_to_relation.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 889a2d7359..201d953692 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1299,10 +1299,10 @@ let rec rebuild_return_type rt =
     | Constrexpr.CProdN(n,t') ->
         CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
     | Constrexpr.CLetIn(na,v,t,t') ->
-	CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
+        CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
     | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous],
                                        Constrexpr.Default Decl_kinds.Explicit, rt)],
-                            CAst.make @@ Constrexpr.CSort(GType UUnknown))
+                             CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true}))
 
 let do_build_inductive
       evd (funconstants: pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
-- 
cgit v1.2.3