From df73f477fd496168bf448d2bfef8cec3cb0643ee Mon Sep 17 00:00:00 2001
From: msozeau
Date: Sat, 16 May 2009 13:53:49 +0000
Subject: (Tentative to) add Canonical Structure resolution to the regular
 unification algorithm. Uses the same code to recognize projections
 (check_conv_record) and the same unification steps on the solution as
 evar_conv. This required to fold the sigma through unify_* along with the
 meta and evar substitutions as this can grow during unification.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12128 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/recordops.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'pretyping/recordops.ml')

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 16d3331aad..79c347cea6 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -310,11 +310,13 @@ let outCanonicalStructure x = fst (outCanonStruct x)
 let lookup_canonical_conversion (proj,pat) =
   List.assoc pat (Refmap.find proj !object_table)
 
+let isEvar_or_Meta c = isEvar c || isMeta c
+
 let is_open_canonical_projection sigma (c,args) =
   try 
     let l = Refmap.find (global_of_constr c) !object_table in
     let n = (snd (List.hd l)).o_NPARAMS in
-    try isEvar (whd_evar sigma (List.nth args n)) with Failure _ -> false
+    try isEvar_or_Meta (whd_evar sigma (List.nth args n)) with Failure _ -> false
   with Not_found -> false
 
 let freeze () =
-- 
cgit v1.2.3