diff options
42 files changed, 497 insertions, 591 deletions
diff --git a/.gitlab-ci.yml b/.gitlab-ci.yml index 1814aaff1..1742660c8 100644 --- a/.gitlab-ci.yml +++ b/.gitlab-ci.yml @@ -314,6 +314,9 @@ ci-hott: ci-iris-lambda-rust: <<: *ci-template +ci-ltac2: + <<: *ci-template + ci-math-classes: <<: *ci-template diff --git a/.travis.yml b/.travis.yml index 3b90f7cf4..7d7a08161 100644 --- a/.travis.yml +++ b/.travis.yml @@ -53,6 +53,7 @@ env: - TEST_TARGET="ci-formal-topology TIMED=1" - TEST_TARGET="ci-hott TIMED=1" - TEST_TARGET="ci-iris-lambda-rust TIMED=1" + - TEST_TARGET="ci-ltac2 TIMED=1" - TEST_TARGET="ci-math-classes TIMED=1" - TEST_TARGET="ci-math-comp TIMED=1" - TEST_TARGET="ci-sf TIMED=1" diff --git a/API/API.ml b/API/API.ml index 6e61063e4..9a67e3111 100644 --- a/API/API.ml +++ b/API/API.ml @@ -80,6 +80,7 @@ module Locus = Locus module Glob_term = Glob_term module Extend = Extend module Misctypes = Misctypes +module Pattern = Pattern module Decl_kinds = Decl_kinds module Vernacexpr = Vernacexpr module Notation_term = Notation_term @@ -118,8 +119,6 @@ module Universes = Universes module UState = UState module Evd = Evd module EConstr = EConstr -module Tactypes = Tactypes -module Pattern = Pattern module Namegen = Namegen module Termops = Termops module Proofview_monad = Proofview_monad @@ -167,6 +166,7 @@ module Univdecls = Univdecls (******************************************************************************) (* interp *) (******************************************************************************) +module Tactypes = Tactypes module Stdarg = Stdarg module Genintern = Genintern module Constrexpr_ops = Constrexpr_ops diff --git a/API/API.mli b/API/API.mli index 065caeac3..d0564f9ec 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1897,6 +1897,328 @@ sig val is_global : global_reference -> Constr.t -> bool end +(******************************************************************************) +(* XXX: Moved from intf *) +(******************************************************************************) +module Pattern : +sig + + type case_info_pattern = + { cip_style : Misctypes.case_style; + cip_ind : Names.inductive option; + cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) + cip_extensible : bool (** does this match end with _ => _ ? *) } + + type constr_pattern = + | PRef of Globnames.global_reference + | PVar of Names.Id.t + | PEvar of Evar.t * constr_pattern array + | PRel of int + | PApp of constr_pattern * constr_pattern array + | PSoApp of Names.Id.t * constr_pattern list + | PProj of Names.Projection.t * constr_pattern + | PLambda of Names.Name.t * constr_pattern * constr_pattern + | PProd of Names.Name.t * constr_pattern * constr_pattern + | PLetIn of Names.Name.t * constr_pattern * constr_pattern option * constr_pattern + | PSort of Misctypes.glob_sort + | PMeta of Names.Id.t option + | PIf of constr_pattern * constr_pattern * constr_pattern + | PCase of case_info_pattern * constr_pattern * constr_pattern * + (int * bool list * constr_pattern) list (** index of constructor, nb of args *) + | PFix of Term.fixpoint + | PCoFix of Term.cofixpoint + +end + +module Evar_kinds : +sig + type obligation_definition_status = + | Define of bool + | Expand + + type matching_var_kind = + | FirstOrderPatVar of Names.Id.t + | SecondOrderPatVar of Names.Id.t + + type t = + | ImplicitArg of Globnames.global_reference * (int * Names.Id.t option) + * bool (** Force inference *) + | BinderType of Names.Name.t + | NamedHole of Names.Id.t (* coming from some ?[id] syntax *) + | QuestionMark of obligation_definition_status * Names.Name.t + | CasesType of bool (* true = a subterm of the type *) + | InternalHole + | TomatchTypeParameter of Names.inductive * int + | GoalEvar + | ImpossibleCase + | MatchingVar of matching_var_kind + | VarInstance of Names.Id.t + | SubEvar of Constr.existential_key +end + +module Glob_term : +sig + type 'a cases_pattern_r = + | PatVar of Names.Name.t + | PatCstr of Names.constructor * 'a cases_pattern_g list * Names.Name.t + and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t + type cases_pattern = [ `any ] cases_pattern_g + type existential_name = Names.Id.t + type 'a glob_constr_r = + | GRef of Globnames.global_reference * Misctypes.glob_level list option + (** An identifier that represents a reference to an object defined + either in the (global) environment or in the (local) context. *) + | GVar of Names.Id.t + (** An identifier that cannot be regarded as "GRef". + Bound variables are typically represented this way. *) + | GEvar of existential_name * (Names.Id.t * 'a glob_constr_g) list + | GPatVar of Evar_kinds.matching_var_kind + | GApp of 'a glob_constr_g * 'a glob_constr_g list + | GLambda of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GProd of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g + | GLetIn of Names.Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g + | GCases of Term.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g + | GLetTuple of Names.Name.t list * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GIf of 'a glob_constr_g * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g + | GRec of 'a fix_kind_g * Names.Id.t array * 'a glob_decl_g list array * + 'a glob_constr_g array * 'a glob_constr_g array + | GSort of Misctypes.glob_sort + | GHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option + | GCast of 'a glob_constr_g * 'a glob_constr_g Misctypes.cast_type + + and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t + + and 'a glob_decl_g = Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g option * 'a glob_constr_g + + and 'a fix_recursion_order_g = + | GStructRec + | GWfRec of 'a glob_constr_g + | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option + + and 'a fix_kind_g = + | GFix of ((int option * 'a fix_recursion_order_g) array * int) + | GCoFix of int + + and 'a predicate_pattern_g = + Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located option + + and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) + + and 'a tomatch_tuples_g = 'a tomatch_tuple_g list + + and 'a cases_clause_g = (Names.Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located + and 'a cases_clauses_g = 'a cases_clause_g list + + type glob_constr = [ `any ] glob_constr_g + type tomatch_tuple = [ `any ] tomatch_tuple_g + type tomatch_tuples = [ `any ] tomatch_tuples_g + type cases_clause = [ `any ] cases_clause_g + type cases_clauses = [ `any ] cases_clauses_g + type glob_decl = [ `any ] glob_decl_g + type fix_kind = [ `any ] fix_kind_g + type predicate_pattern = [ `any ] predicate_pattern_g + type any_glob_constr = + | AnyGlobConstr : 'r glob_constr_g -> any_glob_constr + +end + +module Notation_term : +sig + type scope_name = string + type notation_var_instance_type = + | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList + type tmp_scope_name = scope_name + + type subscopes = tmp_scope_name option * scope_name list + type notation_constr = + | NRef of Globnames.global_reference + | NVar of Names.Id.t + | NApp of notation_constr * notation_constr list + | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option + | NList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool + | NLambda of Names.Name.t * notation_constr * notation_constr + | NProd of Names.Name.t * notation_constr * notation_constr + | NBinderList of Names.Id.t * Names.Id.t * notation_constr * notation_constr + | NLetIn of Names.Name.t * notation_constr * notation_constr option * notation_constr + | NCases of Term.case_style * notation_constr option * + (notation_constr * (Names.Name.t * (Names.inductive * Names.Name.t list) option)) list * + (Glob_term.cases_pattern list * notation_constr) list + | NLetTuple of Names.Name.t list * (Names.Name.t * notation_constr option) * + notation_constr * notation_constr + | NIf of notation_constr * (Names.Name.t * notation_constr option) * + notation_constr * notation_constr + | NRec of Glob_term.fix_kind * Names.Id.t array * + (Names.Name.t * notation_constr option * notation_constr) list array * + notation_constr array * notation_constr array + | NSort of Misctypes.glob_sort + | NCast of notation_constr * notation_constr Misctypes.cast_type + type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list * + notation_constr + type precedence = int + type parenRelation = + | L | E | Any | Prec of precedence + type tolerability = precedence * parenRelation +end + +module Constrexpr : +sig + + type binder_kind = + | Default of Decl_kinds.binding_kind + | Generalized of Decl_kinds.binding_kind * Decl_kinds.binding_kind * bool + + type explicitation = + | ExplByPos of int * Names.Id.t option + | ExplByName of Names.Id.t + type sign = bool + type raw_natural_number = string + type prim_token = + | Numeral of raw_natural_number * sign + | String of string + + type notation = string + type instance_expr = Misctypes.glob_level list + type proj_flag = int option + type abstraction_kind = + | AbsLambda + | AbsPi + + type cases_pattern_expr_r = + | CPatAlias of cases_pattern_expr * Names.Id.t + | CPatCstr of Libnames.reference + * cases_pattern_expr list option * cases_pattern_expr list + (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) + | CPatAtom of Libnames.reference option + | CPatOr of cases_pattern_expr list + | CPatNotation of notation * cases_pattern_notation_substitution + * cases_pattern_expr list + | CPatPrim of prim_token + | CPatRecord of (Libnames.reference * cases_pattern_expr) list + | CPatDelimiters of string * cases_pattern_expr + | CPatCast of cases_pattern_expr * constr_expr + and cases_pattern_expr = cases_pattern_expr_r CAst.t + + and cases_pattern_notation_substitution = + cases_pattern_expr list * cases_pattern_expr list list + + and constr_expr_r = + | CRef of Libnames.reference * instance_expr option + | CFix of Names.Id.t Loc.located * fix_expr list + | CCoFix of Names.Id.t Loc.located * cofix_expr list + | CProdN of binder_expr list * constr_expr + | CLambdaN of binder_expr list * constr_expr + | CLetIn of Names.Name.t Loc.located * constr_expr * constr_expr option * constr_expr + | CAppExpl of (proj_flag * Libnames.reference * instance_expr option) * constr_expr list + | CApp of (proj_flag * constr_expr) * + (constr_expr * explicitation Loc.located option) list + | CRecord of (Libnames.reference * constr_expr) list + | CCases of Term.case_style + * constr_expr option + * case_expr list + * branch_expr list + | CLetTuple of Names.Name.t Loc.located list * (Names.Name.t Loc.located option * constr_expr option) * + constr_expr * constr_expr + | CIf of constr_expr * (Names.Name.t Loc.located option * constr_expr option) + * constr_expr * constr_expr + | CHole of Evar_kinds.t option * Misctypes.intro_pattern_naming_expr * Genarg.raw_generic_argument option + | CPatVar of Names.Id.t + | CEvar of Names.Id.t * (Names.Id.t * constr_expr) list + | CSort of Misctypes.glob_sort + | CCast of constr_expr * constr_expr Misctypes.cast_type + | CNotation of notation * constr_notation_substitution + | CGeneralization of Decl_kinds.binding_kind * abstraction_kind option * constr_expr + | CPrim of prim_token + | CDelimiters of string * constr_expr + and constr_expr = constr_expr_r CAst.t + + and case_expr = constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option + + and branch_expr = + (cases_pattern_expr list Loc.located list * constr_expr) Loc.located + + and binder_expr = + Names.Name.t Loc.located list * binder_kind * constr_expr + + and fix_expr = + Names.Id.t Loc.located * (Names.Id.t Loc.located option * recursion_order_expr) * + local_binder_expr list * constr_expr * constr_expr + + and cofix_expr = + Names.Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr + + and recursion_order_expr = + | CStructRec + | CWfRec of constr_expr + | CMeasureRec of constr_expr * constr_expr option + + and local_binder_expr = + | CLocalAssum of Names.Name.t Loc.located list * binder_kind * constr_expr + | CLocalDef of Names.Name.t Loc.located * constr_expr * constr_expr option + | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located + + and constr_notation_substitution = + constr_expr list * + constr_expr list list * + local_binder_expr list list + + type constr_pattern_expr = constr_expr +end + +module Genredexpr : +sig + + (** The parsing produces initially a list of [red_atom] *) + type 'a red_atom = + | FBeta + | FMatch + | FFix + | FCofix + | FZeta + | FConst of 'a list + | FDeltaBut of 'a list + + (** This list of atoms is immediately converted to a [glob_red_flag] *) + type 'a glob_red_flag = { + rBeta : bool; + rMatch : bool; + rFix : bool; + rCofix : bool; + rZeta : bool; + rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) + rConst : 'a list + } + + (** Generic kinds of reductions *) + type ('a,'b,'c) red_expr_gen = + | Red of bool + | Hnf + | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option + | Cbv of 'b glob_red_flag + | Cbn of 'b glob_red_flag + | Lazy of 'b glob_red_flag + | Unfold of 'b Locus.with_occurrences list + | Fold of 'a list + | Pattern of 'a Locus.with_occurrences list + | ExtraRedExpr of string + | CbvVm of ('b,'c) Util.union Locus.with_occurrences option + | CbvNative of ('b,'c) Util.union Locus.with_occurrences option + + type ('a,'b,'c) may_eval = + | ConstrTerm of 'a + | ConstrEval of ('a,'b,'c) red_expr_gen * 'a + | ConstrContext of Names.Id.t Loc.located * 'a + | ConstrTypeOf of 'a + + type r_trm = Constrexpr.constr_expr + type r_pat = Constrexpr.constr_pattern_expr + type r_cst = Libnames.reference Misctypes.or_by_notation + type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen +end + +(******************************************************************************) +(* XXX: end of moved from intf *) +(******************************************************************************) + module Libobject : sig type obj @@ -2133,7 +2455,6 @@ sig elim : Globnames.global_reference; intro : Globnames.global_reference; typ : Globnames.global_reference } - val gen_reference : string -> string list -> string -> Globnames.global_reference val find_reference : string -> string list -> string -> Globnames.global_reference val check_required_library : string list -> unit val logic_module_name : string list @@ -2215,33 +2536,6 @@ sig end -(* XXX: Moved from intf *) -module Evar_kinds : -sig - type obligation_definition_status = - | Define of bool - | Expand - - type matching_var_kind = - | FirstOrderPatVar of Names.Id.t - | SecondOrderPatVar of Names.Id.t - - type t = - | ImplicitArg of Globnames.global_reference * (int * Names.Id.t option) - * bool (** Force inference *) - | BinderType of Names.Name.t - | NamedHole of Names.Id.t (* coming from some ?[id] syntax *) - | QuestionMark of obligation_definition_status * Names.Name.t - | CasesType of bool (* true = a subterm of the type *) - | InternalHole - | TomatchTypeParameter of Names.inductive * int - | GoalEvar - | ImpossibleCase - | MatchingVar of matching_var_kind - | VarInstance of Names.Id.t - | SubEvar of Constr.existential_key -end - module Evd : sig @@ -2413,164 +2707,6 @@ sig val fresh_sort_in_family : ?loc:Loc.t -> ?rigid:rigid -> Environ.env -> evar_map -> Sorts.family -> evar_map * Sorts.t end -(* XXX: moved from intf *) -module Constrexpr : -sig - - type binder_kind = - | Default of Decl_kinds.binding_kind - | Generalized of Decl_kinds.binding_kind * Decl_kinds.binding_kind * bool - - type explicitation = - | ExplByPos of int * Names.Id.t option - | ExplByName of Names.Id.t - type sign = bool - type raw_natural_number = string - type prim_token = - | Numeral of raw_natural_number * sign - | String of string - - type notation = string - type instance_expr = Misctypes.glob_level list - type proj_flag = int option - type abstraction_kind = - | AbsLambda - | AbsPi - - type cases_pattern_expr_r = - | CPatAlias of cases_pattern_expr * Names.Id.t - | CPatCstr of Libnames.reference - * cases_pattern_expr list option * cases_pattern_expr list - (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) - | CPatAtom of Libnames.reference option - | CPatOr of cases_pattern_expr list - | CPatNotation of notation * cases_pattern_notation_substitution - * cases_pattern_expr list - | CPatPrim of prim_token - | CPatRecord of (Libnames.reference * cases_pattern_expr) list - | CPatDelimiters of string * cases_pattern_expr - | CPatCast of cases_pattern_expr * constr_expr - and cases_pattern_expr = cases_pattern_expr_r CAst.t - - and cases_pattern_notation_substitution = - cases_pattern_expr list * cases_pattern_expr list list - - and constr_expr_r = - | CRef of Libnames.reference * instance_expr option - | CFix of Names.Id.t Loc.located * fix_expr list - | CCoFix of Names.Id.t Loc.located * cofix_expr list - | CProdN of binder_expr list * constr_expr - | CLambdaN of binder_expr list * constr_expr - | CLetIn of Names.Name.t Loc.located * constr_expr * constr_expr option * constr_expr - | CAppExpl of (proj_flag * Libnames.reference * instance_expr option) * constr_expr list - | CApp of (proj_flag * constr_expr) * - (constr_expr * explicitation Loc.located option) list - | CRecord of (Libnames.reference * constr_expr) list - | CCases of Term.case_style - * constr_expr option - * case_expr list - * branch_expr list - | CLetTuple of Names.Name.t Loc.located list * (Names.Name.t Loc.located option * constr_expr option) * - constr_expr * constr_expr - | CIf of constr_expr * (Names.Name.t Loc.located option * constr_expr option) - * constr_expr * constr_expr - | CHole of Evar_kinds.t option * Misctypes.intro_pattern_naming_expr * Genarg.raw_generic_argument option - | CPatVar of Names.Id.t - | CEvar of Names.Id.t * (Names.Id.t * constr_expr) list - | CSort of Misctypes.glob_sort - | CCast of constr_expr * constr_expr Misctypes.cast_type - | CNotation of notation * constr_notation_substitution - | CGeneralization of Decl_kinds.binding_kind * abstraction_kind option * constr_expr - | CPrim of prim_token - | CDelimiters of string * constr_expr - and constr_expr = constr_expr_r CAst.t - - and case_expr = constr_expr * Names.Name.t Loc.located option * cases_pattern_expr option - - and branch_expr = - (cases_pattern_expr list Loc.located list * constr_expr) Loc.located - - and binder_expr = - Names.Name.t Loc.located list * binder_kind * constr_expr - - and fix_expr = - Names.Id.t Loc.located * (Names.Id.t Loc.located option * recursion_order_expr) * - local_binder_expr list * constr_expr * constr_expr - - and cofix_expr = - Names.Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr - - and recursion_order_expr = - | CStructRec - | CWfRec of constr_expr - | CMeasureRec of constr_expr * constr_expr option - - and local_binder_expr = - | CLocalAssum of Names.Name.t Loc.located list * binder_kind * constr_expr - | CLocalDef of Names.Name.t Loc.located * constr_expr * constr_expr option - | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located - - and constr_notation_substitution = - constr_expr list * - constr_expr list list * - local_binder_expr list list - - type constr_pattern_expr = constr_expr -end - -module Genredexpr : -sig - - (** The parsing produces initially a list of [red_atom] *) - type 'a red_atom = - | FBeta - | FMatch - | FFix - | FCofix - | FZeta - | FConst of 'a list - | FDeltaBut of 'a list - - (** This list of atoms is immediately converted to a [glob_red_flag] *) - type 'a glob_red_flag = { - rBeta : bool; - rMatch : bool; - rFix : bool; - rCofix : bool; - rZeta : bool; - rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) - rConst : 'a list - } - - (** Generic kinds of reductions *) - type ('a,'b,'c) red_expr_gen = - | Red of bool - | Hnf - | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option - | Cbv of 'b glob_red_flag - | Cbn of 'b glob_red_flag - | Lazy of 'b glob_red_flag - | Unfold of 'b Locus.with_occurrences list - | Fold of 'a list - | Pattern of 'a Locus.with_occurrences list - | ExtraRedExpr of string - | CbvVm of ('b,'c) Util.union Locus.with_occurrences option - | CbvNative of ('b,'c) Util.union Locus.with_occurrences option - - type ('a,'b,'c) may_eval = - | ConstrTerm of 'a - | ConstrEval of ('a,'b,'c) red_expr_gen * 'a - | ConstrContext of Names.Id.t Loc.located * 'a - | ConstrTypeOf of 'a - - type r_trm = Constrexpr.constr_expr - type r_pat = Constrexpr.constr_pattern_expr - type r_cst = Libnames.reference Misctypes.or_by_notation - type raw_red_expr = (r_trm, r_cst, r_pat) red_expr_gen -end - -(* XXX: end of moved from intf *) - module EConstr : sig type t @@ -2739,37 +2875,6 @@ sig val isLambda : Evd.evar_map -> t -> bool end -(* XXX: Located manually from intf *) -module Pattern : -sig - - type case_info_pattern = - { cip_style : Misctypes.case_style; - cip_ind : Names.inductive option; - cip_ind_tags : bool list option; (** indicates LetIn/Lambda in arity *) - cip_extensible : bool (** does this match end with _ => _ ? *) } - - type constr_pattern = - | PRef of Globnames.global_reference - | PVar of Names.Id.t - | PEvar of Evar.t * constr_pattern array - | PRel of int - | PApp of constr_pattern * constr_pattern array - | PSoApp of Names.Id.t * constr_pattern list - | PProj of Names.Projection.t * constr_pattern - | PLambda of Names.Name.t * constr_pattern * constr_pattern - | PProd of Names.Name.t * constr_pattern * constr_pattern - | PLetIn of Names.Name.t * constr_pattern * constr_pattern option * constr_pattern - | PSort of Misctypes.glob_sort - | PMeta of Names.Id.t option - | PIf of constr_pattern * constr_pattern * constr_pattern - | PCase of case_info_pattern * constr_pattern * constr_pattern * - (int * bool list * constr_pattern) list (** index of constructor, nb of args *) - | PFix of Term.fixpoint - | PCoFix of Term.cofixpoint - -end - module Namegen : sig (** *) @@ -3124,126 +3229,6 @@ sig val interp : ('raw, 'glb, 'top) Genarg.genarg_type -> ('glb, Val.t) interp_fun end -(* XXX: Located manually from intf *) -module Glob_term : -sig - type 'a cases_pattern_r = - | PatVar of Names.Name.t - | PatCstr of Names.constructor * 'a cases_pattern_g list * Names.Name.t - and 'a cases_pattern_g = ('a cases_pattern_r, 'a) DAst.t - type cases_pattern = [ `any ] cases_pattern_g - type existential_name = Names.Id.t - type 'a glob_constr_r = - | GRef of Globnames.global_reference * Misctypes.glob_level list option - (** An identifier that represents a reference to an object defined - either in the (global) environment or in the (local) context. *) - | GVar of Names.Id.t - (** An identifier that cannot be regarded as "GRef". - Bound variables are typically represented this way. *) - | GEvar of existential_name * (Names.Id.t * 'a glob_constr_g) list - | GPatVar of Evar_kinds.matching_var_kind - | GApp of 'a glob_constr_g * 'a glob_constr_g list - | GLambda of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g - | GProd of Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g * 'a glob_constr_g - | GLetIn of Names.Name.t * 'a glob_constr_g * 'a glob_constr_g option * 'a glob_constr_g - | GCases of Term.case_style * 'a glob_constr_g option * 'a tomatch_tuples_g * 'a cases_clauses_g - | GLetTuple of Names.Name.t list * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g - | GIf of 'a glob_constr_g * (Names.Name.t * 'a glob_constr_g option) * 'a glob_constr_g * 'a glob_constr_g - | GRec of 'a fix_kind_g * Names.Id.t array * 'a glob_decl_g list array * - 'a glob_constr_g array * 'a glob_constr_g array - | GSort of Misctypes.glob_sort - | GHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | GCast of 'a glob_constr_g * 'a glob_constr_g Misctypes.cast_type - - and 'a glob_constr_g = ('a glob_constr_r, 'a) DAst.t - - and 'a glob_decl_g = Names.Name.t * Decl_kinds.binding_kind * 'a glob_constr_g option * 'a glob_constr_g - - and 'a fix_recursion_order_g = - | GStructRec - | GWfRec of 'a glob_constr_g - | GMeasureRec of 'a glob_constr_g * 'a glob_constr_g option - - and 'a fix_kind_g = - | GFix of ((int option * 'a fix_recursion_order_g) array * int) - | GCoFix of int - - and 'a predicate_pattern_g = - Names.Name.t * (Names.inductive * Names.Name.t list) Loc.located option - - and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g) - - and 'a tomatch_tuples_g = 'a tomatch_tuple_g list - - and 'a cases_clause_g = (Names.Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located - and 'a cases_clauses_g = 'a cases_clause_g list - - type glob_constr = [ `any ] glob_constr_g - type tomatch_tuple = [ `any ] tomatch_tuple_g - type tomatch_tuples = [ `any ] tomatch_tuples_g - type cases_clause = [ `any ] cases_clause_g - type cases_clauses = [ `any ] cases_clauses_g - type glob_decl = [ `any ] glob_decl_g - type fix_kind = [ `any ] fix_kind_g - type predicate_pattern = [ `any ] predicate_pattern_g - type any_glob_constr = - | AnyGlobConstr : 'r glob_constr_g -> any_glob_constr - -end - -module Notation_term : -sig - type scope_name = string - type notation_var_instance_type = - | NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList - type tmp_scope_name = scope_name - - type subscopes = tmp_scope_name option * scope_name list - type notation_constr = - | NRef of Globnames.global_reference - | NVar of Names.Id.t - | NApp of notation_constr * notation_constr list - | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option - | NList of Names.Id.t * Names.Id.t * notation_constr * notation_constr * bool - | NLambda of Names.Name.t * notation_constr * notation_constr - | NProd of Names.Name.t * notation_constr * notation_constr - | NBinderList of Names.Id.t * Names.Id.t * notation_constr * notation_constr - | NLetIn of Names.Name.t * notation_constr * notation_constr option * notation_constr - | NCases of Term.case_style * notation_constr option * - (notation_constr * (Names.Name.t * (Names.inductive * Names.Name.t list) option)) list * - (Glob_term.cases_pattern list * notation_constr) list - | NLetTuple of Names.Name.t list * (Names.Name.t * notation_constr option) * - notation_constr * notation_constr - | NIf of notation_constr * (Names.Name.t * notation_constr option) * - notation_constr * notation_constr - | NRec of Glob_term.fix_kind * Names.Id.t array * - (Names.Name.t * notation_constr option * notation_constr) list array * - notation_constr array * notation_constr array - | NSort of Misctypes.glob_sort - | NCast of notation_constr * notation_constr Misctypes.cast_type - type interpretation = (Names.Id.t * (subscopes * notation_var_instance_type)) list * - notation_constr - type precedence = int - type parenRelation = - | L | E | Any | Prec of precedence - type tolerability = precedence * parenRelation -end - -module Tactypes : -sig - type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option - type glob_constr_pattern_and_expr = Names.Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern - type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a - type delayed_open_constr = EConstr.constr delayed_open - type delayed_open_constr_with_bindings = EConstr.constr Misctypes.with_bindings delayed_open - type intro_pattern = delayed_open_constr Misctypes.intro_pattern_expr Loc.located - type intro_patterns = delayed_open_constr Misctypes.intro_pattern_expr Loc.located list - type intro_pattern_naming = Misctypes.intro_pattern_naming_expr Loc.located - type or_and_intro_pattern = delayed_open_constr Misctypes.or_and_intro_pattern_expr Loc.located -end - -(* XXX: end of moved from intf *) - (************************************************************************) (* End of modules from engine/ *) (************************************************************************) @@ -4043,8 +4028,7 @@ sig and one_inductive_expr = ident_decl * Constrexpr.local_binder_expr list * Constrexpr.constr_expr option * constructor_expr list end - -(* XXX: end manual intf move *) +(* XXX: end of moved from intf *) module Typeclasses : sig @@ -4198,6 +4182,19 @@ end (* Modules from interp/ *) (************************************************************************) +module Tactypes : +sig + type glob_constr_and_expr = Glob_term.glob_constr * Constrexpr.constr_expr option + type glob_constr_pattern_and_expr = Names.Id.Set.t * glob_constr_and_expr * Pattern.constr_pattern + type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a + type delayed_open_constr = EConstr.constr delayed_open + type delayed_open_constr_with_bindings = EConstr.constr Misctypes.with_bindings delayed_open + type intro_pattern = delayed_open_constr Misctypes.intro_pattern_expr Loc.located + type intro_patterns = delayed_open_constr Misctypes.intro_pattern_expr Loc.located list + type intro_pattern_naming = Misctypes.intro_pattern_naming_expr Loc.located + type or_and_intro_pattern = delayed_open_constr Misctypes.or_and_intro_pattern_expr Loc.located +end + module Genintern : sig open Genarg @@ -4741,14 +4738,6 @@ sig unit -> (Names.Id.t * (Safe_typing.private_constants Entries.definition_entry * Proof_global.proof_universes * Decl_kinds.goal_kind)) 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"] - val current_proof_statement : unit -> Names.Id.t * Decl_kinds.goal_kind * EConstr.types end diff --git a/Makefile.ci b/Makefile.ci index 54ebf211f..0b2cbb663 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -12,6 +12,7 @@ CI_TARGETS=ci-all \ ci-geocoq \ ci-hott \ ci-iris-lambda-rust \ + ci-ltac2 \ ci-math-classes \ ci-math-comp \ ci-metacoq \ @@ -7,7 +7,7 @@ mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs. ## Installation -Go to the [download page](https://coq.inria.fr/download) for Windows and MacOS packages; +Download the pre-built packages of the [latest release](https://github.com/coq/coq/releases/latest) for Windows and MacOS; read the [help page](https://coq.inria.fr/opam/www/using.html) on how to install Coq with OPAM; or refer to the [`INSTALL` file](/INSTALL) for the procedure to install from source. @@ -21,9 +21,6 @@ There is a file named [`CHANGES`](/CHANGES) that explains the differences and th incompatibilities since last versions. If you upgrade Coq, please read it carefully. -## Availability -Coq is available from [coq.inria.fr](http://coq.inria.fr). - ## The Coq Club The Coq Club moderated mailing list is meant to be a standard way to discuss questions about the Coq system and related topics. The @@ -38,11 +35,8 @@ The topics to be discussed in the club should include: * theoretical questions about typed lambda-calculi which are closely related to Coq. -For any questions/suggestions about the Coq Club, please write to -`coq-club-request@inria.fr`. - ## Bugs report -Please report any bug in [our issue tracker](https://github.com/coq/coq/issues). +Please report any bug / feature request in [our issue tracker](https://github.com/coq/coq/issues). To be effective, bug reports should mention the OCaml version used to compile and run Coq, the Coq version (`coqtop -v`), the configuration diff --git a/appveyor.yml b/appveyor.yml index 64c1bedb5..92fc629b3 100644 --- a/appveyor.yml +++ b/appveyor.yml @@ -12,20 +12,22 @@ environment: matrix: - USEOPAM: true ARCH: 64 - - USEOPAM: false - ARCH: 32 - - USEOPAM: false - ARCH: 64 +# Comment out until issue #5998 is fixed. +# - USEOPAM: false +# ARCH: 32 +# - USEOPAM: false +# ARCH: 64 build_script: - cmd: 'call %APPVEYOR_BUILD_FOLDER%\dev\ci\appveyor.bat' test: off -artifacts: - - path: 'dev\nsis\*.exe' - name: installer +# Comment out until issue #5998 is fixed. +#artifacts: +# - path: 'dev\nsis\*.exe' +# name: installer - - path: 'coq-opensource-archive-*.zip' - name: opensource-archive +# - path: 'coq-opensource-archive-*.zip' +# name: opensource-archive diff --git a/checker/checker.ml b/checker/checker.ml index 247a98e63..e960a55fd 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -367,46 +367,11 @@ let initialized = ref false (* XXX: At some point we need to either port the checker to use the feedback system or to remove its use completely. *) -let init_feedback_listener () = - let open Format in - let pp_lvl fmt lvl = let open Feedback in match lvl with - | Error -> fprintf fmt "Error: " - | Info -> fprintf fmt "Info: " - | Debug -> fprintf fmt "Debug: " - | Warning -> fprintf fmt "Warning: " - | Notice -> fprintf fmt "" - in - let pp_loc fmt loc = let open Loc in match loc with - | None -> fprintf fmt "" - | Some loc -> - let where = - match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in - fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" - where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in - let checker_feed (fb : Feedback.feedback) = let open Feedback in - match fb.contents with - | Processed -> () - | Incomplete -> () - | Complete -> () - | ProcessingIn _ -> () - | InProgress _ -> () - | WorkerStatus (_,_) -> () - | AddedAxiom -> () - | GlobRef (_,_,_,_,_) -> () - | GlobDef (_,_,_,_) -> () - | FileDependency (_,_) -> () - | FileLoaded (_,_) -> () - | Custom (_,_,_) -> () - (* Re-enable when we switch back to feedback-based error printing *) - | Message (lvl,loc,msg) -> - Format.eprintf "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg - in ignore(Feedback.add_feeder checker_feed) - let init_with_argv argv = if not !initialized then begin initialized := true; Sys.catch_break false; (* Ctrl-C is fatal during the initialisation *) - init_feedback_listener (); + let _fhandle = Feedback.(add_feeder (console_feedback_listener Format.err_formatter)) in try parse_args argv; if !Flags.debug then Printexc.record_backtrace true; diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh index 5c37b3133..cb1493d6a 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -53,6 +53,12 @@ : ${HoTT_CI_GITURL:=https://github.com/HoTT/HoTT.git} ######################################################################## +# Ltac2 +######################################################################## +: ${ltac2_CI_BRANCH:=master} +: ${ltac2_CI_GITURL:=https://github.com/ppedrot/ltac2.git} + +######################################################################## # GeoCoq ######################################################################## : ${GeoCoq_CI_BRANCH:=master} @@ -80,7 +86,7 @@ # VST ######################################################################## : ${VST_CI_BRANCH:=master} -: ${VST_CI_GITURL:=https://github.com/Zimmi48/VST.git} +: ${VST_CI_GITURL:=https://github.com/PrincetonUniversity/VST.git} ######################################################################## # fiat_parsers diff --git a/dev/ci/ci-bignums.sh b/dev/ci/ci-bignums.sh index ff5935d4c..d68674381 100755 --- a/dev/ci/ci-bignums.sh +++ b/dev/ci/ci-bignums.sh @@ -4,7 +4,7 @@ ci_dir="$(dirname "$0")" # This script could be included inside other ones # Let's avoid to source ci-common twice in this case -if [ -z "${CI_BUILD_DIR}"]; +if [ -z "${CI_BUILD_DIR}" ]; then source ${ci_dir}/ci-common.sh fi diff --git a/dev/ci/ci-ltac2.sh b/dev/ci/ci-ltac2.sh new file mode 100755 index 000000000..4865be31e --- /dev/null +++ b/dev/ci/ci-ltac2.sh @@ -0,0 +1,10 @@ +#!/usr/bin/env bash + +ci_dir="$(dirname "$0")" +source ${ci_dir}/ci-common.sh + +ltac2_CI_DIR=${CI_BUILD_DIR}/coq-dpdgraph + +git_checkout ${ltac2_CI_BRANCH} ${ltac2_CI_GITURL} ${ltac2_CI_DIR} + +( cd ${ltac2_CI_DIR} && make -j ${NJOBS} && make tests && make install ) @@ -68,5 +68,6 @@ install_printer Top_printers.ppist install_printer Top_printers.ppconstrunderbindersidmap install_printer Top_printers.ppunbound_ltac_var_map install_printer Top_printers.ppididmap +install_printer Top_printers.ppidmapgen install_printer Top_printers.ppclosure install_printer Top_printers.ppclosedglobconstr diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 5be8257e8..707adce30 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -24,6 +24,12 @@ passing `-bypass-API`. ### ML API +General deprecation + +- All functions marked [@@ocaml.deprecated] in 8.7 have been + removed. Please, make sure your plugin is warning-free in 8.7 before + trying to port it over 8.8. + We removed the following functions: - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context` diff --git a/dev/top_printers.ml b/dev/top_printers.ml index 2dae96575..e48abce1c 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -86,9 +86,14 @@ let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" let pridmap pr l = let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) - let ppidmap pr l = pp (pridmap pr l) +let pridmapgen l = + let dom = Id.Set.elements (Id.Map.domain l) in + if dom = [] then str "[]" else + str "[domain= " ++ hov 0 (prlist_with_sep spc Id.print dom) ++ str "]" +let ppidmapgen l = pp (pridmapgen l) + let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 (Termops.print_constr (EConstr.of_constr c) ++ diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index 574591185..5fb458588 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -547,7 +547,7 @@ Yet another way of branching without backtracking is the following structure: $v_2$ which must be tactic values. The tactic value $v_1$ is applied in each subgoal independently and if it fails \emph{to progress} then $v_2$ is applied. {\tacexpr}$_1$ {\tt ||} {\tacexpr}$_2$ is equivalent to {\tt - first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tt progress} + first [} {\tt progress} {\tacexpr}$_1$ {\tt |} {\tacexpr}$_2$ {\tt ]} (except that if it fails, it fails like $v_2$). Branching is left-associative. @@ -561,7 +561,7 @@ The tactic is a generalization of the biased-branching tactics above. The expression {\tacexpr}$_1$ is evaluated to $v_1$, which is then applied to each subgoal independently. For each goal where $v_1$ succeeds at -least once, {tacexpr}$_2$ is evaluated to $v_2$ which is then applied +least once, {\tacexpr}$_2$ is evaluated to $v_2$ which is then applied collectively to the generated subgoals. The $v_2$ tactic can trigger backtracking points in $v_1$: where $v_1$ succeeds at least once, {\tt tryif {\tacexpr}$_1$ then {\tacexpr}$_2$ else {\tacexpr}$_3$} is diff --git a/interp/interp.mllib b/interp/interp.mllib index 6d290a325..e3500cfea 100644 --- a/interp/interp.mllib +++ b/interp/interp.mllib @@ -1,3 +1,4 @@ +Tactypes Stdarg Genintern Constrexpr_ops diff --git a/intf/tactypes.ml b/interp/tactypes.ml index 2c42e1311..2c42e1311 100644 --- a/intf/tactypes.ml +++ b/interp/tactypes.ml diff --git a/intf/intf.mllib b/intf/intf.mllib index 523e4b265..38a2a71cc 100644 --- a/intf/intf.mllib +++ b/intf/intf.mllib @@ -3,7 +3,6 @@ Evar_kinds Genredexpr Locus Notation_term -Tactypes Decl_kinds Extend Glob_term diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 3f4e8aa12..eaffc28ac 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -91,7 +91,7 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e) ++ spc ()) ++ + hov 0 (str "Anomaly" ++ spc () ++ quote (raw_anomaly e)) ++ spc () ++ hov 0 (str "Please report at " ++ str Coq_config.wwwbugtracker ++ str ".") else hov 0 (raw_anomaly e) @@ -137,8 +137,3 @@ let handled e = let bottom _ = raise Bottom in try let _ = print_gen bottom !handle_stack e in true with Bottom -> false - -(* Deprecated functions *) -let error string = user_err (str string) -let user_err_loc (loc,hdr,msg) = user_err ~loc ~hdr msg -let errorlabstrm hdr msg = user_err ~hdr msg diff --git a/lib/cErrors.mli b/lib/cErrors.mli index f3253979f..6fcc97a91 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -93,14 +93,3 @@ val noncritical : exn -> bool (** Check whether an exception is handled by some toplevel printer. The [Anomaly] exception is never handled. *) val handled : exn -> bool - -(** Deprecated functions *) -val error : string -> 'a - [@@ocaml.deprecated "use [user_err] instead"] - -val errorlabstrm : string -> Pp.t -> 'a - [@@ocaml.deprecated "use [user_err ~hdr] instead"] - -val user_err_loc : Loc.t * string * Pp.t -> 'a - [@@ocaml.deprecated "use [user_err ~loc] instead"] - diff --git a/lib/feedback.ml b/lib/feedback.ml index 7a126363c..1007582e0 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -63,6 +63,7 @@ let set_id_for_feedback ?(route=default_route) d i = span_id := i; feedback_route := route +let warn_no_listeners = ref true let feedback ?did ?id ?route what = let m = { contents = what; @@ -70,6 +71,8 @@ let feedback ?did ?id ?route what = doc_id = Option.default !doc_id did; span_id = Option.default !span_id id; } in + if !warn_no_listeners && Hashtbl.length feeders = 0 then + Format.eprintf "Warning, feedback message received but no listener to handle it!@\n%!"; Hashtbl.iter (fun _ f -> f m) feeders (* Logging messages *) @@ -81,3 +84,38 @@ let msg_notice ?loc x = feedback_logger ?loc Notice x let msg_warning ?loc x = feedback_logger ?loc Warning x let msg_error ?loc x = feedback_logger ?loc Error x let msg_debug ?loc x = feedback_logger ?loc Debug x + +(* Helper for tools willing to understand only the messages *) +let console_feedback_listener fmt = + let open Format in + let pp_lvl fmt lvl = match lvl with + | Error -> fprintf fmt "Error: " + | Info -> fprintf fmt "Info: " + | Debug -> fprintf fmt "Debug: " + | Warning -> fprintf fmt "Warning: " + | Notice -> fprintf fmt "" + in + let pp_loc fmt loc = let open Loc in match loc with + | None -> fprintf fmt "" + | Some loc -> + let where = + match loc.fname with InFile f -> f | ToplevelInput -> "Toplevel input" in + fprintf fmt "\"%s\", line %d, characters %d-%d:@\n" + where loc.line_nb (loc.bp-loc.bol_pos) (loc.ep-loc.bol_pos) in + let checker_feed (fb : feedback) = + match fb.contents with + | Processed -> () + | Incomplete -> () + | Complete -> () + | ProcessingIn _ -> () + | InProgress _ -> () + | WorkerStatus (_,_) -> () + | AddedAxiom -> () + | GlobRef (_,_,_,_,_) -> () + | GlobDef (_,_,_,_) -> () + | FileDependency (_,_) -> () + | FileLoaded (_,_) -> () + | Custom (_,_,_) -> () + | Message (lvl,loc,msg) -> + fprintf fmt "@[%a@]%a@[%a@]\n%!" pp_loc loc pp_lvl lvl Pp.pp_with msg + in checker_feed diff --git a/lib/feedback.mli b/lib/feedback.mli index 73b84614f..62b909516 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -99,3 +99,11 @@ val msg_error : ?loc:Loc.t -> Pp.t -> unit val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) + +val console_feedback_listener : Format.formatter -> feedback -> unit +(** Helper for tools willing to print to the feedback system *) + +val warn_no_listeners : bool ref +(** The library will print a warning to the console if no listener is + available by default; ML-clients willing to use Coq without a + feedback handler should set this to false. *) diff --git a/lib/flags.ml b/lib/flags.ml index a53a866ab..323b5492d 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -140,10 +140,6 @@ let verbosely f x = without_option quiet f x let if_silent f x = if !quiet then f x let if_verbose f x = if not !quiet then f x -let make_silent flag = quiet := flag -let is_silent () = !quiet -let is_verbose () = not !quiet - let auto_intros = ref true let make_auto_intros flag = auto_intros := flag let is_auto_intros () = !auto_intros diff --git a/lib/flags.mli b/lib/flags.mli index 5233e72a2..0ff3e0a81 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -87,14 +87,6 @@ val verbosely : ('a -> 'b) -> 'a -> 'b val if_silent : ('a -> unit) -> 'a -> unit val if_verbose : ('a -> unit) -> 'a -> unit -(* Deprecated *) -val make_silent : bool -> unit -[@@ocaml.deprecated "Please use Flags.quiet"] -val is_silent : unit -> bool -[@@ocaml.deprecated "Please use Flags.quiet"] -val is_verbose : unit -> bool -[@@ocaml.deprecated "Please use Flags.quiet"] - (* Miscellaneus flags for vernac *) val make_auto_intros : bool -> unit val is_auto_intros : unit -> bool diff --git a/lib/loc.ml b/lib/loc.ml index 4a935a9d9..2cf4d3960 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -84,9 +84,3 @@ let raise ?loc e = let info = Exninfo.add Exninfo.null location loc in Exninfo.iraise (e, info) -(** Deprecated *) -let located_fold_left f x (_,a) = f x a -let located_iter2 f (_,a) (_,b) = f a b -let down_located f (_,a) = f a - - diff --git a/lib/loc.mli b/lib/loc.mli index fde490cc8..800940f21 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -65,14 +65,3 @@ val tag : ?loc:t -> 'a -> 'a located val map : ('a -> 'b) -> 'a located -> 'b located (** Modify an object carrying a location *) - -(** Deprecated functions *) -val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a - [@@ocaml.deprecated "use pattern matching"] - -val down_located : ('a -> 'b) -> 'a located -> 'b - [@@ocaml.deprecated "use pattern matching"] - -val located_iter2 : ('a -> 'b -> unit) -> 'a located -> 'b located -> unit - [@@ocaml.deprecated "use pattern matching"] - diff --git a/library/coqlib.ml b/library/coqlib.ml index 8787738af..141fff033 100644 --- a/library/coqlib.ml +++ b/library/coqlib.ml @@ -377,7 +377,3 @@ let coq_sumbool_ref = lazy (init_reference ["Specif"] "sumbool") let coq_sig_ref = lazy (init_reference ["Specif"] "sig") let coq_or_ref = lazy (init_reference ["Logic"] "or") let coq_iff_ref = lazy (init_reference ["Logic"] "iff") - -(* Deprecated *) -let gen_reference = coq_reference - diff --git a/library/coqlib.mli b/library/coqlib.mli index 17c79d2e1..cc22f1635 100644 --- a/library/coqlib.mli +++ b/library/coqlib.mli @@ -205,7 +205,3 @@ val coq_sig_ref : global_reference lazy_t val coq_or_ref : global_reference lazy_t val coq_iff_ref : global_reference lazy_t - -(* Deprecated functions *) -val gen_reference : message -> string list -> string -> global_reference -[@@ocaml.deprecated "Please use Coqlib.find_reference"] diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index c577cb219..116152568 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -232,10 +232,12 @@ GEXTEND Gram | l = ident -> Name.Name l ] ] ; let_clause: - [ [ id = identref; ":="; te = tactic_expr -> - (id, arg_of_expr te) - | id = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> - (id, arg_of_expr (TacFun(args,te))) ] ] + [ [ (l,id) = identref; ":="; te = tactic_expr -> + ((l,Name id), arg_of_expr te) + | na = ["_" -> (Some !@loc,Anonymous)]; ":="; te = tactic_expr -> + (na, arg_of_expr te) + | (l,id) = identref; args = LIST1 input_fun; ":="; te = tactic_expr -> + ((l,Name id), arg_of_expr (TacFun(args,te))) ] ] ; match_pattern: [ [ IDENT "context"; oid = OPT Constr.ident; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 6522fc28f..38460c669 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -536,8 +536,8 @@ let pr_goal_selector ~toplevel s = let pr_funvar n = spc () ++ Name.print n - let pr_let_clause k pr (id,(bl,t)) = - hov 0 (keyword k ++ spc () ++ pr_lident id ++ prlist pr_funvar bl ++ + let pr_let_clause k pr (na,(bl,t)) = + hov 0 (keyword k ++ spc () ++ pr_lname na ++ prlist pr_funvar bl ++ str " :=" ++ brk (1,1) ++ pr (TacArg (Loc.tag t))) let pr_let_clauses recflag pr = function diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 163973688..9bd3efc6b 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -254,7 +254,7 @@ and 'a gen_tactic_expr = | TacFail of global_flag * int or_var * 'n message_token list | TacInfo of 'a gen_tactic_expr | TacLetIn of rec_flag * - (Id.t located * 'a gen_tactic_arg) list * + (Name.t located * 'a gen_tactic_arg) list * 'a gen_tactic_expr | TacMatch of lazy_flag * 'a gen_tactic_expr * diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index f171fd07d..b16b0a7ba 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -468,9 +468,10 @@ let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function (* Utilities *) let extract_let_names lrc = let fold accu ((loc, name), _) = - if Id.Set.mem name accu then user_err ?loc + Nameops.Name.fold_right (fun id accu -> + if Id.Set.mem id accu then user_err ?loc ~hdr:"glob_tactic" (str "This variable is bound several times.") - else Id.Set.add name accu + else Id.Set.add id accu) name accu in List.fold_left fold Id.Set.empty lrc @@ -812,7 +813,7 @@ let notation_subst bindings tac = let fold id c accu = let loc = Glob_ops.loc_of_glob_constr (fst c) in let c = ConstrMayEval (ConstrTerm c) in - ((loc, id), c) :: accu + ((loc, Name id), c) :: accu in let bindings = Id.Map.fold fold bindings [] in (** This is theoretically not correct due to potential variable capture, but diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index fd75862c6..1a8ec6d6f 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1397,9 +1397,9 @@ and tactic_of_value ist vle = and interp_letrec ist llc u = Proofview.tclUNIT () >>= fun () -> (* delay for the effects of [lref], just in case. *) let lref = ref ist.lfun in - let fold accu ((_, id), b) = + let fold accu ((_, na), b) = let v = of_tacvalue (VRec (lref, TacArg (Loc.tag b))) in - Id.Map.add id v accu + Name.fold_right (fun id -> Id.Map.add id v) na accu in let lfun = List.fold_left fold ist.lfun llc in let () = lref := lfun in @@ -1412,9 +1412,9 @@ and interp_letin ist llc u = | [] -> let ist = { ist with lfun } in val_interp ist u - | ((_, id), body) :: defs -> + | ((_, na), body) :: defs -> Ftactic.bind (interp_tacarg ist body) (fun v -> - fold (Id.Map.add id v lfun) defs) + fold (Name.fold_right (fun id -> Id.Map.add id v) na lfun) defs) in fold ist.lfun llc diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index a69caecab..b2b583ba7 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -888,6 +888,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre | [], [] -> [] | _ -> assert false in aux 1 1 (List.rev nal) cs.cs_args, true in + let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) fsign + else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in let obj ind p v f = if not record then let nal = List.map (fun na -> ltac_interp_name lvar na) nal in @@ -997,6 +1000,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let pi = lift n pred in (* liftn n 2 pred ? *) let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in + let cs_args = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then Context.Rel.map (whd_betaiota !evdref) cs_args + else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in let csgn = List.map (set_name Anonymous) cs_args in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index a87debeff..04374c88b 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1314,7 +1314,9 @@ let pb_equal = function | Reduction.CONV -> Reduction.CONV let report_anomaly e = - let e = UserError (None, Pp.(str "Conversion test raised an anomaly" ++ print e)) in + let msg = Pp.(str "Conversion test raised an anomaly:" ++ + spc () ++ CErrors.print e) in + let e = UserError (None,msg) in let e = CErrors.push e in iraise e diff --git a/pretyping/unification.ml b/pretyping/unification.ml index be9943f33..5eb6b780a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -194,6 +194,10 @@ let pose_all_metas_as_evars env evd t = let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in let ty = EConstr.of_constr ty in let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in + let ty = + if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld + then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *) + else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in let src = Evd.evar_source_of_meta mv !evdref in let ev = Evarutil.e_new_evar env evdref ~src ty in evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref; diff --git a/printing/printer.mli b/printing/printer.mli index cd6e6d63a..fbba14ede 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -81,11 +81,11 @@ val pr_closed_glob : closed_glob_constr -> Pp.t val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_lglob_constr_env : env -> glob_constr -> Pp.t -val pr_lglob_constr : glob_constr -> Pp.t +val pr_lglob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_lglob_constr : 'a glob_constr_g -> Pp.t -val pr_glob_constr_env : env -> glob_constr -> Pp.t -val pr_glob_constr : glob_constr -> Pp.t +val pr_glob_constr_env : env -> 'a glob_constr_g -> Pp.t +val pr_glob_constr : 'a glob_constr_g -> Pp.t val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t val pr_lconstr_pattern : constr_pattern -> Pp.t diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 469e1a011..2d4aba17c 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -230,31 +230,3 @@ let apply_implicit_tactic tac = (); fun env sigma evk -> let solve_by_implicit_tactic () = match !implicit_tactic with | None -> None | Some tac -> Some (apply_implicit_tactic tac) - -(** Deprecated functions *) -let refining = Proof_global.there_are_pending_proofs -let check_no_pending_proofs = Proof_global.check_no_pending_proof - -let get_current_proof_name = Proof_global.get_current_proof_name -let get_all_proof_names = Proof_global.get_all_proof_names - -type lemma_possible_guards = Proof_global.lemma_possible_guards - -let delete_proof = Proof_global.discard -let delete_current_proof = Proof_global.discard_current -let delete_all_proofs = Proof_global.discard_all - -let get_pftreestate () = - Proof_global.give_me_the_proof () - -let set_end_tac tac = - Proof_global.set_endline_tactic tac - -let set_used_variables l = - Proof_global.set_used_variables l - -let get_used_variables () = - Proof_global.get_used_variables () - -let get_universe_decl () = - Proof_global.get_universe_decl () diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index ec176e547..21a65f8eb 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -8,7 +8,6 @@ (** Global proof state. A quite redundant wrapper on {!Proof_global}. *) -open Loc open Names open Constr open Environ @@ -122,84 +121,3 @@ val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) val solve_by_implicit_tactic : unit -> Pretyping.inference_hook option - -(** {5 Deprecated functions in favor of [Proof_global]} *) - -(** {6 ... } *) -(** Several proofs can be opened simultaneously but at most one is - focused at some time. The following functions work by side-effect - on current set of open proofs. In this module, ``proofs'' means an - open proof (something started by vernacular command [Goal], [Lemma] - or [Theorem]), and ``goal'' means a subgoal of the current focused - proof *) - -(** [refining ()] tells if there is some proof in progress, even if a not - focused one *) - -val refining : unit -> bool -[@@ocaml.deprecated "use Proof_global.there_are_pending_proofs"] - -(** [check_no_pending_proofs ()] fails if there is still some proof in - progress *) - -val check_no_pending_proofs : unit -> unit -[@@ocaml.deprecated "use Proof_global.check_no_pending_proofs"] - -(** {6 ... } *) -(** [delete_proof name] deletes proof of name [name] or fails if no proof - has this name *) - -val delete_proof : Id.t located -> unit -[@@ocaml.deprecated "use Proof_global.discard"] - -(** [delete_current_proof ()] deletes current focused proof or fails if - no proof is focused *) - -val delete_current_proof : unit -> unit -[@@ocaml.deprecated "use Proof_global.discard_current"] - -(** [delete_all_proofs ()] deletes all open proofs if any *) -val delete_all_proofs : unit -> unit -[@@ocaml.deprecated "use Proof_global.discard_all"] - -(** [get_pftreestate ()] returns the current focused pending proof. - @raise NoCurrentProof if there is no pending proof. *) - -val get_pftreestate : unit -> Proof.proof -[@@ocaml.deprecated "use Proof_global.give_me_the_proof"] - -(** {6 ... } *) -(** [set_end_tac tac] applies tactic [tac] to all subgoal generate - by [solve] *) - -val set_end_tac : Genarg.glob_generic_argument -> unit -[@@ocaml.deprecated "use Proof_global.set_endline_tactic"] - -(** {6 ... } *) -(** [set_used_variables l] declares that section variables [l] will be - used in the proof *) -val set_used_variables : - Id.t list -> Context.Named.t * Names.Id.t Loc.located list -[@@ocaml.deprecated "use Proof_global.set_used_variables"] - -val get_used_variables : unit -> Context.Named.t option -[@@ocaml.deprecated "use Proof_global.get_used_variables"] - -(** {6 Universe binders } *) -val get_universe_decl : unit -> Univdecls.universe_decl -[@@ocaml.deprecated "use Proof_global.get_universe_decl"] - -(** {6 ... } *) -(** [get_current_proof_name ()] return the name of the current focused - proof or failed if no proof is focused *) -val get_current_proof_name : unit -> Id.t -[@@ocaml.deprecated "use Proof_global.get_current_proof_name"] - -(** [get_all_proof_names ()] returns the list of all pending proof names. - The first name is the current proof, the other names may come in - any order. *) -val get_all_proof_names : unit -> Id.t list -[@@ocaml.deprecated "use Proof_global.get_all_proof_names"] - -type lemma_possible_guards = Proof_global.lemma_possible_guards -[@@ocaml.deprecated "use Proof_global.lemma_possible_guards"] diff --git a/test-suite/bugs/5996.v b/test-suite/bugs/5996.v new file mode 100644 index 000000000..c9e3292b4 --- /dev/null +++ b/test-suite/bugs/5996.v @@ -0,0 +1,8 @@ +Goal Type. + let c := constr:(prod nat nat) in + let c' := (eval pattern nat in c) in + let c' := lazymatch c' with ?f _ => f end in + let c'' := lazymatch c' with fun x : Set => ?f => constr:(forall x : Type, f) end in + let _ := type of c'' in + exact c''. +Defined. diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v index 0219c3bfd..6fbe61a9b 100644 --- a/test-suite/success/destruct.v +++ b/test-suite/success/destruct.v @@ -430,3 +430,9 @@ eexists ?[x]. destruct (S _). change (0 = ?x). Abort. + +Goal (forall P, P 0 -> True/\True) -> True. +intro H. +destruct (H (fun x => True)). +match goal with |- True => idtac end. +Abort. diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v index b8a8ff756..22fb4d757 100644 --- a/test-suite/success/refine.v +++ b/test-suite/success/refine.v @@ -122,3 +122,13 @@ Abort. Goal (forall A : Prop, A -> ~~A). Proof. refine(fun A a f => _). + +(* Checking beta-iota normalization of hypotheses in created evars *) + +Goal {x|x=0} -> True. +refine (fun y => let (x,a) := y in _). +match goal with a:_=0 |- _ => idtac end. + +Goal (forall P, {P 0}+{P 1}) -> True. +refine (fun H => if H (fun x => x=x) then _ else _). +match goal with _:0=0 |- _ => idtac end. |