diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 42a8cac69..0c4fa7055 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -99,6 +99,9 @@ let is_info_scheme env t = match flag_of_type env t with | (Info, TypeScheme) -> true | _ -> false +let push_rel_assum (n, t) env = + Environ.push_rel (LocalAssum (n, t)) env + (*s [type_sign] gernerates a signature aimed at treating a type application. *) let rec type_sign env c = |