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