diff options
| author |  Jason Gross <jgross@mit.edu> | 2015-06-24 15:41:11 +0200 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2015-08-14 02:49:31 -0400 |
| commit | 6aa58955515dff338ea85d59073dfc0d0c7648ab (patch) | |
| tree | ed472dbf020c22a3080bc5e13a398914875bca11 /interp/constrextern.ml | |
| parent | 297b0cb44bbe8ec7304ca635c566815167266d4a (diff) | |
Move type_scope into user space, fix some output logs
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index f57772ecb..1c60d5c2f 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -788,7 +788,7 @@ let rec extern inctx scopes vars r = Miscops.map_cast_type (extern_typ scopes vars) c') and extern_typ (_,scopes) = - extern true (Some Notation.type_scope,scopes) + extern true (Notation.current_type_scope_name (),scopes) and sub_extern inctx (_,scopes) = extern inctx (None,scopes) |