Fix conflicts with latest master.

4 files changed, 19 insertions, 12 deletions

diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index cc9b840bed..4242f06844 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -475,7 +475,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let indnames = List.map (fun ind -> ind.ind_name) indl in
 
   (* In case of template polymorphism, we need to compute more constraints *)
-  let env0 = if poly then env0 else Environ.set_universes_lbound env0 Univ.Level.prop in
+  let env0 = if poly then env0 else Environ.set_universes_lbound env0 UGraph.Bound.Prop in
 
   let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl) =
     interp_params env0 udecl uparamsl paramsl
diff --git a/vernac/library.ml b/vernac/library.ml
index 85db501e84..c30331b221 100644
--- a/vernac/library.ml
+++ b/vernac/library.ml
@@ -89,6 +89,7 @@ type library_disk = {
 type summary_disk = {
   md_name : compilation_unit_name;
   md_deps : (compilation_unit_name * Safe_typing.vodigest) array;
+  md_ocaml : string;
 }
 
 (*s Modules loaded in memory contain the following informations. They are
@@ -251,6 +252,7 @@ let intern_from_file f =
   let (univs : seg_univ option), digest_u = ObjFile.marshal_in_segment ch ~segment:"universes" in
   let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch ~segment:"opaques" in
   ObjFile.close_in ch;
+  System.check_caml_version ~caml:lsd.md_ocaml ~file:f;
   register_library_filename lsd.md_name f;
   add_opaque_table lsd.md_name (ToFetch del_opaque);
   let open Safe_typing in
@@ -401,6 +403,7 @@ let load_library_todo f =
   let tasks, _ = ObjFile.marshal_in_segment ch ~segment:"tasks" in
   let (s4 : seg_proofs), _ = ObjFile.marshal_in_segment ch ~segment:"opaques" in
   ObjFile.close_in ch;
+  System.check_caml_version ~caml:s0.md_ocaml ~file:f;
   if tasks = None then user_err ~hdr:"restart" (str"not a .vio file");
   if s2 = None then user_err ~hdr:"restart" (str"not a .vio file");
   if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file");
@@ -486,6 +489,7 @@ let save_library_to todo_proofs ~output_native_objects dir f otab =
     let sd = {
     md_name = dir;
     md_deps = Array.of_list (current_deps ());
+    md_ocaml = Coq_config.caml_version;
   } in
   let md = {
     md_compiled = cenv;
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml
index 3b9c771b93..32affd562f 100644
--- a/vernac/metasyntax.ml
+++ b/vernac/metasyntax.ml
@@ -1073,12 +1073,12 @@ let make_internalization_vars recvars mainvars typs =
   let extratyps = List.map (fun (x,y) -> (y,List.assoc x maintyps)) recvars in
   maintyps @ extratyps
 
-let make_interpretation_type isrec isonlybinding = function
+let make_interpretation_type isrec isonlybinding default_if_binding = function
   (* Parsed as constr list *)
   | ETConstr (_,None,_) when isrec -> NtnTypeConstrList
-  (* Parsed as constr, but interpreted as a binder: default is to parse it as an ident only *)
+  (* Parsed as constr, but interpreted as a binder *)
   | ETConstr (_,Some bk,_) -> NtnTypeBinder (NtnBinderParsedAsConstr bk)
-  | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr AsIdent)
+  | ETConstr (_,None,_) when isonlybinding -> NtnTypeBinder (NtnBinderParsedAsConstr default_if_binding)
   (* Parsed as constr, interpreted as constr *)
   | ETConstr (_,None,_) -> NtnTypeConstr
   (* Others *)
@@ -1096,7 +1096,9 @@ let subentry_of_constr_prod_entry = function
   | ETConstr (InConstrEntry,_,_) -> InConstrEntrySomeLevel
   | _ -> InConstrEntrySomeLevel
 
-let make_interpretation_vars recvars allvars typs =
+let make_interpretation_vars
+  (* For binders, default is to parse only as an ident *) ?(default_if_binding=AsIdent)
+   recvars allvars typs =
   let eq_subscope (sc1, l1) (sc2, l2) =
     Option.equal String.equal sc1 sc2 &&
     List.equal String.equal l1 l2
@@ -1113,7 +1115,7 @@ let make_interpretation_vars recvars allvars typs =
   Id.Map.mapi (fun x (isonlybinding, sc) ->
     let typ = Id.List.assoc x typs in
     ((subentry_of_constr_prod_entry typ,sc),
-     make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding typ)) mainvars
+     make_interpretation_type (Id.List.mem_assoc x recvars) isonlybinding default_if_binding typ)) mainvars
 
 let check_rule_productivity l =
   if List.for_all (function NonTerminal _ | Break _ -> true | _ -> false) l then
@@ -1792,8 +1794,8 @@ let try_interp_name_alias = function
   | _ -> raise Not_found
 
 let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing } =
-  let vars,reversibility,pat =
-    try [], APrioriReversible, NRef (try_interp_name_alias (vars,c))
+  let acvars,pat,reversibility =
+    try Id.Map.empty, NRef (try_interp_name_alias (vars,c)), APrioriReversible
     with Not_found ->
       let fold accu id = Id.Map.add id NtnInternTypeAny accu in
       let i_vars = List.fold_left fold Id.Map.empty vars in
@@ -1801,10 +1803,11 @@ let add_syntactic_definition ~local deprecation env ident (vars,c) { onlyparsing
         ninterp_var_type = i_vars;
         ninterp_rec_vars = Id.Map.empty;
       } in
-      let nvars, pat, reversibility = interp_notation_constr env nenv c in
-      let map id = let (_,sc) = Id.Map.find id nvars in (id, sc) in
-      List.map map vars, reversibility, pat
+      interp_notation_constr env nenv c
   in
+  let in_pat id = (id,ETConstr (Constrexpr.InConstrEntry,None,(NextLevel,0))) in
+  let interp = make_interpretation_vars ~default_if_binding:AsIdentOrPattern [] acvars (List.map in_pat vars) in
+  let vars = List.map (fun x -> (x, Id.Map.find x interp)) vars in
   let onlyparsing = onlyparsing || fst (printability None false reversibility pat) in
   Syntax_def.declare_syntactic_definition ~local deprecation ident ~onlyparsing (vars,pat)
 
diff --git a/vernac/record.ml b/vernac/record.ml
index 9fda98d08e..36254780cd 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -121,7 +121,7 @@ let typecheck_params_and_fields def poly pl ps records =
      any Set <= i constraint for universes that might actually be instantiated with Prop. *)
   let is_template =
     List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
-  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
+  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 UGraph.Bound.Prop else env0 in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
   let () =
     let error bk {CAst.loc; v=name} =