diff options
| -rw-r--r-- | API/API.ml | 4 | ||||
| -rw-r--r-- | API/API.mli | 683 | ||||
| -rw-r--r-- | checker/checker.ml | 37 | ||||
| -rw-r--r-- | dev/ci/ci-basic-overlay.sh | 2 | ||||
| -rw-r--r-- | dev/doc/changes.md | 6 | ||||
| -rw-r--r-- | doc/refman/RefMan-ltac.tex | 4 | ||||
| -rw-r--r-- | interp/interp.mllib | 1 | ||||
| -rw-r--r-- | interp/tactypes.ml (renamed from intf/tactypes.ml) | 0 | ||||
| -rw-r--r-- | intf/intf.mllib | 1 | ||||
| -rw-r--r-- | lib/cErrors.ml | 5 | ||||
| -rw-r--r-- | lib/cErrors.mli | 11 | ||||
| -rw-r--r-- | lib/feedback.ml | 38 | ||||
| -rw-r--r-- | lib/feedback.mli | 8 | ||||
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/flags.mli | 8 | ||||
| -rw-r--r-- | lib/loc.ml | 6 | ||||
| -rw-r--r-- | lib/loc.mli | 11 | ||||
| -rw-r--r-- | library/coqlib.ml | 4 | ||||
| -rw-r--r-- | library/coqlib.mli | 4 | ||||
| -rw-r--r-- | plugins/ltac/g_ltac.ml4 | 10 | ||||
| -rw-r--r-- | plugins/ltac/pptactic.ml | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacintern.ml | 7 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 8 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 7 | ||||
| -rw-r--r-- | pretyping/unification.ml | 4 | ||||
| -rw-r--r-- | proofs/pfedit.ml | 28 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 82 | ||||
| -rw-r--r-- | test-suite/bugs/5996.v | 8 | ||||
| -rw-r--r-- | test-suite/success/destruct.v | 6 | ||||
| -rw-r--r-- | test-suite/success/refine.v | 10 |
31 files changed, 447 insertions, 566 deletions
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 ccb71179d..d7be4c6d1 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1886,6 +1886,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 @@ -2122,7 +2444,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 @@ -2204,33 +2525,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 @@ -2402,164 +2696,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 @@ -2728,37 +2864,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 (** *) @@ -3113,126 +3218,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/ *) (************************************************************************) @@ -4032,8 +4017,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 @@ -4187,6 +4171,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 @@ -4730,14 +4727,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/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..59a71b608 100644 --- a/dev/ci/ci-basic-overlay.sh +++ b/dev/ci/ci-basic-overlay.sh @@ -80,7 +80,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/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/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..94357aad3 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -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 e467d3e2c..28a13fb40 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/unification.ml b/pretyping/unification.ml index 01c28b5ed..c149aaaaa 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/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 6e4ecd13b..adfe33786 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 Term 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. |