Merge branch 'trunk' into located_switch

12 files changed, 100 insertions, 194 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index b11972cd3..79e0e6164 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -229,11 +229,8 @@ and instance_eq (x1,c1) (x2,c2) =
   Id.equal x1 x2 && constr_expr_eq c1 c2
 
 let constr_loc c = CAst.(c.loc)
-
 let cases_pattern_expr_loc cp = CAst.(cp.loc)
 
-let raw_cases_pattern_expr_loc pe = CAst.(pe.loc)
-
 let local_binder_loc = function
   | CLocalAssum ((loc,_)::_,_,t)
   | CLocalDef ((loc,_),t,None) -> Loc.merge_opt loc (constr_loc t)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index d51576c04..0ff51b060 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -36,7 +36,6 @@ val binder_kind_eq : binder_kind -> binder_kind -> bool
 
 val constr_loc : constr_expr -> Loc.t option
 val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t option
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t option
 val local_binders_loc : local_binder_expr list -> Loc.t option
 
 (** {6 Constructors}*)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index bd7c05e6f..7dc364e5d 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -431,30 +431,6 @@ let intern_assumption intern lvar env nal bk ty =
      let env, b = intern_generalized_binder intern_type lvar env (List.hd nal) b b' t ty in
      env, b
 
-let rec free_vars_of_pat il pt = match CAst.(pt.v) with
-  | CPatCstr (c, l1, l2) ->
-      let il = List.fold_left free_vars_of_pat il (Option.default [] l1) in
-      List.fold_left free_vars_of_pat il l2
-  | CPatAtom ro ->
-      begin match ro with
-      | Some (Ident (loc, i)) -> (loc, i) :: il
-      | Some _ | None -> il
-      end
-  | CPatNotation (n, l1, l2) ->
-      let il = List.fold_left free_vars_of_pat il (fst l1) in
-      List.fold_left (List.fold_left free_vars_of_pat) il (snd l1)
-  | _ -> anomaly (str "free_vars_of_pat")
-
-let intern_local_pattern intern lvar env p =
-  List.fold_left
-    (fun env (loc, i) ->
-       let bk = Default Implicit in
-       let ty = CAst.make ?loc @@ CHole (None, Misctypes.IntroAnonymous, None) in
-       let n = Name i in
-       let env, _ = intern_assumption intern lvar env [(loc, n)] bk ty in
-       env)
-    env (free_vars_of_pat [] p)
-
 let glob_local_binder_of_extended = CAst.with_loc_val (fun ?loc -> function
   | GLocalAssum (na,bk,t) -> (na,bk,None,t)
   | GLocalDef (na,bk,c,Some t) -> (na,bk,Some c,t)
@@ -483,13 +459,15 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
         | Some ty -> ty
         | None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
       in
-      let env = intern_local_pattern intern lvar env p in
-      let il = List.map snd (free_vars_of_pat [] p) in
-      let cp =
+      let il,cp =
         match !intern_cases_pattern_fwd (None,env.scopes) p with
-        | (_, [(_, cp)]) -> cp
+        | (il, [(subst,cp)]) ->
+           if not (Id.Map.equal Id.equal subst Id.Map.empty) then
+             user_err ?loc (str "Unsupported nested \"as\" clause.");
+           il,cp
         | _ -> assert false
       in
+      let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
       let ienv = Id.Set.elements env.ids in
       let id = Namegen.next_ident_away (Id.of_string "pat") ienv in
       let na = (loc, Name id) in
@@ -570,7 +548,8 @@ let traverse_binder (terms,_,_ as subst) avoid (renaming,env) = function
 type letin_param_r =
   | LPLetIn of Name.t * glob_constr * glob_constr option
   | LPCases of (cases_pattern * Id.t list) * Id.t
-and letin_param = letin_param_r Loc.located
+(* Unused thus fatal warning *)
+(* and letin_param = letin_param_r Loc.located *)
 
 let make_letins =
   List.fold_right
@@ -861,9 +840,9 @@ let intern_qualid loc qid intern env lvar us args =
       | Some _, { loc; v = GApp ({ loc = loc' ; v = GRef (ref, None) }, arg) } ->
         CAst.make ?loc @@ GApp (CAst.make ?loc:loc' @@ GRef (ref, us), arg)
       | Some _, _ ->
-        user_err ?loc  (str "Notation " ++ pr_qualid qid ++
-          str " cannot have a universe instance, its expanded head
-               does not start with a reference")
+        user_err ?loc  (str "Notation " ++ pr_qualid qid
+                        ++ str " cannot have a universe instance,"
+                        ++ str " its expanded head does not start with a reference")
       in
       c, projapp, args2
 
@@ -906,7 +885,17 @@ let interp_reference vars r =
 (**********************************************************************)
 (** {5 Cases }                                                        *)
 
-(** {6 Elemtary bricks } *)
+(** Private internalization patterns *)
+type raw_cases_pattern_expr_r =
+  | RCPatAlias of raw_cases_pattern_expr * Id.t
+  | RCPatCstr  of Globnames.global_reference
+    * raw_cases_pattern_expr list * raw_cases_pattern_expr list
+  (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
+  | RCPatAtom  of Id.t option
+  | RCPatOr    of raw_cases_pattern_expr list
+and raw_cases_pattern_expr = raw_cases_pattern_expr_r CAst.ast
+
+(** {6 Elementary bricks } *)
 let apply_scope_env env = function
   | [] -> {env with tmp_scope = None}, []
   | sc::scl -> {env with tmp_scope = sc}, scl
@@ -936,17 +925,6 @@ let find_remaining_scopes pl1 pl2 ref =
   in ((try List.firstn len_pl1 allscs with Failure _ -> simple_adjust_scopes len_pl1 allscs),
       simple_adjust_scopes len_pl2 (aux (impl_list,scope_list)))
 
-let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
-
-let product_of_cases_patterns ids idspl =
-  List.fold_right (fun (ids,pl) (ids',ptaill) ->
-    (ids @ ids',
-     (* Cartesian prod of the or-pats for the nth arg and the tail args *)
-     List.flatten (
-       List.map (fun (subst,p) ->
-	 List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
-    idspl (ids,[Id.Map.empty,[]])
-
 (* @return the first variable that occurs twice in a pattern
 
 naive n^2 algo *)
@@ -994,7 +972,7 @@ let add_implicits_check_length fail nargs nargs_with_letin impls_st len_pl1 pl2
 	      else Int.equal args_len nargs_with_letin || (fst (fail (nargs - List.length impl_list + i))))
 	       ,l)
     |imp::q as il,[] -> if is_status_implicit imp && maximal_insertion_of imp
-      then let (b,out) = aux i (q,[]) in (b,(CAst.make @@ RCPatAtom(None))::out)
+      then let (b,out) = aux i (q,[]) in (b,(CAst.make @@ RCPatAtom None)::out)
       else fail (remaining_args (len_pl1+i) il)
     |imp::q,(hh::tt as l) -> if is_status_implicit imp
       then let (b,out) = aux i (q,l) in (b,(CAst.make @@ RCPatAtom(None))::out)
@@ -1200,15 +1178,25 @@ let alias_of als = match als.alias_ids with
 
 *)
 
-let rec subst_pat_iterator y t = CAst.map (function
+let merge_subst s1 s2 = Id.Map.fold Id.Map.add s1 s2
+
+let product_of_cases_patterns aliases idspl =
+  List.fold_right (fun (ids,pl) (ids',ptaill) ->
+    (ids @ ids',
+     (* Cartesian prod of the or-pats for the nth arg and the tail args *)
+     List.flatten (
+       List.map (fun (subst,p) ->
+	 List.map (fun (subst',ptail) -> (merge_subst subst subst',p::ptail)) ptaill) pl)))
+    idspl (aliases.alias_ids,[aliases.alias_map,[]])
+
+let rec subst_pat_iterator y t = CAst.(map (function
   | RCPatAtom id as p ->
-    begin match id with Some x when Id.equal x y -> t.CAst.v | _ -> p end
+    begin match id with Some x when Id.equal x y -> t.v | _ -> p end
   | RCPatCstr (id,l1,l2) ->
-    RCPatCstr (id, List.map (subst_pat_iterator y t) l1,
-                   List.map (subst_pat_iterator y t) l2)
+    RCPatCstr (id,List.map (subst_pat_iterator y t) l1,
+ 	       List.map (subst_pat_iterator y t) l2)
   | RCPatAlias (p,a) -> RCPatAlias (subst_pat_iterator y t p,a)
-  | RCPatOr pl       -> RCPatOr (List.map (subst_pat_iterator y t) pl)
-  )
+  | RCPatOr pl -> RCPatOr (List.map (subst_pat_iterator y t) pl)))
 
 let drop_notations_pattern looked_for =
   (* At toplevel, Constructors and Inductives are accepted, in recursive calls
@@ -1223,6 +1211,14 @@ let drop_notations_pattern looked_for =
   let test_kind top =
     if top then looked_for else function ConstructRef _ -> () | _ -> raise Not_found
   in
+  (** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+  let rec rcp_of_glob x = CAst.(map (function
+    | GVar id -> RCPatAtom (Some id)
+    | GHole (_,_,_) -> RCPatAtom (None)
+    | GRef (g,_) -> RCPatCstr (g,[],[])
+    | GApp ({ v = GRef (g,_) }, l) -> RCPatCstr (g, List.map rcp_of_glob l,[])
+    | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr "))) x
+  in
   let rec drop_syndef top scopes re pats =
     let (loc,qid) = qualid_of_reference re in
     try
@@ -1296,7 +1292,8 @@ let drop_notations_pattern looked_for =
         CAst.make ?loc @@ RCPatCstr (g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
     | CPatNotation ("- _",([{ CAst.v = CPatPrim(Numeral p) }],[]),[])
 	when Bigint.is_strictly_pos p ->
-      fst (Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes)
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (ensure_kind false loc) (Numeral (Bigint.neg p)) scopes in
+      rcp_of_glob pat
     | CPatNotation ("( _ )",([a],[]),[]) ->
       in_pat top scopes a
     | CPatNotation (ntn, fullargs,extrargs) ->
@@ -1309,7 +1306,9 @@ let drop_notations_pattern looked_for =
       in_not top loc scopes (subst,substlist) extrargs c
     | CPatDelimiters (key, e) ->
       in_pat top (None,find_delimiters_scope ?loc key::snd scopes) e
-    | CPatPrim p -> fst (Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes)
+    | CPatPrim p ->
+      let pat, _df = Notation.interp_prim_token_cases_pattern_expr ?loc (test_kind false) p scopes in
+      rcp_of_glob pat
     | CPatAtom Some id ->
       begin
 	match drop_syndef top scopes id [] with
@@ -1318,8 +1317,21 @@ let drop_notations_pattern looked_for =
       end
     | CPatAtom None -> CAst.make ?loc @@ RCPatAtom None
     | CPatOr pl     -> CAst.make ?loc @@ RCPatOr (List.map (in_pat top scopes) pl)
-    | CPatCast _ ->
-      assert false
+    | CPatCast (_,_) ->
+      (* We raise an error if the pattern contains a cast, due to
+         current restrictions on casts in patterns. Cast in patterns
+         are supportted only in local binders and only at top
+         level. In fact, they are currently eliminated by the
+         parser. The only reason why they are in the
+         [cases_pattern_expr] type is that the parser needs to factor
+         the "(c : t)" notation with user defined notations (such as
+         the pair). In the long term, we will try to support such
+         casts everywhere, and use them to print the domains of
+         lambdas in the encoding of match in constr. This check is
+         here and not in the parser because it would require
+         duplicating the levels of the [pattern] rule. *)
+      CErrors.user_err ?loc ~hdr:"drop_notations_pattern"
+                            (Pp.strbrk "Casts are not supported in this pattern.")
   and in_pat_sc scopes x = in_pat false (x,snd scopes)
   and in_not top loc scopes (subst,substlist as fullsubst) args = function
     | NVar id ->
@@ -1367,7 +1379,7 @@ let drop_notations_pattern looked_for =
 let rec intern_pat genv aliases pat =
   let intern_cstr_with_all_args loc c with_letin idslpl1 pl2 =
     let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
-    let (ids',pll) = product_of_cases_patterns aliases.alias_ids (idslpl1@idslpl2) in
+    let (ids',pll) = product_of_cases_patterns aliases (idslpl1@idslpl2) in
     let pl' = List.map (fun (asubst,pl) ->
       (asubst, CAst.make ?loc @@ PatCstr (c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
@@ -1402,40 +1414,7 @@ let rec intern_pat genv aliases pat =
       check_or_pat_variables loc ids (List.tl idsl);
       (ids,List.flatten pl')
 
-(* [check_no_patcast p] raises an error if [p] contains a cast. This code is a
-   bit ad-hoc, and is due to current restrictions on casts in patterns. We
-   support them only in local binders and only at top level. In fact, they are
-   currently eliminated by the parser. The only reason why they are in the
-   [cases_pattern_expr] type is that the parser needs to factor the "(c : t)"
-   notation with user defined notations (such as the pair). In the long term, we
-   will try to support such casts everywhere, and use them to print the domains
-   of lambdas in the encoding of match in constr. We put this check here and not
-   in the parser because it would require to duplicate the levels of the
-   [pattern] rule. *)
-let rec check_no_patcast pt = match CAst.(pt.v) with
-  | CPatCast (_,_) ->
-     CErrors.user_err ?loc:pt.CAst.loc ~hdr:"check_no_patcast"
-                           (Pp.strbrk "Casts are not supported here.")
-  | CPatDelimiters(_,p)
-  | CPatAlias(p,_) -> check_no_patcast p
-  | CPatCstr(_,opl,pl) ->
-     Option.iter (List.iter check_no_patcast) opl;
-     List.iter check_no_patcast pl
-  | CPatOr pl ->
-     List.iter check_no_patcast pl
-  | CPatNotation(_,subst,pl) ->
-     check_no_patcast_subst subst;
-     List.iter check_no_patcast pl
-  | CPatRecord prl ->
-     List.iter (fun (_,p) -> check_no_patcast p) prl
-  | CPatAtom _ | CPatPrim _ -> ()
-
-and check_no_patcast_subst (pl,pll) =
-  List.iter check_no_patcast pl;
-  List.iter (List.iter check_no_patcast) pll
-
 let intern_cases_pattern genv scopes aliases pat =
-  check_no_patcast pat;
   intern_pat genv aliases
     (drop_notations_pattern (function ConstructRef _ -> () | _ -> raise Not_found) scopes pat)
 
@@ -1444,7 +1423,6 @@ let _ =
     fun scopes p -> intern_cases_pattern (Global.env ()) scopes empty_alias p
 
 let intern_ind_pattern genv scopes pat =
-  check_no_patcast pat;
   let no_not =
     try
       drop_notations_pattern (function (IndRef _ | ConstructRef _) -> () | _ -> raise Not_found) scopes pat
@@ -1459,7 +1437,7 @@ let intern_ind_pattern genv scopes pat =
       let idslpl1 = List.rev_map (intern_pat genv empty_alias) expl_pl in
       let idslpl2 = List.map (intern_pat genv empty_alias) pl2 in
       (with_letin,
-       match product_of_cases_patterns [] (List.rev_append idslpl1 idslpl2) with
+       match product_of_cases_patterns empty_alias (List.rev_append idslpl1 idslpl2) with
        | _,[_,pl] -> (c,chop_params_pattern loc c pl with_letin)
        | _ -> error_bad_inductive_type ?loc)
     | x -> error_bad_inductive_type ?loc
@@ -1798,7 +1776,7 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   and intern_multiple_pattern env n (loc,pl) =
     let idsl_pll = List.map (intern_cases_pattern globalenv (None,env.scopes) empty_alias) pl in
     check_number_of_pattern loc n pl;
-    product_of_cases_patterns [] idsl_pll
+    product_of_cases_patterns empty_alias idsl_pll
 
   (* Expands a disjunction of multiple pattern *)
   and intern_disjunctive_multiple_pattern env loc n mpl =
@@ -2073,8 +2051,6 @@ let interp_binder_evars env evdref na t =
   let t' = locate_if_hole ?loc:(loc_of_glob_constr t) na t in
   understand_tcc_evars env evdref ~expected_type:IsType t'
 
-open Environ
-
 let my_intern_constr env lvar acc c =
   internalize env acc false lvar c
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 758d4e650..fdd50c6a1 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -18,7 +18,6 @@ open Constrexpr
 open Notation_term
 open Pretyping
 open Misctypes
-open Decl_kinds
 
 (** Translation from front abstract syntax of term to untyped terms (glob_constr) *)
 
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index deb567865..cfc6e6c2a 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -19,7 +19,6 @@ open Typeclasses_errors
 open Pp
 open Libobject
 open Nameops
-open Misctypes
 open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
@@ -119,74 +118,14 @@ let free_vars_of_binders ?(bound=Id.Set.empty) l (binders : local_binder_expr li
     | [] -> bdvars, l
   in aux bound l binders
 
-let add_name_to_ids set na =
-  match na with
-  | Anonymous -> set
-  | Name id -> Id.Set.add id set
-
 let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.empty) =
-  let rec vars bound vs { loc; CAst.v = t } = match t with
-    | GVar id ->
+  let rec vars bound vs t = match t with
+    | { loc; CAst.v = GVar id } ->
 	if is_freevar bound (Global.env ()) id then
 	  if Id.List.mem_assoc_sym id vs then vs
 	  else (Loc.tag ?loc id) :: vs
 	else vs
-
-    | GApp (f,args) -> List.fold_left (vars bound) vs (f::args)
-    | GLambda (na,_,ty,c) | GProd (na,_,ty,c) ->
-	let vs' = vars bound vs ty in
-	let bound' = add_name_to_ids bound na in
-	vars bound' vs' c
-    | GLetIn (na,b,ty,c) ->
-	let vs' = vars bound vs b in
-	let vs'' = Option.fold_left (vars bound) vs' ty in
-	let bound' = add_name_to_ids bound na in
-	vars bound' vs'' c
-    | GCases (sty,rtntypopt,tml,pl) ->
-	let vs1 = vars_option bound vs rtntypopt in
-	let vs2 = List.fold_left (fun vs (tm,_) -> vars bound vs tm) vs1 tml in
-	List.fold_left (vars_pattern bound) vs2 pl
-    | GLetTuple (nal,rtntyp,b,c) ->
-	let vs1 = vars_return_type bound vs rtntyp in
-	let vs2 = vars bound vs1 b in
-	let bound' = List.fold_left add_name_to_ids bound nal in
-	vars bound' vs2 c
-    | GIf (c,rtntyp,b1,b2) ->
-	let vs1 = vars_return_type bound vs rtntyp in
-	let vs2 = vars bound vs1 c in
-	let vs3 = vars bound vs2 b1 in
-	vars bound vs3 b2
-    | GRec (fk,idl,bl,tyl,bv) ->
-	let bound' = Array.fold_right Id.Set.add idl bound in
-	let vars_fix i vs fid =
-	  let vs1,bound1 =
-	    List.fold_left
-	      (fun (vs,bound) (na,k,bbd,bty) ->
-		 let vs' = vars_option bound vs bbd in
-		 let vs'' = vars bound vs' bty in
-		 let bound' = add_name_to_ids bound na in
-		 (vs'',bound')
-	      )
-	      (vs,bound')
-	      bl.(i)
-	  in
-	  let vs2 = vars bound1 vs1 tyl.(i) in
-	  vars bound1 vs2 bv.(i)
-	in
-	Array.fold_left_i vars_fix vs idl
-    | GCast (c,k) -> let v = vars bound vs c in
-	(match k with CastConv t | CastVM t -> vars bound v t | _ -> v)
-    | (GSort _ | GHole _ | GRef _ | GEvar _ | GPatVar _) -> vs
-
-  and vars_pattern bound vs (loc,(idl,p,c)) =
-    let bound' = List.fold_right Id.Set.add idl bound  in
-    vars bound' vs c
-
-  and vars_option bound vs = function None -> vs | Some p -> vars bound vs p
-
-  and vars_return_type bound vs (na,tyopt) =
-    let bound' = add_name_to_ids bound na in
-    vars_option bound' vs tyopt
+    | c -> Glob_ops.fold_glob_constr_with_binders Id.Set.add vars bound vs c
   in fun rt -> 
     let vars = List.rev (vars bound [] rt) in
       List.iter (fun (loc, id) ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 6b963b8c8..d19654b10 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
@@ -445,18 +444,22 @@ let notation_of_prim_token = function
   | Numeral n -> "- "^(to_string (neg n))
   | String _ -> raise Not_found
 
-let find_prim_token ?loc g 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
+  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 interp_prim_token_gen ?loc g p local_scopes =
   let scopes = make_current_scopes local_scopes in
   let p_as_ntn = try notation_of_prim_token p with Not_found -> "" in
   try find_interpretation p_as_ntn (find_prim_token ?loc g p) scopes
@@ -466,22 +469,18 @@ let interp_prim_token_gen g ?loc p local_scopes =
       | Numeral n -> str "No interpretation for numeral " ++ str (to_string n)
       | String s -> str "No interpretation for string " ++ qs s) ++ str ".")
 
-let interp_prim_token =
-  interp_prim_token_gen (fun x -> x)
+let interp_prim_token ?loc =
+  interp_prim_token_gen ?loc (fun _ -> ())
 
-(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
-
-let rec rcp_of_glob looked_for = CAst.map (function
-  | GVar id       -> RCPatAtom (Some id)
-  | GHole (_,_,_) -> RCPatAtom None
-  | GRef (g,_)    -> looked_for g; RCPatCstr (g,[],[])
-  | GApp ({ CAst.v = GRef (g,_)},l) ->
-    looked_for g; RCPatCstr (g, List.map (rcp_of_glob looked_for) l,[])
-  | _ -> raise Not_found
-  )
+let rec check_allowed_ref_in_pat looked_for = CAst.(with_val (function
+  | GVar _ | GHole _ -> ()
+  | GRef (g,_) -> looked_for g
+  | GApp ({ v = GRef (g,_) },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 ?loc (check_allowed_ref_in_pat looked_for) p
 
 let interp_notation ?loc ntn local_scopes =
   let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation.mli b/interp/notation.mli
index 10c7b85e4..d271a88fe 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -85,8 +85,9 @@ val declare_string_interpreter : scope_name -> required_module ->
 
 val interp_prim_token : ?loc:Loc.t -> prim_token -> local_scopes ->
   glob_constr * (notation_location * scope_name option)
+(* This function returns a glob_const representing a pattern *)
 val interp_prim_token_cases_pattern_expr : ?loc:Loc.t -> (global_reference -> unit) -> prim_token ->
-  local_scopes -> raw_cases_pattern_expr * (notation_location * scope_name option)
+  local_scopes -> glob_constr * (notation_location * scope_name option)
 
 (** Return the primitive token associated to a [term]/[cases_pattern];
    raise [No_match] if no such token *)
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index dd3043803..74644b206 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1154,10 +1154,6 @@ let term_of_binder bi = CAst.make @@ match bi with
   | Name id -> GVar id
   | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
 
-type glob_decl2 =
-    (name, cases_pattern) Util.union * Decl_kinds.binding_kind *
-      glob_constr option * glob_constr
-
 let match_notation_constr u c (metas,pat) =
   let terms,binders,termlists,binderlists =
     match_ false u ([],[]) metas ([],[],[],[]) c pat in
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index c0dd9e45c..34fc5b2dc 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -6,9 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Misctypes
-open Tactypes
 open Genarg
 open Geninterp
 
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 44a176d94..6a98ee64d 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -10,7 +10,6 @@
 
 open Loc
 open Names
-open Term
 open EConstr
 open Libnames
 open Globnames
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index c3f4c4f30..ed7b0b70d 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -106,5 +106,3 @@ let search_syntactic_definition kn =
   let def = out_pat pat in
   verbose_compat kn def v;
   def
-
-open Goptions
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index eb89b2ef2..4ffb7020f 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -179,8 +179,13 @@ let split_at_annot bl na =
               in
               (List.rev ans, CLocalAssum (r, k, t) :: rest)
             end
-	| CLocalDef _ as x :: rest -> aux (x :: acc) rest
-        | CLocalPattern (loc,_) :: rest ->
+	| CLocalDef ((_,na),_,_) as x :: rest ->
+           if Name.equal (Name id) na then
+             user_err ?loc
+               (Nameops.pr_id id ++ str" must be a proper parameter and not a local definition.")
+           else
+             aux (x :: acc) rest
+        | CLocalPattern (_,_) :: rest ->
             Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
             user_err ?loc