Merge branch 'v8.5'

8 files changed, 72 insertions, 38 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 936343628..6bb047af0 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -102,19 +102,21 @@ let instance_hook k pri global imps ?hook cst =
   Typeclasses.declare_instance pri (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k pri global imps ?hook id poly uctx term termtype =
+let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype =
   let kind = IsDefinition Instance in
-  let uctx = 
+  let evm = 
     let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
 				 (Universes.universes_of_constr term) in
-      Universes.restrict_universe_context uctx levels 
+    Evd.restrict_universe_context evm levels 
   in
+  let pl, uctx = Evd.universe_context ?names:pl evm in
   let entry = 
-    Declare.definition_entry ~types:termtype ~poly ~univs:(Univ.ContextSet.to_context uctx) term
+    Declare.definition_entry ~types:termtype ~poly ~univs:uctx term
   in
   let cdecl = (DefinitionEntry entry, kind) in
   let kn = Declare.declare_constant id cdecl in
     Declare.definition_message id;
+    Universes.register_universe_binders (ConstRef kn) pl;
     instance_hook k pri global imps ?hook (ConstRef kn);
     id
 
@@ -122,7 +124,9 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
     ?(generalize=true)
     ?(tac:unit Proofview.tactic option) ?hook pri =
   let env = Global.env() in
-  let evars = ref (Evd.from_env env) in
+  let ((loc, instid), pl) = instid in
+  let uctx = Evd.make_evar_universe_context env pl in
+  let evars = ref (Evd.from_ctx uctx) in
   let tclass, ids =
     match bk with
     | Implicit ->
@@ -159,7 +163,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       cl, u, c', ctx', ctx, len, imps, args
   in
   let id =
-    match snd instid with
+    match instid with
 	Name id ->
 	  let sp = Lib.make_path id in
 	    if Nametab.exists_cci sp then
@@ -186,11 +190,13 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
 	    nf t
 	in
 	Evarutil.check_evars env Evd.empty !evars termtype;
-	let pl, ctx = Evd.universe_context !evars in
+	let pl, ctx = Evd.universe_context ?names:pl !evars in
 	let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id
 	  (ParameterEntry 
             (None,poly,(termtype,ctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical)
-	in instance_hook k None global imps ?hook (ConstRef cst); id
+	in
+	  Universes.register_universe_binders (ConstRef cst) pl;
+	  instance_hook k None global imps ?hook (ConstRef cst); id
       end
     else (
       let props =
@@ -283,9 +289,8 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
       in
       let term = Option.map nf term in
 	if not (Evd.has_undefined evm) && not (Option.is_empty term) then
-          let ctx = Evd.universe_context_set evm in
-	  declare_instance_constant k pri global imps ?hook id 
-            poly ctx (Option.get term) termtype
+	  declare_instance_constant k pri global imps ?hook id pl
+            poly evm (Option.get term) termtype
 	else if !refine_instance || Option.is_empty term then begin
 	  let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
 	    if Flags.is_program_mode () then
@@ -305,7 +310,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
               let hook = Lemmas.mk_hook hook in
 	      let ctx = Evd.evar_universe_context evm in
 		ignore (Obligations.add_definition id ?term:constr
-			typ ctx ~kind:(Global,poly,Instance) ~hook obls);
+ 			?pl typ ctx ~kind:(Global,poly,Instance) ~hook obls);
 		id
 	    else
 	      (Flags.silently 
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 8dcfabae4..a3e948d96 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -30,8 +30,9 @@ val declare_instance_constant :
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
   Id.t -> (** name *)
+  Id.t Loc.located list option ->
   bool -> (* polymorphic *)
-  Univ.universe_context_set -> (* Universes *)
+  Evd.evar_map -> (* Universes *)
   Constr.t -> (** body *)
   Term.types -> (** type *)
   Names.Id.t
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 4adb66bc9..18b2b1444 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -176,7 +176,9 @@ let _ = Obligations.declare_definition_ref :=
        (fun i k c imps hook -> declare_definition i k c [] imps hook)
 
 let do_definition ident k pl bl red_option c ctypopt hook =
-  let (ce, evd, pl, imps as def) = interp_definition pl bl (pi2 k) red_option c ctypopt in
+  let (ce, evd, pl', imps as def) =
+    interp_definition pl bl (pi2 k) red_option c ctypopt
+  in
     if Flags.is_program_mode () then
       let env = Global.env () in
       let (c,ctx), sideff = Future.force ce.const_entry_body in
@@ -193,9 +195,9 @@ let do_definition ident k pl bl red_option c ctypopt hook =
       let ctx = Evd.evar_universe_context evd in
       let hook = Lemmas.mk_hook (fun l r _ -> Lemmas.call_hook (fun exn -> exn) hook l r) in
 	ignore(Obligations.add_definition
-          ident ~term:c cty ctx ~implicits:imps ~kind:k ~hook obls)
+          ident ~term:c cty ctx ?pl ~implicits:imps ~kind:k ~hook obls)
     else let ce = check_definition def in
-      ignore(declare_definition ident k ce pl imps
+      ignore(declare_definition ident k ce pl' imps
         (Lemmas.mk_hook
           (fun l r -> Lemmas.call_hook (fun exn -> exn) hook l r;r)))
 
@@ -904,10 +906,11 @@ let nf_evar_context sigma ctx =
   List.map (fun (n, b, t) ->
     (n, Option.map (Evarutil.nf_evar sigma) b, Evarutil.nf_evar sigma t)) ctx
 
-let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
+let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   Coqlib.check_required_library ["Coq";"Program";"Wf"];
   let env = Global.env() in
-  let evdref = ref (Evd.from_env env) in
+  let ctx = Evd.make_evar_universe_context env pl in
+  let evdref = ref (Evd.from_ctx ctx) in
   let _, ((env', binders_rel), impls) = interp_context_evars env evdref bl in
   let len = List.length binders_rel in
   let top_env = push_rel_context binders_rel env in
@@ -1013,9 +1016,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
       let hook l gr _ = 
 	let body = it_mkLambda_or_LetIn (mkApp (Universes.constr_of_global gr, [|make|])) binders_rel in
 	let ty = it_mkProd_or_LetIn top_arity binders_rel in
-	let pl, univs = Evd.universe_context !evdref in
+	let pl, univs = Evd.universe_context ?names:pl !evdref in
 	  (*FIXME poly? *)
-	let ce = definition_entry ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
+	let ce = definition_entry ~poly ~types:ty ~univs (Evarutil.nf_evar !evdref body) in
 	(** FIXME: include locality *)
 	let c = Declare.declare_constant recname (DefinitionEntry ce, IsDefinition Definition) in
 	let gr = ConstRef c in
@@ -1039,7 +1042,7 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation =
     Obligations.eterm_obligations env recname !evdref 0 fullcoqc fullctyp 
   in
   let ctx = Evd.evar_universe_context !evdref in
-    ignore(Obligations.add_definition recname ~term:evars_def 
+    ignore(Obligations.add_definition recname ~term:evars_def ?pl
 	     evars_typ ctx evars ~hook)
 
 let interp_recursive isfix fixl notations =
@@ -1260,22 +1263,22 @@ let do_program_recursive local p fixkind fixl ntns =
   | Obligations.IsFixpoint _ -> (local, p, Fixpoint)
   | Obligations.IsCoFixpoint -> (local, p, CoFixpoint)
   in
-  Obligations.add_mutual_definitions defs ~kind ctx ntns fixkind
+  Obligations.add_mutual_definitions defs ~kind ?pl ctx ntns fixkind
 
 let do_program_fixpoint local poly l =
   let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in
     match g, l with
-    | [(n, CWfRec r)], [((((_,id),_),_,bl,typ,def),ntn)] ->
+    | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] ->
 	let recarg = 
 	  match n with
 	  | Some n -> mkIdentC (snd n)
 	  | None ->
 	      errorlabstrm "do_program_fixpoint"
 		(str "Recursive argument required for well-founded fixpoints")
-	in build_wellfounded (id, n, bl, typ, out_def def) r recarg ntn
+	in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn
 	     
-    | [(n, CMeasureRec (m, r))], [((((_,id),_),_,bl,typ,def),ntn)] ->
-	build_wellfounded (id, n, bl, typ, out_def def)
+    | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] ->
+	build_wellfounded (id, pl, n, bl, typ, out_def def) poly
 	  (Option.default (CRef (lt_ref,None)) r) m ntn
 	  
     | _, _ when List.for_all (fun (n, ro) -> ro == CStructRec) g ->
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 8f56cddfa..f46b90111 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -35,7 +35,7 @@ let print_header () =
   ppnl (str "Welcome to Coq " ++ str ver ++ str " (" ++ str rev ++ str ")");
   pp_flush ()
 
-let warning s = msg_warning (strbrk s)
+let warning s = with_option Flags.warn msg_warning (strbrk s)
 
 let toploop = ref None
 
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 819c290af..4a5f14917 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -890,7 +890,17 @@ let explain_is_a_functor () =
   str "Illegal use of a functor."
 
 let explain_incompatible_module_types mexpr1 mexpr2 =
-  str "Incompatible module types."
+  let open Declarations in
+  let rec get_arg = function
+  | NoFunctor _ -> 0
+  | MoreFunctor (_, _, ty) -> succ (get_arg ty)
+  in
+  let len1 = get_arg mexpr1.mod_type in
+  let len2 = get_arg mexpr2.mod_type in
+  if len1 <> len2 then
+    str "Incompatible module types: module expects " ++ int len2 ++
+      str " arguments, found " ++ int len1 ++ str "."
+  else str "Incompatible module types."
 
 let explain_not_equal_module_paths mp1 mp2 =
   str "Non equal modules."
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 6534c39a7..5a47fc0ea 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -537,10 +537,15 @@ let add_break_if_none n = function
   | l -> UnpCut (PpBrk(n,0)) :: l
 
 let check_open_binder isopen sl m =
+  let pr_token = function
+  | Terminal s -> str s
+  | Break n -> str "␣"
+  | _ -> assert false
+  in
   if isopen && not (List.is_empty sl) then
     errorlabstrm "" (str "as " ++ pr_id m ++
       str " is a non-closed binder, no such \"" ++
-      prlist_with_sep spc (function Terminal s -> str s | _ -> assert false) sl
+      prlist_with_sep spc pr_token sl
       ++ strbrk "\" is allowed to occur.")
 
 (* Heuristics for building default printing rules *)
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index fd91cfb5c..0ea9f959f 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -299,6 +299,7 @@ type program_info_aux = {
   prg_body: constr;
   prg_type: constr;
   prg_ctx:  Evd.evar_universe_context;
+  prg_pl: Id.t Loc.located list option;
   prg_obligations: obligations;
   prg_deps : Id.t list;
   prg_fixkind : fixpoint_kind option ;
@@ -498,15 +499,21 @@ let declare_definition prg =
     (Evd.evar_universe_context_subst prg.prg_ctx) in
   let opaque = prg.prg_opaque in
   let fix_exn = Stm.get_fix_exn () in
+  let pl, ctx =
+    Evd.universe_context ?names:prg.prg_pl (Evd.from_ctx prg.prg_ctx) in
   let ce =
     definition_entry ~fix_exn
      ~opaque ~types:(nf typ) ~poly:(pi2 prg.prg_kind)
      ~univs:(Evd.evar_context_universe_context prg.prg_ctx) (nf body)
   in
-    progmap_remove prg;
+  let () = progmap_remove prg in
+  let cst =
     !declare_definition_ref prg.prg_name 
-      prg.prg_kind ce prg.prg_implicits
-      (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
+     prg.prg_kind ce prg.prg_implicits
+     (Lemmas.mk_hook (fun l r -> Lemmas.call_hook fix_exn prg.prg_hook l r prg.prg_ctx; r))
+  in
+  Universes.register_universe_binders cst pl;
+  cst
       
 open Pp
 
@@ -634,7 +641,8 @@ let declare_obligation prg obl body ty uctx =
 	    else
 	      Some (TermObl (it_mkLambda_or_LetIn (mkApp (mkConst constant, args)) ctx)) }
 
-let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls impls kind reduce hook =
+let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
+		   notations obls impls kind reduce hook =
   let obls', b = 
     match b with
     | None ->
@@ -654,7 +662,7 @@ let init_prog_info ?(opaque = false) sign n b t ctx deps fixkind notations obls
 	  obls, b
   in
     { prg_name = n ; prg_body = b; prg_type = reduce t; 
-      prg_ctx = ctx; 
+      prg_ctx = ctx; prg_pl = pl;
       prg_obligations = (obls', Array.length obls');
       prg_deps = deps; prg_fixkind = fixkind ; prg_notations = notations ;
       prg_implicits = impls; prg_kind = kind; prg_reduce = reduce; 
@@ -1016,11 +1024,11 @@ let show_term n =
 	     Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_type ++ spc () ++ str ":=" ++ fnl ()
 	    ++ Printer.pr_constr_env (Global.env ()) Evd.empty prg.prg_body)
 
-let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition) ?tactic
+let add_definition n ?term t ctx ?pl ?(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
   let info = Id.print n ++ str " has type-checked" in
-  let prg = init_prog_info sign ~opaque n term t ctx [] None [] obls implicits kind reduce hook in
+  let prg = init_prog_info sign ~opaque n pl term t ctx [] None [] obls implicits kind reduce hook in
   let obls,_ = prg.prg_obligations in
   if Int.equal (Array.length obls) 0 then (
     Flags.if_verbose msg_info (info ++ str ".");
@@ -1035,13 +1043,13 @@ let add_definition n ?term t ctx ?(implicits=[]) ?(kind=Global,false,Definition)
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
 	| _ -> res)
 
-let add_mutual_definitions l ctx ?tactic ?(kind=Global,false,Definition) ?(reduce=reduce)
+let add_mutual_definitions l ctx ?pl ?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
   let deps = List.map (fun (n, b, t, imps, obls) -> n) l in
     List.iter
     (fun  (n, b, t, imps, obls) ->
-     let prg = init_prog_info sign ~opaque n (Some b) t ctx deps (Some fixkind)
+     let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
      in progmap_add n (Ephemeron.create prg)) l;
     let _defined =
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index b2320a578..e257da016 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -64,6 +64,7 @@ val get_proofs_transparency : unit -> bool
 
 val add_definition : Names.Id.t -> ?term:Term.constr -> Term.types -> 
   Evd.evar_universe_context ->
+  ?pl:(Id.t Loc.located list) -> (* Universe binders *)
   ?implicits:(Constrexpr.explicitation * (bool * bool * bool)) list ->
   ?kind:Decl_kinds.definition_kind ->
   ?tactic:unit Proofview.tactic ->
@@ -81,6 +82,7 @@ val add_mutual_definitions :
   (Names.Id.t * Term.constr * Term.types *
       (Constrexpr.explicitation * (bool * bool * bool)) list * obligation_info) list ->
   Evd.evar_universe_context ->
+  ?pl:(Id.t Loc.located list) -> (* Universe binders *)
   ?tactic:unit Proofview.tactic ->
   ?kind:Decl_kinds.definition_kind ->
   ?reduce:(Term.constr -> Term.constr) ->