New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15375 85f007b7-540e-0410-9357-904b9bb8a0f7

20 files changed, 259 insertions, 516 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 62b8cdcea..299ea8d79 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -21,6 +21,8 @@ open Sign
 open Environ
 open Libnames
 open Impargs
+open Constrexpr
+open Notation_term
 open Topconstr
 open Glob_term
 open Glob_ops
@@ -456,7 +458,7 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
       match t with
 	| PatCstr (loc,_,_,na) ->
 	  let p = apply_notation_to_pattern loc
-	    (match_aconstr_cases_pattern t pat) allscopes vars keyrule in
+	    (match_notation_constr_cases_pattern t pat) allscopes vars keyrule in
 	  insert_pat_alias loc p na
 	| PatVar (loc,Anonymous) -> CPatAtom (loc, None)
 	| PatVar (loc,Name id) -> CPatAtom (loc, Some (Ident (loc,id)))
@@ -910,7 +912,7 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function
           | _ -> raise No_match in
 	(* Try matching ... *)
 	let terms,termlists,binders =
-          match_aconstr !print_universes t pat in
+          match_notation_constr !print_universes t pat in
 	(* Try availability of interpretation ... *)
         let e =
           match keyrule with
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index 21c33f3f3..38f8b6579 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -16,7 +16,8 @@ open Libnames
 open Nametab
 open Glob_term
 open Pattern
-open Topconstr
+open Constrexpr
+open Notation_term
 open Notation
 open Misctypes
 
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index d125caf54..91e0cf6a1 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -20,6 +20,8 @@ open Glob_ops
 open Pattern
 open Pretyping
 open Cases
+open Constrexpr
+open Notation_term
 open Topconstr
 open Nametab
 open Notation
@@ -254,8 +256,8 @@ let contract_pat_notation ntn (l,ll) =
 type intern_env = {
   ids: Names.Idset.t;
   unb: bool;
-  tmp_scope: Topconstr.tmp_scope_name option;
-  scopes: Topconstr.scope_name list;
+  tmp_scope: Notation_term.tmp_scope_name option;
+  scopes: Notation_term.scope_name list;
   impls: internalization_env }
 
 (**********************************************************************)
@@ -363,7 +365,8 @@ let rec check_capture ty = function
 let locate_if_isevar loc na = function
   | GHole _ ->
       (try match na with
-	| Name id -> glob_constr_of_aconstr loc (Reserve.find_reserved_type id)
+	| Name id -> glob_constr_of_notation_constr loc
+	               (Reserve.find_reserved_type id)
 	| Anonymous -> raise Not_found
       with Not_found -> GHole (loc, Evar_kinds.BinderType na))
   | x -> x
@@ -530,7 +533,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
   let rec aux (terms,binderopt as subst') (renaming,env) c =
     let subinfos = renaming,{env with tmp_scope = None} in
     match c with
-    | AVar id ->
+    | NVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
 	(* of the notations *)
@@ -545,7 +548,7 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
 	  (* Happens for local notation joint with inductive/fixpoint defs *)
 	  GVar (loc,id)
       end
-    | AList (x,_,iter,terminator,lassoc) ->
+    | NList (x,_,iter,terminator,lassoc) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (l,(scopt,subscopes)) = List.assoc x termlists in
@@ -556,12 +559,12 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
             (if lassoc then List.rev l else l) termin
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
-    | AHole (Evar_kinds.BinderType (Name id as na)) ->
+    | NHole (Evar_kinds.BinderType (Name id as na)) ->
       let na =
         try snd (coerce_to_name (fst (List.assoc id terms)))
         with Not_found -> na in
       GHole (loc,Evar_kinds.BinderType na)
-    | ABinderList (x,_,iter,terminator) ->
+    | NBinderList (x,_,iter,terminator) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (bl,(scopt,subscopes)) = List.assoc x binders in
@@ -575,15 +578,15 @@ let subst_aconstr_in_glob_constr loc intern lvar subst infos c =
 	make_letins letins res
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
-    | AProd (Name id, AHole _, c') when option_mem_assoc id binderopt ->
+    | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt ->
         let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
 	GProd (loc,na,bk,t,make_letins letins (aux subst' infos c'))
-    | ALambda (Name id,AHole _,c') when option_mem_assoc id binderopt ->
+    | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt ->
         let (loc,(na,bk,t)),letins = snd (Option.get binderopt) in
 	GLambda (loc,na,bk,t,make_letins letins (aux subst' infos c'))
     | t ->
-      glob_constr_of_aconstr_with_binders loc (traverse_binder subst)
-	(aux subst') subinfos t
+      glob_constr_of_notation_constr_with_binders loc
+        (traverse_binder subst) (aux subst') subinfos t
   in aux (terms,None) infos c
 
 let split_by_type ids =
@@ -887,7 +890,7 @@ let chop_params_pattern loc ind args with_letin =
 
 let subst_cases_pattern loc alias intern fullsubst env a =
   let rec aux alias (subst,substlist as fullsubst) = function
-  | AVar id ->
+  | NVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
 	(* of the notations *)
@@ -905,15 +908,15 @@ let subst_cases_pattern loc alias intern fullsubst env a =
 	  [[id],[]], PatVar (loc,Name id)
 	  *)
       end
-  | ARef (ConstructRef c) ->
+  | NRef (ConstructRef c) ->
       ([],[[], PatCstr (loc,c, [], alias)])
-  | AApp (ARef (ConstructRef cstr),args) ->
+  | NApp (NRef (ConstructRef cstr),args) ->
       let idslpll = List.map (aux Anonymous fullsubst) args in
       let ids',pll = product_of_cases_patterns [] idslpll in
       let pl' = List.map (fun (asubst,pl) ->
         asubst,PatCstr (loc,cstr,chop_params_pattern loc (fst cstr) pl false,alias)) pll in
 	ids', pl'
-  | AList (x,_,iter,terminator,lassoc) ->
+  | NList (x,_,iter,terminator,lassoc) ->
       (try
         (* All elements of the list are in scopes (scopt,subscopes) *)
 	let (l,(scopt,subscopes)) = List.assoc x substlist in
@@ -928,12 +931,12 @@ let subst_cases_pattern loc alias intern fullsubst env a =
 	  match pl with PatCstr (loc, c, pl, Anonymous) -> (asubst, PatCstr (loc, c, pl, alias)) | _ -> x) v
       with Not_found ->
           anomaly "Inconsistent substitution of recursive notation")
-  | AHole _ -> ([],[[], PatVar (loc,Anonymous)])
+  | NHole _ -> ([],[[], PatVar (loc,Anonymous)])
   | t -> error_invalid_pattern_notation loc
   in aux alias fullsubst a
 
 let subst_ind_pattern loc intern_ind_patt intern (subst,_ as fullsubst) env = function
-  | AVar id ->
+  | NVar id ->
       begin
 	(* subst remembers the delimiters stack in the interpretation *)
 	(* of the notations *)
@@ -944,9 +947,9 @@ let subst_ind_pattern loc intern_ind_patt intern (subst,_ as fullsubst) env = fu
 	with Not_found ->
 	  anomaly ("Unbound pattern notation variable: "^(string_of_id id))
       end
-  | ARef (IndRef c) ->
+  | NRef (IndRef c) ->
       false, (c, [])
-  | AApp (ARef (IndRef ind),args) ->
+  | NApp (NRef (IndRef ind),args) ->
       let idslpll = List.map (subst_cases_pattern loc Anonymous intern fullsubst env) args in
       begin
 	match product_of_cases_patterns [] idslpll with
@@ -973,11 +976,11 @@ let find_at_head looked_for add_params ref f pats env =
     | SynDef sp ->
       let (vars,a) = Syntax_def.search_syntactic_definition sp in
       (match a with
-	| ARef g ->
+	| NRef g ->
 	  let cstr = looked_for g in
 	  assert (vars=[]);
 	  cstr,add_params cstr, pats
-	| AApp (ARef g,args) ->
+	| NApp (NRef g,args) ->
 	  let cstr = looked_for g in
 	  let nvars = List.length vars in
 	  if List.length pats < nvars then error_not_enough_arguments loc;
@@ -1148,7 +1151,7 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
 	  in
 	intern_pat env aliases self_patt
   | CPatCstr (loc, head, pl) ->
-      if !Topconstr.oldfashion_patterns then
+      if !oldfashion_patterns then
 	let c,idslpl1,pl2 = mustbe_constructor loc (Some (List.length pl)) head intern_pat pl env in
 	let with_letin = check_constructor_length genv loc c false idslpl1 pl2 in
 	intern_cstr_with_all_args loc c with_letin idslpl1 pl2
@@ -1185,10 +1188,10 @@ let rec intern_cases_pattern genv env (ids,asubst as aliases) pat =
       intern_pat {env with scopes=find_delimiters_scope loc key::env.scopes;
 		    tmp_scope = None} aliases e
   | CPatAtom (loc, Some head) ->
-      (match maybe_constructor (if !Topconstr.oldfashion_patterns then Some 0 else None)
+      (match maybe_constructor (if !oldfashion_patterns then Some 0 else None)
 	  head intern_pat env with
 	 | ConstrPat (c,idspl) ->
-	   if !Topconstr.oldfashion_patterns then
+	   if !oldfashion_patterns then
 	     let with_letin = check_constructor_length genv loc c false idspl [] in
 	     intern_cstr_with_all_args loc c with_letin idspl []
 	   else
@@ -1463,7 +1466,7 @@ let internalize sigma globalenv env allow_patvar lvar c =
 	  (Option.fold_left (fun x (_,y) -> match y with | Name y' -> Idset.add y' x |_ -> x) acc na)
 	  inb) Idset.empty tms in
       (* as, in & return vars *)
-      let forbidden_vars = Option.cata Topconstr.free_vars_of_constr_expr as_in_vars rtnpo in
+      let forbidden_vars = Option.cata free_vars_of_constr_expr as_in_vars rtnpo in
       let tms,ex_ids,match_from_in = List.fold_right
 	(fun citm (inds,ex_ids,matchs) ->
 	  let ((tm,ind),extra_id,match_td) = intern_case_item env forbidden_vars citm in
@@ -1782,7 +1785,7 @@ let intern_constr_pattern sigma env ?(as_type=false) ?(ltacvars=([],[])) c =
   let c = intern_gen as_type ~allow_patvar:true ~ltacvars sigma env c in
   pattern_of_glob_constr c
 
-let interp_aconstr ?(impls=empty_internalization_env) vars recvars a =
+let interp_notation_constr ?(impls=empty_internalization_env) vars recvars a =
   let env = Global.env () in
   (* [vl] is intended to remember the scope of the free variables of [a] *)
   let vl = List.map (fun (id,typ) -> (id,(ref None,typ))) vars in
@@ -1790,7 +1793,7 @@ let interp_aconstr ?(impls=empty_internalization_env) vars recvars a =
 						tmp_scope = None; scopes = []; impls = impls}
     false (([],[]),vl) a in
   (* Translate and check that [c] has all its free variables bound in [vars] *)
-  let a = aconstr_of_glob_constr vars recvars c in
+  let a = notation_constr_of_glob_constr vars recvars c in
   (* Splits variables into those that are binding, bound, or both *)
   (* binding and bound *)
   let out_scope = function None -> None,[] | Some (a,l) -> a,l in
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 250871b9e..10fbde605 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -14,7 +14,8 @@ open Environ
 open Libnames
 open Glob_term
 open Pattern
-open Topconstr
+open Constrexpr
+open Notation_term
 open Termops
 open Pretyping
 open Misctypes
@@ -52,7 +53,7 @@ type var_internalization_data =
       (** impargs to automatically add to the variable, e.g. for "JMeq A a B b"
           in implicit mode, this is [A;B] and this adds (A:=A) and (B:=B) *)
     Impargs.implicit_status list * (** signature of impargs of the variable *)
-    scope_name option list (** subscopes of the args of the variable *)
+    Notation_term.scope_name option list (** subscopes of the args of the variable *)
 
 (** A map of free variables to their implicit arguments and scopes *)
 type internalization_env = var_internalization_data Idmap.t
@@ -175,10 +176,11 @@ val global_reference_in_absolute_module : dir_path -> identifier -> constr
     list is a set and this set is [true] for a variable occurring in
     term position, [false] for a variable occurring in binding
     position; [true;false] if in both kinds of position *)
-val interp_aconstr : ?impls:internalization_env ->
+val interp_notation_constr : ?impls:internalization_env ->
   (identifier * notation_var_internalization_type) list ->
   (identifier * identifier) list -> constr_expr ->
-  (identifier * (subscopes * notation_var_internalization_type)) list * aconstr
+  (identifier * (subscopes * notation_var_internalization_type)) list *
+  notation_constr
 
 (** Globalization options *)
 val parsing_explicit : bool ref
diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli
index 90b56e0a9..59a695ee6 100644
--- a/interp/dumpglob.mli
+++ b/interp/dumpglob.mli
@@ -34,10 +34,14 @@ val dump_moddef : Pp.loc -> Names.module_path -> string -> unit
 val dump_modref  : Pp.loc -> Names.module_path -> string -> unit
 val dump_reference  : Pp.loc -> string -> string -> string -> unit
 val dump_libref : Pp.loc -> Names.dir_path -> string -> unit
-val dump_notation_location : (int * int) list -> Topconstr.notation -> (Notation.notation_location * Topconstr.scope_name option) -> unit
+val dump_notation_location : (int * int) list -> Constrexpr.notation ->
+  (Notation.notation_location * Notation_term.scope_name option) -> unit
 val dump_binding : Pp.loc -> Names.Idset.elt -> unit
-val dump_notation : Pp.loc * (Topconstr.notation * Notation.notation_location) -> Topconstr.scope_name option -> bool -> unit
-val dump_constraint :  Topconstr.typeclass_constraint -> bool -> string -> unit
+val dump_notation :
+  Pp.loc * (Constrexpr.notation * Notation.notation_location) ->
+  Notation_term.scope_name option -> bool -> unit
+val dump_constraint :
+  Constrexpr.typeclass_constraint -> bool -> string -> unit
 
 val dump_string : string -> unit
 
diff --git a/interp/genarg.ml b/interp/genarg.ml
index 3597879de..bbb4ae0a1 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -13,7 +13,7 @@ open Names
 open Nameops
 open Nametab
 open Glob_term
-open Topconstr
+open Constrexpr
 open Term
 open Evd
 open Misctypes
diff --git a/interp/genarg.mli b/interp/genarg.mli
index de1fa0fef..7466ae46f 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -14,7 +14,7 @@ open Libnames
 open Glob_term
 open Genredexpr
 open Pattern
-open Topconstr
+open Constrexpr
 open Term
 open Evd
 open Misctypes
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 3384d79a5..a39347d55 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -18,7 +18,7 @@ open Mod_subst
 open Errors
 open Util
 open Glob_term
-open Topconstr
+open Constrexpr
 open Libnames
 open Typeclasses
 open Typeclasses_errors
@@ -111,8 +111,8 @@ let free_vars_of_constr_expr c ?(bound=Idset.empty) l =
   let rec aux bdvars l c = match c with
     | CRef (Ident (loc,id)) -> found loc id bdvars l
     | CNotation (_, "{ _ : _ | _ }", (CRef (Ident (_, id)) :: _, [], [])) when not (Idset.mem id bdvars) ->
-	fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
-    | c -> fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
+	Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux (Idset.add id bdvars) l c
+    | c -> Topconstr.fold_constr_expr_with_binders (fun a l -> Idset.add a l) aux bdvars l c
   in aux bound l c
 
 let ids_of_names l =
@@ -246,7 +246,7 @@ let combine_params avoid fn applied needed =
 	    aux (t' :: ids) avoid' app need
 
       | (x,_) :: _, [] ->
-	  user_err_loc (constr_loc x,"",str "Typeclass does not expect more arguments")
+	  user_err_loc (Topconstr.constr_loc x,"",str "Typeclass does not expect more arguments")
   in aux [] avoid applied needed
 
 let combine_params_freevar =
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 14a1c630c..3d869a019 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -15,7 +15,7 @@ open Environ
 open Nametab
 open Mod_subst
 open Glob_term
-open Topconstr
+open Constrexpr
 open Pp
 open Libnames
 open Typeclasses
@@ -46,9 +46,9 @@ val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> I
 
 val combine_params_freevar :
   Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-  Topconstr.constr_expr * Names.Idset.t
+  Constrexpr.constr_expr * Names.Idset.t
 
 val implicit_application : Idset.t -> ?allow_partial:bool ->
   (Names.Idset.t -> (global_reference * bool) option * (Names.name * Term.constr option * Term.types) ->
-    Topconstr.constr_expr * Names.Idset.t) ->
+    Constrexpr.constr_expr * Names.Idset.t) ->
   constr_expr -> constr_expr * Idset.t
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 5dde644b5..18d3a9c1c 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -12,7 +12,7 @@ open Util
 open Names
 open Entries
 open Libnames
-open Topconstr
+open Constrexpr
 open Constrintern
 
 type module_internalization_error =
diff --git a/interp/modintern.mli b/interp/modintern.mli
index e808cd980..860f66790 100644
--- a/interp/modintern.mli
+++ b/interp/modintern.mli
@@ -12,7 +12,7 @@ open Entries
 open Pp
 open Libnames
 open Names
-open Topconstr
+open Constrexpr
 
 (** Module internalization errors *)
 
diff --git a/interp/notation.ml b/interp/notation.ml
index b6496f535..16fdef469 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -16,9 +16,10 @@ open Term
 open Nametab
 open Libnames
 open Summary
+open Constrexpr
+open Notation_term
 open Glob_term
 open Glob_ops
-open Topconstr
 open Ppextend
 (*i*)
 
@@ -202,12 +203,13 @@ let cases_pattern_key = function
   | PatCstr (_,ref,_,_) -> RefKey (canonical_gr (ConstructRef ref))
   | _ -> Oth
 
-let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
-  | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
-  | AList (_,_,AApp (ARef ref,args),_,_)
-  | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
-  | ARef ref -> RefKey(canonical_gr ref), None
-  | AApp (_,args) -> Oth, Some (List.length args)
+let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
+  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
+  | NList (_,_,NApp (NRef ref,args),_,_)
+  | NBinderList (_,_,NApp (NRef ref,args),_) ->
+      RefKey (canonical_gr ref), Some (List.length args)
+  | NRef ref -> RefKey(canonical_gr ref), None
+  | NApp (_,args) -> Oth, Some (List.length args)
   | _ -> Oth, None
 
 (**********************************************************************)
@@ -321,7 +323,7 @@ let declare_notation_interpretation ntn scopt pat df =
   if scopt = None then scope_stack := SingleNotation ntn :: !scope_stack
 
 let declare_uninterpretation rule (metas,c as pat) =
-  let (key,n) = aconstr_key c in
+  let (key,n) = notation_constr_key c in
   notations_key_table := Gmapl.add key (rule,pat,n) !notations_key_table
 
 let rec find_interpretation ntn find = function
@@ -349,7 +351,7 @@ let find_prim_token g loc p sc =
   (* Try for a user-defined numerical notation *)
   try
     let (_,c),df = find_notation (notation_of_prim_token p) sc in
-    g (glob_constr_of_aconstr loc c),df
+    g (Topconstr.glob_constr_of_notation_constr loc c),df
   with Not_found ->
   (* Try for a primitive numerical notation *)
   let (spdir,interp) = Hashtbl.find prim_token_interpreter_tab sc loc p in
@@ -401,9 +403,9 @@ let uninterp_prim_token c =
     let (sc,numpr,_) =
       Hashtbl.find prim_token_key_table (glob_prim_constr_key c) in
     match numpr c with
-      | None -> raise No_match
+      | None -> raise Topconstr.No_match
       | Some n -> (sc,n)
-  with Not_found -> raise No_match
+  with Not_found -> raise Topconstr.No_match
 
 let uninterp_prim_token_ind_pattern ind args =
   let ref = IndRef ind in
@@ -423,12 +425,12 @@ let uninterp_prim_token_cases_pattern c =
   try
     let k = cases_pattern_key c in
     let (sc,numpr,b) = Hashtbl.find prim_token_key_table k in
-    if not b then raise No_match;
+    if not b then raise Topconstr.No_match;
     let na,c = glob_constr_of_closed_cases_pattern c in
     match numpr c with
-      | None -> raise No_match
+      | None -> raise Topconstr.No_match
       | Some n -> (na,sc,n)
-  with Not_found -> raise No_match
+  with Not_found -> raise Topconstr.No_match
 
 let availability_of_prim_token n printer_scope local_scopes =
   let f scope =
@@ -447,7 +449,7 @@ let exists_notation_in_scope scopt ntn r =
     r' = r
   with Not_found -> false
 
-let isAVar_or_AHole = function AVar _ | AHole _ -> true | _ -> false
+let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false
 
 (**********************************************************************)
 (* Mapping classes to scopes *)
@@ -651,7 +653,7 @@ let pr_scope_classes sc =
 
 let pr_notation_info prglob ntn c =
   str "\"" ++ str ntn ++ str "\" := " ++
-  prglob (glob_constr_of_aconstr dummy_loc c)
+  prglob (Topconstr.glob_constr_of_notation_constr dummy_loc c)
 
 let pr_named_scope prglob scope sc =
  (if scope = default_scope then
@@ -708,8 +710,8 @@ let browse_notation strict ntn map =
 
 let global_reference_of_notation test (ntn,(sc,c,_)) =
   match c with
-  | ARef ref when test ref -> Some (ntn,sc,ref)
-  | AApp (ARef ref, l) when List.for_all isAVar_or_AHole l & test ref ->
+  | NRef ref when test ref -> Some (ntn,sc,ref)
+  | NApp (NRef ref, l) when List.for_all isNVar_or_NHole l & test ref ->
       Some (ntn,sc,ref)
   | _ -> None
 
diff --git a/interp/notation.mli b/interp/notation.mli
index 6eaac73db..d38f3d6bf 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -13,8 +13,9 @@ open Bigint
 open Names
 open Nametab
 open Libnames
+open Constrexpr
 open Glob_term
-open Topconstr
+open Notation_term
 open Ppextend
 
 (** Notations *)
diff --git a/interp/reserve.ml b/interp/reserve.ml
index c3cdd3f72..2cfd6f5ea 100644
--- a/interp/reserve.ml
+++ b/interp/reserve.ml
@@ -16,7 +16,7 @@ open Nameops
 open Summary
 open Libobject
 open Lib
-open Topconstr
+open Notation_term
 open Libnames
 
 type key =
@@ -26,19 +26,19 @@ type key =
 let reserve_table = ref Idmap.empty
 let reserve_revtable = ref Gmapl.empty
 
-let aconstr_key = function (* Rem: AApp(ARef ref,[]) stands for @ref *)
-  | AApp (ARef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
-  | AList (_,_,AApp (ARef ref,args),_,_)
-  | ABinderList (_,_,AApp (ARef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
-  | ARef ref -> RefKey(canonical_gr ref), None
+let notation_constr_key = function (* Rem: NApp(NRef ref,[]) stands for @ref *)
+  | NApp (NRef ref,args) -> RefKey(canonical_gr ref), Some (List.length args)
+  | NList (_,_,NApp (NRef ref,args),_,_)
+  | NBinderList (_,_,NApp (NRef ref,args),_) -> RefKey (canonical_gr ref), Some (List.length args)
+  | NRef ref -> RefKey(canonical_gr ref), None
   | _ -> Oth, None
 
 let cache_reserved_type (_,(id,t)) =
-  let key = fst (aconstr_key t) in
+  let key = fst (notation_constr_key t) in
   reserve_table := Idmap.add id t !reserve_table;
   reserve_revtable := Gmapl.add key (t,id) !reserve_revtable
 
-let in_reserved : identifier * aconstr -> obj =
+let in_reserved : identifier * notation_constr -> obj =
   declare_object {(default_object "RESERVED-TYPE") with
     cache_function = cache_reserved_type }
 
@@ -80,8 +80,8 @@ let revert_reserved_type t =
     let t = Detyping.detype false [] [] t in
     list_try_find
       (fun (pat,id) ->
-	try let _ = match_aconstr false t ([],pat) in Name id
-	with No_match -> failwith "") l
+	try let _ = Topconstr.match_notation_constr false t ([],pat) in Name id
+	with Topconstr.No_match -> failwith "") l
   with Not_found | Failure _ -> Anonymous
 
 let _ = Namegen.set_reserved_typed_name revert_reserved_type
@@ -92,7 +92,8 @@ let anonymize_if_reserved na t = match na with
   | Name id as na ->
       (try
 	if not !Flags.raw_print &
-	   (try aconstr_of_glob_constr [] [] t = find_reserved_type id
+	   (try Topconstr.notation_constr_of_glob_constr [] [] t
+		  = find_reserved_type id
             with UserError _ -> false)
 	then GHole (dummy_loc,Evar_kinds.BinderType na)
 	else t
diff --git a/interp/reserve.mli b/interp/reserve.mli
index f3b9d43a5..d52460b08 100644
--- a/interp/reserve.mli
+++ b/interp/reserve.mli
@@ -9,8 +9,8 @@
 open Pp
 open Names
 open Glob_term
-open Topconstr
+open Notation_term
 
-val declare_reserved_type : identifier located list -> aconstr -> unit
-val find_reserved_type : identifier -> aconstr
+val declare_reserved_type : identifier located list -> notation_constr -> unit
+val find_reserved_type : identifier ->notation_constr
 val anonymize_if_reserved : name -> glob_constr -> glob_constr
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index 66efe5982..6146bc42e 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -19,13 +19,13 @@ open Names
 open Libnames
 open Misctypes
 open Syntax_def
-open Topconstr
+open Notation_term
 
 let global_of_extended_global = function
   | TrueGlobal ref -> ref
   | SynDef kn ->
   match search_syntactic_definition kn with
-  | [],ARef ref -> ref
+  | [],NRef ref -> ref
   | _ -> raise Not_found
 
 let locate_global_with_alias (loc,qid) =
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index eb6f50131..f20d9727d 100644
--- a/interp/syntax_def.ml
+++ b/interp/syntax_def.ml
@@ -11,7 +11,7 @@ open Util
 open Pp
 open Names
 open Libnames
-open Topconstr
+open Notation_term
 open Libobject
 open Lib
 open Nameops
@@ -38,7 +38,7 @@ let load_syntax_constant i ((sp,kn),(local,pat,onlyparse)) =
   Nametab.push_syndef (Nametab.Until i) sp kn
 
 let is_alias_of_already_visible_name sp = function
-  | _,ARef ref ->
+  | _,NRef ref ->
       let (dir,id) = repr_qualid (shortest_qualid_of_global Idset.empty ref) in
       dir = empty_dirpath && id = basename sp
   | _ ->
@@ -58,7 +58,7 @@ let cache_syntax_constant d =
   open_syntax_constant 1 d
 
 let subst_syntax_constant (subst,(local,pat,onlyparse)) =
-  (local,subst_interpretation subst pat,onlyparse)
+  (local,Topconstr.subst_interpretation subst pat,onlyparse)
 
 let classify_syntax_constant (local,_,_ as o) =
   if local then Dispose else Substitute o
@@ -71,7 +71,7 @@ let in_syntax_constant : bool * interpretation * bool -> obj =
     subst_function = subst_syntax_constant;
     classify_function = classify_syntax_constant }
 
-type syndef_interpretation = (identifier * subscopes) list * aconstr
+type syndef_interpretation = (identifier * subscopes) list * notation_constr
 
 (* Coercions to the general format of notation that also supports
    variables bound to list of expressions *)
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 9e15ab970..f0a45389a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -9,14 +9,14 @@
 open Errors
 open Util
 open Names
-open Topconstr
+open Notation_term
 open Glob_term
 open Nametab
 open Libnames
 
 (** Syntactic definitions. *)
 
-type syndef_interpretation = (identifier * subscopes) list * aconstr
+type syndef_interpretation = (identifier * subscopes) list * notation_constr
 
 val declare_syntactic_definition : bool -> identifier -> bool ->
   syndef_interpretation -> unit
diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 9ea6c7e4c..ab603c37d 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -19,56 +19,11 @@ open Term
 open Mod_subst
 open Misctypes
 open Decl_kinds
+open Constrexpr
+open Notation_term
 (*i*)
 
 (**********************************************************************)
-(* This is the subtype of glob_constr allowed in syntactic extensions *)
-
-(* For AList: first constr is iterator, second is terminator;
-   first id is where each argument of the list has to be substituted
-   in iterator and snd id is alternative name just for printing;
-   boolean is associativity *)
-
-type aconstr =
-  (* Part common to glob_constr and cases_pattern *)
-  | ARef of global_reference
-  | AVar of identifier
-  | AApp of aconstr * aconstr list
-  | AHole of Evar_kinds.t
-  | AList of identifier * identifier * aconstr * aconstr * bool
-  (* Part only in glob_constr *)
-  | ALambda of name * aconstr * aconstr
-  | AProd of name * aconstr * aconstr
-  | ABinderList of identifier * identifier * aconstr * aconstr
-  | ALetIn of name * aconstr * aconstr
-  | ACases of case_style * aconstr option *
-      (aconstr * (name * (inductive * name list) option)) list *
-      (cases_pattern list * aconstr) list
-  | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
-  | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
-  | ARec of fix_kind * identifier array *
-      (name * aconstr option * aconstr) list array * aconstr array *
-      aconstr array
-  | ASort of glob_sort
-  | APatVar of patvar
-  | ACast of aconstr * aconstr cast_type
-
-type scope_name = string
-
-type tmp_scope_name = scope_name
-
-type subscopes = tmp_scope_name option * scope_name list
-
-type notation_var_instance_type =
-  | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
-
-type notation_var_internalization_type =
-  | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
-
-type interpretation =
-    (identifier * (subscopes * notation_var_instance_type)) list * aconstr
-
-(**********************************************************************)
 (* Re-interpret a notation as a glob_constr, taking care of binders     *)
 
 let name_to_ident = function
@@ -101,28 +56,28 @@ let rec subst_glob_vars l = function
 
 let ldots_var = id_of_string ".."
 
-let glob_constr_of_aconstr_with_binders loc g f e = function
-  | AVar id -> GVar (loc,id)
-  | AApp (a,args) -> GApp (loc,f e a, List.map (f e) args)
-  | AList (x,y,iter,tail,swap) ->
+let glob_constr_of_notation_constr_with_binders loc g f e = function
+  | NVar id -> GVar (loc,id)
+  | NApp (a,args) -> GApp (loc,f e a, List.map (f e) args)
+  | NList (x,y,iter,tail,swap) ->
       let t = f e tail in let it = f e iter in
       let innerl = (ldots_var,t)::(if swap then [] else [x,GVar(loc,y)]) in
       let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in
       let outerl = (ldots_var,inner)::(if swap then [x,GVar(loc,y)] else []) in
       subst_glob_vars outerl it
-  | ABinderList (x,y,iter,tail) ->
+  | NBinderList (x,y,iter,tail) ->
       let t = f e tail in let it = f e iter in
       let innerl = [(ldots_var,t);(x,GVar(loc,y))] in
       let inner = GApp (loc,GVar (loc,ldots_var),[subst_glob_vars innerl it]) in
       let outerl = [(ldots_var,inner)] in
       subst_glob_vars outerl it
-  | ALambda (na,ty,c) ->
+  | NLambda (na,ty,c) ->
       let e',na = g e na in GLambda (loc,na,Explicit,f e ty,f e' c)
-  | AProd (na,ty,c) ->
+  | NProd (na,ty,c) ->
       let e',na = g e na in GProd (loc,na,Explicit,f e ty,f e' c)
-  | ALetIn (na,b,c) ->
+  | NLetIn (na,b,c) ->
       let e',na = g e na in GLetIn (loc,na,f e b,f e' c)
-  | ACases (sty,rtntypopt,tml,eqnl) ->
+  | NCases (sty,rtntypopt,tml,eqnl) ->
       let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') ->
 	let e',t' = match t with
 	| None -> e',None
@@ -138,28 +93,28 @@ let glob_constr_of_aconstr_with_binders loc g f e = function
 	  list_fold_map (cases_pattern_fold_map loc fold) ([],e) patl in
 	(loc,idl,patl,f e rhs)) eqnl in
       GCases (loc,sty,Option.map (f e') rtntypopt,tml',eqnl')
-  | ALetTuple (nal,(na,po),b,c) ->
+  | NLetTuple (nal,(na,po),b,c) ->
       let e',nal = list_fold_map g e nal in
       let e'',na = g e na in
       GLetTuple (loc,nal,(na,Option.map (f e'') po),f e b,f e' c)
-  | AIf (c,(na,po),b1,b2) ->
+  | NIf (c,(na,po),b1,b2) ->
       let e',na = g e na in
       GIf (loc,f e c,(na,Option.map (f e') po),f e b1,f e b2)
-  | ARec (fk,idl,dll,tl,bl) ->
+  | NRec (fk,idl,dll,tl,bl) ->
       let e,dll = array_fold_map (list_fold_map (fun e (na,oc,b) ->
 	  let e,na = g e na in
 	  (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in
       let e',idl = array_fold_map (to_id g) e idl in
       GRec (loc,fk,idl,dll,Array.map (f e) tl,Array.map (f e') bl)
-  | ACast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k)
-  | ASort x -> GSort (loc,x)
-  | AHole x  -> GHole (loc,x)
-  | APatVar n -> GPatVar (loc,(false,n))
-  | ARef x -> GRef (loc,x)
+  | NCast (c,k) -> GCast (loc,f e c, Miscops.map_cast_type (f e) k)
+  | NSort x -> GSort (loc,x)
+  | NHole x  -> GHole (loc,x)
+  | NPatVar n -> GPatVar (loc,(false,n))
+  | NRef x -> GRef (loc,x)
 
-let rec glob_constr_of_aconstr loc x =
+let rec glob_constr_of_notation_constr loc x =
   let rec aux () x =
-    glob_constr_of_aconstr_with_binders loc (fun () id -> ((),id)) aux () x
+    glob_constr_of_notation_constr_with_binders loc (fun () id -> ((),id)) aux () x
   in aux () x
 
 (****************************************************************************)
@@ -260,17 +215,17 @@ let compare_recursive_parts found f (iterator,subc) =
 	  else iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
-	AList (x,y,iterator,f (Option.get !terminator),lassoc)
+	NList (x,y,iterator,f (Option.get !terminator),lassoc)
     | Some (x,y,None) ->
 	let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
 	let iterator = f iterator in
 	(* found have been collected by compare_constr *)
 	found := newfound;
-	ABinderList (x,y,iterator,f (Option.get !terminator))
+	NBinderList (x,y,iterator,f (Option.get !terminator))
   else
     raise Not_found
 
-let aconstr_and_vars_of_glob_constr a =
+let notation_constr_and_vars_of_glob_constr a =
   let found = ref ([],[],[]) in
   let rec aux c =
     let keepfound = !found in
@@ -287,14 +242,14 @@ let aconstr_and_vars_of_glob_constr a =
     | c ->
 	aux' c
   and aux' = function
-  | GVar (_,id) -> add_id found id; AVar id
-  | GApp (_,g,args) -> AApp (aux g, List.map aux args)
-  | GLambda (_,na,bk,ty,c) -> add_name found na; ALambda (na,aux ty,aux c)
-  | GProd (_,na,bk,ty,c) -> add_name found na; AProd (na,aux ty,aux c)
-  | GLetIn (_,na,b,c) -> add_name found na; ALetIn (na,aux b,aux c)
+  | GVar (_,id) -> add_id found id; NVar id
+  | GApp (_,g,args) -> NApp (aux g, List.map aux args)
+  | GLambda (_,na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
+  | GProd (_,na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
+  | GLetIn (_,na,b,c) -> add_name found na; NLetIn (na,aux b,aux c)
   | GCases (_,sty,rtntypopt,tml,eqnl) ->
       let f (_,idl,pat,rhs) = List.iter (add_id found) idl; (pat,aux rhs) in
-      ACases (sty,Option.map aux rtntypopt,
+      NCases (sty,Option.map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  Option.iter
@@ -304,22 +259,22 @@ let aconstr_and_vars_of_glob_constr a =
   | GLetTuple (loc,nal,(na,po),b,c) ->
       add_name found na;
       List.iter (add_name found) nal;
-      ALetTuple (nal,(na,Option.map aux po),aux b,aux c)
+      NLetTuple (nal,(na,Option.map aux po),aux b,aux c)
   | GIf (loc,c,(na,po),b1,b2) ->
       add_name found na;
-      AIf (aux c,(na,Option.map aux po),aux b1,aux b2)
+      NIf (aux c,(na,Option.map aux po),aux b1,aux b2)
   | GRec (_,fk,idl,dll,tl,bl) ->
       Array.iter (add_id found) idl;
       let dll = Array.map (List.map (fun (na,bk,oc,b) ->
 	 if bk <> Explicit then
 	   error "Binders marked as implicit not allowed in notations.";
 	 add_name found na; (na,Option.map aux oc,aux b))) dll in
-      ARec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
-  | GCast (_,c,k) -> ACast (aux c,Miscops.map_cast_type aux k)
-  | GSort (_,s) -> ASort s
-  | GHole (_,w) -> AHole w
-  | GRef (_,r) -> ARef r
-  | GPatVar (_,(_,n)) -> APatVar n
+      NRec (fk,idl,dll,Array.map aux tl,Array.map aux bl)
+  | GCast (_,c,k) -> NCast (aux c,Miscops.map_cast_type aux k)
+  | GSort (_,s) -> NSort s
+  | GHole (_,w) -> NHole w
+  | GRef (_,r) -> NRef r
+  | GPatVar (_,(_,n)) -> NPatVar n
   | GEvar _ ->
       error "Existential variables not allowed in notations."
 
@@ -369,15 +324,15 @@ let check_variables vars recvars (found,foundrec,foundrecbinding) =
     | NtnInternTypeIdent -> check_bound x in
   List.iter check_type vars
 
-let aconstr_of_glob_constr vars recvars a =
-  let a,found = aconstr_and_vars_of_glob_constr a in
+let notation_constr_of_glob_constr vars recvars a =
+  let a,found = notation_constr_and_vars_of_glob_constr a in
   check_variables vars recvars found;
   a
 
 (* Substitution of kernel names, avoiding a list of bound identifiers *)
 
-let aconstr_of_constr avoiding t =
- aconstr_of_glob_constr [] [] (Detyping.detype false avoiding [] t)
+let notation_constr_of_constr avoiding t =
+ notation_constr_of_glob_constr [] [] (Detyping.detype false avoiding [] t)
 
 let rec subst_pat subst pat =
   match pat with
@@ -388,56 +343,56 @@ let rec subst_pat subst pat =
         if kn' == kn && cpl' == cpl then pat else
           PatCstr (loc,((kn',i),j),cpl',n)
 
-let rec subst_aconstr subst bound raw =
+let rec subst_notation_constr subst bound raw =
   match raw with
-  | ARef ref ->
+  | NRef ref ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-	  aconstr_of_constr bound t
+	  notation_constr_of_constr bound t
 
-  | AVar _ -> raw
+  | NVar _ -> raw
 
-  | AApp (r,rl) ->
-      let r' = subst_aconstr subst bound r
-      and rl' = list_smartmap (subst_aconstr subst bound) rl in
+  | NApp (r,rl) ->
+      let r' = subst_notation_constr subst bound r
+      and rl' = list_smartmap (subst_notation_constr subst bound) rl in
 	if r' == r && rl' == rl then raw else
-	  AApp(r',rl')
+	  NApp(r',rl')
 
-  | AList (id1,id2,r1,r2,b) ->
-      let r1' = subst_aconstr subst bound r1
-      and r2' = subst_aconstr subst bound r2 in
+  | NList (id1,id2,r1,r2,b) ->
+      let r1' = subst_notation_constr subst bound r1
+      and r2' = subst_notation_constr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  AList (id1,id2,r1',r2',b)
+	  NList (id1,id2,r1',r2',b)
 
-  | ALambda (n,r1,r2) ->
-      let r1' = subst_aconstr subst bound r1
-      and r2' = subst_aconstr subst bound r2 in
+  | NLambda (n,r1,r2) ->
+      let r1' = subst_notation_constr subst bound r1
+      and r2' = subst_notation_constr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  ALambda (n,r1',r2')
+	  NLambda (n,r1',r2')
 
-  | AProd (n,r1,r2) ->
-      let r1' = subst_aconstr subst bound r1
-      and r2' = subst_aconstr subst bound r2 in
+  | NProd (n,r1,r2) ->
+      let r1' = subst_notation_constr subst bound r1
+      and r2' = subst_notation_constr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  AProd (n,r1',r2')
+	  NProd (n,r1',r2')
 
-  | ABinderList (id1,id2,r1,r2) ->
-      let r1' = subst_aconstr subst bound r1
-      and r2' = subst_aconstr subst bound r2 in
+  | NBinderList (id1,id2,r1,r2) ->
+      let r1' = subst_notation_constr subst bound r1
+      and r2' = subst_notation_constr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  ABinderList (id1,id2,r1',r2')
+	  NBinderList (id1,id2,r1',r2')
 
-  | ALetIn (n,r1,r2) ->
-      let r1' = subst_aconstr subst bound r1
-      and r2' = subst_aconstr subst bound r2 in
+  | NLetIn (n,r1,r2) ->
+      let r1' = subst_notation_constr subst bound r1
+      and r2' = subst_notation_constr subst bound r2 in
 	if r1' == r1 && r2' == r2 then raw else
-	  ALetIn (n,r1',r2')
+	  NLetIn (n,r1',r2')
 
-  | ACases (sty,rtntypopt,rl,branches) ->
-      let rtntypopt' = Option.smartmap (subst_aconstr subst bound) rtntypopt
+  | NCases (sty,rtntypopt,rl,branches) ->
+      let rtntypopt' = Option.smartmap (subst_notation_constr subst bound) rtntypopt
       and rl' = list_smartmap
         (fun (a,(n,signopt) as x) ->
-	  let a' = subst_aconstr subst bound a in
+	  let a' = subst_notation_constr subst bound a in
 	  let signopt' = Option.map (fun ((indkn,i),nal as z) ->
 	    let indkn' = subst_ind subst indkn in
 	    if indkn == indkn' then z else ((indkn',i),nal)) signopt in
@@ -446,62 +401,62 @@ let rec subst_aconstr subst bound raw =
       and branches' = list_smartmap
                         (fun (cpl,r as branch) ->
                            let cpl' = list_smartmap (subst_pat subst) cpl
-                           and r' = subst_aconstr subst bound r in
+                           and r' = subst_notation_constr subst bound r in
                              if cpl' == cpl && r' == r then branch else
                                (cpl',r'))
                         branches
       in
         if rtntypopt' == rtntypopt && rtntypopt == rtntypopt' &
           rl' == rl && branches' == branches then raw else
-          ACases (sty,rtntypopt',rl',branches')
+          NCases (sty,rtntypopt',rl',branches')
 
-  | ALetTuple (nal,(na,po),b,c) ->
-      let po' = Option.smartmap (subst_aconstr subst bound) po
-      and b' = subst_aconstr subst bound b
-      and c' = subst_aconstr subst bound c in
+  | NLetTuple (nal,(na,po),b,c) ->
+      let po' = Option.smartmap (subst_notation_constr subst bound) po
+      and b' = subst_notation_constr subst bound b
+      and c' = subst_notation_constr subst bound c in
 	if po' == po && b' == b && c' == c then raw else
-	  ALetTuple (nal,(na,po'),b',c')
+	  NLetTuple (nal,(na,po'),b',c')
 
-  | AIf (c,(na,po),b1,b2) ->
-      let po' = Option.smartmap (subst_aconstr subst bound) po
-      and b1' = subst_aconstr subst bound b1
-      and b2' = subst_aconstr subst bound b2
-      and c' = subst_aconstr subst bound c in
+  | NIf (c,(na,po),b1,b2) ->
+      let po' = Option.smartmap (subst_notation_constr subst bound) po
+      and b1' = subst_notation_constr subst bound b1
+      and b2' = subst_notation_constr subst bound b2
+      and c' = subst_notation_constr subst bound c in
 	if po' == po && b1' == b1 && b2' == b2 && c' == c then raw else
-	  AIf (c',(na,po'),b1',b2')
+	  NIf (c',(na,po'),b1',b2')
 
-  | ARec (fk,idl,dll,tl,bl) ->
+  | NRec (fk,idl,dll,tl,bl) ->
       let dll' =
 	array_smartmap (list_smartmap (fun (na,oc,b as x) ->
-	  let oc' =  Option.smartmap (subst_aconstr subst bound) oc in
-	  let b' =  subst_aconstr subst bound b in
+	  let oc' =  Option.smartmap (subst_notation_constr subst bound) oc in
+	  let b' =  subst_notation_constr subst bound b in
 	  if oc' == oc && b' == b then x else (na,oc',b'))) dll in
-      let tl' = array_smartmap (subst_aconstr subst bound) tl in
-      let bl' = array_smartmap (subst_aconstr subst bound) bl in
+      let tl' = array_smartmap (subst_notation_constr subst bound) tl in
+      let bl' = array_smartmap (subst_notation_constr subst bound) bl in
       if dll' == dll && tl' == tl && bl' == bl then raw else
-	  ARec (fk,idl,dll',tl',bl')
+	  NRec (fk,idl,dll',tl',bl')
 
-  | APatVar _ | ASort _ -> raw
+  | NPatVar _ | NSort _ -> raw
 
-  | AHole (Evar_kinds.ImplicitArg (ref,i,b)) ->
+  | NHole (Evar_kinds.ImplicitArg (ref,i,b)) ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-	  AHole (Evar_kinds.InternalHole)
-  | AHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _
+	  NHole (Evar_kinds.InternalHole)
+  | NHole (Evar_kinds.BinderType _ |Evar_kinds.QuestionMark _
 	  |Evar_kinds.CasesType |Evar_kinds.InternalHole
 	  |Evar_kinds.TomatchTypeParameter _ |Evar_kinds.GoalEvar
 	  |Evar_kinds.ImpossibleCase |Evar_kinds.MatchingVar _) -> raw
 
-  | ACast (r1,k) ->
-      let r1' = subst_aconstr subst bound r1 in
-      let k' = Miscops.smartmap_cast_type (subst_aconstr subst bound) k in
-      if r1' == r1 && k' == k then raw else ACast(r1',k')
+  | NCast (r1,k) ->
+      let r1' = subst_notation_constr subst bound r1 in
+      let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in
+      if r1' == r1 && k' == k then raw else NCast(r1',k')
 
 let subst_interpretation subst (metas,pat) =
   let bound = List.map fst metas in
-  (metas,subst_aconstr subst bound pat)
+  (metas,subst_notation_constr subst bound pat)
 
-(* Pattern-matching glob_constr and aconstr *)
+(* Pattern-matching glob_constr and notation_constr *)
 
 let abstract_return_type_context pi mklam tml rtno =
   Option.map (fun rtn ->
@@ -516,9 +471,9 @@ let abstract_return_type_context_glob_constr =
     (fun na c ->
       GLambda(dummy_loc,na,Explicit,GHole(dummy_loc,Evar_kinds.InternalHole),c))
 
-let abstract_return_type_context_aconstr =
+let abstract_return_type_context_notation_constr =
   abstract_return_type_context snd
-    (fun na c -> ALambda(na,AHole Evar_kinds.InternalHole,c))
+    (fun na c -> NLambda(na,NHole Evar_kinds.InternalHole,c))
 
 exception No_match
 
@@ -633,60 +588,60 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
   match (a1,a2) with
 
   (* Matching notation variable *)
-  | r1, AVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1
+  | r1, NVar id2 when List.mem id2 tmetas -> bind_env alp sigma id2 r1
 
   (* Matching recursive notations for terms *)
-  | r1, AList (x,_,iter,termin,lassoc) ->
+  | r1, NList (x,_,iter,termin,lassoc) ->
       match_alist (match_hd u alp) metas sigma r1 x iter termin lassoc
 
   (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-  | GLambda (_,na1,bk,t1,b1), ABinderList (x,_,ALambda (Name id2,_,b2),termin)->
+  | GLambda (_,na1,bk,t1,b1), NBinderList (x,_,NLambda (Name id2,_,b2),termin)->
       let (decls,b) = match_iterated_binders true [(na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
       match_in u alp metas (bind_binder sigma x decls) b termin
-  | GProd (_,na1,bk,t1,b1), ABinderList (x,_,AProd (Name id2,_,b2),termin)
+  | GProd (_,na1,bk,t1,b1), NBinderList (x,_,NProd (Name id2,_,b2),termin)
       when na1 <> Anonymous ->
       let (decls,b) = match_iterated_binders false [(na1,bk,None,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
       match_in u alp metas (bind_binder sigma x decls) b termin
   (* Matching recursive notations for binders: general case *)
-  | r, ABinderList (x,_,iter,termin) ->
+  | r, NBinderList (x,_,iter,termin) ->
       match_abinderlist_with_app (match_hd u alp) metas sigma r x iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (_,na,bk,t,b1), ALambda (Name id,_,b2) when List.mem id blmetas ->
+  | GLambda (_,na,bk,t,b1), NLambda (Name id,_,b2) when List.mem id blmetas ->
       match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
-  | GProd (_,na,bk,t,b1), AProd (Name id,_,b2)
+  | GProd (_,na,bk,t,b1), NProd (Name id,_,b2)
       when List.mem id blmetas & na <> Anonymous ->
       match_in u alp metas (bind_binder sigma id [(na,bk,None,t)]) b1 b2
 
   (* Matching compositionally *)
-  | GVar (_,id1), AVar id2 when alpha_var id1 id2 alp -> sigma
-  | GRef (_,r1), ARef r2 when (eq_gr r1 r2) -> sigma
-  | GPatVar (_,(_,n1)), APatVar n2 when n1=n2 -> sigma
-  | GApp (loc,f1,l1), AApp (f2,l2) ->
+  | GVar (_,id1), NVar id2 when alpha_var id1 id2 alp -> sigma
+  | GRef (_,r1), NRef r2 when (eq_gr r1 r2) -> sigma
+  | GPatVar (_,(_,n1)), NPatVar n2 when n1=n2 -> sigma
+  | GApp (loc,f1,l1), NApp (f2,l2) ->
       let n1 = List.length l1 and n2 = List.length l2 in
       let f1,l1,f2,l2 =
 	if n1 < n2 then
-	  let l21,l22 = list_chop (n2-n1) l2 in f1,l1, AApp (f2,l21), l22
+	  let l21,l22 = list_chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
 	else if n1 > n2 then
 	  let l11,l12 = list_chop (n1-n2) l1 in GApp (loc,f1,l11),l12, f2,l2
 	else f1,l1, f2, l2 in
       let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_in u alp metas sigma f1 f2) l1 l2
-  | GLambda (_,na1,_,t1,b1), ALambda (na2,t2,b2) ->
+  | GLambda (_,na1,_,t1,b1), NLambda (na2,t2,b2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-  | GProd (_,na1,_,t1,b1), AProd (na2,t2,b2) ->
+  | GProd (_,na1,_,t1,b1), NProd (na2,t2,b2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-  | GLetIn (_,na1,t1,b1), ALetIn (na2,t2,b2) ->
+  | GLetIn (_,na1,t1,b1), NLetIn (na2,t2,b2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
-  | GCases (_,sty1,rtno1,tml1,eqnl1), ACases (sty2,rtno2,tml2,eqnl2)
+  | GCases (_,sty1,rtno1,tml1,eqnl1), NCases (sty2,rtno2,tml2,eqnl2)
       when sty1 = sty2
 	 & List.length tml1 = List.length tml2
 	 & List.length eqnl1 = List.length eqnl2 ->
       let rtno1' = abstract_return_type_context_glob_constr tml1 rtno1 in
-      let rtno2' = abstract_return_type_context_aconstr tml2 rtno2 in
+      let rtno2' = abstract_return_type_context_notation_constr tml2 rtno2 in
       let sigma =
 	try Option.fold_left2 (match_in u alp metas) sigma rtno1' rtno2'
 	with Option.Heterogeneous -> raise No_match
@@ -695,17 +650,17 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
       (fun s (tm1,_) (tm2,_) ->
         match_in u alp metas s tm1 tm2) sigma tml1 tml2 in
       List.fold_left2 (match_equations u alp metas) sigma eqnl1 eqnl2
-  | GLetTuple (_,nal1,(na1,to1),b1,c1), ALetTuple (nal2,(na2,to2),b2,c2)
+  | GLetTuple (_,nal1,(na1,to1),b1,c1), NLetTuple (nal2,(na2,to2),b2,c2)
       when List.length nal1 = List.length nal2 ->
       let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
       let sigma = match_in u alp metas sigma b1 b2 in
       let (alp,sigma) =
 	List.fold_left2 (match_names metas) (alp,sigma) nal1 nal2 in
       match_in u alp metas sigma c1 c2
-  | GIf (_,a1,(na1,to1),b1,c1), AIf (a2,(na2,to2),b2,c2) ->
+  | GIf (_,a1,(na1,to1),b1,c1), NIf (a2,(na2,to2),b2,c2) ->
       let sigma = match_opt (match_binders u alp metas na1 na2) sigma to1 to2 in
       List.fold_left2 (match_in u alp metas) sigma [a1;b1;c1] [a2;b2;c2]
-  | GRec (_,fk1,idl1,dll1,tl1,bl1), ARec (fk2,idl2,dll2,tl2,bl2)
+  | GRec (_,fk1,idl1,dll1,tl1,bl1), NRec (fk2,idl2,dll2,tl2,bl2)
       when match_fix_kind fk1 fk2 & Array.length idl1 =  Array.length idl2 &
 	array_for_all2 (fun l1 l2 -> List.length l1 = List.length l2) dll1 dll2
 	->
@@ -719,21 +674,21 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
       let alp,sigma = array_fold_right2 (fun id1 id2 alsig ->
 	match_names metas alsig (Name id1) (Name id2)) idl1 idl2 (alp,sigma) in
       array_fold_left2 (match_in u alp metas) sigma bl1 bl2
-  | GCast(_,c1,CastConv t1), ACast (c2,CastConv t2)
-  | GCast(_,c1,CastVM t1), ACast (c2,CastVM t2) ->
+  | GCast(_,c1,CastConv t1), NCast (c2,CastConv t2)
+  | GCast(_,c1,CastVM t1), NCast (c2,CastVM t2) ->
       match_in u alp metas (match_in u alp metas sigma c1 c2) t1 t2
-  | GCast(_,c1, CastCoerce), ACast(c2, CastCoerce) ->
+  | GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) ->
       match_in u alp metas sigma c1 c2
-  | GSort (_,GType _), ASort (GType None) when not u -> sigma
-  | GSort (_,s1), ASort s2 when s1 = s2 -> sigma
-  | GPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
-  | a, AHole _ -> sigma
+  | GSort (_,GType _), NSort (GType None) when not u -> sigma
+  | GSort (_,s1), NSort s2 when s1 = s2 -> sigma
+  | GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
+  | a, NHole _ -> sigma
 
   (* On the fly eta-expansion so as to use notations of the form
      "exists x, P x" for "ex P"; expects type not given because don't know
      otherwise how to ensure it corresponds to a well-typed eta-expansion;
      ensure at least one constructor is consumed to avoid looping *)
-  | b1, ALambda (Name id,AHole _,b2) when inner ->
+  | b1, NLambda (Name id,NHole _,b2) when inner ->
       let id' = Namegen.next_ident_away id (free_glob_vars b1) in
       match_in u alp metas (bind_binder sigma id
        [(Name id',Explicit,None,GHole(dummy_loc,Evar_kinds.BinderType (Name id')))])
@@ -758,7 +713,7 @@ and match_equations u alp metas sigma (_,_,patl1,rhs1) (patl2,rhs2) =
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
-let match_aconstr u c (metas,pat) =
+let match_notation_constr u c (metas,pat) =
   let vars = list_split_by (fun (_,(_,x)) -> x <> NtnTypeBinderList) metas in
   let vars = (List.map fst (fst vars), List.map fst (snd vars)) in
   let terms,termlists,binders = match_ false u [] vars ([],[],[]) c pat in
@@ -795,11 +750,11 @@ let bind_env_cases_pattern (sigma,sigmalist,x as fullsigma) var v =
 
 let rec match_cases_pattern metas sigma a1 a2 =
  match (a1,a2) with
-  | r1, AVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[]
-  | PatVar (_,Anonymous), AHole _ -> sigma,[]
-  | PatCstr (loc,(ind,_ as r1),largs,_), ARef (ConstructRef r2) when r1 = r2 ->
+  | r1, NVar id2 when List.mem id2 metas -> (bind_env_cases_pattern sigma id2 r1),[]
+  | PatVar (_,Anonymous), NHole _ -> sigma,[]
+  | PatCstr (loc,(ind,_ as r1),largs,_), NRef (ConstructRef r2) when r1 = r2 ->
       sigma,largs
-  | PatCstr (loc,(ind,_ as r1),args1,_), AApp (ARef (ConstructRef r2),l2)
+  | PatCstr (loc,(ind,_ as r1),args1,_), NApp (NRef (ConstructRef r2),l2)
       when r1 = r2 ->
       let l1 = add_patterns_for_params (fst r1) args1 in
       let le2 = List.length l2 in
@@ -809,7 +764,7 @@ let rec match_cases_pattern metas sigma a1 a2 =
       else
 	let l1',more_args = Util.list_chop le2 l1 in
 	(List.fold_left2 (match_cases_pattern_no_more_args metas) sigma l1' l2),more_args
-  | r1, AList (x,_,iter,termin,lassoc) ->
+  | r1, NList (x,_,iter,termin,lassoc) ->
       (match_alist (fun (metas,_) -> match_cases_pattern_no_more_args metas)
 	(metas,[]) (pi1 sigma,pi2 sigma,()) r1 x iter termin lassoc),[]
   | _ -> raise No_match
@@ -841,7 +796,7 @@ let reorder_canonically_substitution terms termlists metas =
       | NtnTypeBinderList -> assert false)
     metas ([],[])
 
-let match_aconstr_cases_pattern c (metas,pat) =
+let match_notation_constr_cases_pattern c (metas,pat) =
   let vars = List.map fst metas in
   let (terms,termlists,()),more_args = match_cases_pattern vars ([],[],()) c pat in
   reorder_canonically_substitution terms termlists metas,more_args
@@ -851,89 +806,6 @@ let match_aconstr_ind_pattern ind args (metas,pat) =
   let (terms,termlists,()),more_args = match_ind_pattern vars ([],[],()) ind args pat in
   reorder_canonically_substitution terms termlists metas,more_args
 
-(**********************************************************************)
-(*s Concrete syntax for terms *)
-
-type notation = string
-
-type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-
-type binder_kind = Default of binding_kind | Generalized of binding_kind * binding_kind * bool
-
-type abstraction_kind = AbsLambda | AbsPi
-
-type proj_flag = int option (* [Some n] = proj of the n-th visible argument *)
-
-type prim_token = Numeral of Bigint.bigint | String of string
-
-type cases_pattern_expr =
-  | CPatAlias of loc * cases_pattern_expr * identifier
-  | CPatCstr of loc * reference * cases_pattern_expr list
-  | CPatCstrExpl of loc * reference * cases_pattern_expr list
-  | CPatAtom of loc * reference option
-  | CPatOr of loc * cases_pattern_expr list
-  | CPatNotation of loc * notation * cases_pattern_notation_substitution
-  | CPatPrim of loc * prim_token
-  | CPatRecord of loc * (reference * cases_pattern_expr) list
-  | CPatDelimiters of loc * string * cases_pattern_expr
-
-and cases_pattern_notation_substitution =
-    cases_pattern_expr list *     (** for constr subterms *)
-    cases_pattern_expr list list  (** for recursive notations *)
-
-type constr_expr =
-  | CRef of reference
-  | CFix of loc * identifier located * fix_expr list
-  | CCoFix of loc * identifier located * cofix_expr list
-  | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
-  | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
-  | CLetIn of loc * name located * constr_expr * constr_expr
-  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
-  | CApp of loc * (proj_flag * constr_expr) *
-      (constr_expr * explicitation located option) list
-  | CRecord of loc * constr_expr option * (reference * constr_expr) list
-  | CCases of loc * case_style * constr_expr option *
-      (constr_expr * (name located option * cases_pattern_expr option)) list *
-      (loc * cases_pattern_expr list located list * constr_expr) list
-  | CLetTuple of loc * name located list * (name located option * constr_expr option) *
-      constr_expr * constr_expr
-  | CIf of loc * constr_expr * (name located option * constr_expr option)
-      * constr_expr * constr_expr
-  | CHole of loc * Evar_kinds.t option
-  | CPatVar of loc * (bool * patvar)
-  | CEvar of loc * existential_key * constr_expr list option
-  | CSort of loc * glob_sort
-  | CCast of loc * constr_expr * constr_expr cast_type
-  | CNotation of loc * notation * constr_notation_substitution
-  | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
-  | CPrim of loc * prim_token
-  | CDelimiters of loc * string * constr_expr
-
-and fix_expr =
-    identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
-
-and cofix_expr =
-    identifier located * local_binder list * constr_expr * constr_expr
-
-and recursion_order_expr =
-  | CStructRec
-  | CWfRec of constr_expr
-  | CMeasureRec of constr_expr * constr_expr option (* measure, relation *)
-
-and local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * binder_kind * constr_expr
-
-and constr_notation_substitution =
-    constr_expr list *      (* for constr subterms *)
-    constr_expr list list * (* for recursive notations *)
-    local_binder list list      (* for binders subexpressions *)
-
-type typeclass_constraint = name located * binding_kind * constr_expr
-
-and typeclass_context = typeclass_constraint list
-
-type constr_pattern_expr = constr_expr
 
 let oldfashion_patterns = ref (true)
 let write_oldfashion_patterns = Goptions.declare_bool_option {
diff --git a/interp/topconstr.mli b/interp/topconstr.mli
index 101c39eea..760ee14a5 100644
--- a/interp/topconstr.mli
+++ b/interp/topconstr.mli
@@ -15,66 +15,17 @@ open Term
 open Mod_subst
 open Misctypes
 open Decl_kinds
+open Constrexpr
+open Notation_term
 
-(** Topconstr: definitions of [aconstr] et [constr_expr] *)
-
-(** {6 aconstr } *)
-(** This is the subtype of glob_constr allowed in syntactic extensions 
-   No location since intended to be substituted at any place of a text 
-   Complex expressions such as fixpoints and cofixpoints are excluded, 
-   non global expressions such as existential variables also *)
-
-type aconstr =
-  (** Part common to [glob_constr] and [cases_pattern] *)
-  | ARef of global_reference
-  | AVar of identifier
-  | AApp of aconstr * aconstr list
-  | AHole of Evar_kinds.t
-  | AList of identifier * identifier * aconstr * aconstr * bool
-  (** Part only in [glob_constr] *)
-  | ALambda of name * aconstr * aconstr
-  | AProd of name * aconstr * aconstr
-  | ABinderList of identifier * identifier * aconstr * aconstr
-  | ALetIn of name * aconstr * aconstr
-  | ACases of case_style * aconstr option *
-      (aconstr * (name * (inductive * name list) option)) list *
-      (cases_pattern list * aconstr) list
-  | ALetTuple of name list * (name * aconstr option) * aconstr * aconstr
-  | AIf of aconstr * (name * aconstr option) * aconstr * aconstr
-  | ARec of fix_kind * identifier array *
-      (name * aconstr option * aconstr) list array * aconstr array *
-      aconstr array
-  | ASort of glob_sort
-  | APatVar of patvar
-  | ACast of aconstr * aconstr cast_type
-
-type scope_name = string
-
-type tmp_scope_name = scope_name
-
-type subscopes = tmp_scope_name option * scope_name list
-
-(** Type of the meta-variables of an aconstr: in a recursive pattern x..y,
-    x carries the sequence of objects bound to the list x..y  *)
-type notation_var_instance_type =
-  | NtnTypeConstr | NtnTypeConstrList | NtnTypeBinderList
-
-(** Type of variables when interpreting a constr_expr as an aconstr:
-    in a recursive pattern x..y, both x and y carry the individual type
-    of each element of the list x..y *)
-type notation_var_internalization_type =
-  | NtnInternTypeConstr | NtnInternTypeBinder | NtnInternTypeIdent
-
-(** This characterizes to what a notation is interpreted to *)
-type interpretation =
-    (identifier * (subscopes * notation_var_instance_type)) list * aconstr
+(** Topconstr *)
 
 (** Translate a glob_constr into a notation given the list of variables
     bound by the notation; also interpret recursive patterns           *)
 
-val aconstr_of_glob_constr :
+val notation_constr_of_glob_constr :
   (identifier * notation_var_internalization_type) list ->
-  (identifier * identifier) list -> glob_constr -> aconstr
+  (identifier * identifier) list -> glob_constr -> notation_constr
 
 (** Name of the special identifier used to encode recursive notations  *)
 val ldots_var : identifier
@@ -84,23 +35,26 @@ val eq_glob_constr : glob_constr -> glob_constr -> bool
 
 (** Re-interpret a notation as a glob_constr, taking care of binders     *)
 
-val glob_constr_of_aconstr_with_binders : loc ->
+val glob_constr_of_notation_constr_with_binders : loc ->
   ('a -> name -> 'a * name) ->
-  ('a -> aconstr -> glob_constr) -> 'a -> aconstr -> glob_constr
+  ('a -> notation_constr -> glob_constr) ->
+  'a -> notation_constr -> glob_constr
 
-val glob_constr_of_aconstr : loc -> aconstr -> glob_constr
+val glob_constr_of_notation_constr : loc -> notation_constr -> glob_constr
 
-(** [match_aconstr] matches a glob_constr against a notation interpretation;
+(** [match_notation_constr] matches a glob_constr against a notation interpretation;
     raise [No_match] if the matching fails   *)
 
 exception No_match
 
-val match_aconstr : bool -> glob_constr -> interpretation ->
+val match_notation_constr : bool -> glob_constr -> interpretation ->
       (glob_constr * subscopes) list * (glob_constr list * subscopes) list *
       (glob_decl list * subscopes) list
 
-val match_aconstr_cases_pattern :  cases_pattern -> interpretation ->
-      ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list)
+val match_notation_constr_cases_pattern :
+  cases_pattern -> interpretation ->
+  ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) *
+    (cases_pattern list)
 
 val match_aconstr_ind_pattern : inductive -> cases_pattern  list -> interpretation ->
       ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (cases_pattern list)
@@ -109,94 +63,6 @@ val match_aconstr_ind_pattern : inductive -> cases_pattern  list -> interpretati
 
 val subst_interpretation : substitution -> interpretation -> interpretation
 
-(** {6 Concrete syntax for terms }                                        *)
-
-type notation = string
-
-type explicitation = ExplByPos of int * identifier option | ExplByName of identifier
-
-type binder_kind =
-  | Default of binding_kind
-  | Generalized of binding_kind * binding_kind * bool
-      (** Inner binding, outer bindings, typeclass-specific flag
-	 for implicit generalization of superclasses *)
-
-type abstraction_kind = AbsLambda | AbsPi
-
-type proj_flag = int option (** [Some n] = proj of the n-th visible argument *)
-
-type prim_token = Numeral of Bigint.bigint | String of string
-
-type cases_pattern_expr =
-  | CPatAlias of loc * cases_pattern_expr * identifier
-  | CPatCstr of loc * reference * cases_pattern_expr list
-  | CPatCstrExpl of loc * reference * cases_pattern_expr list
-  | CPatAtom of loc * reference option
-  | CPatOr of loc * cases_pattern_expr list
-  | CPatNotation of loc * notation * cases_pattern_notation_substitution
-  | CPatPrim of loc * prim_token
-  | CPatRecord of loc * (reference * cases_pattern_expr) list
-  | CPatDelimiters of loc * string * cases_pattern_expr
-
-and cases_pattern_notation_substitution =
-    cases_pattern_expr list *     (** for constr subterms *)
-    cases_pattern_expr list list  (** for recursive notations *)
-
-type constr_expr =
-  | CRef of reference
-  | CFix of loc * identifier located * fix_expr list
-  | CCoFix of loc * identifier located * cofix_expr list
-  | CProdN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
-  | CLambdaN of loc * (name located list * binder_kind * constr_expr) list * constr_expr
-  | CLetIn of loc * name located * constr_expr * constr_expr
-  | CAppExpl of loc * (proj_flag * reference) * constr_expr list
-  | CApp of loc * (proj_flag * constr_expr) *
-      (constr_expr * explicitation located option) list
-  | CRecord of loc * constr_expr option * (reference * constr_expr) list
-  | CCases of loc * case_style * constr_expr option *
-      (constr_expr * (name located option * cases_pattern_expr option)) list *
-      (loc * cases_pattern_expr list located list * constr_expr) list
-  | CLetTuple of loc * name located list * (name located option * constr_expr option) *
-      constr_expr * constr_expr
-  | CIf of loc * constr_expr * (name located option * constr_expr option)
-      * constr_expr * constr_expr
-  | CHole of loc * Evar_kinds.t option
-  | CPatVar of loc * (bool * patvar)
-  | CEvar of loc * existential_key * constr_expr list option
-  | CSort of loc * glob_sort
-  | CCast of loc * constr_expr * constr_expr cast_type
-  | CNotation of loc * notation * constr_notation_substitution
-  | CGeneralization of loc * binding_kind * abstraction_kind option * constr_expr
-  | CPrim of loc * prim_token
-  | CDelimiters of loc * string * constr_expr
-
-and fix_expr =
-    identifier located * (identifier located option * recursion_order_expr) * local_binder list * constr_expr * constr_expr
-
-and cofix_expr =
-    identifier located * local_binder list * constr_expr * constr_expr
-
-and recursion_order_expr =
-  | CStructRec
-  | CWfRec of constr_expr
-  | CMeasureRec of constr_expr * constr_expr option (** measure, relation *)
-
-(** Anonymous defs allowed ?? *)
-and local_binder =
-  | LocalRawDef of name located * constr_expr
-  | LocalRawAssum of name located list * binder_kind * constr_expr
-
-and constr_notation_substitution =
-    constr_expr list *      (** for constr subterms *)
-    constr_expr list list * (** for recursive notations *)
-    local_binder list list (** for binders subexpressions *)
-
-type typeclass_constraint = name located * binding_kind * constr_expr
-
-and typeclass_context = typeclass_constraint list
-
-type constr_pattern_expr = constr_expr
-
 val oldfashion_patterns : bool ref
 
 (** Utilities on constr_expr                                           *)
@@ -259,17 +125,6 @@ val map_constr_expr_with_binders :
   (identifier -> 'a -> 'a) -> ('a -> constr_expr -> constr_expr) ->
       'a -> constr_expr -> constr_expr
 
-(** Concrete syntax for modules and module types                       *)
-
-type with_declaration_ast =
-  | CWith_Module of identifier list located * qualid located
-  | CWith_Definition of identifier list located * constr_expr
-
-type module_ast =
-  | CMident of qualid located
-  | CMapply of loc * module_ast * module_ast
-  | CMwith of loc * module_ast * with_declaration_ast
-
 val ntn_loc :
   loc -> constr_notation_substitution -> string -> (int * int) list
 val patntn_loc :