From 105db906ae45e792d1caeeb2e3fb7f69944b2caa Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Apr 2014 12:53:41 +0200
Subject: - Fixes for canonical structure resolution (check that the initial
 term indeed unifies with the projected term, keeping track of universes). -
 Fix the [unify] tactic to fail properly. - Fix unification to disallow
 lowering a global Type(i) universe to Prop or Set.

---
 pretyping/recordops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/recordops.mli')

diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index b1763a359e..4a03d9bc53 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -66,7 +66,7 @@ type obj_typ = {
 val cs_pattern_of_constr : constr -> cs_pattern * int * constr list
 val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds
 
-val lookup_canonical_conversion : (global_reference * cs_pattern) -> obj_typ
+val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ
 val declare_canonical_structure : global_reference -> unit
 val is_open_canonical_projection :
   Environ.env -> Evd.evar_map -> (constr * constr Reductionops.Stack.t) -> bool
-- 
cgit v1.2.3