1 files changed, 65 insertions, 56 deletions

diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 2d2f1cd2..d232f086 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -75,11 +75,7 @@ let rec contract3' env sigma a b c = function
   | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities
   | UnifUnivInconsistency _ as x -> contract3 env sigma a b c, x
   | CannotSolveConstraint ((pb,env',t,u),x) ->
-      let t = EConstr.of_constr t in
-      let u = EConstr.of_constr u in
       let env',t,u = contract2 env' sigma t u in
-      let t = EConstr.Unsafe.to_constr t in
-      let u = EConstr.Unsafe.to_constr u in
       let y,x = contract3' env sigma a b c x in
       y,CannotSolveConstraint ((pb,env',t,u),x)
 
@@ -90,7 +86,7 @@ let j_nf_betaiotaevar env sigma j =
     uj_type = Reductionops.nf_betaiota env sigma j.uj_type }
 
 let jv_nf_betaiotaevar env sigma jl =
-  Array.map (fun j -> j_nf_betaiotaevar env sigma j) jl
+  Array.Smart.map (fun j -> j_nf_betaiotaevar env sigma j) jl
 
 (** Printers *)
 
@@ -198,12 +194,6 @@ let rec pr_disjunction pr = function
   | a::l -> pr a ++ str "," ++ spc () ++ pr_disjunction pr l
   | [] -> assert false
 
-let pr_puniverses f env (c,u) = 
-  f env c ++ 
-  (if Flags.is_universe_polymorphism () && not (Univ.Instance.is_empty u) then
-    str"(*" ++ Univ.Instance.pr Universes.pr_with_global_universes u ++ str"*)"
-  else mt())
-
 let explain_elim_arity env sigma ind sorts c pj okinds =
   let open EConstr in
   let env = make_all_name_different env sigma in
@@ -266,7 +256,7 @@ let explain_ill_formed_branch env sigma c ci actty expty =
   let pa, pe = pr_explicit env sigma (simp actty) (simp expty) in
   strbrk "In pattern-matching on term" ++ brk(1,1) ++ pc ++
   spc () ++ strbrk "the branch for constructor" ++ spc () ++
-  quote (pr_puniverses pr_constructor env ci) ++
+  quote (pr_pconstructor env sigma ci) ++
   spc () ++ str "has type" ++ brk(1,1) ++ pa ++ spc () ++
   str "which should be" ++ brk(1,1) ++ pe ++ str "."
 
@@ -318,12 +308,10 @@ let explain_unification_error env sigma p1 p2 = function
      | UnifUnivInconsistency p ->
         if !Constrextern.print_universes then
 	  [str "universe inconsistency: " ++
-          Univ.explain_universe_inconsistency Universes.pr_with_global_universes p]
+          Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes p]
 	else
           [str "universe inconsistency"]
      | CannotSolveConstraint ((pb,env,t,u),e) ->
-        let t = EConstr.of_constr t in
-        let u = EConstr.of_constr u in
         let env = make_all_name_different env sigma in
         (strbrk "cannot satisfy constraint " ++ pr_leconstr_env env sigma t ++
         str " == " ++ pr_leconstr_env env sigma u)
@@ -403,11 +391,10 @@ let explain_unexpected_type env sigma actual_type expected_type =
   str "where" ++ spc () ++ prexp ++ str " was expected."
 
 let explain_not_product env sigma c =
-  let c = EConstr.to_constr sigma c in
-  let pr = pr_lconstr_env env sigma c in
+  let pr = pr_econstr_env env sigma c in
   str "The type of this term is a product" ++ spc () ++
   str "while it is expected to be" ++
-  (if Constr.is_Type c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
+  (if EConstr.isType sigma c then str " a sort" else (brk(1,1) ++ pr)) ++ str "."
 
 (* TODO: use the names *)
 (* (co)fixpoints *)
@@ -526,11 +513,15 @@ let pr_trailing_ne_context_of env sigma =
   then str "."
   else (str " in environment:"++ pr_context_unlimited env sigma)
 
-let rec explain_evar_kind env sigma evk ty = function
+let rec explain_evar_kind env sigma evk ty =
+    let open Evar_kinds in
+    function
   | Evar_kinds.NamedHole id ->
       strbrk "the existential variable named " ++ Id.print id
-  | Evar_kinds.QuestionMark _ ->
+  | Evar_kinds.QuestionMark {qm_record_field=None} ->
       strbrk "this placeholder of type " ++ ty
+  | Evar_kinds.QuestionMark {qm_record_field=Some {fieldname; recordname}} ->
+          str "field " ++ (Printer.pr_constant env fieldname) ++ str " of record " ++ (Printer.pr_inductive env recordname)
   | Evar_kinds.CasesType false ->
       strbrk "the type of this pattern-matching problem"
   | Evar_kinds.CasesType true ->
@@ -559,23 +550,29 @@ let rec explain_evar_kind env sigma evk ty = function
   | Evar_kinds.VarInstance id ->
       strbrk "an instance of type " ++ ty ++
       str " for the variable " ++ Id.print id
-  | Evar_kinds.SubEvar evk' ->
+  | Evar_kinds.SubEvar (where,evk') ->
       let evi = Evd.find sigma evk' in
       let pc = match evi.evar_body with
-      | Evar_defined c -> pr_leconstr_env env sigma (EConstr.of_constr c)
+      | Evar_defined c -> pr_leconstr_env env sigma c
       | Evar_empty -> assert false in
-      let ty' = EConstr.of_constr evi.evar_concl in
+      let ty' = evi.evar_concl in
+      (match where with
+      | Some Evar_kinds.Body -> str "the body of "
+      | Some Evar_kinds.Domain -> str "the domain of "
+      | Some Evar_kinds.Codomain -> str "the codomain of "
+      | None ->
       pr_existential_key sigma evk ++ str " of type " ++ ty ++
       str " in the partial instance " ++ pc ++
-      str " found for " ++ explain_evar_kind env sigma evk'
+      str " found for ") ++
+      explain_evar_kind env sigma evk'
       (pr_leconstr_env env sigma ty') (snd evi.evar_source)
 
 let explain_typeclass_resolution env sigma evi k =
-  match Typeclasses.class_of_constr sigma (EConstr.of_constr evi.evar_concl) with
+  match Typeclasses.class_of_constr sigma evi.evar_concl with
   | Some _ ->
     let env = Evd.evar_filtered_env evi in
       fnl () ++ str "Could not find an instance for " ++
-      pr_lconstr_env env sigma evi.evar_concl ++
+      pr_leconstr_env env sigma evi.evar_concl ++
       pr_trailing_ne_context_of env sigma
   | _ -> mt()
 
@@ -584,14 +581,14 @@ let explain_placeholder_kind env sigma c e =
   | Some (SeveralInstancesFound n) ->
       strbrk " (several distinct possible type class instances found)"
   | None ->
-      match Typeclasses.class_of_constr sigma (EConstr.of_constr c) with
+      match Typeclasses.class_of_constr sigma c with
       | Some _ -> strbrk " (no type class instance found)"
       | _ -> mt ()
 
 let explain_unsolvable_implicit env sigma evk explain =
   let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in
   let env = Evd.evar_filtered_env evi in
-  let type_of_hole = pr_lconstr_env env sigma evi.evar_concl in
+  let type_of_hole = pr_leconstr_env env sigma evi.evar_concl in
   let pe = pr_trailing_ne_context_of env sigma in
   strbrk "Cannot infer " ++
   explain_evar_kind env sigma evk type_of_hole (snd evi.evar_source) ++
@@ -634,8 +631,7 @@ let explain_refiner_cannot_generalize env sigma ty =
   pr_leconstr_env env sigma ty ++ str "."
 
 let explain_no_occurrence_found env sigma c id =
-  let c = EConstr.to_constr sigma c in
-  str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++
+  str "Found no subterm matching " ++ pr_leconstr_env env sigma c ++
   str " in " ++
     (match id with
       | Some id -> Id.print id
@@ -682,6 +678,11 @@ let explain_unsatisfied_constraints env sigma cst =
     Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++ 
     spc () ++ str "(maybe a bugged tactic)."
 
+let explain_undeclared_universe env sigma l =
+  strbrk "Undeclared universe: " ++
+    Termops.pr_evd_level sigma l ++
+    spc () ++ str "(maybe a bugged tactic)."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -719,6 +720,8 @@ let explain_type_error env sigma err =
       explain_wrong_case_info env ind ci
   | UnsatisfiedConstraints cst ->
       explain_unsatisfied_constraints env sigma cst
+  | UndeclaredUniverse l ->
+     explain_undeclared_universe env sigma l
 
 let pr_position (cl,pos) =
   let clpos = match cl with
@@ -760,7 +763,7 @@ let pr_constraints printenv env sigma evars cstrs =
       let evs =
         prlist
         (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++
-            str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l
+            str " : " ++ pr_leconstr_env env' sigma evi.evar_concl ++ fnl ()) l
       in
       h 0 (pe ++ evs ++ pr_evar_constraints sigma cstrs)
     else
@@ -849,9 +852,9 @@ let explain_not_match_error = function
     str "the body of definitions differs"
   | NotConvertibleTypeField (env, typ1, typ2) ->
     str "expected type" ++ spc ()  ++
-    quote (Printer.safe_pr_lconstr_env env Evd.empty typ2) ++ spc () ++
+    quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) typ2) ++ spc () ++
     str "but found type" ++ spc () ++
-    quote (Printer.safe_pr_lconstr_env env Evd.empty typ1)
+    quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) typ1)
   | NotSameConstructorNamesField ->
     str "constructor names differ"
   | NotSameInductiveNameInBlockField ->
@@ -884,12 +887,12 @@ let explain_not_match_error = function
     str"polymorphic universe instances do not match"
   | IncompatibleUniverses incon ->
     str"the universe constraints are inconsistent: " ++
-      Univ.explain_universe_inconsistency Universes.pr_with_global_universes incon
+      Univ.explain_universe_inconsistency UnivNames.pr_with_global_universes incon
   | IncompatiblePolymorphism (env, t1, t2) ->
     str "conversion of polymorphic values generates additional constraints: " ++
-      quote (Printer.safe_pr_lconstr_env env Evd.empty t1) ++ spc () ++
+      quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t1) ++ spc () ++
       str "compared to " ++ spc () ++
-      quote (Printer.safe_pr_lconstr_env env Evd.empty t2)
+      quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2)
   | IncompatibleConstraints cst ->
     str " the expected (polymorphic) constraints do not imply " ++
       let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in
@@ -1009,8 +1012,9 @@ let explain_module_internalization_error = function
 (* Typeclass errors *)
 
 let explain_not_a_class env c =
-  let c = EConstr.to_constr Evd.empty c in
-  pr_constr_env env Evd.empty c ++ str" is not a declared type class."
+  let sigma = Evd.from_env env in
+  let c = EConstr.to_constr sigma c in
+  pr_constr_env env sigma c ++ str" is not a declared type class."
 
 let explain_unbound_method env cid { CAst.v = id } =
   str "Unbound method name " ++ Id.print (id) ++ spc () ++
@@ -1023,14 +1027,13 @@ let pr_constr_exprs exprs =
 
 let explain_mismatched_contexts env c i j =
   str"Mismatched contexts while declaring instance: " ++ brk (1,1) ++
-    hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env Evd.empty j) ++
+    hov 1 (str"Expected:" ++ brk (1, 1) ++ pr_rel_context env (Evd.from_env env) j) ++
     fnl () ++ brk (1,1) ++
     hov 1 (str"Found:" ++ brk (1, 1) ++ pr_constr_exprs i)
 
 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 *)
 
@@ -1085,19 +1088,19 @@ let explain_refiner_error env sigma = function
 (* Inductive errors *)
 
 let error_non_strictly_positive env c v =
-  let pc = pr_lconstr_env env Evd.empty c in
-  let pv = pr_lconstr_env env Evd.empty v in
+  let pc = pr_lconstr_env env (Evd.from_env env) c in
+  let pv = pr_lconstr_env env (Evd.from_env env) v in
   str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
   brk(1,1) ++ pc ++ str "."
 
 let error_ill_formed_inductive env c v =
-  let pc = pr_lconstr_env env Evd.empty c in
-  let pv = pr_lconstr_env env Evd.empty v in
+  let pc = pr_lconstr_env env (Evd.from_env env) c in
+  let pv = pr_lconstr_env env (Evd.from_env env) v in
   str "Not enough arguments applied to the " ++ pv ++
   str " in" ++ brk(1,1) ++ pc ++ str "."
 
 let error_ill_formed_constructor env id c v nparams nargs =
-  let pv = pr_lconstr_env env Evd.empty v in
+  let pv = pr_lconstr_env env (Evd.from_env env) v in
   let atomic = Int.equal (nb_prod Evd.empty (EConstr.of_constr c)) (** FIXME *) 0 in
   str "The type of constructor" ++ brk(1,1) ++ Id.print id ++ brk(1,1) ++
   str "is not valid;" ++ brk(1,1) ++
@@ -1117,12 +1120,12 @@ let error_ill_formed_constructor env id c v nparams nargs =
 
 let pr_ltype_using_barendregt_convention_env env c =
   (* Use goal_concl_style as an approximation of Barendregt's convention (?) *)
-  quote (pr_goal_concl_style_env env Evd.empty (EConstr.of_constr c))
+  quote (pr_goal_concl_style_env env (Evd.from_env env) (EConstr.of_constr c))
 
 let error_bad_ind_parameters env c n v1 v2  =
   let pc = pr_ltype_using_barendregt_convention_env env c in
-  let pv1 = pr_lconstr_env env Evd.empty v1 in
-  let pv2 = pr_lconstr_env env Evd.empty v2 in
+  let pv1 = pr_lconstr_env env (Evd.from_env env) v1 in
+  let pv2 = pr_lconstr_env env (Evd.from_env env) v2 in
   str "Last occurrence of " ++ pv2 ++ str " must have " ++ pv1 ++
   str " as " ++ pr_nth n ++ str " argument in" ++ brk(1,1) ++ pc ++ str "."
 
@@ -1140,7 +1143,7 @@ let error_same_names_overlap idl =
   prlist_with_sep pr_comma Id.print idl ++ str "."
 
 let error_not_an_arity env c =
-  str "The type" ++ spc () ++ pr_lconstr_env env Evd.empty c ++ spc () ++
+  str "The type" ++ spc () ++ pr_lconstr_env env (Evd.from_env env) c ++ spc () ++
   str "is not an arity."
 
 let error_bad_entry () =
@@ -1230,12 +1233,7 @@ let explain_wrong_numarg_inductive env ind n =
   str " expects " ++ decline_string n "argument" ++ str "."
 
 let explain_unused_clause env pats =
-(* Without localisation
-  let s = if List.length pats > 1 then "s" else "" in
-  (str ("Unused clause with pattern"^s) ++ spc () ++
-    hov 0 (pr_sequence pr_cases_pattern pats) ++ str ")")
-*)
-  str "This clause is redundant."
+  str "Pattern \"" ++ hov 0 (prlist_with_sep pr_comma pr_cases_pattern pats) ++ strbrk "\" is redundant in this clause."
 
 let explain_non_exhaustive env pats =
   str "Non exhaustive pattern-matching: no clause found for " ++
@@ -1307,6 +1305,7 @@ let map_ptype_error f = function
 | IllTypedRecBody (n, na, jv, t) ->
   IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
 | UnsatisfiedConstraints g -> UnsatisfiedConstraints g
+| UndeclaredUniverse l -> UndeclaredUniverse l
 
 let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->
@@ -1314,4 +1313,14 @@ let explain_reduction_tactic_error = function
       str "The abstracted term" ++ spc () ++
       quote (pr_goal_concl_style_env env sigma c) ++
       spc () ++ str "is not well typed." ++ fnl () ++
-      explain_type_error env' Evd.empty e
+      explain_type_error env' (Evd.from_env env') e
+
+let explain_numeral_notation_error env sigma = function
+  | Notation.UnexpectedTerm c ->
+    (strbrk "Unexpected term " ++
+     pr_constr_env env sigma c ++
+     strbrk " while parsing a numeral notation.")
+  | Notation.UnexpectedNonOptionTerm c ->
+    (strbrk "Unexpected non-option term " ++
+     pr_constr_env env sigma c ++
+     strbrk " while parsing a numeral notation.")