aboutsummaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
authorMatthieu Sozeau2016-04-04 14:49:06 +0200
committerMatthieu Sozeau2016-04-04 14:49:06 +0200
commit16536fd734d6a7aaa6ff85f56cef629df74ce36a (patch)
treea9ffc8d0830c7c826ea164b5267f95985365fe63 /interp/constrextern.ml
parent5569a06d062f913c66cbcb8bd01d4505e603d321 (diff)
parent6aa58955515dff338ea85d59073dfc0d0c7648ab (diff)
Merge branch 'trunk-function_scope' of https://github.com/JasonGross/coq into JasonGross-trunk-function_scope
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 49892bec49..592f593330 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -793,7 +793,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)