- Allow parsing of @const@{instance} for specifying universe instances of polymorphic

constants.

4 files changed, 17 insertions, 4 deletions

diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4
index 81645a580f..69ba73c673 100644
--- a/parsing/g_constr.ml4
+++ b/parsing/g_constr.ml4
@@ -161,7 +161,7 @@ GEXTEND Gram
   ;
   constr:
     [ [ c = operconstr LEVEL "8" -> c
-      | "@"; f=global -> CAppExpl(!@loc,(None,f,None),[]) ] ]
+      | "@"; f=global; i = instance -> CAppExpl(!@loc,(None,f,i),[]) ] ]
   ;
   operconstr:
     [ "200" RIGHTA
@@ -185,7 +185,7 @@ GEXTEND Gram
     | "90" RIGHTA [ ]
     | "10" LEFTA
       [ f=operconstr; args=LIST1 appl_arg -> CApp(!@loc,(None,f),args)
-      | "@"; f=global; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f,None),args)
+      | "@"; f=global; i = instance; args=LIST0 NEXT -> CAppExpl(!@loc,(None,f,i),args)
       | "@"; (locid,id) = pattern_identref; args=LIST1 identref ->
           let args = List.map (fun x -> CRef (Ident x,None), None) args in
           CApp(!@loc,(None,CPatVar(locid,(true,id))),args) ]
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2b3e943559..4936ba4264 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -386,6 +386,7 @@ let is_rigid_head flags t =
   match kind_of_term t with
   | Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta))
   | Ind (i,u) -> true
+  | Construct _ -> true
   | Fix _ | CoFix _ -> true
   | _ -> false
 
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 019fad0ce8..5b6c072839 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -118,8 +118,16 @@ let pr_name = pr_name
 let pr_qualid = pr_qualid
 let pr_patvar = pr_id
 
+let pr_glob_sort_instance = function
+  | GProp -> str "Prop"
+  | GSet -> str "Set"
+  | GType u -> 
+    (match u with 
+    | Some u -> str u
+    | None -> str "Type")
+
 let pr_universe_instance l =
-  pr_opt (pr_in_comment (prlist_with_sep spc pr_glob_sort)) l
+  pr_opt (pr_in_comment (prlist_with_sep spc pr_glob_sort_instance)) l
 
 let pr_cref ref us =
   pr_reference ref ++ pr_universe_instance us
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 9d6e9756dd..db74e5aa18 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -861,7 +861,11 @@ let explain_unsatisfiable_constraints env evd constr comp =
   | None -> Typeclasses.is_resolvable evi
   | Some comp -> Typeclasses.is_resolvable evi && Evar.Set.mem evk comp
   in
-  let undef = Evar.Map.filter is_kept undef in
+  let undef = 
+    let m = Evar.Map.filter is_kept undef in
+      if Evar.Map.is_empty m then undef
+      else m
+  in
   match constr with
   | None ->
     str "Unable to satisfy the following constraints:" ++ fnl () ++