From 70930579d8454a4ff50ee0ea1e97a55863bf01f6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 2 Apr 2017 15:53:14 +0200
Subject: More explicit message when a {struct x} argument refers to a local
 definition.

---
 interp/topconstr.ml | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 89e04b69d2..513fa8f161 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -176,7 +176,12 @@ let split_at_annot bl na =
               in
               (List.rev ans, CLocalAssum (r, k, t) :: rest)
             end
-	| CLocalDef _ as x :: rest -> aux (x :: acc) 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 (loc,_,_) :: rest ->
             Loc.raise ~loc (Stream.Error "pattern with quote not allowed after fix")
 	| [] ->
-- 
cgit v1.2.3


From 4e70791036a1ab189579e109b428f46f45698b59 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 13 Apr 2017 12:13:04 +0200
Subject: Adding a fold_glob_constr_with_binders combinator.

Binding generalizable_vars_of_glob_constr, occur_glob_constr,
free_glob_vars, and bound_glob_vars on it.

Most of the functions of which it factorizes the code were bugged with
respect to bindings in the return clause of "match" and in either the
types or the bodies of "fix/cofix".
---
 interp/implicit_quantifiers.ml | 56 +-----------------------------------------
 1 file changed, 1 insertion(+), 55 deletions(-)

(limited to 'interp')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 7f11c0a3b6..d6749e918f 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -131,61 +131,7 @@ let generalizable_vars_of_glob_constr ?(bound=Id.Set.empty) ?(allowed=Id.Set.emp
 	  if Id.List.mem_assoc id vs then vs
 	  else (id, loc) :: vs
 	else vs
-    | GApp (loc,f,args) -> List.fold_left (vars bound) vs (f::args)
-    | GLambda (loc,na,_,ty,c) | GProd (loc,na,_,ty,c) ->
-	let vs' = vars bound vs ty in
-	let bound' = add_name_to_ids bound na in
-	vars bound' vs' c
-    | GLetIn (loc,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 (loc,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 (loc,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 (loc,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 (loc,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 (loc,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 (id, loc) ->
-- 
cgit v1.2.3


From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 interp/notation_ops.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'interp')

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 8b4fadb5a0..d08fb107be 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -1141,10 +1141,6 @@ let term_of_binder = function
   | Name id -> GVar (Loc.ghost,id)
   | Anonymous -> GHole (Loc.ghost,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
-- 
cgit v1.2.3


From 4e84e83911c1cf7613a35b921b1e68e097f84b5a Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:11:47 +0200
Subject: Remove unused [open] statements

---
 interp/constrintern.ml  | 2 --
 interp/constrintern.mli | 1 -
 interp/stdarg.ml        | 2 --
 interp/stdarg.mli       | 1 -
 interp/syntax_def.ml    | 2 --
 5 files changed, 8 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d75487ecf3..389880c5c5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -2045,8 +2045,6 @@ let interp_binder_evars env evdref na t =
   let t' = locate_if_hole (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 758d4e650b..fdd50c6a1e 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/stdarg.ml b/interp/stdarg.ml
index 341ff5662c..5920b0d508 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 113fe40ba7..ac40a23281 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 c3f4c4f302..ed7b0b70d4 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
-- 
cgit v1.2.3


From b20d52da0d040fe37bb75b0b739ad7686f9af127 Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Sat, 22 Apr 2017 12:55:46 +0200
Subject: Warning 29: non escaped end of line may be non portable

---
 interp/constrintern.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 389880c5c5..3f99a3c7c0 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -855,9 +855,9 @@ let intern_qualid loc qid intern env lvar us args =
       | Some _, GApp (loc, GRef (loc', ref, None), arg) ->
          GApp (loc, GRef (loc', 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
 
-- 
cgit v1.2.3


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')

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 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 26 Apr 2017 12:15:26 +0200
Subject: Renaming allow_patvar flag of intern_gen into pattern_mode.

This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
---
 interp/constrintern.ml  | 12 ++++++------
 interp/constrintern.mli |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d75487ecf3..94924374a8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1516,7 +1516,7 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
+let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
   let rec intern env = function
     | CRef (ref,us) as x ->
 	let (c,imp,subscopes,l),_ =
@@ -1747,9 +1747,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
         in
 	GHole (loc, k, naming, solve)
     (* Parsing pattern variables *)
-    | CPatVar (loc, n) when allow_patvar ->
+    | CPatVar (loc, n) when pattern_mode ->
 	GPatVar (loc, (true,n))
-    | CEvar (loc, n, []) when allow_patvar ->
+    | CEvar (loc, n, []) when pattern_mode ->
 	GPatVar (loc, (false,n))
     (* end *)
     (* Parsing existential variables *)
@@ -1934,13 +1934,13 @@ let empty_ltac_sign = {
 }
 
 let intern_gen kind env
-               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
+               ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
                c =
   let tmp_scope = scope_of_type_kind kind in
   internalize env {ids = extract_ids env; unb = false;
 		         tmp_scope = tmp_scope; scopes = [];
 			 impls = impls}
-    allow_patvar (ltacvars, Id.Map.empty) c
+    pattern_mode (ltacvars, Id.Map.empty) c
 
 let intern_constr env c = intern_gen WithoutTypeConstraint env c
 
@@ -2013,7 +2013,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
 
 let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
   let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
-            ~allow_patvar:true ~ltacvars env c in
+            ~pattern_mode:true ~ltacvars env c in
   pattern_of_glob_constr c
 
 let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 758d4e650b..2142d42bce 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -82,7 +82,7 @@ val intern_constr : env -> constr_expr -> glob_constr
 val intern_type : env -> constr_expr -> glob_constr
 
 val intern_gen : typing_constraint -> env ->
-  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
+  ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
-- 
cgit v1.2.3


From 7943b1fade775af48917d54878e65b80217be038 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 28 Apr 2017 16:15:10 +0200
Subject: Using a more explicit algebraic type for evars of kind "MatchingVar".

A priori considered to be a good programming style.
---
 interp/constrextern.ml | 12 +++++++-----
 interp/constrintern.ml |  4 ++--
 2 files changed, 9 insertions(+), 7 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 59b8b4e5b9..bdbfd8c277 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -654,9 +654,11 @@ let rec extern inctx scopes vars r =
   | GEvar (loc,n,l) ->
       extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (loc,(b,n)) ->
-      if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
-        if b then CPatVar (loc,n) else CEvar (loc,n,[])
+  | GPatVar (loc,kind) ->
+       if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
+       (match kind with
+         | Evar_kinds.SecondOrderPatVar n -> CPatVar (loc,n)
+         | Evar_kinds.FirstOrderPatVar n -> CEvar (loc,n,[]))
 
   | GApp (loc,f,args) ->
       (match f with
@@ -1029,13 +1031,13 @@ let rec glob_of_pat env sigma = function
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar (loc,id)
   | PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
-  | PMeta (Some n) -> GPatVar (loc,(false,n))
+  | PMeta (Some n) -> GPatVar (loc,Evar_kinds.FirstOrderPatVar n)
   | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None),
 			 [glob_of_pat env sigma c])
   | PApp (f,args) ->
       GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
-      GApp (loc,GPatVar (loc,(true,n)),
+      GApp (loc,GPatVar (loc,Evar_kinds.SecondOrderPatVar n),
         List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
       GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 94924374a8..ea1802ccfa 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1748,9 +1748,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	GHole (loc, k, naming, solve)
     (* Parsing pattern variables *)
     | CPatVar (loc, n) when pattern_mode ->
-	GPatVar (loc, (true,n))
+	GPatVar (loc, Evar_kinds.SecondOrderPatVar n)
     | CEvar (loc, n, []) when pattern_mode ->
-	GPatVar (loc, (false,n))
+	GPatVar (loc, Evar_kinds.FirstOrderPatVar n)
     (* end *)
     (* Parsing existential variables *)
     | CEvar (loc, n, l) ->
-- 
cgit v1.2.3


From 4f742e14441581ece247d33020055f15732f126b Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Apr 2017 22:14:09 +0200
Subject: Revert "Using a more explicit algebraic type for evars of kind
 "MatchingVar"."

I'm sure this was pushed by accident, since testing shows immediately
that it breaks the compilation of the ssreflect plugin, hence all
developments relying on it in Travis.
---
 interp/constrextern.ml | 12 +++++-------
 interp/constrintern.ml |  4 ++--
 2 files changed, 7 insertions(+), 9 deletions(-)

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index bdbfd8c277..59b8b4e5b9 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -654,11 +654,9 @@ let rec extern inctx scopes vars r =
   | GEvar (loc,n,l) ->
       extern_evar loc n (List.map (on_snd (extern false scopes vars)) l)
 
-  | GPatVar (loc,kind) ->
-       if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
-       (match kind with
-         | Evar_kinds.SecondOrderPatVar n -> CPatVar (loc,n)
-         | Evar_kinds.FirstOrderPatVar n -> CEvar (loc,n,[]))
+  | GPatVar (loc,(b,n)) ->
+      if !print_meta_as_hole then CHole (loc, None, Misctypes.IntroAnonymous, None) else
+        if b then CPatVar (loc,n) else CEvar (loc,n,[])
 
   | GApp (loc,f,args) ->
       (match f with
@@ -1031,13 +1029,13 @@ let rec glob_of_pat env sigma = function
       with Not_found -> Id.of_string ("_UNBOUND_REL_"^(string_of_int n)) in
       GVar (loc,id)
   | PMeta None -> GHole (loc,Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
-  | PMeta (Some n) -> GPatVar (loc,Evar_kinds.FirstOrderPatVar n)
+  | PMeta (Some n) -> GPatVar (loc,(false,n))
   | PProj (p,c) -> GApp (loc,GRef (loc, ConstRef (Projection.constant p),None),
 			 [glob_of_pat env sigma c])
   | PApp (f,args) ->
       GApp (loc,glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
   | PSoApp (n,args) ->
-      GApp (loc,GPatVar (loc,Evar_kinds.SecondOrderPatVar n),
+      GApp (loc,GPatVar (loc,(true,n)),
         List.map (glob_of_pat env sigma) args)
   | PProd (na,t,c) ->
       GProd (loc,na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index ea1802ccfa..94924374a8 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1748,9 +1748,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	GHole (loc, k, naming, solve)
     (* Parsing pattern variables *)
     | CPatVar (loc, n) when pattern_mode ->
-	GPatVar (loc, Evar_kinds.SecondOrderPatVar n)
+	GPatVar (loc, (true,n))
     | CEvar (loc, n, []) when pattern_mode ->
-	GPatVar (loc, Evar_kinds.FirstOrderPatVar n)
+	GPatVar (loc, (false,n))
     (* end *)
     (* Parsing existential variables *)
     | CEvar (loc, n, l) ->
-- 
cgit v1.2.3


From 1c8ed18d5f67d7d5656342584b8dcf8a441cb87f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Apr 2017 22:15:06 +0200
Subject: Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."

This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
---
 interp/constrintern.ml  | 12 ++++++------
 interp/constrintern.mli |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 94924374a8..d75487ecf3 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1516,7 +1516,7 @@ let extract_explicit_arg imps args =
 (**********************************************************************)
 (* Main loop                                                          *)
 
-let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
+let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
   let rec intern env = function
     | CRef (ref,us) as x ->
 	let (c,imp,subscopes,l),_ =
@@ -1747,9 +1747,9 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         in
 	GHole (loc, k, naming, solve)
     (* Parsing pattern variables *)
-    | CPatVar (loc, n) when pattern_mode ->
+    | CPatVar (loc, n) when allow_patvar ->
 	GPatVar (loc, (true,n))
-    | CEvar (loc, n, []) when pattern_mode ->
+    | CEvar (loc, n, []) when allow_patvar ->
 	GPatVar (loc, (false,n))
     (* end *)
     (* Parsing existential variables *)
@@ -1934,13 +1934,13 @@ let empty_ltac_sign = {
 }
 
 let intern_gen kind env
-               ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
+               ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign)
                c =
   let tmp_scope = scope_of_type_kind kind in
   internalize env {ids = extract_ids env; unb = false;
 		         tmp_scope = tmp_scope; scopes = [];
 			 impls = impls}
-    pattern_mode (ltacvars, Id.Map.empty) c
+    allow_patvar (ltacvars, Id.Map.empty) c
 
 let intern_constr env c = intern_gen WithoutTypeConstraint env c
 
@@ -2013,7 +2013,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c =
 
 let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c =
   let c = intern_gen (if as_type then IsType else WithoutTypeConstraint)
-            ~pattern_mode:true ~ltacvars env c in
+            ~allow_patvar:true ~ltacvars env c in
   pattern_of_glob_constr c
 
 let interp_notation_constr ?(impls=empty_internalization_env) nenv a =
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 2142d42bce..758d4e650b 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -82,7 +82,7 @@ val intern_constr : env -> constr_expr -> glob_constr
 val intern_type : env -> constr_expr -> glob_constr
 
 val intern_gen : typing_constraint -> env ->
-  ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
+  ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> glob_constr
 
 val intern_pattern : env -> cases_pattern_expr ->
-- 
cgit v1.2.3


From e5bf991cd1094ff1d5bc2f121bb6e85c8b1320c0 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 5 May 2017 18:12:55 +0200
Subject: Remove dead code and unused open.

---
 interp/implicit_quantifiers.ml | 6 ------
 1 file changed, 6 deletions(-)

(limited to 'interp')

diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index d6749e918f..19c872b310 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,11 +118,6 @@ 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 = function
     | GVar (loc,id) ->
-- 
cgit v1.2.3


From a05cdcb00edbf0e35190f2d724c4a8c46d6cf9a3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 15 May 2017 03:00:04 +0200
Subject: Typo in comments of constrintern.

---
 interp/constrintern.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3f99a3c7c0..b57a046796 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -900,7 +900,7 @@ let interp_reference vars r =
 (**********************************************************************)
 (** {5 Cases }                                                        *)
 
-(** {6 Elemtary bricks } *)
+(** {6 Elementary bricks } *)
 let apply_scope_env env = function
   | [] -> {env with tmp_scope = None}, []
   | sc::scl -> {env with tmp_scope = sc}, scl
-- 
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/constrexpr_ops.ml  |  6 ------
 interp/constrexpr_ops.mli |  1 -
 interp/constrintern.ml    | 36 +++++++++++++++++++++++++++++++-----
 interp/notation.ml        | 25 +++++++++++++------------
 interp/notation.mli       |  4 +++-
 5 files changed, 47 insertions(+), 25 deletions(-)

(limited to 'interp')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index a592b4cff8..542f9feaf6 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -263,12 +263,6 @@ let cases_pattern_expr_loc = function
   | CPatDelimiters (loc,_,_) -> loc
   | CPatCast(loc,_,_) -> loc
 
-let raw_cases_pattern_expr_loc = function
-  | RCPatAlias (loc,_,_) -> loc
-  | RCPatCstr (loc,_,_,_) -> loc
-  | RCPatAtom (loc,_) -> loc
-  | RCPatOr (loc,_) -> loc
-
 let local_binder_loc = function
   | CLocalAssum ((loc,_)::_,_,t)
   | CLocalDef ((loc,_),t,None) -> Loc.merge loc (constr_loc t)
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index f6d97e107d..b547288e3f 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
 val cases_pattern_expr_loc : cases_pattern_expr -> Loc.t
-val raw_cases_pattern_expr_loc : raw_cases_pattern_expr -> Loc.t
 val local_binders_loc : local_binder_expr list -> Loc.t
 
 (** {6 Constructors}*)
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3f99a3c7c0..b183418009 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -900,6 +900,21 @@ let interp_reference vars r =
 (**********************************************************************)
 (** {5 Cases }                                                        *)
 
+(** Private internalization patterns *)
+type raw_cases_pattern_expr =
+  | RCPatAlias of Loc.t * raw_cases_pattern_expr * Id.t
+  | RCPatCstr  of Loc.t * Globnames.global_reference
+    * raw_cases_pattern_expr list * raw_cases_pattern_expr list
+  (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *)
+  | RCPatAtom  of Loc.t * Id.t option
+  | RCPatOr    of Loc.t * raw_cases_pattern_expr list
+
+let raw_cases_pattern_expr_loc = function
+  | RCPatAlias (loc,_,_) -> loc
+  | RCPatCstr (loc,_,_,_) -> loc
+  | RCPatAtom (loc,_) -> loc
+  | RCPatOr (loc,_) -> loc
+
 (** {6 Elemtary bricks } *)
 let apply_scope_env env = function
   | [] -> {env with tmp_scope = None}, []
@@ -1198,8 +1213,8 @@ let rec subst_pat_iterator y t p = match p with
   | RCPatAtom (_,id) ->
     begin match id with Some x when Id.equal x y -> t | _ -> p end
   | RCPatCstr (loc,id,l1,l2) ->
-     RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
-	       List.map (subst_pat_iterator y t) l2)
+    RCPatCstr (loc,id,List.map (subst_pat_iterator y t) l1,
+ 	       List.map (subst_pat_iterator y t) l2)
   | RCPatAlias (l,p,a) -> RCPatAlias (l,subst_pat_iterator y t p,a)
   | RCPatOr (l,pl) -> RCPatOr (l,List.map (subst_pat_iterator y t) pl)
 
@@ -1216,6 +1231,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 = function
+    | GVar (loc,id) -> RCPatAtom (loc,Some id)
+    | GHole (loc,_,_,_) -> RCPatAtom (loc,None)
+    | GRef (loc,g,_) -> RCPatCstr (loc, g,[],[])
+    | GApp (loc,GRef (_,g,_),l) -> RCPatCstr (loc, g, List.map rcp_of_glob l,[])
+    | _ -> CErrors.anomaly Pp.(str "Invalid return pattern from Notation.interp_prim_token_cases_pattern_expr ")
+  in
   let rec drop_syndef top scopes re pats =
     let (loc,qid) = qualid_of_reference re in
     try
@@ -1285,8 +1308,9 @@ let drop_notations_pattern looked_for =
         let (argscs1,_) = find_remaining_scopes expl_pl pl g in
         RCPatCstr (loc, g, List.map2 (in_pat_sc scopes) argscs1 expl_pl @ List.map (in_pat false scopes) pl, [])
     | CPatNotation (loc,"- _",([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)
+      when Bigint.is_strictly_pos p ->
+      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 (loc, ntn, fullargs,extrargs) ->
@@ -1299,7 +1323,9 @@ let drop_notations_pattern looked_for =
       in_not top loc scopes (subst,substlist) extrargs c
     | CPatDelimiters (loc, key, e) ->
       in_pat top (None,find_delimiters_scope loc key::snd scopes) e
-    | CPatPrim (loc,p) -> fst (Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes)
+    | CPatPrim (loc,p) ->
+      let (pat, _df) = Notation.interp_prim_token_cases_pattern_expr loc (test_kind false) p scopes in
+      rcp_of_glob pat
     | CPatAtom (loc, Some id) ->
       begin
 	match drop_syndef top scopes id [] with
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
diff --git a/interp/notation.mli b/interp/notation.mli
index 2e92a00a8c..300480ff1c 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -85,8 +85,10 @@ val declare_string_interpreter : scope_name -> required_module ->
 
 val interp_prim_token : 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.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 *)
-- 
cgit v1.2.3


From e4ca8679e6700cfd6563890eb7d9e4ee59bede57 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 15 May 2017 02:25:52 +0200
Subject: [interp] Rework check for casts inside patterns.

1969e10f25df0c913600099b7b98ea273a064017 introduced a check so a cast
in a pattern is not a fatal error.

We move this check to the internalization function, which is the
logical place to raise it, removing a bit boilerplate code.
---
 interp/constrintern.ml | 51 +++++++++++++++-----------------------------------
 1 file changed, 15 insertions(+), 36 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index b183418009..405d63dfe7 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1335,8 +1335,21 @@ let drop_notations_pattern looked_for =
     | CPatAtom (loc,None) -> RCPatAtom (loc,None)
     | CPatOr (loc, pl) ->
       RCPatOr (loc,List.map (in_pat top scopes) pl)
-    | CPatCast _ ->
-      assert false
+    | CPatCast (loc,_,_) ->
+      (* 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 ->
@@ -1418,40 +1431,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 = function
-  | CPatCast (loc,_,_) ->
-     CErrors.user_err ~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)
 
@@ -1460,7 +1440,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
-- 
cgit v1.2.3


From e2de94b90e8802fa5c5dc33c7daf6b8ce5646bfa Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 14 May 2017 00:10:57 +0200
Subject: Fixing a bug with nested "as" clauses in "match".

---
 interp/constrintern.ml | 28 ++++++++++++++--------------
 1 file changed, 14 insertions(+), 14 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index c916fcd886..80de11e3ee 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -947,17 +947,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 *)
@@ -1212,6 +1201,17 @@ let alias_of als = match als.alias_ids with
 
 *)
 
+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 p = match p with
   | RCPatAtom (_,id) ->
     begin match id with Some x when Id.equal x y -> t | _ -> p end
@@ -1376,7 +1376,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, PatCstr (loc,c,chop_params_pattern loc (fst c) pl with_letin,alias_of aliases))) pll in
     ids',pl' in
@@ -1466,7 +1466,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 (raw_cases_pattern_expr_loc x)
@@ -1796,7 +1796,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 =
-- 
cgit v1.2.3


From 00964706efe8f6b13e38b57ddb45fac516feb958 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 13 May 2017 23:31:08 +0200
Subject: Fixing bug #5222 (anomaly with "`pat" in the presence of scope
 delimiters).

We seized this opportunity to factorize the code for interning `pat
with more general pre-existing code.

More precisely: There was already a function to compute the free
variables of a pattern. Commit c6d9d4fb rewrote an approximation of it
and #5222 hits cases non-treated by this function. We remove the
partially-defined redundant code and use instead the existing code
since intern_cases_pattern, already called, was already doing this
computation. (In doing so, we discover a bug in merging names in the
presence of nested "as" clauses, which we fix in previous
commit. Additionally, intern_local_pattern was misleadingly overkill
to simply mean a folding on Id.Set.add and we avoid the detour.
---
 interp/constrintern.ml | 35 ++++++-----------------------------
 1 file changed, 6 insertions(+), 29 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 80de11e3ee..4e76fe9aae 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -432,31 +432,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 =
-  function
-  | CPatCstr (loc, 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 (loc, ro) ->
-      begin match ro with
-      | Some (Ident (loc, i)) -> (loc, i) :: il
-      | Some _ | None -> il
-      end
-  | CPatNotation (loc, 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 = CHole (loc, 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)
-
 type binder_data =
   | BDRawDef of (Loc.t * glob_binder)
   | BDPattern of
@@ -490,13 +465,15 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio
         | Some ty -> ty
         | None -> CHole(loc,None,Misctypes.IntroAnonymous,None)
       in
-      let env = intern_local_pattern intern lvar env 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 (loc,"",str "Unsupported nested \"as\" clause.");
+           il,cp
         | _ -> assert false
       in
-      let il = List.map snd (free_vars_of_pat [] p) in
+      let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
       (env, BDPattern(loc,(cp,il),lvar,env,tyc) :: bl)
 
 let intern_generalization intern env lvar loc bk ak c =
-- 
cgit v1.2.3