diff options
Diffstat (limited to 'library/declare.ml')
| -rw-r--r-- | library/declare.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/library/declare.ml b/library/declare.ml index ff46ad72ae..5e87c1a749 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -57,12 +57,11 @@ let cache_variable (sp,(id,(ty,_,_) as vd,imps)) = if imps then declare_var_implicits id; vartab := Spmap.add sp vd !vartab -let load_variable _ = anomaly "we shouldn't load a variable" +let load_variable _ = () -let open_variable _ = anomaly "we shouldn't open a variable" +let open_variable _ = () -let specification_variable _ = - anomaly "we shouldn't extract the specification of a variable" +let specification_variable x = x let (in_variable, out_variable) = let od = { |