From 33aaa5d64771c3644de4771338c371ce6b865647 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 8 Apr 2020 17:23:44 +0200
Subject: If a custom entry has global, a bound variable is valid in this
 entry.

This is due to "global" being a syntactic notation, thus including ident.

Parsing was automatically supporting this. This commit adds support for printing.
---
 interp/constrextern.ml | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 0396e556cf..a37bac3275 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -453,7 +453,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat =
     with No_match ->
     let loc = pat.CAst.loc in
     match DAst.get pat with
-    | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
+    | PatVar (Name id) when entry_has_global custom || entry_has_ident custom ->
+      CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id)))
     | pat ->
     match availability_of_entry_coercion custom InConstrEntrySomeLevel with
     | None -> raise No_match
@@ -935,7 +936,8 @@ let rec extern inctx ?impargs scopes vars r =
   match DAst.get r with
   | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us)
 
-  | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id)
+  | GVar id when entry_has_global (fst scopes) || entry_has_ident (fst scopes) ->
+      CAst.make ?loc (extern_var ?loc id)
 
   | c ->
 
-- 
cgit v1.2.3