From a71f586e23b0e68032c556bfa1c37df8f4358c71 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 17 Mar 2019 10:40:31 +0100
Subject: Fix constr_matching on SProp

---
 pretyping/pattern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/pattern.ml')

diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 2ca7f21e8d..d1c0a4ea2a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -32,7 +32,7 @@ type constr_pattern =
   | PLambda of Name.t * constr_pattern * constr_pattern
   | PProd of Name.t * constr_pattern * constr_pattern
   | PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
-  | PSort of Glob_term.glob_sort
+  | PSort of Sorts.family
   | PMeta of patvar option
   | PIf of constr_pattern * constr_pattern * constr_pattern
   | PCase of case_info_pattern * constr_pattern * constr_pattern *
-- 
cgit v1.2.3