From 87910d7be9bd50de4db80f70c6e287c7c7994460 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Tue, 25 Apr 2017 14:31:15 +0200
Subject: Fix 4.04 warnings

---
 interp/notation.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 90ac7f7296..6aa6f54c05 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -22,7 +22,6 @@ open Glob_ops
 open Ppextend
 open Context.Named.Declaration
 
-module NamedDecl = Context.Named.Declaration
 (*i*)
 
 (*s A scope is a set of notations; it includes
-- 
cgit v1.2.3


From b643916aed4093eb7f21116aaef726cab561bc27 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 15 May 2017 01:10:54 +0200
Subject: [interp] [ast] Make raw_cases_pattern_expr private.

The type `raw_cases_pattern_expr` is used only in the interpretation
of notation patterns. Indeed, this should be a private type thus we
make it local to `Constrintern`; it makes no sense to expose it in the
public AST.

The patch is routine, except for the case used to interpret primitives
in patterns. We now return a `glob_constr` representing the raw
pattern, instead of the private raw pattern type. This could be
further refactored but have opted to be conservative here.

This patch is a refinement of b2953849b999d1c3b42c0f494b234f2a93ac7754
, see the commentaries there for more information about
`raw_cases_pattern_expr`.
---
 interp/notation.ml | 25 +++++++++++++------------
 1 file changed, 13 insertions(+), 12 deletions(-)

(limited to 'interp/notation.ml')

diff --git a/interp/notation.ml b/interp/notation.ml
index 6aa6f54c05..7be2fe0f01 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -444,16 +444,20 @@ let notation_of_prim_token = function
   | Numeral n -> "- "^(to_string (neg n))
   | String _ -> raise Not_found
 
-let find_prim_token g loc p sc =
+let find_prim_token check_allowed loc p sc =
   (* Try for a user-defined numerical notation *)
   try
     let (_,c),df = find_notation (notation_of_prim_token p) sc in
-    g (Notation_ops.glob_constr_of_notation_constr loc c),df
+    let pat = Notation_ops.glob_constr_of_notation_constr loc c in
+    check_allowed pat;
+    pat, df
   with Not_found ->
   (* Try for a primitive numerical notation *)
   let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
   check_required_module loc sc spdir;
-  g (interp ()), ((dirpath (fst spdir),DirPath.empty),"")
+  let pat = interp () in
+  check_allowed pat;
+  pat, ((dirpath (fst spdir),DirPath.empty),"")
 
 let interp_prim_token_gen g loc p local_scopes =
   let scopes = make_current_scopes local_scopes in
@@ -466,20 +470,17 @@ let interp_prim_token_gen g loc p local_scopes =
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
 let interp_prim_token =
-  interp_prim_token_gen (fun x -> x)
+  interp_prim_token_gen (fun _ -> ())
 
-(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
-
-let rec rcp_of_glob looked_for = function
-  | GVar (loc,id) -> RCPatAtom (loc,Some id)
-  | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
-  | GRef (loc,g,_) -> looked_for g; RCPatCstr (loc, g,[],[])
+let rec check_allowed_ref_in_pat looked_for = function
+  | GVar _ | GHole _ -> ()
+  | GRef (_,g,_) -> looked_for g
   | GApp (loc,GRef (_,g,_),l) ->
-    looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
+    looked_for g; List.iter (check_allowed_ref_in_pat looked_for) l
   | _ -> raise Not_found
 
 let interp_prim_token_cases_pattern_expr loc looked_for p =
-  interp_prim_token_gen (rcp_of_glob looked_for) loc p
+  interp_prim_token_gen (check_allowed_ref_in_pat looked_for) loc p
 
 let interp_notation loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
-- 
cgit v1.2.3