From f713e6c195d1de177b43cab7c2902f5160f6af9f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 24 Mar 2017 02:18:53 +0100 Subject: A fix to #5414 (ident bound by ltac names now known for "match"). Also taking into account a name in the return clause and in the indices. Note the double meaning ``bound as a term to match'' and ``binding in the "as" clause'' when the term to match is a variable for all of "match", "if" and "let". --- API/API.mli | 38 +++++++++++++++++++------------------- 1 file changed, 19 insertions(+), 19 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index d844e8bf52..2045fadaef 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2510,6 +2510,20 @@ sig and closed_glob_constr = Glob_term.closed_glob_constr = { closure: closure; term: glob_constr } + + type var_map = Pattern.constr_under_binders Names.Id.Map.t + type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t + type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t + type ltac_var_map = Glob_term.ltac_var_map = { + ltac_constrs : var_map; + (** Ltac variables bound to constrs *) + ltac_uconstrs : uconstr_var_map; + (** Ltac variables bound to untyped constrs *) + ltac_idents: Names.Id.t Names.Id.Map.t; + (** Ltac variables bound to identifiers *) + ltac_genargs : unbound_ltac_var_map; + (** Ltac variables bound to other kinds of arguments *) + } end module Libnames : @@ -2875,10 +2889,6 @@ sig | IsType | WithoutTypeConstraint - type var_map = Pattern.constr_under_binders Names.Id.Map.t - type uconstr_var_map = Glob_term.closed_glob_constr Names.Id.Map.t - type unbound_ltac_var_map = Geninterp.Val.t Names.Id.Map.t - type inference_hook = Environ.env -> Evd.evar_map -> Evar.t -> Evd.evar_map * EConstr.constr type inference_flags = Pretyping.inference_flags = { use_typeclasses : bool; @@ -2888,22 +2898,11 @@ sig expand_evars : bool } - type ltac_var_map = Pretyping.ltac_var_map = { - ltac_constrs : var_map; - (** Ltac variables bound to constrs *) - ltac_uconstrs : uconstr_var_map; - (** Ltac variables bound to untyped constrs *) - ltac_idents: Names.Id.t Names.Id.Map.t; - (** Ltac variables bound to identifiers *) - ltac_genargs : unbound_ltac_var_map; - (** Ltac variables bound to other kinds of arguments *) - } type pure_open_constr = Evd.evar_map * EConstr.constr - type glob_constr_ltac_closure = ltac_var_map * Glob_term.glob_constr + type glob_constr_ltac_closure = Glob_term.ltac_var_map * Glob_term.glob_constr - val empty_lvar : ltac_var_map val understand_ltac : inference_flags -> - Environ.env -> Evd.evar_map -> ltac_var_map -> + Environ.env -> Evd.evar_map -> Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> pure_open_constr val understand_tcc : ?flags:inference_flags -> Environ.env -> Evd.evar_map -> ?expected_type:typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr @@ -2917,11 +2916,11 @@ sig val interp_elimination_sort : Misctypes.glob_sort -> Sorts.family val register_constr_interp0 : ('r, 'g, 't) Genarg.genarg_type -> - (unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit + (Glob_term.unbound_ltac_var_map -> Environ.env -> Evd.evar_map -> EConstr.types -> 'g -> EConstr.constr * Evd.evar_map) -> unit val all_and_fail_flags : inference_flags val ise_pretype_gen : inference_flags -> Environ.env -> Evd.evar_map -> - ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr + Glob_term.ltac_var_map -> typing_constraint -> Glob_term.glob_constr -> Evd.evar_map * EConstr.constr end module Evarconv : @@ -3746,6 +3745,7 @@ sig val cases_pattern_of_glob_constr : Names.Name.t -> Glob_term.glob_constr -> Glob_term.cases_pattern val map_glob_constr : (Glob_term.glob_constr -> Glob_term.glob_constr) -> Glob_term.glob_constr -> Glob_term.glob_constr + val empty_lvar : Glob_term.ltac_var_map end module Indrec : -- cgit v1.2.3 From f610068823b33bdc0af752a646df05b98489d7ce Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Jun 2017 06:08:02 +0200 Subject: [proof] Deprecate redundant wrappers. As we would like to reduce the role of proof_global in future versions, we start to deprecate old compatibility aliases in `Pfedit` in favor of the real functions underlying the 8.5 proof engine. We also deprecate a couple of alias types and explicitly mark the few remaining uses of `Pfedit`. --- API/API.mli | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index d844e8bf52..f25dcccb82 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3417,6 +3417,8 @@ sig (** @raise NoCurrentProof when outside proof mode. *) val discard_all : unit -> unit + val discard_current : unit -> unit + val get_current_proof_name : unit -> Names.Id.t end module Nametab : @@ -3889,11 +3891,18 @@ sig val solve : ?with_end_tac:unit Proofview.tactic -> Vernacexpr.goal_selector -> int option -> unit Proofview.tactic -> Proof.proof -> Proof.proof * bool - val delete_current_proof : unit -> unit val cook_proof : unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind)) - val get_current_proof_name : unit -> Names.Id.t + val get_current_context : unit -> Evd.evar_map * Environ.env + + (* Deprecated *) + val delete_current_proof : unit -> unit + [@@ocaml.deprecated "use Proof_global.discard_current"] + + val get_current_proof_name : unit -> Names.Id.t + [@@ocaml.deprecated "use Proof_global.get_current_proof_name"] + end module Tactics : -- cgit v1.2.3 From 63896b2443e71e47c016fc9d0709cc22cf24f288 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 12:37:55 +0200 Subject: [lib] Remove obsolete state-management function add_frozen_state AFAICS this function predates modern state-handling; nowadays summaries are stored by the STM and nobody were using this information. --- API/API.mli | 1 - 1 file changed, 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index d844e8bf52..0b5183947b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2634,7 +2634,6 @@ module Lib : sig | ClosedModule of library_segment | OpenedSection of Libnames.object_prefix * Summary.frozen | ClosedSection of library_segment - | FrozenState of Summary.frozen and library_segment = (Libnames.object_name * node) list -- cgit v1.2.3 From 0fad09306982a88ff8d633d36abdc440dd542ab3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 13 Jun 2017 10:33:56 +0200 Subject: Dualize the unsafe flag of refine into typecheck and make it mandatory. --- API/API.mli | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 20a637c1fa..5a833d08ad 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4100,7 +4100,7 @@ sig module New : sig - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic + val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.constr) -> unit Proofview.tactic val reduce_after_refine : unit Proofview.tactic end module Simple : @@ -4490,7 +4490,7 @@ end module Refine : sig - val refine : ?unsafe:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic + val refine : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * EConstr.t) -> unit Proofview.tactic val solve_constraints : unit Proofview.tactic end -- cgit v1.2.3 From d038839a32978548051573286e22462d68d42ee6 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 26 Apr 2016 17:30:30 +0200 Subject: Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t) This string contains the base-10 representation of the number (big endian) Note that some inner parsing stuff still uses bigints, see egramcoq.ml --- API/API.mli | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 20a637c1fa..ba0e00a020 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2055,8 +2055,10 @@ sig type explicitation = Constrexpr.explicitation = | ExplByPos of int * Names.Id.t option | ExplByName of Names.Id.t + type sign = bool + type raw_natural_number = string type prim_token = Constrexpr.prim_token = - | Numeral of Bigint.bigint + | Numeral of raw_natural_number * sign | String of string type notation = string type instance_expr = Misctypes.glob_level list -- cgit v1.2.3 From 2bc76bf063da72d1db38c3c0d29c747b0fe23f78 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 22 Feb 2017 18:32:23 +0100 Subject: G_prim: the bigint entry keeps numbers in raw strings --- API/grammar_API.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'API') diff --git a/API/grammar_API.mli b/API/grammar_API.mli index 44aae771f6..b39ee30b53 100644 --- a/API/grammar_API.mli +++ b/API/grammar_API.mli @@ -116,7 +116,7 @@ sig val pattern_identref : Names.Id.t located Gram.Entry.e val base_ident : Names.Id.t Gram.Entry.e val natural : int Gram.Entry.e - val bigint : Bigint.bigint Gram.Entry.e + val bigint : Constrexpr.raw_natural_number Gram.Entry.e val integer : int Gram.Entry.e val string : string Gram.Entry.e val qualid : API.Libnames.qualid located Gram.Entry.e -- cgit v1.2.3 From da0459552dd4ac253e45bb519d99a5a718105313 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 13 Jun 2017 21:38:59 +0200 Subject: API additions for coq-dpdgraph --- API/API.mli | 21 ++++++++++++++++++++- 1 file changed, 20 insertions(+), 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 20a637c1fa..a662517406 100644 --- a/API/API.mli +++ b/API/API.mli @@ -72,6 +72,7 @@ sig val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds end type 'a puniverses = 'a * Instance.t + val out_punivs : 'a puniverses -> 'a module Constraint : module type of struct include Univ.Constraint end @@ -1034,7 +1035,16 @@ sig | Undef of inline | Def of Term.constr Mod_subst.substituted | OpaqueDef of Opaqueproof.opaque - type constant_type = Declarations.constant_type + type template_arity = Declarations.template_arity = { + template_param_levels : Univ.Level.t option list; + template_level : Univ.Universe.t; + } + + type ('a, 'b) declaration_arity = ('a, 'b) Declarations.declaration_arity = + | RegularArity of 'a + | TemplateArity of 'b + + type constant_type = (Prelude.types, Context.Rel.t * template_arity) declaration_arity type constant_universes = Declarations.constant_universes type projection_body = Declarations.projection_body = { proj_ind : Names.MutInd.t; @@ -1131,6 +1141,11 @@ sig uj_val : 'constr; uj_type : 'types } + type 'types punsafe_type_judgment = 'types Environ.punsafe_type_judgment = { + utj_val : 'types; + utj_type : Sorts.t } + + type unsafe_type_judgment = Term.types punsafe_type_judgment val empty_env : env val lookup_mind : Names.MutInd.t -> env -> Declarations.mutual_inductive_body val push_rel : Context.Rel.Declaration.t -> env -> env @@ -1156,6 +1171,7 @@ sig val fold_named_context_reverse : ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a val evaluable_named : Names.Id.t -> Environ.env -> bool + val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env end module UGraph : @@ -1219,6 +1235,7 @@ end module Typeops : sig + val infer_type : Environ.env -> Term.types -> Environ.unsafe_type_judgment val type_of_constant_type : Environ.env -> Declarations.constant_type -> Term.types val type_of_constant_in : Environ.env -> Term.pconstant -> Term.types end @@ -2631,6 +2648,7 @@ sig type universe_opt_subst = Universes.universe_opt_subst val fresh_inductive_instance : Environ.env -> Names.inductive -> Term.pinductive Univ.in_universe_context_set val new_Type : Names.DirPath.t -> Term.types + val type_of_global : Globnames.global_reference -> Term.types Univ.in_universe_context_set val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr val universes_of_constr : Term.constr -> Univ.LSet.t @@ -3473,6 +3491,7 @@ sig type ltac_constant = Names.KerName.t + val global : Libnames.reference -> Globnames.global_reference val global_of_path : Libnames.full_path -> Globnames.global_reference val shortest_qualid_of_global : Names.Id.Set.t -> Globnames.global_reference -> Libnames.qualid val path_of_global : Globnames.global_reference -> Libnames.full_path -- cgit v1.2.3 From 706b16c3c714f91bfff33ce340aec6f2d24fe246 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Sat, 10 Jun 2017 15:54:31 +0200 Subject: API: exports Mltop.module_is_known to both API.mli and grammar_API.mli --- API/API.mli | 1 + API/grammar_API.mli | 1 + 2 files changed, 2 insertions(+) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 20a637c1fa..9714f52b91 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3307,6 +3307,7 @@ sig val declare_cache_obj : (unit -> unit) -> string -> unit val add_known_plugin : (unit -> unit) -> string -> unit val add_known_module : string -> unit + val module_is_known : string -> bool end (* All items in the Proof_type module are deprecated. *) diff --git a/API/grammar_API.mli b/API/grammar_API.mli index 44aae771f6..4da5b380fe 100644 --- a/API/grammar_API.mli +++ b/API/grammar_API.mli @@ -211,6 +211,7 @@ end module Mltop : sig val add_known_module : string -> unit + val module_is_known : string -> bool val declare_cache_obj : (unit -> unit) -> string -> unit end module Vernacinterp : -- cgit v1.2.3 From 44f462aa380de847452c0809d15c86649d5d6a7a Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Tue, 28 Mar 2017 19:24:02 +0200 Subject: Extend definition of inductives to include subtyping info --- API/API.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 69278e7c9f..e2c43dab82 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1094,6 +1094,7 @@ sig mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; mind_universes : Univ.UContext.t; + mind_subtyping : Univ.universe_context; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } -- cgit v1.2.3 From fd1f420aef96822bed2ce14214c34e41ceda9b4e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sat, 1 Apr 2017 17:35:39 +0200 Subject: Using UInfoInd for universes in inductive types It stores both universe constraints and subtyping information for blocks of inductive declarations. At this stage the there is no inference or checking implemented. The subtyping information simply encodes equality of levels for the condition of subtyping. --- API/API.mli | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index e2c43dab82..cea879ba3c 100644 --- a/API/API.mli +++ b/API/API.mli @@ -86,6 +86,8 @@ sig type universe_context = UContext.t [@@ocaml.deprecated "alias of API.Names.UContext.t"] + type universe_info_ind = Univ.UInfoInd.t + module LSet : module type of struct include Univ.LSet end module ContextSet : sig @@ -1093,8 +1095,7 @@ sig mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; - mind_universes : Univ.UContext.t; - mind_subtyping : Univ.universe_context; + mind_universes : Univ.universe_info_ind; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } -- cgit v1.2.3 From 40f56eb0f79e208fc4b1b4ed2f0fb49c69c13a2f Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Sun, 21 May 2017 14:46:30 +0200 Subject: Squashed commit of the following: Except I have disabled the minimization of universes after sections as it seems to interfere with the STM machinery causing files like test-suite/vio/print.v to loop when processed asynchronously. This is very peculiar and needs more investigation as the aforementioned file does not have any sections or any universe polymorphic definitions! commit fc785326080b9451eb4700b16ccd3f7df214e0ed Author: Amin Timany Date: Mon Apr 24 17:14:21 2017 +0200 Revert STL to monomorphic commit 62b573fb13d290d8fe4c85822da62d3e5e2a6996 Author: Amin Timany Date: Mon Apr 24 17:02:42 2017 +0200 Try unifying universes before apply subtyping commit ff393742c37b9241c83498e84c2274967a1a58dc Author: Amin Timany Date: Sun Apr 23 13:49:04 2017 +0200 Compile more of STL with universe polymorphism commit 5c831b41ebd1fc32e2dd976697c8e474f48580d6 Author: Amin Timany Date: Tue Apr 18 21:26:45 2017 +0200 Made more progress on compiling the standard library commit b8550ffcce0861794116eb3b12b84e1158c2b4f8 Author: Amin Timany Date: Sun Apr 16 22:55:19 2017 +0200 Make more number theoretic modules monomorphic commit 29d126d4d4910683f7e6aada2a25209151e41b10 Author: Amin Timany Date: Fri Apr 14 16:11:48 2017 +0200 WIP more of standard library compiles Also: Matthieu fixed a bug in rewrite system which was faulty when introducing new morphisms (Add Morphism) command. commit 23bc33b843f098acaba4c63c71c68f79c4641f8c Author: Amin Timany Date: Fri Apr 14 11:39:21 2017 +0200 WIP: more of the standard library compiles We have implemented convertibility of constructors up-to mutual subtyping of their corresponding inductive types. This is similar to the behavior of template polymorphism. commit d0abc5c50d593404fb41b98d588c3843382afd4f Author: Amin Timany Date: Wed Apr 12 19:02:39 2017 +0200 WIP: trying to get the standard library compile with universe polymorphism We are trying to prune universes after section ends. Sections add a load of universes that are not appearing in the body, type or the constraints. --- API/API.ml | 1 + API/API.mli | 7 +++++-- 2 files changed, 6 insertions(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.ml b/API/API.ml index 2b7bbd561b..515b152e42 100644 --- a/API/API.ml +++ b/API/API.ml @@ -138,6 +138,7 @@ module Typeclasses = Typeclasses module Pretype_errors = Pretype_errors module Notation = Notation module Declarations = Declarations +module Univops = Univops module Declareops = Declareops module Globnames = Globnames module Environ = Environ diff --git a/API/API.mli b/API/API.mli index cea879ba3c..a4ae6347c0 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1124,6 +1124,11 @@ sig | SFBmodtype of module_type_body end +module Univops : sig + val universes_of_constr : Term.constr -> Univ.LSet.t + val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t +end + module Environ : sig type env = Prelude.env @@ -2651,8 +2656,6 @@ sig val new_Type : Names.DirPath.t -> Term.types val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr - val universes_of_constr : Term.constr -> Univ.LSet.t - val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context val new_sort_in_family : Sorts.family -> Sorts.t -- cgit v1.2.3 From 9468e4b49bd2f397b5e1bd2b7994cc84929fb6ac Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 27 Apr 2017 20:16:35 +0200 Subject: Fix bugs and add an option for cumulativity --- API/API.mli | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index a4ae6347c0..a993b0277c 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1095,6 +1095,7 @@ sig mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; + mind_cumulative : bool; mind_universes : Univ.universe_info_ind; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; @@ -1907,6 +1908,7 @@ end module Decl_kinds : sig type polymorphic = bool + type cumulative_inductive_flag = bool type recursivity_kind = Decl_kinds.recursivity_kind = | Finite | CoFinite @@ -2388,7 +2390,7 @@ sig | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * inline * (plident list * Constrexpr.constr_expr) with_coercion list - | VernacInductive of Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list + | VernacInductive of Decl_kinds.cumulative_inductive_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of @@ -4743,7 +4745,9 @@ sig type one_inductive_impls = Command.one_inductive_impls val do_mutual_inductive : - (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> Decl_kinds.polymorphic -> + (Vernacexpr.one_inductive_expr * Vernacexpr.decl_notation list) list -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> unit val do_definition : Names.Id.t -> Decl_kinds.definition_kind -> Vernacexpr.lident list option -> @@ -4767,7 +4771,9 @@ sig structured_inductive_expr * Libnames.qualid list * Vernacexpr.decl_notation list val interp_mutual_inductive : - structured_inductive_expr -> Vernacexpr.decl_notation list -> Decl_kinds.polymorphic -> + structured_inductive_expr -> Vernacexpr.decl_notation list -> + Decl_kinds.cumulative_inductive_flag -> + Decl_kinds.polymorphic -> Decl_kinds.private_flag -> Decl_kinds.recursivity_kind -> Entries.mutual_inductive_entry * Universes.universe_binders * one_inductive_impls list -- cgit v1.2.3 From ff918e4bb0ae23566e038f4b55d84dd2c343f95e Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Thu, 1 Jun 2017 16:18:19 +0200 Subject: Clean up universes of constants and inductives --- API/API.mli | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index a993b0277c..ecce22c1de 100644 --- a/API/API.mli +++ b/API/API.mli @@ -84,9 +84,11 @@ sig end type universe_context = UContext.t - [@@ocaml.deprecated "alias of API.Names.UContext.t"] + [@@ocaml.deprecated "alias of API.Univ.UContext.t"] - type universe_info_ind = Univ.UInfoInd.t + type abstract_universe_context = Univ.AUContext.t + type cumulativity_info = Univ.CumulativityInfo.t + type abstract_cumulativity_info = Univ.ACumulativityInfo.t module LSet : module type of struct include Univ.LSet end module ContextSet : @@ -1047,12 +1049,12 @@ sig proj_body : Term.constr; } type typing_flags = Declarations.typing_flags + type constant_body = Declarations.constant_body = { const_hyps : Context.Named.t; const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; - const_polymorphic : bool; const_universes : constant_universes; const_proj : projection_body option; const_inline_code : bool; @@ -1085,6 +1087,13 @@ sig | MEident of Names.ModPath.t | MEapply of module_alg_expr * Names.ModPath.t | MEwith of module_alg_expr * with_declaration + + type abstrac_inductive_universes = Declarations.abstrac_inductive_universes = + | Monomorphic_ind of Univ.UContext.t + | Polymorphic_ind of Univ.abstract_universe_context + | Cumulative_ind of Univ.abstract_cumulativity_info + + type mutual_inductive_body = Declarations.mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : Declarations.record_body option; @@ -1094,9 +1103,7 @@ sig mind_nparams : int; mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; - mind_polymorphic : bool; - mind_cumulative : bool; - mind_universes : Univ.universe_info_ind; + mind_universes : abstrac_inductive_universes; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } -- cgit v1.2.3 From a4969591f391d857a9efd038338e1a80fc68950b Mon Sep 17 00:00:00 2001 From: Amin Timany Date: Wed, 14 Jun 2017 16:32:47 +0200 Subject: A short cleanup --- API/API.mli | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index ecce22c1de..899bafa1fd 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1088,12 +1088,11 @@ sig | MEapply of module_alg_expr * Names.ModPath.t | MEwith of module_alg_expr * with_declaration - type abstrac_inductive_universes = Declarations.abstrac_inductive_universes = + type abstract_inductive_universes = Declarations.abstract_inductive_universes = | Monomorphic_ind of Univ.UContext.t | Polymorphic_ind of Univ.abstract_universe_context | Cumulative_ind of Univ.abstract_cumulativity_info - type mutual_inductive_body = Declarations.mutual_inductive_body = { mind_packets : one_inductive_body array; mind_record : Declarations.record_body option; @@ -1103,7 +1102,7 @@ sig mind_nparams : int; mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; - mind_universes : abstrac_inductive_universes; + mind_universes : Declarations.abstract_inductive_universes; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } -- cgit v1.2.3 From 0437339ccac602d692b5b8c071b77ac756805520 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 15 Jun 2017 16:41:09 +0200 Subject: Removing Proof_type from the API. Unluckily, this forces replacing a lot of code in plugins, because the API defined the type of goals and tactics in Proof_type, and by the no-alias rule, this was the only one. But Proof_type was already implicitly deprecated, so that the API should have relied on Tacmach instead. --- API/API.ml | 13 -------- API/API.mli | 101 ++++++++++++++++++++++++++---------------------------------- 2 files changed, 44 insertions(+), 70 deletions(-) (limited to 'API') diff --git a/API/API.ml b/API/API.ml index 2b7bbd561b..60703e1fa8 100644 --- a/API/API.ml +++ b/API/API.ml @@ -200,16 +200,3 @@ module Entries = | ParameterEntry of parameter_entry | ProjectionEntry of projection_entry end - -(* NOTE: It does not make sense to replace the following "module expression" - simply with "module Proof_type = Proof_type" because - there is only "proofs/proof_type.mli"; - there is no "proofs/proof_type.ml" file *) -module Proof_type = - struct - type goal = Goal.goal - type tactic = goal Evd.sigma -> goal list Evd.sigma - type rule = Proof_type.prim_rule = - | Cut of bool * bool * Names.Id.t * Term.types - | Refine of Term.constr - end diff --git a/API/API.mli b/API/API.mli index 69278e7c9f..9ed952dc2f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -3310,17 +3310,6 @@ sig val module_is_known : string -> bool end -(* All items in the Proof_type module are deprecated. *) -module Proof_type : -sig - type goal = Evar.t - type rule = Proof_type.prim_rule = - | Cut of bool * bool * Names.Id.t * Term.types - | Refine of Term.constr - - type tactic = goal Evd.sigma -> goal list Evd.sigma -end - module Redexpr : sig type red_expr = @@ -3332,61 +3321,61 @@ end module Tacmach : sig - type tactic = Proof_type.tactic - [@@ocaml.deprecated "alias for API.Proof_type.tactic"] + type tactic = Goal.goal Evd.sigma -> Goal.goal list Evd.sigma type 'a sigma = 'a Evd.sigma [@@ocaml.deprecated "alias of API.Evd.sigma"] val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma - val pf_reduction_of_red_expr : Proof_type.goal Evd.sigma -> Redexpr.red_expr -> EConstr.constr -> Evd.evar_map * EConstr.constr + val pf_reduction_of_red_expr : Goal.goal Evd.sigma -> Redexpr.red_expr -> EConstr.constr -> Evd.evar_map * EConstr.constr - val pf_unsafe_type_of : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.types + val pf_unsafe_type_of : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.types - val pf_get_new_id : Names.Id.t -> Proof_type.goal Evd.sigma -> Names.Id.t + val pf_get_new_id : Names.Id.t -> Goal.goal Evd.sigma -> Names.Id.t - val pf_env : Proof_type.goal Evd.sigma -> Environ.env + val pf_env : Goal.goal Evd.sigma -> Environ.env - val pf_concl : Proof_type.goal Evd.sigma -> EConstr.types + val pf_concl : Goal.goal Evd.sigma -> EConstr.types - val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Proof_type.goal Evd.sigma -> 'a + val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> Goal.goal Evd.sigma -> 'a - val pf_get_hyp : Proof_type.goal Evd.sigma -> Names.Id.t -> EConstr.named_declaration - val pf_get_hyp_typ : Proof_type.goal Evd.sigma -> Names.Id.t -> EConstr.types - val project : Proof_type.goal Evd.sigma -> Evd.evar_map - val refine : EConstr.constr -> Proof_type.tactic - val pf_type_of : Proof_type.goal Evd.sigma -> EConstr.constr -> Evd.evar_map * EConstr.types + val pf_get_hyp : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.named_declaration + val pf_get_hyp_typ : Goal.goal Evd.sigma -> Names.Id.t -> EConstr.types + val project : Goal.goal Evd.sigma -> Evd.evar_map + val refine : EConstr.constr -> tactic + val refine_no_check : EConstr.constr -> tactic + val pf_type_of : Goal.goal Evd.sigma -> EConstr.constr -> Evd.evar_map * EConstr.types - val pf_hyps : Proof_type.goal Evd.sigma -> EConstr.named_context + val pf_hyps : Goal.goal Evd.sigma -> EConstr.named_context - val pf_ids_of_hyps : Proof_type.goal Evd.sigma -> Names.Id.t list + val pf_ids_of_hyps : Goal.goal Evd.sigma -> Names.Id.t list - val pf_reduce_to_atomic_ind : Proof_type.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types + val pf_reduce_to_atomic_ind : Goal.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types - val pf_reduce_to_quantified_ind : Proof_type.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types + val pf_reduce_to_quantified_ind : Goal.goal Evd.sigma -> EConstr.types -> (Names.inductive * EConstr.EInstance.t) * EConstr.types val pf_eapply : (Environ.env -> Evd.evar_map -> 'a -> Evd.evar_map * 'b) -> Evar.t Evd.sigma -> 'a -> Evar.t Evd.sigma * 'b val pf_unfoldn : (Locus.occurrences * Names.evaluable_global_reference) list - -> Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr + -> Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr - val pf_reduce : (Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr) -> Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr + val pf_reduce : (Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr) -> Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr - val pf_conv_x : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool + val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool - val pf_is_matching : Proof_type.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool + val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool - val pf_hyps_types : Proof_type.goal Evd.sigma -> (Names.Id.t * EConstr.types) list + val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list - val pr_gls : Proof_type.goal Evd.sigma -> Pp.std_ppcmds + val pr_gls : Goal.goal Evd.sigma -> Pp.std_ppcmds - val pf_nf_betaiota : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr + val pf_nf_betaiota : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr - val pf_last_hyp : Proof_type.goal Evd.sigma -> EConstr.named_declaration + val pf_last_hyp : Goal.goal Evd.sigma -> EConstr.named_declaration - val pf_nth_hyp_id : Proof_type.goal Evd.sigma -> int -> Names.Id.t + val pf_nth_hyp_id : Goal.goal Evd.sigma -> int -> Names.Id.t val sig_it : 'a Evd.sigma -> 'a @@ -3395,7 +3384,7 @@ sig val pf_apply : (Environ.env -> Evd.evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a val project : 'a Proofview.Goal.t -> Evd.evar_map val pf_unsafe_type_of : 'a Proofview.Goal.t -> EConstr.constr -> EConstr.types - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a + val of_old : (Goal.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a val pf_env : 'a Proofview.Goal.t -> Environ.env val pf_ids_of_hyps : 'a Proofview.Goal.t -> Names.Id.t list @@ -3516,21 +3505,19 @@ sig val repackage : Evd.evar_map ref -> 'a -> 'a Evd.sigma - val refiner : Proof_type.rule -> Proof_type.tactic - - val tclSHOWHYPS : Proof_type.tactic -> Proof_type.tactic + val tclSHOWHYPS : Tacmach.tactic -> Tacmach.tactic exception FailError of int * Pp.std_ppcmds Lazy.t - val tclEVARS : Evd.evar_map -> Proof_type.tactic - val tclMAP : ('a -> Proof_type.tactic) -> 'a list -> Proof_type.tactic - val tclREPEAT : Proof_type.tactic -> Proof_type.tactic - val tclORELSE : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic - val tclFAIL : int -> Pp.std_ppcmds -> Proof_type.tactic - val tclIDTAC : Proof_type.tactic - val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic - val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic - val tclTRY : Proof_type.tactic -> Proof_type.tactic - val tclAT_LEAST_ONCE : Proof_type.tactic -> Proof_type.tactic + val tclEVARS : Evd.evar_map -> Tacmach.tactic + val tclMAP : ('a -> Tacmach.tactic) -> 'a list -> Tacmach.tactic + val tclREPEAT : Tacmach.tactic -> Tacmach.tactic + val tclORELSE : Tacmach.tactic -> Tacmach.tactic -> Tacmach.tactic + val tclFAIL : int -> Pp.std_ppcmds -> Tacmach.tactic + val tclIDTAC : Tacmach.tactic + val tclTHEN : Tacmach.tactic -> Tacmach.tactic -> Tacmach.tactic + val tclTHENLIST : Tacmach.tactic list -> Tacmach.tactic + val tclTRY : Tacmach.tactic -> Tacmach.tactic + val tclAT_LEAST_ONCE : Tacmach.tactic -> Tacmach.tactic end module Termops : @@ -3668,7 +3655,7 @@ module Printer : sig val pr_named_context : Environ.env -> Evd.evar_map -> Context.Named.t -> Pp.std_ppcmds val pr_rel_context : Environ.env -> Evd.evar_map -> Context.Rel.t -> Pp.std_ppcmds - val pr_goal : Proof_type.goal Evd.sigma -> Pp.std_ppcmds + val pr_goal : Goal.goal Evd.sigma -> Pp.std_ppcmds val pr_constr_env : Prelude.env -> Prelude.evar_map -> Term.constr -> Pp.std_ppcmds val pr_lconstr_env : Prelude.env -> Prelude.evar_map -> Term.constr -> Pp.std_ppcmds @@ -4124,7 +4111,7 @@ end module Tacticals : sig - open Proof_type + open Tacmach val tclORELSE : tactic -> tactic -> tactic val tclDO : int -> tactic -> tactic val tclIDTAC : tactic @@ -4132,7 +4119,7 @@ sig val tclTHEN : tactic -> tactic -> tactic val tclTHENLIST : tactic list -> tactic val pf_constr_of_global : - Globnames.global_reference -> (EConstr.constr -> Proof_type.tactic) -> Proof_type.tactic + Globnames.global_reference -> (EConstr.constr -> Tacmach.tactic) -> Tacmach.tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic val tclTRY : tactic -> tactic val tclCOMPLETE : tactic -> tactic @@ -4153,13 +4140,13 @@ sig val tclTHENSEQ : tactic list -> tactic [@@ocaml.deprecated "alias of API.Tacticals.tclTHENLIST"] - val nLastDecls : int -> Proof_type.goal Evd.sigma -> EConstr.named_context + val nLastDecls : int -> Goal.goal Evd.sigma -> EConstr.named_context val tclTHEN_i : tactic -> (int -> tactic) -> tactic val tclPROGRESS : tactic -> tactic - val elimination_sort_of_goal : Proof_type.goal Evd.sigma -> Sorts.family + val elimination_sort_of_goal : Goal.goal Evd.sigma -> Sorts.family module New : sig @@ -4539,7 +4526,7 @@ sig val autounfold_tac : Hints.hint_db_name list option -> Locus.clause -> unit Proofview.tactic val autounfold_one : Hints.hint_db_name list -> Locus.hyp_location option -> unit Proofview.tactic val eauto_with_bases : - ?debug:Hints.debug -> bool * int -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> Proof_type.tactic + ?debug:Hints.debug -> bool * int -> Tactypes.delayed_open_constr list -> Hints.hint_db list -> Tacmach.tactic end module Class_tactics : -- cgit v1.2.3 From d8874dd855d748aaaf504890487ab15ffd7a677d Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 12 Jun 2017 11:41:40 +0200 Subject: [ide] Add route_id parameter to query call. This is necessary in order for clients to identify the results of queries. This is a minor breaking change of the protocol, affecting only this particular call. This change is necessary in order to fix bug ####. --- API/API.mli | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 69278e7c9f..b5928c023d 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2266,10 +2266,9 @@ sig | VtQed of vernac_qed_type | VtProofStep of proof_step | VtProofMode of string - | VtQuery of vernac_part_of_script * report_with + | VtQuery of vernac_part_of_script * Feedback.route_id | VtStm of vernac_control * vernac_part_of_script | VtUnknown - and report_with = Stateid.t * Feedback.route_id and vernac_qed_type = Vernacexpr.vernac_qed_type = | VtKeep | VtKeepAsAxiom -- cgit v1.2.3 From 94e0cbc26718fe3fecc58f6f8673f5f8abb0ce31 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 21 Jun 2017 15:12:21 +0200 Subject: [vernac] Remove stale bool parameter from `VernacStartTheoremProof` `VernacStartTheoremProof` contained a stale bool parameter from 15 years ago, which is unused today. --- API/API.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'API') diff --git a/API/API.mli b/API/API.mli index 1e078bb77e..9f13f51fce 100644 --- a/API/API.mli +++ b/API/API.mli @@ -2407,7 +2407,7 @@ sig | VernacNotationAddFormat of string * string * string | VernacDefinition of (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * plident * definition_expr - | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list * bool + | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of Constrexpr.constr_expr | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * -- cgit v1.2.3