Extending support for mixing binders and terms in abbreviations.

3 files changed, 9 insertions, 26 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f82783f47d..9d0552817f 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -976,10 +976,6 @@ let split_by_type_pat ?loc ids subst =
   assert (terms = [] && termlists = []);
   subst
 
-let make_subst ids l =
-  let fold accu (id, scopes) a = Id.Map.add id (a, scopes) accu in
-  List.fold_left2 fold Id.Map.empty ids l
-
 let intern_notation intern env ntnvars loc ntn fullargs =
   (* Adjust to parsing of { } *)
   let ntn,fullargs = contract_curly_brackets ntn fullargs in
@@ -1113,8 +1109,7 @@ let intern_qualid ?(no_secvar=false) qid intern env ntnvars us args =
       if List.length args < nids then error_not_enough_arguments ?loc;
       let args1,args2 = List.chop nids args in
       check_no_explicitation args1;
-      let terms = make_subst ids (List.map fst args1) in
-      let subst = (terms, Id.Map.empty, Id.Map.empty, Id.Map.empty) in
+      let subst = split_by_type ids (List.map fst args1,[],[],[]) in
       let infos = (Id.Map.empty, env) in
       let c = instantiate_notation_constr loc intern intern_cases_pattern_as_binder ntnvars subst infos c in
       let loc = c.loc in
@@ -1624,8 +1619,8 @@ let drop_notations_pattern looked_for genv =
               let nvars = List.length vars in
               if List.length pats < nvars then error_not_enough_arguments ?loc:qid.loc;
               let pats1,pats2 = List.chop nvars pats in
-              let subst = make_subst vars pats1 in
-              let idspl1 = List.map (in_not false qid.loc scopes (subst, Id.Map.empty) []) args in
+              let subst = split_by_type_pat vars (pats1,[]) in
+              let idspl1 = List.map (in_not false qid.loc scopes subst []) args in
               let (_,argscs) = find_remaining_scopes pats1 pats2 g in
               Some (g, idspl1, List.map2 (in_pat_sc scopes) argscs pats2)
         | _ -> raise Not_found
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 7184f5ea29..bd3e234a91 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -8,7 +8,6 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Util
 open Pp
 open CErrors
 open Names
@@ -82,16 +81,9 @@ let in_syntax_constant : (bool * syndef) -> obj =
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
-type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-
-(* Coercions to the general format of notation that also supports
-   variables bound to list of expressions *)
-let in_pat (ids,ac) = (List.map (fun (id,sc) -> (id,((Constrexpr.InConstrEntrySomeLevel,sc),NtnTypeConstr))) ids,ac)
-let out_pat (ids,ac) = (List.map (fun (id,((_,sc),typ)) -> (id,sc)) ids,ac)
-
 let declare_syntactic_definition ~local deprecation id ~onlyparsing pat =
   let syndef =
-    { syndef_pattern = in_pat pat;
+    { syndef_pattern = pat;
       syndef_onlyparsing = onlyparsing;
       syndef_deprecation = deprecation;
     }
@@ -106,14 +98,12 @@ let warn_deprecated_syntactic_definition =
 
 let search_syntactic_definition ?loc kn =
   let syndef = KNmap.find kn !syntax_table in
-  let def = out_pat syndef.syndef_pattern in
   Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
-  def
+  syndef.syndef_pattern
 
 let search_filtered_syntactic_definition ?loc filter kn =
   let syndef = KNmap.find kn !syntax_table in
-  let def = out_pat syndef.syndef_pattern in
-  let res = filter def in
+  let res = filter syndef.syndef_pattern in
   if Option.has_some res then
     Option.iter (fun d -> warn_deprecated_syntactic_definition ?loc (kn,d)) syndef.syndef_deprecation;
   res
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 8b323462a1..66a3132f2a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -13,12 +13,10 @@ open Notation_term
 
 (** Syntactic definitions. *)
 
-type syndef_interpretation = (Id.t * subscopes) list * notation_constr
-
 val declare_syntactic_definition : local:bool -> Deprecation.t option -> Id.t ->
-  onlyparsing:bool -> syndef_interpretation -> unit
+  onlyparsing:bool -> interpretation -> unit
 
-val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> syndef_interpretation
+val search_syntactic_definition : ?loc:Loc.t -> KerName.t -> interpretation
 
 val search_filtered_syntactic_definition : ?loc:Loc.t ->
-  (syndef_interpretation -> 'a option) -> KerName.t -> 'a option
+  (interpretation -> 'a option) -> KerName.t -> 'a option