diff options
| author | Gaëtan Gilbert | 2020-02-24 14:24:10 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-13 15:18:18 +0200 |
| commit | b98ef72ee300e52dd2c67f03da358e3c2102cdbb (patch) | |
| tree | ceddc2c4523978cfa0436047b44f3f326eeba106 /vernac/canonical.ml | |
| parent | 2d6b7d5997037d9a94524a733867f64cd34e851c (diff) | |
pass filters around
Diffstat (limited to 'vernac/canonical.ml')
| -rw-r--r-- | vernac/canonical.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/canonical.ml b/vernac/canonical.ml index 390ed62bee..eaa6c84791 100644 --- a/vernac/canonical.ml +++ b/vernac/canonical.ml @@ -28,7 +28,7 @@ let discharge_canonical_structure (_,((gref, _ as x), local)) = let inCanonStruc : (GlobRef.t * inductive) * bool -> obj = declare_object {(default_object "CANONICAL-STRUCTURE") with - open_function = open_canonical_structure; + open_function = simple_open open_canonical_structure; cache_function = cache_canonical_structure; subst_function = (fun (subst,(c,local)) -> subst_canonical_structure subst c, local); classify_function = (fun x -> Substitute x); |