diff options
42 files changed, 67 insertions, 97 deletions
diff --git a/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh new file mode 100644 index 0000000000..0c47f6a60b --- /dev/null +++ b/dev/ci/user-overlays/10665-ejgallego-api+varkind.sh @@ -0,0 +1,9 @@ +if [ "$CI_PULL_REQUEST" = "10665" ] || [ "$CI_BRANCH" = "api+varkind" ]; then + + elpi_CI_REF=api+varkind + elpi_CI_GITURL=https://github.com/ejgallego/coq-elpi + + quickchick_CI_REF=api+varkind + quickchick_CI_GITURL=https://github.com/ejgallego/QuickChick + +fi diff --git a/interp/constrexpr.ml b/interp/constrexpr.ml index e4af0fcee0..49b9149675 100644 --- a/interp/constrexpr.ml +++ b/interp/constrexpr.ml @@ -10,7 +10,6 @@ open Names open Libnames -open Decl_kinds (** {6 Concrete syntax for terms } *) @@ -39,8 +38,8 @@ type explicitation = | ExplByName of Id.t type binder_kind = - | Default of binding_kind - | Generalized of binding_kind * bool + | Default of Glob_term.binding_kind + | Generalized of Glob_term.binding_kind * bool (** (Inner binding always Implicit) Outer bindings, typeclass-specific flag for implicit generalization of superclasses *) @@ -121,7 +120,7 @@ and constr_expr_r = | CSort of Glob_term.glob_sort | CCast of constr_expr * constr_expr Glob_term.cast_type | CNotation of notation * constr_notation_substitution - | CGeneralization of binding_kind * abstraction_kind option * constr_expr + | CGeneralization of Glob_term.binding_kind * abstraction_kind option * constr_expr | CPrim of prim_token | CDelimiters of string * constr_expr and constr_expr = constr_expr_r CAst.t diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml index 8fce24249c..3f216b0d63 100644 --- a/interp/constrexpr_ops.ml +++ b/interp/constrexpr_ops.ml @@ -17,25 +17,19 @@ open Namegen open Glob_term open Constrexpr open Notation -open Decl_kinds (***********************) (* For binders parsing *) -let binding_kind_eq bk1 bk2 = match bk1, bk2 with -| Explicit, Explicit -> true -| Implicit, Implicit -> true -| _ -> false - let abstraction_kind_eq ak1 ak2 = match ak1, ak2 with | AbsLambda, AbsLambda -> true | AbsPi, AbsPi -> true | _ -> false let binder_kind_eq b1 b2 = match b1, b2 with -| Default bk1, Default bk2 -> binding_kind_eq bk1 bk2 +| Default bk1, Default bk2 -> Glob_ops.binding_kind_eq bk1 bk2 | Generalized (ck1, b1), Generalized (ck2, b2) -> - binding_kind_eq ck1 ck2 && + Glob_ops.binding_kind_eq ck1 ck2 && (if b1 then b2 else not b2) | _ -> false @@ -172,7 +166,7 @@ let rec constr_expr_eq e1 e2 = | CPrim i1, CPrim i2 -> prim_token_eq i1 i2 | CGeneralization (bk1, ak1, e1), CGeneralization (bk2, ak2, e2) -> - binding_kind_eq bk1 bk2 && + Glob_ops.binding_kind_eq bk1 bk2 && Option.equal abstraction_kind_eq ak1 ak2 && constr_expr_eq e1 e2 | CDelimiters(s1,e1), CDelimiters(s2,e2) -> diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli index 3ed240d356..a05a9cb999 100644 --- a/interp/constrexpr_ops.mli +++ b/interp/constrexpr_ops.mli @@ -26,9 +26,6 @@ val constr_expr_eq : constr_expr -> constr_expr -> bool val local_binder_eq : local_binder_expr -> local_binder_expr -> bool (** Equality on [local_binder_expr]. Same properties as [constr_expr_eq]. *) -val binding_kind_eq : Decl_kinds.binding_kind -> Decl_kinds.binding_kind -> bool -(** Equality on [binding_kind] *) - val binder_kind_eq : binder_kind -> binder_kind -> bool (** Equality on [binder_kind] *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 96392edb11..217381d854 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -27,7 +27,6 @@ open Glob_ops open Pattern open Notation open Detyping -open Decl_kinds module NamedDecl = Context.Named.Declaration (*i*) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index f341071728..f2cb4ae5c7 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -31,7 +31,6 @@ open Notation_term open Notation_ops open Notation open Inductiveops -open Decl_kinds open Context.Rel.Declaration (** constr_expr -> glob_constr translation: diff --git a/interp/impargs.ml b/interp/impargs.ml index 3f2a1b075c..5f41c2a366 100644 --- a/interp/impargs.ml +++ b/interp/impargs.ml @@ -15,7 +15,6 @@ open Names open Constr open Globnames open Declarations -open Decl_kinds open Lib open Libobject open EConstr @@ -486,12 +485,17 @@ let subst_implicits_decl subst (r,imps as o) = let subst_implicits (subst,(req,l)) = (ImplLocal,List.Smart.map (subst_implicits_decl subst) l) +(* This was moved out of lib.ml, however it is not stored with regular + implicit data *) +let sec_implicits = + Summary.ref Id.Map.empty ~name:"section-implicits" + let impls_of_context ctx = let map decl = let id = NamedDecl.get_id decl in - match Lib.variable_section_kind id with - | Implicit -> Some (id, Manual, (true, true)) - | _ -> None + match Id.Map.get id !sec_implicits with + | Glob_term.Implicit -> Some (id, Manual, (true, true)) + | Glob_term.Explicit -> None in List.rev_map map (List.filter (NamedDecl.is_local_assum) ctx) @@ -579,9 +583,10 @@ let declare_implicits local ref = if is_local local ref then ImplLocal else ImplInteractive(flags,ImplAuto) in declare_implicits_gen req flags ref -let declare_var_implicits id = +let declare_var_implicits id ~impl = let flags = !implicit_args in - declare_implicits_gen ImplLocal flags (GlobRef.VarRef id) + sec_implicits := Id.Map.add id impl !sec_implicits; + declare_implicits_gen ImplLocal flags (GlobRef.VarRef id) let declare_constant_implicits con = let flags = !implicit_args in diff --git a/interp/impargs.mli b/interp/impargs.mli index 90a7944642..2751b9d40b 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -93,7 +93,7 @@ val compute_implicits_names : env -> Evd.evar_map -> types -> Name.t list (** {6 Computation of implicits (done using the global environment). } *) -val declare_var_implicits : variable -> unit +val declare_var_implicits : variable -> impl:Glob_term.binding_kind -> unit val declare_constant_implicits : Constant.t -> unit val declare_mib_implicits : MutInd.t -> unit diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 9f6281ae15..455471a472 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -11,7 +11,6 @@ (*i*) open Names open Context -open Decl_kinds open CErrors open Util open Glob_term diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 2fa78bb9f3..f30a874426 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -15,7 +15,6 @@ open Names open Nameops open Constr open Globnames -open Decl_kinds open Namegen open Glob_term open Glob_ops diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml deleted file mode 100644 index 17746645ee..0000000000 --- a/library/decl_kinds.ml +++ /dev/null @@ -1,11 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* <O___,, * (see CREDITS file for the list of authors) *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(* * (see LICENSE file for the text of the license) *) -(************************************************************************) - -type binding_kind = Explicit | Implicit diff --git a/library/lib.ml b/library/lib.ml index 6b01eb07e9..3f51826315 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -441,9 +441,6 @@ let empty_section_data ~poly = { let sectab = Summary.ref ([] : section_data list) ~name:"section-context" -let sec_implicits = - Summary.ref Id.Map.empty ~name:"section-implicits" - let check_same_poly p sec = if p != sec.sec_poly then user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.") @@ -452,14 +449,13 @@ let add_section ~poly () = List.iter (fun tab -> check_same_poly poly tab) !sectab; sectab := empty_section_data ~poly :: !sectab -let add_section_variable ~name ~kind ~poly = +let add_section_variable ~name ~poly = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | s :: sl -> List.iter (fun tab -> check_same_poly poly tab) !sectab; let s = { s with sec_entry = Variable {id=name} :: s.sec_entry } in - sectab := s :: sl; - sec_implicits := Id.Map.add name kind !sec_implicits + sectab := s :: sl let add_section_context ctx = match !sectab with @@ -576,8 +572,6 @@ let section_segment_of_reference = let open GlobRef in function let variable_section_segment_of_reference gr = (section_segment_of_reference gr).abstr_ctx -let variable_section_kind id = Id.Map.get id !sec_implicits - let section_instance = let open GlobRef in function | VarRef id -> let eq = function diff --git a/library/lib.mli b/library/lib.mli index 7dc8b52282..9ffa69ef93 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -177,12 +177,11 @@ val section_segment_of_mutual_inductive: MutInd.t -> abstr_info val section_segment_of_reference : GlobRef.t -> abstr_info val variable_section_segment_of_reference : GlobRef.t -> Constr.named_context -val variable_section_kind : Id.t -> Decl_kinds.binding_kind val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array val is_in_section : GlobRef.t -> bool -val add_section_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> unit +val add_section_variable : name:Id.t -> poly:bool -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit diff --git a/library/library.mllib b/library/library.mllib index 84937ede93..3b75438ccd 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -1,4 +1,3 @@ -Decl_kinds Libnames Globnames Libobject diff --git a/parsing/g_constr.mlg b/parsing/g_constr.mlg index 78a12a2e7d..ea44e748c9 100644 --- a/parsing/g_constr.mlg +++ b/parsing/g_constr.mlg @@ -19,7 +19,6 @@ open Constrexpr_ops open Util open Tok open Namegen -open Decl_kinds open Pcoq open Pcoq.Prim diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index 730ae48393..a836335d4d 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -1600,7 +1600,7 @@ let register_mes interactive_proof fname rec_impls wf_mes_expr wf_rel_expr_opt w let b = Names.Id.of_string "___b" in Constrexpr_ops.mkLambdaC( [CAst.make @@ Name a; CAst.make @@ Name b], - Constrexpr.Default Decl_kinds.Explicit, + Constrexpr.Default Glob_term.Explicit, wf_arg_type, Constrexpr_ops.mkAppC(wf_rel_expr, [ diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index 6eb8c42d1d..ddd6ecfb5c 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -1300,7 +1300,7 @@ let rec rebuild_return_type rt = | Constrexpr.CLetIn(na,v,t,t') -> CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t') | _ -> CAst.make ?loc @@ Constrexpr.CProdN([Constrexpr.CLocalAssum ([CAst.make Anonymous], - Constrexpr.Default Decl_kinds.Explicit, rt)], + Constrexpr.Default Explicit, rt)], CAst.make @@ Constrexpr.CSort(UAnonymous {rigid=true})) let do_build_inductive diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index d36d86a65b..fbf63c69dd 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -4,7 +4,6 @@ open Glob_term open CErrors open Util open Names -open Decl_kinds (* Some basic functions to rebuild glob_constr diff --git a/plugins/ltac/g_tactic.mlg b/plugins/ltac/g_tactic.mlg index 7cd43cb5cd..9b52b710c1 100644 --- a/plugins/ltac/g_tactic.mlg +++ b/plugins/ltac/g_tactic.mlg @@ -24,7 +24,6 @@ open Tactypes open Tactics open Inv open Locus -open Decl_kinds open Pcoq @@ -450,9 +449,9 @@ GRAMMAR EXTEND Gram | -> { true } ] ] ; simple_binder: - [ [ na=name -> { ([na],Default Explicit, CAst.make ~loc @@ + [ [ na=name -> { ([na],Default Glob_term.Explicit, CAst.make ~loc @@ CHole (Some (Evar_kinds.BinderType na.CAst.v), IntroAnonymous, None)) } - | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Explicit,c) } + | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> { (nal,Default Glob_term.Explicit,c) } ] ] ; fixdecl: diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 0e38ce575b..6df068883c 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -20,7 +20,6 @@ open Stdarg open Notation_gram open Tactypes open Locus -open Decl_kinds open Genredexpr open Ppconstr open Pputils @@ -1097,7 +1096,7 @@ let pr_goal_selector ~toplevel s = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else match DAst.get ty with - Glob_term.GProd(na,Explicit,a,b) -> + Glob_term.GProd(na,Glob_term.Explicit,a,b) -> strip_ty (([CAst.make na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in strip_ty [] n ty diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 33e9f871fd..473612fda7 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,7 +181,6 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term -open Decl_kinds let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) diff --git a/plugins/ssr/ssrparser.mlg b/plugins/ssr/ssrparser.mlg index 175a863ad8..a1f707ffa8 100644 --- a/plugins/ssr/ssrparser.mlg +++ b/plugins/ssr/ssrparser.mlg @@ -32,7 +32,6 @@ open Ppconstr open Namegen open Tactypes -open Decl_kinds open Constrexpr open Constrexpr_ops @@ -1337,20 +1336,20 @@ ARGUMENT EXTEND ssrbinder TYPED AS (ssrfwdfmt * constr) PRINTED BY { pr_ssrbinde | [ ssrbvar(bv) ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ")" ] -> { let { CAst.loc=xloc } as x = bvar_lname bv in (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Explicit,mkCHole xloc)],mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x],Default Glob_term.Explicit,mkCHole xloc)],mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ":" lconstr(t) ")" ] -> { let x = bvar_lname bv in (FwdPose, [BFdecl 1]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Explicit, t)], mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(bv) ne_ssrbvar_list(bvs) ":" lconstr(t) ")" ] -> { let xs = List.map bvar_lname (bv :: bvs) in let n = List.length xs in (FwdPose, [BFdecl n]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Explicit, t)], mkCHole (Some loc)) } + CAst.make ~loc @@ CLambdaN ([CLocalAssum (xs, Default Glob_term.Explicit, t)], mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":" lconstr(t) ":=" lconstr(v) ")" ] -> { (FwdPose,[BFdef]), CAst.make ~loc @@ CLetIn (bvar_lname id, v, Some t, mkCHole (Some loc)) } | [ "(" ssrbvar(id) ":=" lconstr(v) ")" ] -> @@ -1362,7 +1361,7 @@ GRAMMAR EXTEND Gram ssrbinder: [ [ ["of" -> { () } | "&" -> { () } ]; c = operconstr LEVEL "99" -> { (FwdPose, [BFvar]), - CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Explicit,c)],mkCHole (Some loc)) } ] + CAst.make ~loc @@ CLambdaN ([CLocalAssum ([CAst.make ~loc Anonymous],Default Glob_term.Explicit,c)],mkCHole (Some loc)) } ] ]; END @@ -1391,7 +1390,7 @@ let push_binders c2 bs = let rec fix_binders = let open CAst in function | (_, { v = CLambdaN ([CLocalAssum(xs, _, t)], _) } ) :: bs -> - CLocalAssum (xs, Default Explicit, t) :: fix_binders bs + CLocalAssum (xs, Default Glob_term.Explicit, t) :: fix_binders bs | (_, { v = CLetIn (x, v, oty, _) } ) :: bs -> CLocalDef (x, v, oty) :: fix_binders bs | _ -> [] @@ -1521,7 +1520,7 @@ let intro_id_to_binder = List.map (function | IPatId id -> let { CAst.loc=xloc } as x = bvar_lname (mkCVar id) in (FwdPose, [BFvar]), - CAst.make @@ CLambdaN ([CLocalAssum([x], Default Explicit, mkCHole xloc)], + CAst.make @@ CLambdaN ([CLocalAssum([x], Default Glob_term.Explicit, mkCHole xloc)], mkCHole None) | _ -> anomaly "non-id accepted as binder") diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg index 0adabb0673..f3f1d713e9 100644 --- a/plugins/ssr/ssrvernac.mlg +++ b/plugins/ssr/ssrvernac.mlg @@ -27,7 +27,6 @@ open Notation_ops open Notation_term open Glob_term open Stdarg -open Decl_kinds open Pp open Ppconstr open Printer diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 17db25660f..4d7a04f5ee 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -36,7 +36,6 @@ open Ppconstr open Printer open Globnames open Namegen -open Decl_kinds open Evar_kinds open Constrexpr open Constrexpr_ops diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index a148a3bc73..9808c61255 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -112,7 +112,7 @@ let vernac_numeral_notation local ty f g scope opts = let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in let arrow x y = - mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in let opt r = app (mkRefC (q_option ())) r in let constructors = get_constructors tyc in diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml index 8c0f9a3339..c92acb0f55 100644 --- a/plugins/syntax/string_notation.ml +++ b/plugins/syntax/string_notation.ml @@ -61,7 +61,7 @@ let vernac_string_notation local ty f g scope = let of_ty = Smartlocate.global_with_alias g in let cty = cref ty in let arrow x y = - mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in let constructors = get_constructors tyc in (* Check the type of f *) diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2061b41292..e8c83c7de9 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -25,7 +25,6 @@ open Namegen open Libnames open Globnames open Mod_subst -open Decl_kinds open Context.Named.Declaration open Ltac_pretype diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index cc9f520583..9eb014aa62 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -57,10 +57,10 @@ val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.Set.t -> ( val share_pattern_names : (Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> 'a) -> int -> - (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list -> + (Name.t * binding_kind * 'b option * 'a) list -> Id.Set.t -> names_context -> 'c -> Pattern.constr_pattern -> Pattern.constr_pattern -> - (Name.t * Decl_kinds.binding_kind * 'b option * 'a) list * 'a * 'a + (Name.t * binding_kind * 'b option * 'a) list * 'a * 'a val detype_closed_glob : ?lax:bool -> bool -> Id.Set.t -> env -> evar_map -> closed_glob_constr -> glob_constr diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml index 6bde3dfd81..93f5923474 100644 --- a/pretyping/glob_ops.ml +++ b/pretyping/glob_ops.ml @@ -67,9 +67,9 @@ let glob_sort_eq u1 u2 = match u1, u2 with | (UNamed _ | UAnonymous _), _ -> false let binding_kind_eq bk1 bk2 = match bk1, bk2 with - | Decl_kinds.Explicit, Decl_kinds.Explicit -> true - | Decl_kinds.Implicit, Decl_kinds.Implicit -> true - | (Decl_kinds.Explicit | Decl_kinds.Implicit), _ -> false + | Explicit, Explicit -> true + | Implicit, Implicit -> true + | (Explicit | Implicit), _ -> false let case_style_eq s1 s2 = let open Constr in match s1, s2 with | LetStyle, LetStyle -> true diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli index 467b72e520..37aa31d094 100644 --- a/pretyping/glob_ops.mli +++ b/pretyping/glob_ops.mli @@ -48,6 +48,9 @@ val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_const val map_glob_constr : (glob_constr -> glob_constr) -> glob_constr -> glob_constr +(** Equality on [binding_kind] *) +val binding_kind_eq : binding_kind -> binding_kind -> bool + (** Ensure traversal from left to right *) val map_glob_constr_left_to_right : (glob_constr -> glob_constr) -> glob_constr -> glob_constr diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml index 7c859a5332..10e9d60fd5 100644 --- a/pretyping/glob_term.ml +++ b/pretyping/glob_term.ml @@ -17,7 +17,6 @@ arguments and pattern-matching compilation are not. *) open Names -open Decl_kinds type existential_name = Id.t @@ -66,6 +65,8 @@ and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t type cases_pattern = [ `any ] cases_pattern_g +type binding_kind = Explicit | Implicit + (** Representation of an internalized (or in other words globalized) term. *) type 'a glob_constr_r = | GRef of GlobRef.t * glob_level list option diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 99e3c5025e..ccc3b6e83c 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -18,7 +18,6 @@ open Context open Glob_term open Pp open Mod_subst -open Decl_kinds open Pattern open Environ diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c28c3ab730..4fed526cfc 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1193,7 +1193,7 @@ let path_convertible env sigma p q = let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in let mkGVar id = DAst.make @@ Glob_term.GVar(id) in let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in - let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Decl_kinds.Explicit,t,b) in + let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Explicit,t,b) in let mkGHole () = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in let path_to_gterm p = match p with diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index aea4f23205..5ed96dd5e3 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -21,7 +21,6 @@ open Glob_term open Constrexpr open Constrexpr_ops open Notation_gram -open Decl_kinds open Namegen (*i*) diff --git a/tactics/declare.ml b/tactics/declare.ml index 391524ebda..c280760e84 100644 --- a/tactics/declare.ml +++ b/tactics/declare.ml @@ -300,7 +300,7 @@ let declare_private_constant ?role ?(local = ImportDefaultBehavior) ~name ~kind (** Declaration of section variables and local definitions *) type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:Constr.types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } (* This object is only for things which iterate over objects to find variables (only Prettyp.print_context AFAICT) *) @@ -317,7 +317,6 @@ let declare_variable ~name ~kind d = | SectionLocalAssum {typ;univs;poly;impl} -> let () = declare_universe_context ~poly univs in let () = Global.push_named_assum (name,typ) in - let impl = if impl then Decl_kinds.Implicit else Decl_kinds.Explicit in impl, true, poly | SectionLocalDef (de) -> (* The body should already have been forced upstream because it is a @@ -342,14 +341,14 @@ let declare_variable ~name ~kind d = secdef_type = de.proof_entry_type; } in let () = Global.push_named_def (name, se) in - Decl_kinds.Explicit, de.proof_entry_opaque, + Glob_term.Explicit, de.proof_entry_opaque, poly in Nametab.push (Nametab.Until 1) (Libnames.make_path DirPath.empty name) (GlobRef.VarRef name); - add_section_variable ~name ~kind:impl ~poly; + add_section_variable ~name ~poly; Decls.(add_variable_data name {opaque;kind}); add_anonymous_leaf (inVariable ()); - Impargs.declare_var_implicits name; + Impargs.declare_var_implicits ~impl name; Notation.declare_ref_arguments_scope Evd.empty (GlobRef.VarRef name) (** Declaration of inductive blocks *) diff --git a/tactics/declare.mli b/tactics/declare.mli index 89b41076f7..4ae9f6c7ae 100644 --- a/tactics/declare.mli +++ b/tactics/declare.mli @@ -23,7 +23,7 @@ open Entries type variable_declaration = | SectionLocalDef of Evd.side_effects Proof_global.proof_entry - | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:bool } + | SectionLocalAssum of { typ:types; univs:Univ.ContextSet.t; poly:bool; impl:Glob_term.binding_kind } type 'a constant_entry = | DefinitionEntry of 'a Proof_global.proof_entry diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a3a88df21e..61e0e41eb9 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -258,7 +258,6 @@ type equation_kind = exception NoEquationFound open Glob_term -open Decl_kinds open Evar_kinds let mkPattern c = snd (Patternops.pattern_of_glob_constr c) diff --git a/vernac/classes.ml b/vernac/classes.ml index 075d89d0df..d5f5656e1d 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -28,9 +28,7 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration (*i*) -open Decl_kinds - -let set_typeclass_transparency c local b = +let set_typeclass_transparency c local b = Hints.add_hints ~local [typeclasses_db] (Hints.HintsTransparencyEntry (Hints.HintsReferences [c], b)) @@ -527,7 +525,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 (Implicit, Some AbsPi, tclass) + if generalize then CAst.make @@ CGeneralization (Glob_term.Implicit, 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/comAssumption.ml b/vernac/comAssumption.ml index 7d365db85c..e3f90ab98c 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -100,7 +100,7 @@ let next_uctx = let declare_assumptions idl is_coe ~scope ~poly ~kind typ uctx pl imps nl = let refs, _ = List.fold_left (fun (refs,uctx) id -> - let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps false nl id in + let ref = declare_assumption is_coe ~scope ~poly ~kind typ uctx pl imps Glob_term.Explicit nl id in ref::refs, next_uctx uctx) ([],uctx) idl in @@ -292,7 +292,7 @@ let context ~poly l = | Some (Name id',_) -> Id.equal name id' | _ -> false in - let impl = List.exists test impls in + let impl = if List.exists test impls then Glob_term.Implicit else Glob_term.Explicit in let scope = if Lib.sections_are_opened () then DeclareDef.Discharge else DeclareDef.Global ImportDefaultBehavior in match b with diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index 1632c3d578..2715bd8305 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -34,7 +34,7 @@ val declare_assumption -> Entries.universes_entry -> UnivNames.universe_binders -> Impargs.manual_implicits - -> bool (** implicit *) + -> Glob_term.binding_kind -> Declaremods.inline -> variable CAst.t -> GlobRef.t * Univ.Instance.t diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index adfb058942..7809425a10 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -258,7 +258,7 @@ let save_remaining_recthms env sigma ~poly ~scope ~udecl uctx body opaq i { Rect let open DeclareDef in (match scope with | Discharge -> - let impl = false in (* copy values from Vernacentries *) + let impl = Glob_term.Explicit in let univs = match univs with | Polymorphic_entry (_, univs) -> (* What is going on here? *) diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index d4b2029e99..b712d7e264 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -170,7 +170,7 @@ type inductive_expr = type one_inductive_expr = lident * local_binder_expr list * constr_expr option * constructor_expr list -type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr +type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr and typeclass_context = typeclass_constraint list type proof_expr = |