diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-02 10:07:05 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-08-02 10:07:05 +0000 |
| commit | 4d3fd35d44844d054417294cdbb2421c8e37fb65 (patch) | |
| tree | 123e3213788972961dc53ca94332f775aa7149c5 /pretyping/recordops.ml | |
| parent | e715aa54418f44d660a717b245f463167ac9372e (diff) | |
Patch to simplify is_open_canonical_projection
(courtesy from François Garillot)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index ccedf1520..0f1b9ac97 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -332,8 +332,7 @@ let lookup_canonical_conversion (proj,pat) = 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 + let n = find_projection_nparams (global_of_constr c) in try isEvar_or_Meta (whd_evar sigma (List.nth args n)) with Failure _ -> false with Not_found -> false |