diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-26 11:22:40 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-26 16:10:13 +0200 |
| commit | dd21327dbc388dfbff88834ae628df062b1b7c04 (patch) | |
| tree | 89bf3ebd53126d7861d999889a6d3a526ba3152a /pretyping/recordops.ml | |
| parent | 0a42f8d2434d6c5471d47c99d815762783cdca95 (diff) | |
Fix canonical structure resolution which was launched on the results of
eta-expansion, creating a loop. This is now deactivated. Fixes bugs #3665 and #3667.
Diffstat (limited to 'pretyping/recordops.ml')
| -rw-r--r-- | pretyping/recordops.ml | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 494138541..66aa85ecd 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -308,9 +308,6 @@ let declare_canonical_structure ref = let lookup_canonical_conversion (proj,pat) = assoc_pat pat (Refmap.find proj !object_table) - (* let cst, u' = destConst cs.o_DEF in *) - (* { cs with o_DEF = mkConstU (cst, u) } *) - let is_open_canonical_projection env sigma (c,args) = try let ref = global_of_constr c in |