From 2ac8e0edebe0d9a6bde4d997327dbd2ffcde08b6 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 4 Jun 2014 15:42:41 +0200
Subject: - Allow parsing of @const@{instance} for specifying universe
 instances of polymorphic constants.

---
 pretyping/unification.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping')

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
 
-- 
cgit v1.2.3