diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-27 10:36:05 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-06-27 17:07:28 +0200 |
| commit | b2f9a315ceb3d9d2f0fca89722da20b8b061f24f (patch) | |
| tree | 6fdd3bdab208fa3c73060d50de1820852b78145f /pretyping/recordops.ml | |
| parent | 4db867c45dafc7ed7b524a8d089cd57b7944feca (diff) | |
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.
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 35ac90de5..494138541 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 |