Merge PR #7570: [api] Move `Constrexpr` to the `interp` module.

71 files changed, 377 insertions, 367 deletions

diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 346b7c7dd..4838dd734 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -41,6 +41,15 @@ Printer.ml API
   pr_subgoal and pr_goal was removed to simplify the code.  It was
   earlierly used by PCoq.
 
+Source code organization
+
+- We have eliminated / fused some redundant modules and relocated a
+  few interfaces files. The `intf` folder is gone, and now for example
+  `Constrexpr` is located in `interp/`, `Vernacexpr` in `vernac/` and
+  so on. Changes should be compatible, but in a few cases stricter
+  layering requirements may mean that functions have moved. In all
+  cases adapting is a matter of changing the module name.
+
 Vernacular commands
 
 - The implementation of vernacular commands has been refactored so it
diff --git a/engine/uState.ml b/engine/uState.ml
index 15cf4d4c1..643c621fd 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -305,8 +305,20 @@ let reference_of_level uctx =
 let pr_uctx_level uctx l =
   Libnames.pr_reference (reference_of_level uctx l)
 
+type ('a, 'b) gen_universe_decl = {
+  univdecl_instance : 'a; (* Declared universes *)
+  univdecl_extensible_instance : bool; (* Can new universes be added *)
+  univdecl_constraints : 'b; (* Declared constraints *)
+  univdecl_extensible_constraints : bool (* Can new constraints be added *) }
+
 type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+
+let default_univ_decl =
+  { univdecl_instance = [];
+    univdecl_extensible_instance = true;
+    univdecl_constraints = Univ.Constraint.empty;
+    univdecl_extensible_constraints = true }
 
 let error_unbound_universes left uctx =
   let open Univ in
@@ -367,7 +379,6 @@ let check_implication uctx cstrs cstrs' =
       (str "Universe constraints are not implied by the ones declared.")
 
 let check_mono_univ_decl uctx decl =
-  let open Misctypes in
   let () =
     let names = decl.univdecl_instance in
     let extensible = decl.univdecl_extensible_instance in
@@ -380,7 +391,6 @@ let check_mono_univ_decl uctx decl =
   uctx.uctx_local
 
 let check_univ_decl ~poly uctx decl =
-  let open Misctypes in
   let ctx =
     let names = decl.univdecl_instance in
     let extensible = decl.univdecl_extensible_instance in
diff --git a/engine/uState.mli b/engine/uState.mli
index d1678a155..e2f25642e 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -138,8 +138,16 @@ val refresh_undefined_univ_variables : t -> t * Univ.universe_level_subst
 (** Universe minimization *)
 val minimize : t -> t
 
+type ('a, 'b) gen_universe_decl = {
+  univdecl_instance : 'a; (* Declared universes *)
+  univdecl_extensible_instance : bool; (* Can new universes be added *)
+  univdecl_constraints : 'b; (* Declared constraints *)
+  univdecl_extensible_constraints : bool (* Can new constraints be added *) }
+
 type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (Misctypes.lident list, Univ.Constraint.t) gen_universe_decl
+
+val default_univ_decl : universe_decl
 
 (** [check_univ_decl ctx decl]
 
diff --git a/pretyping/constrexpr.ml b/interp/constrexpr.ml
index 1443dfb51..ca6ea94f0 100644
--- a/pretyping/constrexpr.ml
+++ b/interp/constrexpr.ml
@@ -16,8 +16,7 @@ open Decl_kinds
 (** {6 Concrete syntax for terms } *)
 
 (** [constr_expr] is the abstract syntax tree produced by the parser *)
-
-type universe_decl_expr = (lident list, Glob_term.glob_constraint list) gen_universe_decl
+type universe_decl_expr = (lident list, Glob_term.glob_constraint list) UState.gen_universe_decl
 
 type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 3eb5acfc5..1be1dd96c 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -600,3 +600,35 @@ let _ = Goptions.declare_bool_option {
   Goptions.optread = (fun () -> !asymmetric_patterns);
   Goptions.optwrite = (fun a -> asymmetric_patterns:=a);
 }
+
+(** Local universe and constraint declarations. *)
+
+let interp_univ_constraints env evd cstrs =
+  let interp (evd,cstrs) (u, d, u') =
+    let ul = Pretyping.interp_known_glob_level evd u in
+    let u'l = Pretyping.interp_known_glob_level evd u' in
+    let cstr = (ul,d,u'l) in
+    let cstrs' = Univ.Constraint.add cstr cstrs in
+    try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
+        evd, cstrs'
+    with Univ.UniverseInconsistency e ->
+      CErrors.user_err ~hdr:"interp_constraint"
+        (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
+  in
+  List.fold_left interp (evd,Univ.Constraint.empty) cstrs
+
+let interp_univ_decl env decl =
+  let open UState in
+  let pl : lident list = decl.univdecl_instance in
+  let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
+  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
+  let decl = { univdecl_instance = pl;
+    univdecl_extensible_instance = decl.univdecl_extensible_instance;
+    univdecl_constraints = cstrs;
+    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
+  in evd, decl
+
+let interp_univ_decl_opt env l =
+  match l with
+  | None -> Evd.from_env env, UState.default_univ_decl
+  | Some decl -> interp_univ_decl env decl
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index 2df9e5a8c..b4f0886ac 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -116,3 +116,10 @@ val error_invalid_pattern_notation : ?loc:Loc.t -> unit -> 'a
 
 (** Placeholder for global option, should be moved to a parameter *)
 val asymmetric_patterns : bool ref
+
+(** Local universe and constraint declarations. *)
+val interp_univ_decl : Environ.env -> universe_decl_expr ->
+                       Evd.evar_map * UState.universe_decl
+
+val interp_univ_decl_opt : Environ.env -> universe_decl_expr option ->
+                       Evd.evar_map * UState.universe_decl
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 3a88284e4..45c0e9c42 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -820,11 +820,11 @@ let split_by_type ids subst =
     | NtnTypeConstr ->
        let terms,terms' = bind id scl terms terms' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder NtnBinderParsedAsConstr (Extend.AsIdentOrPattern | Extend.AsStrictPattern) ->
+    | NtnTypeBinder NtnBinderParsedAsConstr (AsIdentOrPattern | AsStrictPattern) ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
        let binders' = Id.Map.add id (coerce_to_cases_pattern_expr a,(false,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
-    | NtnTypeBinder NtnBinderParsedAsConstr Extend.AsIdent ->
+    | NtnTypeBinder NtnBinderParsedAsConstr AsIdent ->
        let a,terms = match terms with a::terms -> a,terms | _ -> assert false in
        let binders' = Id.Map.add id (cases_pattern_of_name (coerce_to_name a),(true,scl)) binders' in
        (terms,termlists,binders,binderlists),(terms',termlists',binders',binderlists')
diff --git a/pretyping/genredexpr.ml b/interp/genredexpr.ml
index 80697461a..80697461a 100644
--- a/pretyping/genredexpr.ml
+++ b/interp/genredexpr.ml
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 289890544..b48db9ac5 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -17,12 +17,14 @@ open Glob_term
 open Constrexpr
 open Libnames
 open Typeclasses
-open Typeclasses_errors
 open Pp
 open Libobject
 open Nameops
 open Context.Rel.Declaration
 
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *)
+let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m))
+
 module RelDecl = Context.Rel.Declaration
 (*i*)
 
@@ -238,7 +240,7 @@ let implicit_application env ?(allow_partial=true) f ty =
 	      let applen = List.fold_left (fun acc (x, y) -> opt_succ y acc) 0 par in
 	      let needlen = List.fold_left (fun acc x -> opt_succ x acc) 0 ci in
 		if not (Int.equal needlen applen) then
-		  Typeclasses_errors.mismatched_ctx_inst (Global.env ()) Parameters (List.map fst par) rd
+                  mismatched_ctx_inst_err (Global.env ()) Typeclasses_errors.Parameters (List.map fst par) rd
 	    end;
 	  let pars = List.rev (List.combine ci rd) in
 	  let args, avoid = combine_params avoid f par pars in
diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli
index 39d0174f9..e64c5c542 100644
--- a/interp/implicit_quantifiers.mli
+++ b/interp/implicit_quantifiers.mli
@@ -45,3 +45,7 @@ val implicit_application : Id.Set.t -> ?allow_partial:bool ->
   (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t ->
     Constrexpr.constr_expr * Id.Set.t) ->
   constr_expr -> constr_expr * Id.Set.t
+
+(* Should be likely located elsewhere *)
+exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *)
+val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a
diff --git a/interp/interp.mllib b/interp/interp.mllib
index 37a327a7d..3668455ae 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,3 +1,6 @@
+Constrexpr
+Genredexpr
+Redops
 Tactypes
 Stdarg
 Genintern
@@ -7,7 +10,6 @@ Notation
 Syntax_def
 Smartlocate
 Constrexpr_ops
-Ppextend
 Dumpglob
 Reserve
 Impargs
diff --git a/interp/modintern.ml b/interp/modintern.ml
index dc93d8dc4..fefd2ab6f 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -63,7 +63,7 @@ let transl_with_decl env = function
   | CWith_Module ({CAst.v=fqid},qid) ->
       WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
   | CWith_Definition ({CAst.v=fqid},udecl,c) ->
-    let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
+    let sigma, udecl = Constrexpr_ops.interp_univ_decl_opt env udecl in
     let c, ectx = interp_constr env sigma c in
     begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
       | Entries.Polymorphic_const_entry ctx ->
diff --git a/interp/notation.ml b/interp/notation.ml
index 192c477be..05fcd0e7f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -20,7 +20,6 @@ open Constrexpr
 open Notation_term
 open Glob_term
 open Glob_ops
-open Ppextend
 open Context.Named.Declaration
 
 (*i*)
@@ -56,9 +55,6 @@ type scope = {
   delimiters: delimiters option
 }
 
-(* Uninterpreted notation map: notation -> level * DirPath.t *)
-let notation_level_map = ref String.Map.empty
-
 (* Scopes table: scope_name -> symbol_interpretation *)
 let scope_map = ref String.Map.empty
 
@@ -75,44 +71,6 @@ let default_scope = "" (* empty name, not available from outside *)
 let init_scope_map () =
   scope_map := String.Map.add default_scope empty_scope !scope_map
 
-(**********************************************************************)
-(* Operations on scopes *)
-
-let parenRelation_eq t1 t2 = match t1, t2 with
-| L, L | E, E | Any, Any -> true
-| Prec l1, Prec l2 -> Int.equal l1 l2
-| _ -> false
-
-open Extend
-
-let production_level_eq l1 l2 = true (* (l1 = l2) *)
-
-let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
-| NextLevel, NextLevel -> true
-| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
-| (NextLevel | NumLevel _), _ -> false *)
-
-let constr_entry_key_eq eq v1 v2 = match v1, v2 with
-| ETName, ETName -> true
-| ETReference, ETReference -> true
-| ETBigint, ETBigint -> true
-| ETBinder b1, ETBinder b2 -> b1 == b2
-| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
-| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
-| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
-| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
-| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
-
-let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
-  let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
-  let prod_eq (l1,pp1) (l2,pp2) =
-    if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
-    else production_level_eq l1 l2 in
-  Int.equal l1 l2 && List.equal tolerability_eq t1 t2
-  && List.equal (constr_entry_key_eq prod_eq) u1 u2
-
-let level_eq = level_eq_gen false
-
 let declare_scope scope =
   try let _ = String.Map.find scope !scope_map in ()
   with Not_found ->
@@ -427,18 +385,6 @@ let rec find_without_delimiters find (ntn_scope,ntn) = function
       (* Can we switch to [scope]? Yes if it has defined delimiters *)
       find_with_delimiters ntn_scope
 
-(* Uninterpreted notation levels *)
-
-let declare_notation_level ?(onlyprint=false) ntn level =
-  if String.Map.mem ntn !notation_level_map then
-    anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
-  notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
-
-let level_of_notation ?(onlyprint=false) ntn =
-  let (level,onlyprint') = String.Map.find ntn !notation_level_map in
-  if onlyprint' && not onlyprint then raise Not_found;
-  level
-
 (* The mapping between notations and their interpretation *)
 
 let warn_notation_overridden =
@@ -1113,63 +1059,24 @@ let pr_visibility prglob = function
   | None -> pr_scope_stack prglob !scope_stack
 
 (**********************************************************************)
-(* Mapping notations to concrete syntax *)
-
-type unparsing_rule = unparsing list * precedence
-type extra_unparsing_rules = (string * string) list
-(* Concrete syntax for symbolic-extension table *)
-let notation_rules =
-  ref (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
-
-let declare_notation_rule ntn ~extra unpl gram =
-  notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
-
-let find_notation_printing_rule ntn =
-  try pi1 (String.Map.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
-let find_notation_extra_printing_rules ntn =
-  try pi2 (String.Map.find ntn !notation_rules)
-  with Not_found -> []
-let find_notation_parsing_rules ntn =
-  try pi3 (String.Map.find ntn !notation_rules)
-  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
-
-let get_defined_notations () =
-  String.Set.elements @@ String.Map.domain !notation_rules
-
-let add_notation_extra_printing_rule ntn k v =
-  try
-    notation_rules :=
-      let p, pp, gr = String.Map.find ntn !notation_rules in
-      String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
-  with Not_found ->
-    user_err ~hdr:"add_notation_extra_printing_rule"
-      (str "No such Notation.")
-
-(**********************************************************************)
 (* Synchronisation with reset *)
 
 let freeze _ =
- (!scope_map, !notation_level_map, !scope_stack, !arguments_scope,
-  !delimiters_map, !notations_key_table, !notation_rules,
-  !scope_class_map)
+ (!scope_map, !scope_stack, !arguments_scope,
+  !delimiters_map, !notations_key_table, !scope_class_map)
 
-let unfreeze (scm,nlm,scs,asc,dlm,fkm,pprules,clsc) =
+let unfreeze (scm,scs,asc,dlm,fkm,clsc) =
   scope_map := scm;
-  notation_level_map := nlm;
   scope_stack := scs;
   delimiters_map := dlm;
   arguments_scope := asc;
   notations_key_table := fkm;
-  notation_rules := pprules;
   scope_class_map := clsc
 
 let init () =
   init_scope_map ();
-  notation_level_map := String.Map.empty;
   delimiters_map := String.Map.empty;
   notations_key_table := KeyMap.empty;
-  notation_rules := String.Map.empty;
   scope_class_map := initial_scope_class_map
 
 let _ =
diff --git a/interp/notation.mli b/interp/notation.mli
index ccc67fe49..b177b7f1e 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -14,7 +14,6 @@ open Libnames
 open Constrexpr
 open Glob_term
 open Notation_term
-open Ppextend
 
 (** Notations *)
 
@@ -32,8 +31,6 @@ val declare_scope : scope_name -> unit
 
 val current_scopes : unit -> scopes
 
-val level_eq : level -> level -> bool
-
 (** Check where a scope is opened or not in a scope list, or in
  * the current opened scopes *)
 val scope_is_open_in_scopes : scope_name -> scopes -> bool
@@ -135,11 +132,6 @@ val uninterp_ind_pattern_notations : inductive -> notation_rule list
 val availability_of_notation : scope_name option * notation -> local_scopes ->
   (scope_name option * delimiters option) option
 
-(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
-
-val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
-val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
-
 (** {6 Miscellaneous} *)
 
 val interp_notation_as_global_reference : ?loc:Loc.t -> (GlobRef.t -> bool) ->
@@ -200,21 +192,6 @@ val locate_notation : (glob_constr -> Pp.t) -> notation ->
 
 val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t
 
-(** {6 Printing rules for notations} *)
-
-(** Declare and look for the printing rule for symbolic notations *)
-type unparsing_rule = unparsing list * precedence
-type extra_unparsing_rules = (string * string) list
-val declare_notation_rule :
-  notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
-val find_notation_printing_rule : notation -> unparsing_rule
-val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
-val find_notation_parsing_rules : notation -> notation_grammar
-val add_notation_extra_printing_rule : notation -> string -> string -> unit
-
-(** Returns notations with defined parsing/printing rules *)
-val get_defined_notations : unit -> notation list
-
 (** Rem: printing rules for primitive token are canonical *)
 
 val with_notation_protection : ('a -> 'b) -> 'a -> 'b
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index b0480aa70..f208b23fb 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -687,7 +687,7 @@ let is_onlybinding_meta id metas =
 let is_onlybinding_pattern_like_meta isvar id metas =
   try match Id.List.assoc id metas with
       | _,NtnTypeBinder (NtnBinderParsedAsConstr
-                           (Extend.AsIdentOrPattern | Extend.AsStrictPattern)) -> true
+                           (AsIdentOrPattern | AsStrictPattern)) -> true
       | _,NtnTypeBinder (NtnParsedAsPattern strict) -> not (strict && isvar)
       | _ -> false
   with Not_found -> false
diff --git a/interp/notation_term.ml b/interp/notation_term.ml
index 1a46746cc..52a6354a0 100644
--- a/interp/notation_term.ml
+++ b/interp/notation_term.ml
@@ -62,6 +62,11 @@ type subscopes = tmp_scope_name option * scope_name list
 (** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
     x carries the sequence of objects bound to the list x..y  *)
 
+type constr_as_binder_kind =
+  | AsIdent
+  | AsIdentOrPattern
+  | AsStrictPattern
+
 type notation_binder_source =
   (* This accepts only pattern *)
   (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
@@ -69,7 +74,7 @@ type notation_binder_source =
   (* This accepts only ident *)
   | NtnParsedAsIdent
   (* This accepts ident, or pattern, or both *)
-  | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind
+  | NtnBinderParsedAsConstr of constr_as_binder_kind
 
 type notation_var_instance_type =
   | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
@@ -91,33 +96,3 @@ type notation_interp_env = {
   ninterp_var_type : notation_var_internalization_type Id.Map.t;
   ninterp_rec_vars : Id.t Id.Map.t;
 }
-
-type grammar_constr_prod_item =
-  | GramConstrTerminal of Tok.t
-  | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
-  | GramConstrListMark of int * bool * int
-    (* tells action rule to make a list of the n previous parsed items;
-       concat with last parsed list when true; additionally release
-       the p last items as if they were parsed autonomously *)
-
-(** Dealing with precedences *)
-
-type precedence = int
-type parenRelation = L | E | Any | Prec of precedence
-type tolerability = precedence * parenRelation
-
-type level = precedence * tolerability list * Extend.constr_entry_key list
-
-(** Grammar rules for a notation *)
-
-type one_notation_grammar = {
-  notgram_level : level;
-  notgram_assoc : Extend.gram_assoc option;
-  notgram_notation : Constrexpr.notation;
-  notgram_prods : grammar_constr_prod_item list list;
-}
-
-type notation_grammar = {
-  notgram_onlyprinting : bool;
-  notgram_rules : one_notation_grammar list
-}
diff --git a/pretyping/redops.ml b/interp/redops.ml
index 90c3bdfae..b9a74136e 100644
--- a/pretyping/redops.ml
+++ b/interp/redops.ml
@@ -42,3 +42,23 @@ let make_red_flag l =
 let all_flags =
   {rBeta = true; rMatch = true; rFix = true; rCofix = true;
    rZeta = true; rDelta = true; rConst = []}
+
+(** Mapping [red_expr_gen] *)
+
+let map_flags f flags =
+  { flags with rConst = List.map f flags.rConst }
+
+let map_occs f (occ,e) = (occ,f e)
+
+let map_red_expr_gen f g h = function
+  | Fold l -> Fold (List.map f l)
+  | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
+  | Simpl (flags,occs_o) ->
+     Simpl (map_flags g flags, Option.map (map_occs (Util.map_union g h)) occs_o)
+  | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
+  | Cbv flags -> Cbv (map_flags g flags)
+  | Lazy flags -> Lazy (map_flags g flags)
+  | CbvVm occs_o -> CbvVm (Option.map (map_occs (Util.map_union g h)) occs_o)
+  | CbvNative occs_o -> CbvNative (Option.map (map_occs (Util.map_union g h)) occs_o)
+  | Cbn flags -> Cbn (map_flags g flags)
+  | ExtraRedExpr _ | Red _ | Hnf as x -> x
diff --git a/pretyping/redops.mli b/interp/redops.mli
index 285931ecd..7254f29b2 100644
--- a/pretyping/redops.mli
+++ b/interp/redops.mli
@@ -13,3 +13,8 @@ open Genredexpr
 val make_red_flag : 'a red_atom list -> 'a glob_red_flag
 
 val all_flags : 'a glob_red_flag
+
+(** Mapping [red_expr_gen] *)
+
+val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
+  ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
diff --git a/library/misctypes.ml b/library/misctypes.ml
index a3c887045..cfae07484 100644
--- a/library/misctypes.ml
+++ b/library/misctypes.ml
@@ -112,9 +112,3 @@ type multi =
   | UpTo of int
   | RepeatStar
   | RepeatPlus
-
-type ('a, 'b) gen_universe_decl = {
-  univdecl_instance : 'a; (* Declared universes *)
-  univdecl_extensible_instance : bool; (* Can new universes be added *)
-  univdecl_constraints : 'b; (* Declared constraints *)
-  univdecl_extensible_constraints : bool (* Can new constraints be added *) }
diff --git a/parsing/extend.ml b/parsing/extend.ml
index 734b859f6..f2af594ef 100644
--- a/parsing/extend.ml
+++ b/parsing/extend.ml
@@ -31,11 +31,6 @@ type production_level =
   | NextLevel
   | NumLevel of int
 
-type constr_as_binder_kind =
-  | AsIdent
-  | AsIdentOrPattern
-  | AsStrictPattern
-
 (** User-level types used to tell how to parse or interpret of the non-terminal *)
 
 type 'a constr_entry_key_gen =
@@ -44,7 +39,7 @@ type 'a constr_entry_key_gen =
   | ETBigint
   | ETBinder of bool  (* open list of binders if true, closed list of binders otherwise *)
   | ETConstr of 'a
-  | ETConstrAsBinder of constr_as_binder_kind * 'a
+  | ETConstrAsBinder of Notation_term.constr_as_binder_kind * 'a
   | ETPattern of bool * int option (* true = strict pattern, i.e. not a single variable *)
   | ETOther of string * string
 
diff --git a/parsing/notation_gram.ml b/parsing/notation_gram.ml
new file mode 100644
index 000000000..346350641
--- /dev/null
+++ b/parsing/notation_gram.ml
@@ -0,0 +1,42 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Extend
+
+(** Dealing with precedences *)
+
+type precedence = int
+type parenRelation = L | E | Any | Prec of precedence
+type tolerability = precedence * parenRelation
+
+type level = precedence * tolerability list * constr_entry_key list
+
+type grammar_constr_prod_item =
+  | GramConstrTerminal of Tok.t
+  | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
+  | GramConstrListMark of int * bool * int
+    (* tells action rule to make a list of the n previous parsed items;
+       concat with last parsed list when true; additionally release
+       the p last items as if they were parsed autonomously *)
+
+(** Grammar rules for a notation *)
+
+type one_notation_grammar = {
+  notgram_level : level;
+  notgram_assoc : Extend.gram_assoc option;
+  notgram_notation : Constrexpr.notation;
+  notgram_prods : grammar_constr_prod_item list list;
+}
+
+type notation_grammar = {
+  notgram_onlyprinting : bool;
+  notgram_rules : one_notation_grammar list
+}
diff --git a/parsing/notgram_ops.ml b/parsing/notgram_ops.ml
new file mode 100644
index 000000000..071e6db20
--- /dev/null
+++ b/parsing/notgram_ops.ml
@@ -0,0 +1,65 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Pp
+open CErrors
+open Util
+open Extend
+open Notation_gram
+
+(* Uninterpreted notation levels *)
+
+let notation_level_map = Summary.ref ~name:"notation_level_map" String.Map.empty
+
+let declare_notation_level ?(onlyprint=false) ntn level =
+  if String.Map.mem ntn !notation_level_map then
+    anomaly (str "Notation " ++ str ntn ++ str " is already assigned a level.");
+  notation_level_map := String.Map.add ntn (level,onlyprint) !notation_level_map
+
+let level_of_notation ?(onlyprint=false) ntn =
+  let (level,onlyprint') = String.Map.find ntn !notation_level_map in
+  if onlyprint' && not onlyprint then raise Not_found;
+  level
+
+(**********************************************************************)
+(* Operations on scopes *)
+
+let parenRelation_eq t1 t2 = match t1, t2 with
+| L, L | E, E | Any, Any -> true
+| Prec l1, Prec l2 -> Int.equal l1 l2
+| _ -> false
+
+let production_level_eq l1 l2 = true (* (l1 = l2) *)
+
+let production_position_eq pp1 pp2 = true (* pp1 = pp2 *) (* match pp1, pp2 with
+| NextLevel, NextLevel -> true
+| NumLevel n1, NumLevel n2 -> Int.equal n1 n2
+| (NextLevel | NumLevel _), _ -> false *)
+
+let constr_entry_key_eq eq v1 v2 = match v1, v2 with
+| ETName, ETName -> true
+| ETReference, ETReference -> true
+| ETBigint, ETBigint -> true
+| ETBinder b1, ETBinder b2 -> b1 == b2
+| ETConstr lev1, ETConstr lev2 -> eq lev1 lev2
+| ETConstrAsBinder (bk1,lev1), ETConstrAsBinder (bk2,lev2) -> eq lev1 lev2 && bk1 = bk2
+| ETPattern (b1,n1), ETPattern (b2,n2) -> b1 = b2 && Option.equal Int.equal n1 n2
+| ETOther (s1,s1'), ETOther (s2,s2') -> String.equal s1 s2 && String.equal s1' s2'
+| (ETName | ETReference | ETBigint | ETBinder _ | ETConstr _ | ETPattern _ | ETOther _ | ETConstrAsBinder _), _ -> false
+
+let level_eq_gen strict (l1, t1, u1) (l2, t2, u2) =
+  let tolerability_eq (i1, r1) (i2, r2) = Int.equal i1 i2 && parenRelation_eq r1 r2 in
+  let prod_eq (l1,pp1) (l2,pp2) =
+    if strict then production_level_eq l1 l2 && production_position_eq pp1 pp2
+    else production_level_eq l1 l2 in
+  Int.equal l1 l2 && List.equal tolerability_eq t1 t2
+  && List.equal (constr_entry_key_eq prod_eq) u1 u2
+
+let level_eq = level_eq_gen false
diff --git a/pretyping/univdecls.mli b/parsing/notgram_ops.mli
index 305d045b1..f427a607b 100644
--- a/pretyping/univdecls.mli
+++ b/parsing/notgram_ops.mli
@@ -8,14 +8,13 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-(** Local universe and constraint declarations. *)
-type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
+(* Merge with metasyntax? *)
+open Constrexpr
+open Notation_gram
 
-val default_univ_decl : universe_decl
+val level_eq : level -> level -> bool
 
-val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr ->
-                       Evd.evar_map * universe_decl
+(** {6 Declare and test the level of a (possibly uninterpreted) notation } *)
 
-val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option ->
-                       Evd.evar_map * universe_decl
+val declare_notation_level : ?onlyprint:bool -> notation -> level -> unit
+val level_of_notation : ?onlyprint:bool -> notation -> level (** raise [Not_found] if no level or not respecting onlyprint *)
diff --git a/parsing/parsing.mllib b/parsing/parsing.mllib
index da4a0421b..2154f2f88 100644
--- a/parsing/parsing.mllib
+++ b/parsing/parsing.mllib
@@ -1,6 +1,9 @@
 Tok
 CLexer
 Extend
+Notation_gram
+Ppextend
+Notgram_ops
 Pcoq
 G_constr
 G_prim
diff --git a/interp/ppextend.ml b/parsing/ppextend.ml
index c75d9e12f..d2b50fa83 100644
--- a/interp/ppextend.ml
+++ b/parsing/ppextend.ml
@@ -8,8 +8,10 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
+open Util
 open Pp
-open Notation_term
+open CErrors
+open Notation_gram
 
 (*s Pretty-print. *)
 
@@ -41,3 +43,34 @@ type unparsing =
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
+
+type unparsing_rule = unparsing list * precedence
+type extra_unparsing_rules = (string * string) list
+(* Concrete syntax for symbolic-extension table *)
+let notation_rules =
+  Summary.ref ~name:"notation-rules" (String.Map.empty : (unparsing_rule * extra_unparsing_rules * notation_grammar) String.Map.t)
+
+let declare_notation_rule ntn ~extra unpl gram =
+  notation_rules := String.Map.add ntn (unpl,extra,gram) !notation_rules
+
+let find_notation_printing_rule ntn =
+  try pi1 (String.Map.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No printing rule found for " ++ str ntn ++ str ".")
+let find_notation_extra_printing_rules ntn =
+  try pi2 (String.Map.find ntn !notation_rules)
+  with Not_found -> []
+let find_notation_parsing_rules ntn =
+  try pi3 (String.Map.find ntn !notation_rules)
+  with Not_found -> anomaly (str "No parsing rule found for " ++ str ntn ++ str ".")
+
+let get_defined_notations () =
+  String.Set.elements @@ String.Map.domain !notation_rules
+
+let add_notation_extra_printing_rule ntn k v =
+  try
+    notation_rules :=
+      let p, pp, gr = String.Map.find ntn !notation_rules in
+      String.Map.add ntn (p, (k,v) :: pp, gr) !notation_rules
+  with Not_found ->
+    user_err ~hdr:"add_notation_extra_printing_rule"
+      (str "No such Notation.")
diff --git a/interp/ppextend.mli b/parsing/ppextend.mli
index c81058e72..9f61e121a 100644
--- a/interp/ppextend.mli
+++ b/parsing/ppextend.mli
@@ -8,7 +8,8 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open Notation_term
+open Constrexpr
+open Notation_gram
 
 (** {6 Pretty-print. } *)
 
@@ -26,6 +27,9 @@ val ppcmd_of_box : ppbox -> Pp.t -> Pp.t
 
 val ppcmd_of_cut : ppcut -> Pp.t
 
+(** {6 Printing rules for notations} *)
+
+(** Declare and look for the printing rule for symbolic notations *)
 type unparsing =
   | UnpMetaVar of int * parenRelation
   | UnpBinderMetaVar of int * parenRelation
@@ -34,3 +38,15 @@ type unparsing =
   | UnpTerminal of string
   | UnpBox of ppbox * unparsing Loc.located list
   | UnpCut of ppcut
+
+type unparsing_rule = unparsing list * precedence
+type extra_unparsing_rules = (string * string) list
+
+val declare_notation_rule : notation -> extra:extra_unparsing_rules -> unparsing_rule -> notation_grammar -> unit
+val find_notation_printing_rule : notation -> unparsing_rule
+val find_notation_extra_printing_rules : notation -> extra_unparsing_rules
+val find_notation_parsing_rules : notation -> notation_grammar
+val add_notation_extra_printing_rule : notation -> string -> string -> unit
+
+(** Returns notations with defined parsing/printing rules *)
+val get_defined_notations : unit -> notation list
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 702b83034..4e7c8b754 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -251,7 +251,7 @@ END
 let pr_by_arg_tac _prc _prlc prtac opt_c =
   match opt_c with
     | None -> mt ()
-    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
+    | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
 
 ARGUMENT EXTEND by_arg_tac
   TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e5a4f090e..ff697e3c7 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -66,7 +66,7 @@ val wit_by_arg_tac :
   Geninterp.Val.t option) Genarg.genarg_type
 
 val pr_by_arg_tac : 
-  (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
+  (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
   raw_tactic_expr option -> Pp.t
 
 val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 3dfe308a5..b29af6680 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Genarg
 open Geninterp
 open Stdarg
 open Libnames
-open Notation_term
+open Notation_gram
 open Misctypes
 open Locus
 open Decl_kinds
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 799a52cc8..5d2a99618 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -17,7 +17,7 @@ open Names
 open Misctypes
 open Environ
 open Constrexpr
-open Notation_term
+open Notation_gram
 open Tacexpr
 
 type 'a grammar_tactic_prod_item_expr =
@@ -153,5 +153,5 @@ val pr_value : tolerability -> Val.t -> Pp.t
 
 val ltop : tolerability
 
-val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
   'a Genprint.top_printer
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index a1d8b087e..50bf687b1 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -112,7 +112,7 @@ let subst_glob_constr_or_pattern subst (bvars,c,p) =
   (bvars,subst_glob_constr subst c,subst_pattern subst p)
 
 let subst_redexp subst =
-  Miscops.map_red_expr_gen
+  Redops.map_red_expr_gen
     (subst_glob_constr subst)
     (subst_evaluable subst)
     (subst_glob_constr_or_pattern subst)
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 138b42e54..fbfbdb110 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -64,7 +64,7 @@ DECLARE PLUGIN "ssreflect_plugin"
  * we thus save the lexer to restore it at the end of the file *)
 let frozen_lexer = CLexer.get_keyword_state () ;;
 
-let tacltop = (5,Notation_term.E)
+let tacltop = (5,Notation_gram.E)
 
 let pr_ssrtacarg _ _ prt = prt tacltop
 ARGUMENT EXTEND ssrtacarg TYPED AS tactic PRINTED BY pr_ssrtacarg
diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli
index 2ac7c7e26..7cd3751ce 100644
--- a/plugins/ssr/ssrparser.mli
+++ b/plugins/ssr/ssrparser.mli
@@ -14,11 +14,11 @@ open Ltac_plugin
 
 val ssrtacarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtacarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtacarg : 'a -> 'b -> (Notation_term.tolerability -> 'c) -> 'c
+val pr_ssrtacarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c) -> 'c
 
 val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry
 val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type
-val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> 'd
+val pr_ssrtclarg : 'a -> 'b -> (Notation_gram.tolerability -> 'c -> 'd) -> 'c -> 'd
 
 val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type
 
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 1b536bfda..1697e54ab 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -10,7 +10,6 @@
 
 open Util
 open Misctypes
-open Genredexpr
 
 (** Mapping [cast_type] *)
 
@@ -42,26 +41,6 @@ let intro_pattern_naming_eq nam1 nam2 = match nam1, nam2 with
 | IntroFresh id1, IntroFresh id2 -> Names.Id.equal id1 id2
 | _ -> false
 
-(** Mapping [red_expr_gen] *)
-
-let map_flags f flags =
-  { flags with rConst = List.map f flags.rConst }
-
-let map_occs f (occ,e) = (occ,f e)
-
-let map_red_expr_gen f g h = function
-  | Fold l -> Fold (List.map f l)
-  | Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
-  | Simpl (flags,occs_o) ->
-     Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o)
-  | Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
-  | Cbv flags -> Cbv (map_flags g flags)
-  | Lazy flags -> Lazy (map_flags g flags)
-  | CbvVm occs_o -> CbvVm (Option.map (map_occs (map_union g h)) occs_o)
-  | CbvNative occs_o -> CbvNative (Option.map (map_occs (map_union g h)) occs_o)
-  | Cbn flags -> Cbn (map_flags g flags)
-  | ExtraRedExpr _ | Red _ | Hnf as x -> x
-
 (** Mapping bindings *)
 
 let map_explicit_bindings f l =
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index 1d4504541..6a84fb9eb 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -9,7 +9,6 @@
 (************************************************************************)
 
 open Misctypes
-open Genredexpr
 
 (** Mapping [cast_type] *)
 
@@ -25,11 +24,6 @@ val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
 val intro_pattern_naming_eq :
   intro_pattern_naming_expr -> intro_pattern_naming_expr -> bool
 
-(** Mapping [red_expr_gen] *)
-
-val map_red_expr_gen : ('a -> 'd) -> ('b -> 'e) -> ('c -> 'f) ->
-  ('a,'b,'c) red_expr_gen -> ('d,'e,'f) red_expr_gen
-
 (** Mapping bindings *)
 
 val map_bindings : ('a -> 'b) -> 'a bindings -> 'b bindings
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index c48decdb0..3d9b5d3cf 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -16,13 +16,10 @@ Evarsolve
 Recordops
 Evarconv
 Typing
-Constrexpr
-Genredexpr
 Miscops
 Glob_term
 Ltac_pretype
 Glob_ops
-Redops
 Pattern
 Patternops
 Constr_matching
@@ -37,4 +34,3 @@ Indrec
 Cases
 Pretyping
 Unification
-Univdecls
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 89c5d7e7b..a1ac53c73 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -12,7 +12,6 @@
 open Names
 open EConstr
 open Environ
-open Constrexpr
 (*i*)
 
 type contexts = Parameters | Properties
@@ -20,7 +19,6 @@ type contexts = Parameters | Properties
 type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of GlobRef.t * Misctypes.lident (* Class name, method *)
-    | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
@@ -29,5 +27,3 @@ let typeclass_error env err = raise (TypeClassError (env, err))
 let not_a_class env c = typeclass_error env (NotAClass c)
 
 let unbound_method env cid id = typeclass_error env (UnboundMethod (cid, id))
-
-let mismatched_ctx_inst env c n m = typeclass_error env (MismatchedContextInstance (c, n, m))
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 4aabc0aee..1003f2ae1 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -11,14 +11,12 @@
 open Names
 open EConstr
 open Environ
-open Constrexpr
 
 type contexts = Parameters | Properties
 
 type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of GlobRef.t * Misctypes.lident (** Class name, method *)
-  | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
@@ -26,5 +24,3 @@ val not_a_class : env -> constr -> 'a
 
 val unbound_method : env -> GlobRef.t -> Misctypes.lident -> 'a
 
-val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a
-
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
deleted file mode 100644
index 8864be576..000000000
--- a/pretyping/univdecls.ml
+++ /dev/null
@@ -1,52 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-open CErrors
-
-(** Local universes and constraints declarations *)
-type universe_decl =
-  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
-
-let default_univ_decl =
-  let open Misctypes in
-  { univdecl_instance = [];
-    univdecl_extensible_instance = true;
-    univdecl_constraints = Univ.Constraint.empty;
-    univdecl_extensible_constraints = true }
-
-let interp_univ_constraints env evd cstrs =
-  let interp (evd,cstrs) (u, d, u') =
-    let ul = Pretyping.interp_known_glob_level evd u in
-    let u'l = Pretyping.interp_known_glob_level evd u' in
-    let cstr = (ul,d,u'l) in
-    let cstrs' = Univ.Constraint.add cstr cstrs in
-    try let evd = Evd.add_constraints evd (Univ.Constraint.singleton cstr) in
-        evd, cstrs'
-    with Univ.UniverseInconsistency e ->
-      user_err ~hdr:"interp_constraint"
-        (Univ.explain_universe_inconsistency (Termops.pr_evd_level evd) e)
-  in
-  List.fold_left interp (evd,Univ.Constraint.empty) cstrs
-
-let interp_univ_decl env decl =
-  let open Misctypes in
-  let pl : lident list = decl.univdecl_instance in
-  let evd = Evd.from_ctx (UState.make_with_initial_binders (Environ.universes env) pl) in
-  let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
-  let decl = { univdecl_instance = pl;
-    univdecl_extensible_instance = decl.univdecl_extensible_instance;
-    univdecl_constraints = cstrs;
-    univdecl_extensible_constraints = decl.univdecl_extensible_constraints }
-  in evd, decl
-
-let interp_univ_decl_opt env l =
-  match l with
-  | None -> Evd.from_env env, default_univ_decl
-  | Some decl -> interp_univ_decl env decl
diff --git a/printing/genprint.ml b/printing/genprint.ml
index 1bb7838a4..fa53a8794 100644
--- a/printing/genprint.ml
+++ b/printing/genprint.ml
@@ -19,15 +19,15 @@ open Geninterp
 (* Printing generic values *)
 
 type 'a with_level =
-  { default_already_surrounded : Notation_term.tolerability;
-    default_ensure_surrounded : Notation_term.tolerability;
+  { default_already_surrounded : Notation_gram.tolerability;
+    default_ensure_surrounded : Notation_gram.tolerability;
     printer : 'a }
 
 type printer_result =
 | PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
 
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
 
 type top_printer_result =
 | TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/genprint.mli b/printing/genprint.mli
index fd5dd7259..1a31025a9 100644
--- a/printing/genprint.mli
+++ b/printing/genprint.mli
@@ -13,15 +13,15 @@
 open Genarg
 
 type 'a with_level =
-  { default_already_surrounded : Notation_term.tolerability;
-    default_ensure_surrounded : Notation_term.tolerability;
+  { default_already_surrounded : Notation_gram.tolerability;
+    default_ensure_surrounded : Notation_gram.tolerability;
     printer : 'a }
 
 type printer_result =
 | PrinterBasic of (unit -> Pp.t)
-| PrinterNeedsLevel of (Notation_term.tolerability -> Pp.t) with_level
+| PrinterNeedsLevel of (Notation_gram.tolerability -> Pp.t) with_level
 
-type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_term.tolerability -> Pp.t
+type printer_fun_with_level = Environ.env -> Evd.evar_map -> Notation_gram.tolerability -> Pp.t
 
 type top_printer_result =
 | TopPrinterBasic of (unit -> Pp.t)
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 2a5f38697..e877b3c63 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -19,7 +19,7 @@ open Constr
 open Libnames
 open Pputils
 open Ppextend
-open Notation_term
+open Notation_gram
 open Constrexpr
 open Constrexpr_ops
 open Decl_kinds
@@ -88,8 +88,6 @@ let tag_var = tag Tag.variable
     | Numeral (_,b) -> if b then lposint else lnegint
     | String _ -> latom
 
-  open Notation
-
   let print_hunks n pr pr_patt pr_binders (terms, termlists, binders, binderlists) unps =
     let env = ref terms and envlist = ref termlists and bl = ref binders and bll = ref binderlists in
     let pop r = let a = List.hd !r in r := List.tl !r; a in
diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli
index 127c4471c..05f48ec79 100644
--- a/printing/ppconstr.mli
+++ b/printing/ppconstr.mli
@@ -16,7 +16,7 @@ open Libnames
 open Constrexpr
 open Names
 open Misctypes
-open Notation_term
+open Notation_gram
 
 val prec_less : precedence -> tolerability -> bool
 
diff --git a/printing/printer.mli b/printing/printer.mli
index ac0e12979..7a8b963d2 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -36,7 +36,7 @@ val pr_constr              : constr -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t
 
-val pr_constr_n_env        : env -> evar_map -> Notation_term.tolerability -> constr -> Pp.t
+val pr_constr_n_env        : env -> evar_map -> Notation_gram.tolerability -> constr -> Pp.t
 
 (** Same, but resilient to [Nametab] errors. Prints fully-qualified
     names when [shortest_qualid_of_global] has failed. Prints "??"
@@ -57,7 +57,7 @@ val pr_leconstr_env     : env -> evar_map -> EConstr.t -> Pp.t
 val pr_leconstr         : EConstr.t -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
-val pr_econstr_n_env    : env -> evar_map -> Notation_term.tolerability -> EConstr.t -> Pp.t
+val pr_econstr_n_env    : env -> evar_map -> Notation_gram.tolerability -> EConstr.t -> Pp.t
 
 val pr_etype_env           : env -> evar_map -> EConstr.types -> Pp.t
 val pr_letype_env           : env -> evar_map -> EConstr.types -> Pp.t
@@ -87,7 +87,7 @@ val pr_type_env            : env -> evar_map -> types -> Pp.t
 val pr_type                : types -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
 
-val pr_closed_glob_n_env   : env -> evar_map -> Notation_term.tolerability -> closed_glob_constr -> Pp.t
+val pr_closed_glob_n_env   : env -> evar_map -> Notation_gram.tolerability -> closed_glob_constr -> Pp.t
 val pr_closed_glob_env     : env -> evar_map -> closed_glob_constr -> Pp.t
 val pr_closed_glob         : closed_glob_constr -> Pp.t
 [@@ocaml.deprecated "The global printing API is deprecated, please use the _env functions"]
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 805635dfa..7b7973224 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -24,7 +24,7 @@ open Decl_kinds
     proof of mutually dependent theorems) *)
 
 val start_proof :
-  Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
+  Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map -> named_context_val -> EConstr.constr ->
   ?init_tac:unit Proofview.tactic ->
   Proof_global.proof_terminator -> unit
 
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d5cb5b09f..3abdd129e 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -97,7 +97,7 @@ type pstate = {
   proof : Proof.t;
   strength : Decl_kinds.goal_kind;
   mode : proof_mode CEphemeron.key;
-  universe_decl: Univdecls.universe_decl;
+  universe_decl: UState.universe_decl;
 }
 
 type t = pstate list
@@ -238,13 +238,6 @@ let activate_proof_mode mode =
 let disactivate_current_proof_mode () =
   CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ())
 
-let default_universe_decl =
-  let open Misctypes in
-  { univdecl_instance = [];
-    univdecl_extensible_instance = true;
-    univdecl_constraints = Univ.Constraint.empty;
-    univdecl_extensible_constraints = true }
-
 (** [start_proof sigma id pl str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
     conclusion); [str] describes what kind of theorem/definition this
@@ -253,7 +246,7 @@ let default_universe_decl =
     end of the proof to close the proof. The proof is started in the
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
-let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
+let start_proof sigma id ?(pl=UState.default_univ_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
@@ -265,7 +258,7 @@ let start_proof sigma id ?(pl=default_universe_decl) str goals terminator =
     universe_decl = pl } in
   push initial_state pstates
 
-let start_dependent_proof id ?(pl=default_universe_decl) str goals terminator =
+let start_dependent_proof id ?(pl=UState.default_univ_decl) str goals terminator =
   let initial_state = {
     pid = id;
     terminator = CEphemeron.create terminator;
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index de4cec488..0141cacb9 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -71,14 +71,14 @@ val apply_terminator : proof_terminator -> proof_ending -> unit
     evar map [sigma] (which can typically contain universe
     constraints), and with universe bindings pl. *)
 val start_proof :
-  Evd.evar_map -> Names.Id.t -> ?pl:Univdecls.universe_decl ->
+  Evd.evar_map -> Names.Id.t -> ?pl:UState.universe_decl ->
   Decl_kinds.goal_kind -> (Environ.env * EConstr.types) list  ->
     proof_terminator -> unit
 
 (** Like [start_proof] except that there may be dependencies between
     initial goals. *)
 val start_dependent_proof :
-  Names.Id.t -> ?pl:Univdecls.universe_decl -> Decl_kinds.goal_kind ->
+  Names.Id.t -> ?pl:UState.universe_decl -> Decl_kinds.goal_kind ->
   Proofview.telescope -> proof_terminator -> unit
 
 (** Update the proofs global environment after a side-effecting command
@@ -130,7 +130,7 @@ val set_used_variables :
 val get_used_variables : unit -> Context.Named.t option
 
 (** Get the universe declaration associated to the current proof. *)
-val get_universe_decl : unit -> Univdecls.universe_decl
+val get_universe_decl : unit -> UState.universe_decl
 
 module V82 : sig
   val get_current_initial_conclusions : unit -> Names.Id.t *(EConstr.types list *
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index f9e7bbfac..03ebc3275 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -263,7 +263,7 @@ let subst_mps subst c =
   EConstr.of_constr (Mod_subst.subst_mps subst (EConstr.Unsafe.to_constr c))
 
 let subst_red_expr subs =
-  Miscops.map_red_expr_gen
+  Redops.map_red_expr_gen
     (subst_mps subs)
     (Mod_subst.subst_evaluable_reference subs)
     (Patternops.subst_pattern subs)
diff --git a/vernac/classes.ml b/vernac/classes.ml
index c82208980..946a7bb32 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -77,8 +77,8 @@ let existing_instance glob g info =
                          ~hdr:"declare_instance"
                          (Pp.str "Constant does not build instances of a declared type class.")
 
-let mismatched_params env n m = mismatched_ctx_inst env Parameters n m
-let mismatched_props env n m = mismatched_ctx_inst env Properties n m
+let mismatched_params env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Parameters n m
+let mismatched_props env n m = Implicit_quantifiers.mismatched_ctx_inst_err env Properties n m
 
 (* Declare everything in the parameters as implicit, and the class instance as well *)
 
@@ -137,7 +137,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
   ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
   let ({CAst.loc;v=instid}, pl) = instid in
-  let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
+  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let tclass, ids =
     match bk with
     | Decl_kinds.Implicit ->
diff --git a/vernac/classes.mli b/vernac/classes.mli
index 631da8400..eea2a211d 100644
--- a/vernac/classes.mli
+++ b/vernac/classes.mli
@@ -32,7 +32,7 @@ val declare_instance_constant :
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(GlobRef.t -> unit) ->
   Id.t -> (** name *)
-  Univdecls.universe_decl ->
+  UState.universe_decl ->
   bool -> (* polymorphic *)
   Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 492ae1d9b..a8ac52846 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -136,7 +136,7 @@ let do_assumptions kind nl l =
   let open Context.Named.Declaration in
   let env = Global.env () in
   let udecl, l = process_assumptions_udecls kind l in
-  let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
+  let sigma, udecl = interp_univ_decl_opt env udecl in
   let l =
     if pi2 kind (* poly *) then
       (* Separate declarations so that A B : Type puts A and B in different levels. *)
diff --git a/vernac/comDefinition.ml b/vernac/comDefinition.ml
index 2d4bd6779..f55c852c0 100644
--- a/vernac/comDefinition.ml
+++ b/vernac/comDefinition.ml
@@ -65,7 +65,7 @@ let interp_definition pl bl poly red_option c ctypopt =
   let open EConstr in
   let env = Global.env() in
   (* Explicitly bound universes and constraints *)
-  let evd, decl = Univdecls.interp_univ_decl_opt env pl in
+  let evd, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   (* Build the parameters *)
   let evd, (impls, ((env_bl, ctx), imps1)) = interp_context_evars env evd bl in
   (* Build the type *)
diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli
index 6f81c4575..7f1c902c0 100644
--- a/vernac/comDefinition.mli
+++ b/vernac/comDefinition.mli
@@ -29,4 +29,4 @@ val do_definition : program_mode:bool ->
 val interp_definition :
   universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr ->
   constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map *
-                        Univdecls.universe_decl * Impargs.manual_implicits
+                        UState.universe_decl * Impargs.manual_implicits
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml
index d996443d6..ea731b34c 100644
--- a/vernac/comFixpoint.ml
+++ b/vernac/comFixpoint.ml
@@ -173,11 +173,12 @@ let interp_recursive ~program_mode ~cofix fixl notations =
         | None , acc -> acc
         | x , None -> x
         | Some ls , Some us ->
-           let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
+          let open UState in
+          let lsu = ls.univdecl_instance and usu = us.univdecl_instance in
            if not (CList.for_all2eq (fun x y -> Id.equal x.CAst.v y.CAst.v) lsu usu) then
              user_err Pp.(str "(co)-recursive definitions should all have the same universe binders");
            Some us) fixl None in
-  let sigma, decl = Univdecls.interp_univ_decl_opt env all_universes in
+  let sigma, decl = interp_univ_decl_opt env all_universes in
   let sigma, (fixctxs, fiximppairs, fixannots) =
     on_snd List.split3 @@
       List.fold_left_map (fun sigma -> interp_fix_context env sigma ~cofix) sigma fixl in
diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli
index 36c2993af..a6992a30b 100644
--- a/vernac/comFixpoint.mli
+++ b/vernac/comFixpoint.mli
@@ -49,7 +49,7 @@ val interp_recursive :
   structured_fixpoint_expr list -> decl_notation list ->
 
   (* env / signature / univs / evar_map *)
-  (Environ.env * EConstr.named_context * Univdecls.universe_decl * Evd.evar_map) *
+  (Environ.env * EConstr.named_context * UState.universe_decl * Evd.evar_map) *
   (* names / defs / types *)
   (Id.t list * Constr.constr option list * Constr.types list) *
   (* ctx per mutual def / implicits / struct annotations *)
@@ -74,19 +74,19 @@ type recursive_preentry =
 val interp_fixpoint :
   cofix:bool ->
   structured_fixpoint_expr list -> decl_notation list ->
-  recursive_preentry * Univdecls.universe_decl * UState.t *
+  recursive_preentry * UState.universe_decl * UState.t *
   (EConstr.rel_context * Impargs.manual_implicits * int option) list
 
 (** Registering fixpoints and cofixpoints in the environment *)
 (** [Not used so far] *)
 val declare_fixpoint :
   locality -> polymorphic ->
-  recursive_preentry * Univdecls.universe_decl * UState.t *
+  recursive_preentry * UState.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   Proof_global.lemma_possible_guards -> decl_notation list -> unit
 
 val declare_cofixpoint : locality -> polymorphic ->
-  recursive_preentry * Univdecls.universe_decl * UState.t *
+  recursive_preentry * UState.universe_decl * UState.t *
   (Context.Rel.t * Impargs.manual_implicits * int option) list ->
   decl_notation list -> unit
 
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 790e83dbe..101c14266 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -333,7 +333,7 @@ let interp_mutual_inductive (paramsl,indl) notations cum poly prv finite =
   List.iter check_param paramsl;
   let env0 = Global.env() in
   let pl = (List.hd indl).ind_univs in
-  let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+  let sigma, decl = interp_univ_decl_opt env0 pl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
     interp_context_evars env0 sigma paramsl
   in
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index f41e0fc44..a6d7fccf3 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -91,7 +91,7 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let lift_rel_context n l = Termops.map_rel_context_with_binders (liftn n) l in
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let sigma, decl = Univdecls.interp_univ_decl_opt env pl in
+  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
   let sigma, (_, ((env', binders_rel), impls)) = interp_context_evars env sigma bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
diff --git a/vernac/egramcoq.ml b/vernac/egramcoq.ml
index 5f63d21c4..e7a308dda 100644
--- a/vernac/egramcoq.ml
+++ b/vernac/egramcoq.ml
@@ -8,14 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-open CErrors
 open Util
-open Pcoq
+open CErrors
+open Names
+open Libnames
 open Constrexpr
-open Notation_term
 open Extend
-open Libnames
-open Names
+open Notation_gram
+open Pcoq
 
 (**********************************************************************)
 (* This determines (depending on the associativity of the current
diff --git a/vernac/egramcoq.mli b/vernac/egramcoq.mli
index e15add10f..b0341e6a1 100644
--- a/vernac/egramcoq.mli
+++ b/vernac/egramcoq.mli
@@ -15,5 +15,5 @@
 
 (** {5 Adding notations} *)
 
-val extend_constr_grammar : Notation_term.one_notation_grammar -> unit
+val extend_constr_grammar : Notation_gram.one_notation_grammar -> unit
 (** Add a term notation rule to the parsing system. *)
diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml
index f68dcae26..504e7095b 100644
--- a/vernac/explainErr.ml
+++ b/vernac/explainErr.ml
@@ -66,6 +66,8 @@ let process_vernac_interp_error exn = match fst exn with
       wrap_vernac_error exn (Himsg.explain_pretype_error ctx sigma te)
   | Typeclasses_errors.TypeClassError(env, te) ->
       wrap_vernac_error exn (Himsg.explain_typeclass_error env te)
+  | Implicit_quantifiers.MismatchedContextInstance(e,c,l,x) ->
+    wrap_vernac_error exn (Himsg.explain_mismatched_contexts e c l x)
   | InductiveError e ->
       wrap_vernac_error exn (Himsg.explain_inductive_error e)
   | Modops.ModuleTypingError e ->
diff --git a/vernac/g_vernac.ml4 b/vernac/g_vernac.ml4
index 6c7df8cfa..dd8149d0a 100644
--- a/vernac/g_vernac.ml4
+++ b/vernac/g_vernac.ml4
@@ -230,6 +230,7 @@ GEXTEND Gram
                 ext = [ "+" -> true | -> false ]; "}" -> (l',ext)
               | ext = [ "}" -> true | "|}" -> false ] -> ([], ext) ]
          ->
+         let open UState in
          { univdecl_instance = l;
            univdecl_extensible_instance = ext;
            univdecl_constraints = fst cs;
@@ -1147,8 +1148,8 @@ GEXTEND Gram
     [ [ "at"; n = level -> n ] ]
   ;
   constr_as_binder_kind:
-    [ [ "as"; IDENT "ident" -> AsIdent
-      | "as"; IDENT "pattern" -> AsIdentOrPattern
-      | "as"; IDENT "strict"; IDENT "pattern" -> AsStrictPattern ] ]
+    [ [ "as"; IDENT "ident" -> Notation_term.AsIdent
+      | "as"; IDENT "pattern" -> Notation_term.AsIdentOrPattern
+      | "as"; IDENT "strict"; IDENT "pattern" -> Notation_term.AsStrictPattern ] ]
   ;
 END
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index d4c5def6f..5d671ef52 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -1033,7 +1033,6 @@ let explain_mismatched_contexts env c i j =
 let explain_typeclass_error env = function
   | NotAClass c -> explain_not_a_class env c
   | UnboundMethod (cid, id) -> explain_unbound_method env cid id
-  | MismatchedContextInstance (c,i,j) -> explain_mismatched_contexts env c i j
 
 (* Refiner errors *)
 
diff --git a/vernac/himsg.mli b/vernac/himsg.mli
index 0e20d18c6..1d3807502 100644
--- a/vernac/himsg.mli
+++ b/vernac/himsg.mli
@@ -25,6 +25,8 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t
 
 val explain_inductive_error : inductive_error -> Pp.t
 
+val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t
+
 val explain_typeclass_error : env -> typeclass_error -> Pp.t
 
 val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 3c7ede3c9..ce74f2344 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -436,7 +436,7 @@ let start_proof_with_initialization kind sigma decl recguard thms snl hook =
 let start_proof_com ?inference_hook kind thms hook =
   let env0 = Global.env () in
   let decl = fst (List.hd thms) in
-  let evd, decl = Univdecls.interp_univ_decl_opt env0 (snd decl) in
+  let evd, decl = Constrexpr_ops.interp_univ_decl_opt env0 (snd decl) in
   let evd, thms = List.fold_left_map (fun evd ((id, _), (bl, t)) ->
     let evd, (impls, ((env, ctx), imps)) = interp_context_evars env0 evd bl in
     let evd, (t', imps') = interp_type_evars_impls ~impls env evd t in
@@ -456,7 +456,7 @@ let start_proof_com ?inference_hook kind thms hook =
      you look at the previous lines... *)
   let thms = List.map (fun (n, (t, info)) -> (n, (nf_evar evd t, info))) thms in
   let () =
-    let open Misctypes in
+    let open UState in
     if not (decl.univdecl_extensible_instance && decl.univdecl_extensible_constraints) then
        ignore (Evd.check_univ_decl ~poly:(pi2 kind) evd decl)
   in
diff --git a/vernac/lemmas.mli b/vernac/lemmas.mli
index 398f7d6d0..c9e4876ee 100644
--- a/vernac/lemmas.mli
+++ b/vernac/lemmas.mli
@@ -21,13 +21,13 @@ val call_hook :
 (** A hook start_proof calls on the type of the definition being started *)
 val set_start_hook : (EConstr.types -> unit) -> unit
 
-val start_proof : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
+val start_proof : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(Proof_global.lemma_possible_guards -> unit declaration_hook -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
    unit declaration_hook -> unit
 
-val start_proof_univs : Id.t -> ?pl:Univdecls.universe_decl -> goal_kind -> Evd.evar_map ->
+val start_proof_univs : Id.t -> ?pl:UState.universe_decl -> goal_kind -> Evd.evar_map ->
   ?terminator:(Proof_global.lemma_possible_guards -> (UState.t option -> unit declaration_hook) -> Proof_global.proof_terminator) ->
   ?sign:Environ.named_context_val -> EConstr.types ->
   ?init_tac:unit Proofview.tactic -> ?compute_guard:Proof_global.lemma_possible_guards -> 
@@ -39,7 +39,7 @@ val start_proof_com :
   unit declaration_hook -> unit
 
 val start_proof_with_initialization :
-  goal_kind -> Evd.evar_map -> Univdecls.universe_decl ->
+  goal_kind -> Evd.evar_map -> UState.universe_decl ->
   (bool * Proof_global.lemma_possible_guards * unit Proofview.tactic list option) option ->
   (Id.t (* name of thm *) *
      (EConstr.types (* type of thm *) * (Name.t list (* names to pre-introduce *) * Impargs.manual_explicitation list))) list
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index e038f54dd..2245e762f 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -15,6 +15,7 @@ open Names
 open Constrexpr
 open Constrexpr_ops
 open Notation_term
+open Notation_gram
 open Notation_ops
 open Ppextend
 open Extend
@@ -709,7 +710,7 @@ let error_parsing_incompatible_level ntn ntn' oldprec prec =
     pr_level ntn prec ++ str ".")
 
 type syntax_extension = {
-  synext_level : Notation_term.level;
+  synext_level : Notation_gram.level;
   synext_notation : notation;
   synext_notgram : notation_grammar;
   synext_unparsing : unparsing list;
@@ -728,8 +729,8 @@ let check_and_extend_constr_grammar ntn rule =
     let ntn_for_grammar = rule.notgram_notation in
     if String.equal ntn ntn_for_grammar then raise Not_found;
     let prec = rule.notgram_level in
-    let oldprec = Notation.level_of_notation ntn_for_grammar in
-    if not (Notation.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
+    let oldprec = Notgram_ops.level_of_notation ntn_for_grammar in
+    if not (Notgram_ops.level_eq prec oldprec) then error_parsing_incompatible_level ntn ntn_for_grammar oldprec prec;
   with Not_found ->
     Egramcoq.extend_constr_grammar rule
 
@@ -738,16 +739,16 @@ let cache_one_syntax_extension se =
   let prec = se.synext_level in
   let onlyprint = se.synext_notgram.notgram_onlyprinting in
   try
-    let oldprec = Notation.level_of_notation ~onlyprint ntn in
-    if not (Notation.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
+    let oldprec = Notgram_ops.level_of_notation ~onlyprint ntn in
+    if not (Notgram_ops.level_eq prec oldprec) then error_incompatible_level ntn oldprec prec;
   with Not_found ->
     if is_active_compat se.synext_compat then begin
       (* Reserve the notation level *)
-      Notation.declare_notation_level ntn prec ~onlyprint;
+      Notgram_ops.declare_notation_level ntn prec ~onlyprint;
       (* Declare the parsing rule *)
       if not onlyprint then List.iter (check_and_extend_constr_grammar ntn) se.synext_notgram.notgram_rules;
       (* Declare the notation rule *)
-      Notation.declare_notation_rule ntn
+      declare_notation_rule ntn
         ~extra:se.synext_extra (se.synext_unparsing, pi1 prec) se.synext_notgram
     end
 
@@ -1061,7 +1062,7 @@ let find_precedence lev etyps symbols onlyprint =
       [],Option.get lev
 
 let check_curly_brackets_notation_exists () =
-  try let _ = Notation.level_of_notation "{ _ }" in ()
+  try let _ = Notgram_ops.level_of_notation "{ _ }" in ()
   with Not_found ->
     user_err Pp.(str "Notations involving patterns of the form \"{ _ }\" are treated \n\
 specially and require that the notation \"{ _ }\" is already reserved.")
@@ -1274,10 +1275,10 @@ exception NoSyntaxRule
 
 let recover_notation_syntax ntn =
   try
-    let prec = Notation.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
-    let pp_rule,_ = Notation.find_notation_printing_rule ntn in
-    let pp_extra_rules = Notation.find_notation_extra_printing_rules ntn in
-    let pa_rule = Notation.find_notation_parsing_rules ntn in
+    let prec = Notgram_ops.level_of_notation ~onlyprint:true ntn (* Be as little restrictive as possible *) in
+    let pp_rule,_ = find_notation_printing_rule ntn in
+    let pp_extra_rules = find_notation_extra_printing_rules ntn in
+    let pa_rule = find_notation_parsing_rules ntn in
     { synext_level = prec;
       synext_notation = ntn;
       synext_notgram = pa_rule;
@@ -1444,7 +1445,7 @@ let add_notation_extra_printing_rule df k v =
   let notk = 
     let _,_, symbs = analyze_notation_tokens ~onlyprint:true df in
     make_notation_key symbs in
-  Notation.add_notation_extra_printing_rule notk k v
+  add_notation_extra_printing_rule notk k v
 
 (* Infix notations *)
 
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 6ef8294df..1a3b1f39b 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -308,7 +308,7 @@ type program_info_aux = {
   prg_body: constr;
   prg_type: constr;
   prg_ctx:  UState.t;
-  prg_univdecl: Univdecls.universe_decl;
+  prg_univdecl: UState.universe_decl;
   prg_obligations: obligations;
   prg_deps : Id.t list;
   prg_fixkind : fixpoint_kind option ;
@@ -1099,7 +1099,7 @@ let show_term n =
              Printer.pr_constr_env env sigma prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
             ++ Printer.pr_constr_env env sigma prg.prg_body)
 
-let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
+let add_definition n ?term t ctx ?(univdecl=UState.default_univ_decl)
                    ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
     ?(reduce=reduce) ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) obls =
   let sign = Decls.initialize_named_context_for_proof () in
@@ -1119,7 +1119,7 @@ let add_definition n ?term t ctx ?(univdecl=Univdecls.default_univ_decl)
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ctx ?(univdecl=Univdecls.default_univ_decl) ?tactic
+let add_mutual_definitions l ctx ?(univdecl=UState.default_univ_decl) ?tactic
                            ?(kind=Global,false,Definition) ?(reduce=reduce)
     ?(hook=Lemmas.mk_hook (fun _ _ _ -> ())) ?(opaque = false) notations fixkind =
   let sign = Decls.initialize_named_context_for_proof () in
diff --git a/vernac/obligations.mli b/vernac/obligations.mli
index 4b6165fb1..b1eaf51ac 100644
--- a/vernac/obligations.mli
+++ b/vernac/obligations.mli
@@ -54,7 +54,7 @@ val default_tactic : unit Proofview.tactic ref
 
 val add_definition : Names.Id.t -> ?term:constr -> types -> 
   UState.t ->
-  ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
+  ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
@@ -72,7 +72,7 @@ val add_mutual_definitions :
   (Names.Id.t * constr * types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   UState.t ->
-  ?univdecl:Univdecls.universe_decl -> (* Universe binders and constraints *)
+  ?univdecl:UState.universe_decl -> (* Universe binders and constraints *)
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(constr -> constr) ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 3655947a5..7aff758e9 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -55,7 +55,7 @@ open Pputils
            (if extensible then str"+" else mt())
 
   let pr_universe_decl l =
-    let open Misctypes in
+    let open UState in
     match l with
     | None -> mt ()
     | Some l ->
@@ -102,7 +102,7 @@ open Pputils
     | NumLevel n -> keyword "at" ++ spc () ++ keyword "level" ++ spc () ++ int n
     | NextLevel -> keyword "at" ++ spc () ++ keyword "next" ++ spc () ++ keyword "level"
 
-  let pr_constr_as_binder_kind = function
+  let pr_constr_as_binder_kind = let open Notation_term in function
     | AsIdent -> keyword "as ident"
     | AsIdentOrPattern -> keyword "as pattern"
     | AsStrictPattern -> keyword "as strict pattern"
diff --git a/vernac/record.ml b/vernac/record.ml
index 5ff118473..e6a3afe4e 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -102,7 +102,7 @@ let binders_of_decls = List.map binder_of_decl
 
 let typecheck_params_and_fields finite def id poly pl t ps nots fs =
   let env0 = Global.env () in
-  let sigma, decl = Univdecls.interp_univ_decl_opt env0 pl in
+  let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
   let _ =
     let error bk {CAst.loc; v=name} =
       match bk, name with
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 4ff9d105b..74355e1a7 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -207,7 +207,7 @@ type proof_expr =
 
 type syntax_modifier =
   | SetItemLevel of string list * Extend.production_level
-  | SetItemLevelAsBinder of string list * Extend.constr_as_binder_kind * Extend.production_level option
+  | SetItemLevelAsBinder of string list * Notation_term.constr_as_binder_kind * Extend.production_level option
   | SetLevel of int
   | SetAssoc of Extend.gram_assoc
   | SetEntryType of string * Extend.simple_constr_prod_entry_key