Fast path in Canonical structure detection. We do not always compute the normal

form of a potential canonical argument anymore, and we check that it may be part
of a canonical structure first.

1 files changed, 4 insertions, 1 deletions

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 35ac90de57..494138541f 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -313,7 +313,10 @@ let lookup_canonical_conversion (proj,pat) =
 
 let is_open_canonical_projection env sigma (c,args) =
   try
-    let n = find_projection_nparams (global_of_constr c) in
+    let ref = global_of_constr c in
+    let n = find_projection_nparams ref in
+    (** Check if there is some canonical projection attached to this structure *)
+    let _ = Refmap.find ref !object_table in
     try
       let arg = whd_betadeltaiota env sigma (Stack.nth args n) in
       let hd = match kind_of_term arg with App (hd, _) -> hd | _ -> arg in