Merge branch 'v8.6'

9 files changed, 58 insertions, 40 deletions

diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index ad4a13c218..6512f3defa 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -48,25 +48,34 @@ let set_typeclass_transparency c local b =
     
 let _ =
   Hook.set Typeclasses.add_instance_hint_hook
-    (fun inst path local pri poly ->
+    (fun inst path local info poly ->
      let inst' = match inst with IsConstr c -> Hints.IsConstr (c, Univ.ContextSet.empty)
        | IsGlobal gr -> Hints.IsGlobRef gr
      in
-      Flags.silently (fun () ->
+     let info =
+       let open Vernacexpr in
+       { info with hint_pattern =
+		   Option.map
+		     (Constrintern.intern_constr_pattern (Global.env()))
+		     info.hint_pattern } in
+     Flags.silently (fun () ->
 	Hints.add_hints local [typeclasses_db]
 	  (Hints.HintsResolveEntry
-	     [pri, poly, false, Hints.PathHints path, inst'])) ());
+	     [info, poly, false, Hints.PathHints path, inst'])) ());
   Hook.set Typeclasses.set_typeclass_transparency_hook set_typeclass_transparency;
   Hook.set Typeclasses.classes_transparent_state_hook
     (fun () -> Hints.Hint_db.transparent_state (Hints.searchtable_map typeclasses_db))
-        
+
+open Vernacexpr
+
 (** TODO: add subinstances *)
-let existing_instance glob g pri =
+let existing_instance glob g info =
   let c = global g in
+  let info = Option.default Hints.empty_hint_info info in
   let instance = Global.type_of_global_unsafe c in
   let _, r = decompose_prod_assum instance in
     match class_of_constr r with
-      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc pri glob 
+      | Some (_, ((tc,u), _)) -> add_instance (new_instance tc info glob
   (*FIXME*) (Flags.use_polymorphic_flag ()) c)
       | None -> user_err ~loc:(loc_of_reference g)
                          ~hdr:"declare_instance"
@@ -101,12 +110,12 @@ let id_of_class cl =
 
 open Pp
 
-let instance_hook k pri global imps ?hook cst =
+let instance_hook k info global imps ?hook cst =
   Impargs.maybe_declare_manual_implicits false cst ~enriching:false imps;
-  Typeclasses.declare_instance pri (not global) cst;
+  Typeclasses.declare_instance (Some info) (not global) cst;
   (match hook with Some h -> h cst | None -> ())
 
-let declare_instance_constant k pri global imps ?hook id pl poly evm term termtype =
+let declare_instance_constant k info global imps ?hook id pl poly evm term termtype =
   let kind = IsDefinition Instance in
   let evm = 
     let levels = Univ.LSet.union (Universes.universes_of_constr termtype) 
@@ -121,7 +130,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty
   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);
+    instance_hook k info global imps ?hook (ConstRef kn);
     id
 
 let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
@@ -133,7 +142,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
   let evars = ref (Evd.from_ctx uctx) in
   let tclass, ids =
     match bk with
-    | Implicit ->
+    | Decl_kinds.Implicit ->
 	Implicit_quantifiers.implicit_application Id.Set.empty ~allow_partial:false
 	  (fun avoid (clname, _) ->
 	    match clname with
@@ -301,7 +310,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) p
 	      let hook vis gr _ =
 		let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 		  Impargs.declare_manual_implicits false gr ~enriching:false [imps];
-		  Typeclasses.declare_instance pri (not global) (ConstRef cst)
+		  Typeclasses.declare_instance (Some pri) (not global) (ConstRef cst)
 	      in
 	      let obls, constr, typ =
 		match term with 
@@ -380,7 +389,7 @@ let context poly l =
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest id decl in
 	match class_of_constr t with
 	| Some (rels, ((tc,_), args) as _cl) ->
-	    add_instance (Typeclasses.new_instance tc None false (*FIXME*)
+	    add_instance (Typeclasses.new_instance tc Hints.empty_hint_info false (*FIXME*)
 			    poly (ConstRef cst));
             status
 	    (* declare_subclasses (ConstRef cst) cl *)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 7beb873e63..d2cb788eae 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -20,12 +20,12 @@ val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
-val existing_instance : bool -> reference -> int option -> unit
-(** globality, reference, priority *)
+val existing_instance : bool -> reference -> Vernacexpr.hint_info_expr option -> unit
+(** globality, reference, optional priority and pattern information *)
 
 val declare_instance_constant :
   typeclass ->
-  int option -> (** priority *)
+  Vernacexpr.hint_info_expr -> (** priority *)
   bool -> (** globality *)
   Impargs.manual_explicitation list -> (** implicits *)
   ?hook:(Globnames.global_reference -> unit) ->
@@ -48,7 +48,7 @@ val new_instance :
   ?generalize:bool ->
   ?tac:unit Proofview.tactic  ->
   ?hook:(Globnames.global_reference -> unit) ->
-  int option ->
+  Vernacexpr.hint_info_expr ->
   Id.t
 
 (** Setting opacity *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index ef918ef8d9..a8cd52ae8a 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1131,7 +1131,7 @@ let interp_recursive isfix fixl notations =
       () in
 
   (* Instantiate evars and check all are resolved *)
-  let evd = consider_remaining_unif_problems env_rec !evdref in
+  let evd = solve_unif_constraints_with_heuristics env_rec !evdref in
   let evd, nf = nf_evars_and_universes evd in
   let fixdefs = List.map (Option.map nf) fixdefs in
   let fixtypes = List.map nf fixtypes in
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 5ae1c36ed8..d9f8ed8815 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -524,7 +524,7 @@ let parse_args arglist =
     |"-control-channel" -> Spawned.control_channel := get_host_port opt (next())
     |"-vio2vo" -> add_compile false (next ()); Flags.compilation_mode := Vio2Vo
     |"-toploop" -> set_toploop (next ())
-    |"-w" | "-W" -> CWarnings.set_flags (next ())
+    |"-w" | "-W" -> CWarnings.set_flags (CWarnings.normalize_flags_string (next ()))
     |"-o" -> Flags.compilation_output_name := Some (next())
 
     (* Options with zero arg *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c43b32762a..76de9d7adb 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -563,8 +563,9 @@ let definition_structure (kind,poly,finite,(is_coe,((loc,idstruc),pl)),ps,cfs,id
       typecheck_params_and_fields (kind = Class true) idstruc pl s ps notations fs) () in
   let sign = structure_signature (fields@params) in
   let gr = match kind with
-    | Class def ->
-	let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
+  | Class def ->
+     let priorities = List.map (fun id -> {hint_priority = id; hint_pattern = None}) priorities in
+     let gr = declare_class finite def poly ctx (loc,idstruc) idbuild
 	  implpars params arity template implfs fields is_coe coers priorities sign in
 	gr
     | _ ->
diff --git a/toplevel/record.mli b/toplevel/record.mli
index b094255634..c50e577860 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -38,7 +38,8 @@ val declare_structure :
   inductive
 
 val definition_structure :
-  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind * plident with_coercion * local_binder list *
+  inductive_kind * Decl_kinds.polymorphic * Decl_kinds.recursivity_kind *
+  plident with_coercion * local_binder list *
   (local_decl_expr with_instance with_priority with_notation) list *
   Id.t * constr_expr option -> global_reference
 
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index de41f7b190..956a402617 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -61,8 +61,8 @@ let print_usage_channel co command =
 \n  -v                     print Coq version and exit\
 \n  -list-tags             print highlight color tags known by Coq and exit\
 \n\
-\n  -quiet                 unset display of extra information (implies -w none)\
-\n  -w (all|none)          configure display of warnings\
+\n  -quiet                 unset display of extra information (implies -w \"-all\")\
+\n  -w (w1,..,wn)          configure display of warnings\
 \n  -color (yes|no|auto)   configure color output\
 \n\
 \n  -q                     skip loading of rcfile\
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 0f3a90c3e5..0e72a044c1 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -143,7 +143,7 @@ let pr_new_syntax_in_context loc chan_beautify ocom =
       | None -> mt() in
     let after = comment (CLexer.extract_comments (snd loc)) in
     if !beautify_file then
-      Pp.msg_with ~pp_tag:Ppstyle.pp_tag !Pp_control.std_ft (hov 0 (before ++ com ++ after))
+      Pp.msg_with !Pp_control.std_ft (hov 0 (before ++ com ++ after))
     else
       Feedback.msg_info (hov 4 (str"New Syntax:" ++ fnl() ++ (hov 0 com)));
     States.unfreeze fs;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index ede88399ef..cd61bf7ff3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -842,9 +842,9 @@ let vernac_instance abst locality poly sup inst props pri =
 let vernac_context poly l =
   if not (Classes.context poly l) then Feedback.feedback Feedback.AddedAxiom
 
-let vernac_declare_instances locality ids pri =
+let vernac_declare_instances locality insts =
   let glob = not (make_section_locality locality) in
-  List.iter (fun id -> Classes.existing_instance glob id pri) ids
+  List.iter (fun (id, info) -> Classes.existing_instance glob id (Some info)) insts
 
 let vernac_declare_class id =
   Record.declare_existing_class (Nametab.global id)
@@ -1083,11 +1083,10 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
     | name1 :: names1, name2 :: names2 ->
        if Name.equal name1 name2 then
          name1 :: names_union names1 names2
-       else error "Arguments lists should agree on names they provide."
+       else error "Argument lists should agree on the names they provide."
   in
 
-  let initial = List.make num_args Anonymous in
-  let names = List.fold_left names_union initial names in
+  let names = List.fold_left names_union [] names in
 
   let rec rename prev_names names =
     match prev_names, names with
@@ -1108,19 +1107,23 @@ let vernac_arguments locality reference args more_implicits nargs_for_red flags
   let names = rename prev_names names in
   let renaming_specified = Option.has_some !example_renaming in
 
-  if not (List.distinct_f Name.compare (List.filter ((!=) Anonymous) names)) then
-    error "Arguments names must be distinct.";
-
   if !rename_flag_required && not rename_flag then
     user_err ~hdr:"vernac_declare_arguments"
       (strbrk "To rename arguments the \"rename\" flag must be specified."
-    ++
+    ++ spc () ++
        match !example_renaming with
        | None -> mt ()
        | Some (o,n) ->
-          str "\nArgument " ++ pr_name o ++
+          str "Argument " ++ pr_name o ++
             str " renamed to " ++ pr_name n ++ str ".");
 
+  let duplicate_names =
+    List.duplicates Name.equal (List.filter ((!=) Anonymous) names)
+  in
+  if not (List.is_empty duplicate_names) then begin
+    let duplicates = prlist_with_sep pr_comma pr_name duplicate_names in
+    user_err (strbrk "Some argument names are duplicated: " ++ duplicates)
+  end;
 
   (* Parts of this code are overly complicated because the implicit arguments
      API is completely crazy: positions (ExplByPos) are elaborated to
@@ -1492,7 +1495,7 @@ let _ =
       optwrite = (fun b ->  Constrintern.parsing_explicit := b) }
 
 let _ =
-  declare_string_option
+  declare_string_option ~preprocess:CWarnings.normalize_flags_string
     { optsync  = true;
       optdepr  = false;
       optname  = "warnings display";
@@ -1571,7 +1574,7 @@ let get_current_context_of_args = function
 let vernac_check_may_eval redexp glopt rc =
   let (sigma, env) = get_current_context_of_args glopt in
   let sigma', c = interp_open_constr env sigma rc in
-  let sigma' = Evarconv.consider_remaining_unif_problems env sigma' in
+  let sigma' = Evarconv.solve_unif_constraints_with_heuristics env sigma' in
   Evarconv.check_problems_are_solved env sigma';
   let sigma',nf = Evarutil.nf_evars_and_universes sigma' in
   let pl, uctx = Evd.universe_context sigma' in
@@ -1907,6 +1910,10 @@ let vernac_check_guard () =
 exception End_of_input
 
 let vernac_load interp fname =
+  let interp x =
+    let proof_mode = Proof_global.get_default_proof_mode_name () in
+    Proof_global.activate_proof_mode proof_mode;
+    interp x in
   let parse_sentence = Flags.with_option Flags.we_are_parsing
     (fun po ->
     match Pcoq.Gram.entry_parse Pcoq.main_entry po with
@@ -1990,10 +1997,10 @@ let interp ?proof ~loc locality poly c =
       vernac_identity_coercion locality poly local id s t
 
   (* Type classes *)
-  | VernacInstance (abst, sup, inst, props, pri) ->
-      vernac_instance abst locality poly sup inst props pri
+  | VernacInstance (abst, sup, inst, props, info) ->
+      vernac_instance abst locality poly sup inst props info
   | VernacContext sup -> vernac_context poly sup
-  | VernacDeclareInstances (ids, pri) -> vernac_declare_instances locality ids pri
+  | VernacDeclareInstances insts -> vernac_declare_instances locality insts
   | VernacDeclareClass id -> vernac_declare_class id
 
   (* Solving *)