aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/constrintern.ml27
-rw-r--r--interp/impargs.ml61
-rw-r--r--interp/impargs.mli5
-rw-r--r--interp/implicit_quantifiers.ml10
-rw-r--r--parsing/g_constr.mlg22
-rw-r--r--plugins/ssr/ssrvernac.mlg2
-rw-r--r--pretyping/glob_ops.ml5
-rw-r--r--pretyping/glob_term.ml2
-rw-r--r--printing/ppconstr.ml9
-rw-r--r--test-suite/success/Generalization.v6
-rw-r--r--test-suite/success/ImplicitArguments.v12
-rw-r--r--test-suite/success/implicit.v7
-rw-r--r--vernac/classes.ml2
-rw-r--r--vernac/comArguments.ml2
-rw-r--r--vernac/comArguments.mli2
-rw-r--r--vernac/comAssumption.ml2
-rw-r--r--vernac/g_vernac.mlg15
-rw-r--r--vernac/ppvernac.ml8
-rw-r--r--vernac/prettyp.ml12
-rw-r--r--vernac/vernacexpr.ml4
20 files changed, 137 insertions, 78 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f4ae5bf676..ab20f1b3ef 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -330,15 +330,18 @@ let exists_name na l =
| _ -> false
let build_impls ?loc n bk na acc =
- match bk with
- | Implicit ->
+ let impl_status max =
let na =
- if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
- else na in
+ if exists_name na acc then begin warn_shadowed_implicit_name ?loc na; Anonymous end
+ else na in
let impl = match na with
- | Name id -> Some (ExplByName id,Manual,(true,true))
- | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
- impl :: acc
+ | Name id -> Some (ExplByName id,Manual,(true,true))
+ | Anonymous -> Some (ExplByPos (n,None),Manual,(true,true)) in
+ impl
+ in
+ match bk with
+ | NonMaxImplicit -> impl_status false :: acc
+ | MaxImplicit -> impl_status true :: acc
| Explicit -> None :: acc
let impls_binder_list =
@@ -426,7 +429,7 @@ let warn_unexpected_implicit_binder_declaration =
Pp.(fun () -> str "Unexpected implicit binder declaration.")
let check_implicit_meaningful ?loc k env =
- if k = Implicit && env.impl_binder_index = None then
+ if k <> Explicit && env.impl_binder_index = None then
warn_unexpected_implicit_binder_declaration ?loc ()
let intern_generalized_binder intern_type ntnvars
@@ -444,7 +447,7 @@ let intern_generalized_binder intern_type ntnvars
check_implicit_meaningful ?loc b' env;
let bl = List.map
CAst.(map (fun id ->
- (Name id, Implicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
+ (Name id, MaxImplicit, DAst.make ?loc @@ GHole (Evar_kinds.BinderType (Name id), IntroAnonymous, None))))
fvs
in
let na = match na with
@@ -2500,8 +2503,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl =
let r = Retyping.relevance_of_type env sigma t in
let d = LocalAssum (make_annot na r,t) in
let impls =
- if k == Implicit then CAst.make (Some (na,true)) :: impls
- else CAst.make None :: impls
+ match k with
+ | NonMaxImplicit -> CAst.make (Some (na,false)) :: impls
+ | MaxImplicit -> CAst.make (Some (na,true)) :: impls
+ | Explicit -> CAst.make None :: impls
in
(push_rel d env, sigma, d::params, succ n, impls)
| Some b ->
diff --git a/interp/impargs.ml b/interp/impargs.ml
index e2c732809a..9b50d9ca71 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -14,6 +14,7 @@ open Util
open Names
open Constr
open Globnames
+open Glob_term
open Declarations
open Lib
open Libobject
@@ -80,10 +81,24 @@ let with_implicit_protection f x =
let () = implicit_args := oflags in
iraise reraise
-let set_maximality imps b =
+type on_trailing_implicit = Error | Info | Silent
+
+let msg_trailing_implicit (fail : on_trailing_implicit) id =
+ let str1 = "Argument " ^ Names.Id.to_string id ^ " is a trailing implicit, " in
+ match fail with
+ | Error ->
+ user_err (strbrk (str1 ^ "so it can't be declared non maximal. Please use { } instead of [ ]."))
+ | Info ->
+ Flags.if_verbose Feedback.msg_info (strbrk (str1 ^ "so it has been declared maximally inserted."))
+ | Silent -> ()
+
+let set_maximality fail id imps b =
(* Force maximal insertion on ending implicits (compatibility) *)
- let is_set x = match x with None -> false | _ -> true in
- b || List.for_all is_set imps
+ b || (
+ let is_set x = match x with None -> false | _ -> true in
+ let b' = List.for_all is_set imps in
+ if b' then msg_trailing_implicit fail id;
+ b')
(*s Computation of implicit arguments *)
@@ -302,6 +317,11 @@ let is_status_implicit = function
let name_of_pos k = Id.of_string ("arg_" ^ string_of_int k)
+let binding_kind_of_status = function
+ | Some (_, _, (false, _)) -> NonMaxImplicit
+ | Some (_, _, (true, _)) -> MaxImplicit
+ | None -> Explicit
+
let name_of_implicit = function
| None -> anomaly (Pp.str "Not an implicit argument.")
| Some (ExplByName id,_,_) -> id
@@ -340,19 +360,19 @@ let rec prepare_implicits f = function
| (Anonymous, Some _)::_ -> anomaly (Pp.str "Unnamed implicit.")
| (Name id, Some imp)::imps ->
let imps' = prepare_implicits f imps in
- Some (ExplByName id,imp,(set_maximality imps' f.maximal,true)) :: imps'
+ Some (ExplByName id,imp,(set_maximality Silent id imps' f.maximal,true)) :: imps'
| _::imps -> None :: prepare_implicits f imps
-let set_manual_implicits flags enriching autoimps l =
+let set_manual_implicits silent flags enriching autoimps l =
(* Compare with automatic implicits to recover printing data and names *)
let rec merge k autoimps explimps = match autoimps, explimps with
| autoimp::autoimps, explimp::explimps ->
let imps' = merge (k+1) autoimps explimps in
begin match autoimp, explimp.CAst.v with
| (Name id,_), Some (_,max) ->
- Some (ExplByName id, Manual, (set_maximality imps' max, true))
+ Some (ExplByName id, Manual, (set_maximality (if silent then Silent else Error) id imps' max, true))
| (Name id,Some exp), None when enriching ->
- Some (ExplByName id, exp, (set_maximality imps' flags.maximal, true))
+ Some (ExplByName id, exp, (set_maximality (if silent then Silent else Info) id imps' flags.maximal, true))
| (Name _,_), None -> None
| (Anonymous,_), Some (Name id,max) ->
Some (ExplByName id,Manual,(max,true))
@@ -497,8 +517,9 @@ let impls_of_context ctx =
let map decl =
let id = NamedDecl.get_id decl in
match Id.Map.get id !sec_implicits with
- | Glob_term.Implicit -> Some (ExplByName id, Manual, (true, true))
- | Glob_term.Explicit -> None
+ | NonMaxImplicit -> Some (ExplByName id, Manual, (false, true))
+ | MaxImplicit -> Some (ExplByName id, Manual, (true, true))
+ | Explicit -> None
in
List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx)
@@ -608,7 +629,7 @@ type manual_implicits = (Name.t * bool) option CAst.t list
let compute_implicits_with_manual env sigma typ enriching l =
let autoimpls = compute_auto_implicits env sigma !implicit_args enriching typ in
- set_manual_implicits !implicit_args enriching autoimpls l
+ set_manual_implicits true !implicit_args enriching autoimpls l
let check_inclusion l =
(* Check strict inclusion *)
@@ -636,7 +657,7 @@ let declare_manual_implicits local ref ?enriching l =
let t = of_constr t in
let enriching = Option.default flags.auto enriching in
let autoimpls = compute_auto_implicits env sigma flags enriching t in
- let l = [DefaultImpArgs, set_manual_implicits flags enriching autoimpls l] in
+ let l = [DefaultImpArgs, set_manual_implicits false flags enriching autoimpls l] in
let req =
if is_local local ref then ImplLocal
else ImplInteractive(flags,ImplManual (List.length autoimpls))
@@ -647,22 +668,16 @@ let maybe_declare_manual_implicits local ref ?enriching l =
declare_manual_implicits local ref ?enriching l
-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
-
let compute_implicit_statuses autoimps l =
let rec aux i = function
- | _ :: autoimps, NotImplicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
- | Name id :: autoimps, MaximallyImplicit :: manualimps ->
+ | _ :: autoimps, Explicit :: manualimps -> None :: aux (i+1) (autoimps, manualimps)
+ | Name id :: autoimps, MaxImplicit :: manualimps ->
Some (ExplByName id, Manual, (true, true)) :: aux (i+1) (autoimps, manualimps)
- | Name id :: autoimps, Implicit :: manualimps ->
+ | Name id :: autoimps, NonMaxImplicit :: manualimps ->
let imps' = aux (i+1) (autoimps, manualimps) in
- let max = set_maximality imps' false in
- if max then msg_trailing_implicit id;
+ let max = set_maximality Error id imps' false in
Some (ExplByName id, Manual, (max, true)) :: imps'
- | Anonymous :: _, (Implicit | MaximallyImplicit) :: _ ->
+ | Anonymous :: _, (NonMaxImplicit | MaxImplicit) :: _ ->
user_err ~hdr:"set_implicits"
(strbrk ("Argument number " ^ string_of_int i ^ " (anonymous in original definition) cannot be declared implicit."))
| autoimps, [] -> List.map (fun _ -> None) autoimps
@@ -684,7 +699,7 @@ let set_implicits local ref l =
check_rigidity (is_rigid env sigma t);
(* Sort by number of implicits, decreasing *)
let is_implicit = function
- | NotImplicit -> false
+ | Explicit -> false
| _ -> true in
let l = List.map (fun imps -> (imps,List.count is_implicit imps)) l in
let l = List.sort (fun (_,n1) (_,n2) -> n2 - n1) l in
diff --git a/interp/impargs.mli b/interp/impargs.mli
index ef3c2496f4..65e7fd8aaf 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -77,6 +77,7 @@ type implicit_side_condition
type implicits_list = implicit_side_condition * implicit_status list
val is_status_implicit : implicit_status -> bool
+val binding_kind_of_status : implicit_status -> Glob_term.binding_kind
val is_inferable_implicit : bool -> int -> implicit_status -> bool
val name_of_implicit : implicit_status -> Id.t
val maximal_insertion_of : implicit_status -> bool
@@ -113,12 +114,10 @@ val declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
val maybe_declare_manual_implicits : bool -> GlobRef.t -> ?enriching:bool ->
manual_implicits -> unit
-type implicit_kind = Implicit | MaximallyImplicit | NotImplicit
-
(** [set_implicits local ref l]
Manual declaration of implicit arguments.
`l` is a list of possible sequences of implicit statuses. *)
-val set_implicits : bool -> GlobRef.t -> implicit_kind list list -> unit
+val set_implicits : bool -> GlobRef.t -> Glob_term.binding_kind list list -> unit
val implicits_of_global : GlobRef.t -> implicits_list list
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 8b457ab37b..ffbb982ab7 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -203,8 +203,9 @@ let warn_ignoring_implicit_status =
let implicits_of_glob_constr ?(with_products=true) l =
let add_impl ?loc na bk l = match bk with
- | Implicit -> CAst.make ?loc (Some (na,true)) :: l
- | _ -> CAst.make ?loc None :: l
+ | NonMaxImplicit -> CAst.make ?loc (Some (na,false)) :: l
+ | MaxImplicit -> CAst.make ?loc (Some (na,true)) :: l
+ | Explicit -> CAst.make ?loc None :: l
in
let rec aux c =
match DAst.get c with
@@ -212,8 +213,9 @@ let implicits_of_glob_constr ?(with_products=true) l =
if with_products then add_impl na bk (aux b)
else
let () = match bk with
- | Implicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
- | _ -> ()
+ | NonMaxImplicit
+ | MaxImplicit -> warn_ignoring_implicit_status na ?loc:c.CAst.loc
+ | Explicit -> ()
in []
| GLambda (na, bk, t, b) -> add_impl ?loc:t.CAst.loc na bk (aux b)
| GLetIn (na, b, t, c) -> aux c
diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg
index af1e973261..dcc3a87b11 100644
--- a/parsing/g_constr.mlg
+++ b/parsing/g_constr.mlg
@@ -205,7 +205,7 @@ GRAMMAR EXTEND Gram
| "{"; c = binder_constr ; "}" ->
{ CAst.make ~loc @@ CNotation((InConstrEntrySomeLevel,"{ _ }"),([c],[],[],[])) }
| "`{"; c = operconstr LEVEL "200"; "}" ->
- { CAst.make ~loc @@ CGeneralization (Implicit, None, c) }
+ { CAst.make ~loc @@ CGeneralization (MaxImplicit, None, c) }
| "`("; c = operconstr LEVEL "200"; ")" ->
{ CAst.make ~loc @@ CGeneralization (Explicit, None, c) } ] ]
;
@@ -431,17 +431,27 @@ GRAMMAR EXTEND Gram
| "("; id = name; ":"; t = lconstr; ":="; c = lconstr; ")" ->
{ [CLocalDef (id,c,Some t)] }
| "{"; id = name; "}" ->
- { [CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+ { [CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
| "{"; id = name; idl = LIST1 name; ":"; c = lconstr; "}" ->
- { [CLocalAssum (id::idl,Default Implicit,c)] }
+ { [CLocalAssum (id::idl,Default MaxImplicit,c)] }
| "{"; id = name; ":"; c = lconstr; "}" ->
- { [CLocalAssum ([id],Default Implicit,c)] }
+ { [CLocalAssum ([id],Default MaxImplicit,c)] }
| "{"; id = name; idl = LIST1 name; "}" ->
- { List.map (fun id -> CLocalAssum ([id],Default Implicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
+ { List.map (fun id -> CLocalAssum ([id],Default MaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
+ | "["; id = name; "]" ->
+ { [CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))] }
+ | "["; id = name; idl = LIST1 name; ":"; c = lconstr; "]" ->
+ { [CLocalAssum (id::idl,Default NonMaxImplicit,c)] }
+ | "["; id = name; ":"; c = lconstr; "]" ->
+ { [CLocalAssum ([id],Default NonMaxImplicit,c)] }
+ | "["; id = name; idl = LIST1 name; "]" ->
+ { List.map (fun id -> CLocalAssum ([id],Default NonMaxImplicit, CAst.make ~loc @@ CHole (None, IntroAnonymous, None))) (id::idl) }
| "`("; tc = LIST1 typeclass_constraint SEP "," ; ")" ->
{ List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Explicit, b), t)) tc }
| "`{"; tc = LIST1 typeclass_constraint SEP "," ; "}" ->
- { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (Implicit, b), t)) tc }
+ { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (MaxImplicit, b), t)) tc }
+ | "`["; tc = LIST1 typeclass_constraint SEP "," ; "]" ->
+ { List.map (fun (n, b, t) -> CLocalAssum ([n], Generalized (NonMaxImplicit, b), t)) tc }
| "'"; p = pattern LEVEL "0" ->
{ let (p, ty) =
match p.CAst.v with
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index d8dbf2f3dc..b212e7046a 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -151,7 +151,7 @@ let declare_one_prenex_implicit locality f =
with _ -> errorstrm (pr_qualid f ++ str " is not declared") in
let rec loop = function
| a :: args' when Impargs.is_status_implicit a ->
- Impargs.MaximallyImplicit :: loop args'
+ MaxImplicit :: loop args'
| args' when List.exists Impargs.is_status_implicit args' ->
errorstrm (str "Expected prenex implicits for " ++ pr_qualid f)
| _ -> [] in
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 02c2fc4a13..0969b3cc03 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -68,8 +68,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
| Explicit, Explicit -> true
- | Implicit, Implicit -> true
- | (Explicit | Implicit), _ -> false
+ | NonMaxImplicit, NonMaxImplicit -> true
+ | MaxImplicit, MaxImplicit -> true
+ | (Explicit | NonMaxImplicit | MaxImplicit), _ -> false
let case_style_eq s1 s2 = let open Constr in match s1, s2 with
| LetStyle, LetStyle -> true
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 44323441b6..485a19421d 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -65,7 +65,7 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t
type cases_pattern = [ `any ] cases_pattern_g
-type binding_kind = Explicit | Implicit
+type binding_kind = Explicit | MaxImplicit | NonMaxImplicit
(** Representation of an internalized (or in other words globalized) term. *)
type 'a glob_constr_r =
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index b55a41471a..2416819a6a 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -143,7 +143,8 @@ let tag_var = tag Tag.variable
let pr_generalization bk ak c =
let hd, tl =
match bk with
- | Implicit -> "{", "}"
+ | NonMaxImplicit -> "[", "]"
+ | MaxImplicit -> "{", "}"
| Explicit -> "(", ")"
in (* TODO: syntax Abstraction Kind *)
str "`" ++ str hd ++ c ++ str tl
@@ -324,12 +325,14 @@ let tag_var = tag Tag.variable
let surround_impl k p =
match k with
| Explicit -> str"(" ++ p ++ str")"
- | Implicit -> str"{" ++ p ++ str"}"
+ | NonMaxImplicit -> str"[" ++ p ++ str"]"
+ | MaxImplicit -> str"{" ++ p ++ str"}"
let surround_implicit k p =
match k with
| Explicit -> p
- | Implicit -> (str"{" ++ p ++ str"}")
+ | NonMaxImplicit -> str"[" ++ p ++ str"]"
+ | MaxImplicit -> (str"{" ++ p ++ str"}")
let pr_binder many pr (nal,k,t) =
match k with
diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
index de34e007d2..df729588f4 100644
--- a/test-suite/success/Generalization.v
+++ b/test-suite/success/Generalization.v
@@ -11,4 +11,10 @@ Admitted.
Print a_eq_b.
+Require Import Morphisms.
+Class Equiv A := equiv : A -> A -> Prop.
+Class Setoid A `{Equiv A} := setoid_equiv:> Equivalence (equiv).
+
+Lemma vcons_proper A `[Equiv A] `[!Setoid A] (x : True) : True.
+Admitted.
diff --git a/test-suite/success/ImplicitArguments.v b/test-suite/success/ImplicitArguments.v
index b16e4a1186..ebbd783dc4 100644
--- a/test-suite/success/ImplicitArguments.v
+++ b/test-suite/success/ImplicitArguments.v
@@ -1,3 +1,15 @@
+
+Axiom foo : forall (x y z t : nat), nat.
+
+Arguments foo {_} _ [z] t.
+Check (foo 1).
+Arguments foo {_} _ {z} {t}.
+Fail Arguments foo {_} _ [z] {t}.
+Check (foo 1).
+
+Definition foo1 [m] n := n + m.
+Check (foo1 1).
+
Inductive vector {A : Type} : nat -> Type :=
| vnil : vector 0
| vcons : A -> forall {n'}, vector n' -> vector (S n').
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index ecaaedca53..6e12733999 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -157,3 +157,10 @@ Check fun f : forall {_:nat}, nat => f (arg_1:=0).
Set Warnings "+syntax".
Check id (fun x => let f c {a} (b:a=a) := b in f true (eq_refl 0)).
Set Warnings "syntax".
+
+
+Axiom eq0le0 : forall (n : nat) (x : n = 0), n <= 0.
+Variable eq0le0' : forall (n : nat) {x : n = 0}, n <= 0.
+Axiom eq0le0'' : forall (n : nat) {x : n = 0}, n <= 0.
+Definition eq0le0''' : forall (n : nat) {x : n = 0}, n <= 0. Admitted.
+Fail Axiom eq0le0'''' : forall [n : nat] {x : n = 0}, n <= 0.
diff --git a/vernac/classes.ml b/vernac/classes.ml
index 77bc4e4f8a..b92c9e9b71 100644
--- a/vernac/classes.ml
+++ b/vernac/classes.ml
@@ -510,7 +510,7 @@ let do_instance_program env env' sigma ?hook ~global ~poly cty k u ctx ctx' pri
let interp_instance_context ~program_mode env ctx ~generalize pl tclass =
let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env pl in
let tclass =
- if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, Some AbsPi, tclass)
+ if generalize then CAst.make @@ CGeneralization (Glob_term.MaxImplicit, Some AbsPi, tclass)
else tclass
in
let sigma, (impls, ((env', ctx), imps)) = interp_context_evars ~program_mode env sigma ctx in
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 15077298aa..9d43debb77 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -228,7 +228,7 @@ let vernac_arguments ~section_local reference args more_implicits flags =
let implicits = List.map (List.map snd) implicits in
let implicits_specified = match implicits with
- | [l] -> List.exists (function Impargs.NotImplicit -> false | _ -> true) l
+ | [l] -> List.exists (function Glob_term.Explicit -> false | _ -> true) l
| _ -> true in
if implicits_specified && clear_implicits_flag then
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli
index 71effddf67..cbc5fc15e2 100644
--- a/vernac/comArguments.mli
+++ b/vernac/comArguments.mli
@@ -12,6 +12,6 @@ val vernac_arguments
: section_local:bool
-> Libnames.qualid Constrexpr.or_by_notation
-> Vernacexpr.vernac_argument_status list
- -> (Names.Name.t * Impargs.implicit_kind) list list
+ -> (Names.Name.t * Glob_term.binding_kind) list list
-> Vernacexpr.arguments_modifier list
-> unit
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml
index 625ffb5a06..d97bf6724c 100644
--- a/vernac/comAssumption.ml
+++ b/vernac/comAssumption.ml
@@ -270,7 +270,7 @@ let context ~poly l =
| Some (Name id',_) -> Id.equal name id'
| _ -> false
in
- let impl = Glob_term.(if List.exists test impls then Implicit else Explicit) in
+ let impl = Glob_term.(if List.exists test impls then MaxImplicit else Explicit) in (* ??? *)
name,b,t,impl)
ctx
in
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3302231fd1..d0374bc4fa 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -16,7 +16,6 @@ open Util
open Names
open Glob_term
open Vernacexpr
-open Impargs
open Constrexpr
open Constrexpr_ops
open Extend
@@ -817,7 +816,7 @@ GRAMMAR EXTEND Gram
{ let name, recarg_like, notation_scope = item in
[RealArg { name=name; recarg_like=recarg_like;
notation_scope=notation_scope;
- implicit_status = NotImplicit}] }
+ implicit_status = Explicit}] }
| "/" -> { [VolatileArg] }
| "&" -> { [BidiArg] }
| "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter ->
@@ -827,7 +826,7 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = NotImplicit}) items }
+ implicit_status = Explicit}) items }
| "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter ->
{ let f x = match sc, x with
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
@@ -835,7 +834,7 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = Implicit}) items }
+ implicit_status = NonMaxImplicit}) items }
| "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter ->
{ let f x = match sc, x with
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
@@ -843,16 +842,16 @@ GRAMMAR EXTEND Gram
List.map (fun (name,recarg_like,notation_scope) ->
RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
- implicit_status = MaximallyImplicit}) items }
+ implicit_status = MaxImplicit}) items }
]
];
(* Same as [argument_spec_block], but with only implicit status and names *)
more_implicits_block: [
- [ name = name -> { [(name.CAst.v, NotImplicit)] }
+ [ name = name -> { [(name.CAst.v, Explicit)] }
| "["; items = LIST1 name; "]" ->
- { List.map (fun name -> (name.CAst.v, Impargs.Implicit)) items }
+ { List.map (fun name -> (name.CAst.v, NonMaxImplicit)) items }
| "{"; items = LIST1 name; "}" ->
- { List.map (fun name -> (name.CAst.v, MaximallyImplicit)) items }
+ { List.map (fun name -> (name.CAst.v, MaxImplicit)) items }
]
];
strategy_level:
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index a1bd99c237..82132a1af6 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1076,14 +1076,14 @@ let string_of_definition_object_kind = let open Decls in function
let pr_br imp force x =
let left,right =
match imp with
- | Impargs.Implicit -> str "[", str "]"
- | Impargs.MaximallyImplicit -> str "{", str "}"
- | Impargs.NotImplicit -> if force then str"(",str")" else mt(),mt()
+ | Glob_term.NonMaxImplicit -> str "[", str "]"
+ | Glob_term.MaxImplicit -> str "{", str "}"
+ | Glob_term.Explicit -> if force then str"(",str")" else mt(),mt()
in
left ++ x ++ right
in
let get_arguments_like s imp tl =
- if s = None && imp = Impargs.NotImplicit then [], tl
+ if s = None && imp = Glob_term.Explicit then [], tl
else
let rec fold extra = function
| RealArg arg :: tl when
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 2cd1cf7c65..62ba6b157a 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -260,18 +260,18 @@ let implicit_name_of_pos = function
| Constrexpr.ExplByPos (n,k) -> Anonymous
let implicit_kind_of_status = function
- | None -> Anonymous, NotImplicit
- | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then MaximallyImplicit else Implicit
+ | None -> Anonymous, Glob_term.Explicit
+ | Some (pos,_,(maximal,_)) -> implicit_name_of_pos pos, if maximal then Glob_term.MaxImplicit else Glob_term.NonMaxImplicit
let dummy = {
- Vernacexpr.implicit_status = NotImplicit;
+ Vernacexpr.implicit_status = Glob_term.Explicit;
name = Anonymous;
recarg_like = false;
notation_scope = None;
}
let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
- name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit
+ name = Anonymous && not recarg_like && notation_scope = None && implicit_status = Glob_term.Explicit
let rec main_implicits i renames recargs scopes impls =
if renames = [] && recargs = [] && scopes = [] && impls = [] then []
@@ -283,8 +283,8 @@ let rec main_implicits i renames recargs scopes impls =
let (name, implicit_status) =
match renames, impls with
| _, (Some _ as i) :: _ -> implicit_kind_of_status i
- | name::_, _ -> (name,NotImplicit)
- | [], (None::_ | []) -> (Anonymous, NotImplicit)
+ | name::_, _ -> (name,Glob_term.Explicit)
+ | [], (None::_ | []) -> (Anonymous, Glob_term.Explicit)
in
let notation_scope = match scopes with
| scope :: _ -> Option.map CAst.make scope
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 1daa244986..22a8de7f99 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -254,7 +254,7 @@ type vernac_one_argument_status = {
name : Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
- implicit_status : Impargs.implicit_kind;
+ implicit_status : Glob_term.binding_kind;
}
type vernac_argument_status =
@@ -386,7 +386,7 @@ type nonrec vernac_expr =
| VernacArguments of
qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
- (Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
+ (Name.t * Glob_term.binding_kind) list list (* Extra implicit status lists *) *
arguments_modifier list
| VernacReserve of simple_binder list
| VernacGeneralizable of (lident list) option
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:19:57 +0000