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/declareInd.ml | |
| parent | 2d6b7d5997037d9a94524a733867f64cd34e851c (diff) | |
pass filters around
Diffstat (limited to 'vernac/declareInd.ml')
| -rw-r--r-- | vernac/declareInd.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/declareInd.ml b/vernac/declareInd.ml index 2610f16d92..203e11d6ab 100644 --- a/vernac/declareInd.ml +++ b/vernac/declareInd.ml @@ -65,7 +65,7 @@ let objInductive : inductive_obj Libobject.Dyn.tag = declare_object_full {(default_object "INDUCTIVE") with cache_function = cache_inductive; load_function = load_inductive; - open_function = open_inductive; + open_function = todo_filter open_inductive; classify_function = (fun a -> Substitute a); subst_function = ident_subst_function; discharge_function = discharge_inductive; |