diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/impargs.ml | 8 | ||||
| -rw-r--r-- | interp/notation.ml | 2 | ||||
| -rw-r--r-- | interp/notation.mli | 2 |
4 files changed, 6 insertions, 8 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 28f4f5aed6..cc0c1e4602 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -678,7 +678,7 @@ let remove_one_coercion inctx c = try match match_coercion_app c with | Some (loc,r,pars,args) when not (!Flags.raw_print || !print_coercions) -> let nargs = List.length args in - (match Classops.hide_coercion r with + (match Coercionops.hide_coercion r with | Some n when (n - pars) < nargs && (inctx || (n - pars)+1 < nargs) -> (* We skip the coercion *) let l = List.skipn (n - pars) args in diff --git a/interp/impargs.ml b/interp/impargs.ml index df28b32f81..e2c732809a 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -646,11 +646,9 @@ let maybe_declare_manual_implicits local ref ?enriching l = if List.exists (fun x -> x.CAst.v <> None) l then declare_manual_implicits local ref ?enriching l -(* TODO: either turn these warnings on and document them, or handle these cases sensibly *) -let warn_set_maximal_deprecated = - CWarnings.create ~name:"set-maximal-deprecated" ~category:"deprecated" - (fun i -> strbrk ("Argument number " ^ string_of_int i ^ " is a trailing implicit so must be maximal")) +let msg_trailing_implicit id = + user_err (strbrk ("Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, so it can't be declared non maximal. Please use { } instead of [ ].")) type implicit_kind = Implicit | MaximallyImplicit | NotImplicit @@ -662,7 +660,7 @@ let compute_implicit_statuses autoimps l = | Name id :: autoimps, Implicit :: manualimps -> let imps' = aux (i+1) (autoimps, manualimps) in let max = set_maximality imps' false in - if max then warn_set_maximal_deprecated i; + if max then msg_trailing_implicit id; Some (ExplByName id, Manual, (max, true)) :: imps' | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ -> user_err ~hdr:"set_implicits" diff --git a/interp/notation.ml b/interp/notation.ml index 5dc1658824..93969f3718 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -1430,7 +1430,7 @@ let isNVar_or_NHole = function NVar _ | NHole _ -> true | _ -> false (**********************************************************************) (* Mapping classes to scopes *) -open Classops +open Coercionops type scope_class = cl_typ diff --git a/interp/notation.mli b/interp/notation.mli index 864e500d56..ea5125f7ec 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -271,7 +271,7 @@ val compute_type_scope : Evd.evar_map -> EConstr.types -> scope_name option (** Get the current scope bound to Sortclass, if it exists *) val current_type_scope_name : unit -> scope_name option -val scope_class_of_class : Classops.cl_typ -> scope_class +val scope_class_of_class : Coercionops.cl_typ -> scope_class (** Building notation key *) |