diff options
Diffstat (limited to 'pretyping/recordops.ml')
| -rwxr-xr-x | pretyping/recordops.ml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index cc53ae7f3f..cfccdb5e68 100755 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -117,6 +117,8 @@ let subst_obj subst obj = let object_table = (ref [] : ((global_reference * global_reference) * obj_typ) list ref) +let canonical_structures () = !object_table + let cache_canonical_structure (_,(cst,lo)) = List.iter (fun (o,_ as x) -> if not (List.mem_assoc o !object_table) then |