Merge branch 'v8.5'

2 files changed, 21 insertions, 25 deletions

diff --git a/interp/interp.mllib b/interp/interp.mllib
index c9a0315267..96b52959a0 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -3,12 +3,12 @@ Constrarg
 Genintern
 Constrexpr_ops
 Notation_ops
-Topconstr
 Ppextend
 Notation
 Dumpglob
 Syntax_def
 Smartlocate
+Topconstr
 Reserve
 Impargs
 Implicit_quantifiers
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 837630183e..db38a85d42 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -38,27 +38,11 @@ let error_invalid_pattern_notation loc =
 (**********************************************************************)
 (* Functions on constr_expr *)
 
-let ids_of_cases_indtype =
-  let rec vars_of ids = function
-    (* We deal only with the regular cases *)
-    | (CPatCstr (_,_,l1,l2)|CPatNotation (_,_,(l1,[]),l2)) ->
-      List.fold_left vars_of (List.fold_left vars_of [] l2) l1
-    (* assume the ntn is applicative and does not instantiate the head !! *)
-    | CPatDelimiters(_,_,c) -> vars_of ids c
-    | CPatAtom (_, Some (Libnames.Ident (_, x))) -> x::ids
-    | _ -> ids in
-  vars_of []
-
-let ids_of_cases_tomatch tms =
-  List.fold_right
-    (fun (_,ona,indnal) l ->
-      Option.fold_right (fun t -> (@) (ids_of_cases_indtype t))
-      indnal (Option.fold_right (Loc.down_located name_cons) ona l))
-    tms []
-
 let is_constructor id =
-  try ignore (Nametab.locate_extended (qualid_of_ident id)); true
-  with Not_found -> true
+  try Globnames.isConstructRef
+        (Smartlocate.global_of_extended_global
+           (Nametab.locate_extended (qualid_of_ident id)))
+  with Not_found -> false
 
 let rec cases_pattern_fold_names f a = function
   | CPatRecord (_, l) ->
@@ -82,6 +66,17 @@ let ids_of_pattern_list =
       (List.fold_left (cases_pattern_fold_names Id.Set.add)))
     Id.Set.empty
 
+let ids_of_cases_indtype p =
+  Id.Set.elements (cases_pattern_fold_names Id.Set.add Id.Set.empty p)
+
+let ids_of_cases_tomatch tms =
+  List.fold_right
+    (fun (_, ona, indnal) l ->
+      Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
+      indnal
+        (Option.fold_right (Loc.down_located (name_fold Id.Set.add)) ona l))
+    tms Id.Set.empty
+
 let rec fold_constr_expr_binders g f n acc b = function
   | (nal,bk,t)::l ->
       let nal = snd (List.split nal) in
@@ -119,7 +114,7 @@ let fold_constr_expr_with_binders g f n acc = function
   | CRecord (loc,l) -> List.fold_left (fun acc (id, c) -> f n acc c) acc l
   | CCases (loc,sty,rtnpo,al,bl) ->
       let ids = ids_of_cases_tomatch al in
-      let acc = Option.fold_left (f (List.fold_right g ids n)) acc rtnpo in
+      let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
       List.fold_right (fun (loc,patl,rhs) acc ->
 	let ids = ids_of_pattern_list patl in
@@ -220,10 +215,11 @@ let map_constr_expr_with_binders g f e = function
   | CPrim _ | CRef _ as x -> x
   | CRecord (loc,l) -> CRecord (loc,List.map (fun (id, c) -> (id, f e c)) l)
   | CCases (loc,sty,rtnpo,a,bl) ->
-      (* TODO: apply g on the binding variables in pat... *)
-      let bl = List.map (fun (loc,pat,rhs) -> (loc,pat,f e rhs)) bl in
+      let bl = List.map (fun (loc,patl,rhs) ->
+        let ids = ids_of_pattern_list patl in
+        (loc,patl,f (Id.Set.fold g ids e) rhs)) bl in
       let ids = ids_of_cases_tomatch a in
-      let po = Option.map (f (List.fold_right g ids e)) rtnpo in
+      let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (loc, sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
   | CLetTuple (loc,nal,(ona,po),b,c) ->
       let e' = List.fold_right (Loc.down_located (name_fold g)) nal e in