From 8beca748d992cd08e2dd7448c8b28dadbcea4a16 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 01:09:11 +0100 Subject: Cleaning up interfaces. We make mli files look to what they were looking before the move to EConstr by opening this module. --- pretyping/find_subterm.ml | 4 +- pretyping/find_subterm.mli | 15 ++++---- pretyping/pretype_errors.mli | 87 ++++++++++++++++++++++---------------------- pretyping/pretyping.ml | 2 +- pretyping/pretyping.mli | 31 ++++++++-------- pretyping/tacred.ml | 1 - pretyping/tacred.mli | 17 +++++---- pretyping/unification.ml | 3 +- tactics/leminv.mli | 3 +- tactics/tacticals.mli | 31 ++++++++-------- tactics/tactics.ml | 1 - 11 files changed, 99 insertions(+), 96 deletions(-) diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 15409f2b86..d09686f6e2 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -141,8 +141,8 @@ let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t = let replace_term_occ_modulo evd occs test bywhat t = let occs',like_first = match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in - EConstr.Unsafe.to_constr (proceed_with_occurrences - (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t) + proceed_with_occurrences + (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t let replace_term_occ_decl_modulo evd occs test bywhat d = let (plocs,hyploc),like_first = diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli index c7db84e3c7..3d2ebb72df 100644 --- a/pretyping/find_subterm.mli +++ b/pretyping/find_subterm.mli @@ -11,11 +11,12 @@ open Term open Evd open Pretype_errors open Environ +open EConstr (** Finding subterms, possibly up to some unification function, possibly at some given occurrences *) -exception NotUnifiable of (EConstr.constr * EConstr.constr * unification_error) option +exception NotUnifiable of (constr * constr * unification_error) option exception SubtermUnificationError of subterm_unification_error @@ -26,7 +27,7 @@ exception SubtermUnificationError of subterm_unification_error with None. *) type 'a testing_function = { - match_fun : 'a -> EConstr.constr -> 'a; + match_fun : 'a -> constr -> 'a; merge_fun : 'a -> 'a -> 'a; mutable testing_state : 'a; mutable last_found : position_reporting option @@ -34,7 +35,7 @@ type 'a testing_function = { (** This is the basic testing function, looking for exact matches of a closed term *) -val make_eq_univs_test : env -> evar_map -> EConstr.constr -> evar_map testing_function +val make_eq_univs_test : env -> evar_map -> constr -> evar_map testing_function (** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm modulo a testing function [test] and replaces successfully @@ -42,27 +43,27 @@ val make_eq_univs_test : env -> evar_map -> EConstr.constr -> evar_map testing_f ()]; it turns a NotUnifiable exception raised by the testing function into a SubtermUnificationError. *) val replace_term_occ_modulo : evar_map -> occurrences or_like_first -> - 'a testing_function -> (unit -> EConstr.constr) -> EConstr.constr -> constr + 'a testing_function -> (unit -> constr) -> constr -> constr (** [replace_term_occ_decl_modulo] is similar to [replace_term_occ_modulo] but for a named_declaration. *) val replace_term_occ_decl_modulo : evar_map -> (occurrences * hyp_location_flag) or_like_first -> - 'a testing_function -> (unit -> EConstr.constr) -> + 'a testing_function -> (unit -> constr) -> Context.Named.Declaration.t -> Context.Named.Declaration.t (** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC), unifying universes which results in a set of constraints. *) val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first -> - EConstr.constr -> EConstr.constr -> constr * evar_map + constr -> constr -> constr * evar_map (** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of closed [c] at positions [occl] by [Rel 1] in [decl]. *) val subst_closed_term_occ_decl : env -> evar_map -> (occurrences * hyp_location_flag) or_like_first -> - EConstr.constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map + constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map (** Miscellaneous *) val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 0ebe4817ca..7cef14339b 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -9,52 +9,53 @@ open Names open Term open Environ +open EConstr open Type_errors (** {6 The type of errors raised by the pretyper } *) type unification_error = - | OccurCheck of existential_key * EConstr.constr - | NotClean of EConstr.existential * env * EConstr.constr + | OccurCheck of existential_key * constr + | NotClean of existential * env * constr | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * EConstr.constr * EConstr.constr + | ConversionFailed of env * constr * constr | MetaOccurInBody of existential_key - | InstanceNotSameType of existential_key * env * EConstr.types * EConstr.types + | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option -type position_reporting = (position * int) * EConstr.t +type position_reporting = (position * int) * constr -type subterm_unification_error = bool * position_reporting * position_reporting * (EConstr.constr * EConstr.constr * unification_error) option +type subterm_unification_error = bool * position_reporting * position_reporting * (constr * constr * unification_error) option -type type_error = (EConstr.constr, EConstr.types) ptype_error +type type_error = (constr, types) ptype_error type pretype_error = (** Old Case *) - | CantFindCaseType of EConstr.constr + | CantFindCaseType of constr (** Type inference unification *) - | ActualTypeNotCoercible of EConstr.unsafe_judgment * EConstr.types * unification_error + | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) - | UnifOccurCheck of existential_key * EConstr.constr + | UnifOccurCheck of existential_key * constr | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option - | CannotUnify of EConstr.constr * EConstr.constr * unification_error option - | CannotUnifyLocal of EConstr.constr * EConstr.constr * EConstr.constr - | CannotUnifyBindingType of constr * constr - | CannotGeneralize of constr - | NoOccurrenceFound of EConstr.constr * Id.t option - | CannotFindWellTypedAbstraction of EConstr.constr * EConstr.constr list * (env * type_error) option - | WrongAbstractionType of Name.t * EConstr.constr * EConstr.types * EConstr.types + | CannotUnify of constr * constr * unification_error option + | CannotUnifyLocal of constr * constr * constr + | CannotUnifyBindingType of Constr.constr * Constr.constr + | CannotGeneralize of Constr.constr + | NoOccurrenceFound of constr * Id.t option + | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option + | WrongAbstractionType of Name.t * constr * types * types | AbstractionOverMeta of Name.t * Name.t - | NonLinearUnification of Name.t * EConstr.constr + | NonLinearUnification of Name.t * constr (** Pretyping *) | VarNotFound of Id.t - | UnexpectedType of EConstr.constr * EConstr.constr - | NotProduct of EConstr.constr + | UnexpectedType of constr * constr + | NotProduct of constr | TypingError of type_error | CannotUnifyOccurrences of subterm_unification_error | UnsatisfiableConstraints of @@ -67,85 +68,85 @@ val precatchable_exception : exn -> bool (** Raising errors *) val error_actual_type : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> unification_error -> 'b val error_actual_type_core : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> EConstr.constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b val error_cant_apply_not_functional : ?loc:Loc.t -> env -> Evd.evar_map -> - EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b + unsafe_judgment -> unsafe_judgment array -> 'b val error_cant_apply_bad_type : - ?loc:Loc.t -> env -> Evd.evar_map -> int * EConstr.constr * EConstr.constr -> - EConstr.unsafe_judgment -> EConstr.unsafe_judgment array -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> int * constr * constr -> + unsafe_judgment -> unsafe_judgment array -> 'b val error_case_not_inductive : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_ill_formed_branch : ?loc:Loc.t -> env -> Evd.evar_map -> - EConstr.constr -> pconstructor -> EConstr.constr -> EConstr.constr -> 'b + constr -> pconstructor -> constr -> constr -> 'b val error_number_branches : ?loc:Loc.t -> env -> Evd.evar_map -> - EConstr.unsafe_judgment -> int -> 'b + unsafe_judgment -> int -> 'b val error_ill_typed_rec_body : ?loc:Loc.t -> env -> Evd.evar_map -> - int -> Name.t array -> EConstr.unsafe_judgment array -> EConstr.types array -> 'b + int -> Name.t array -> unsafe_judgment array -> types array -> 'b val error_elim_arity : ?loc:Loc.t -> env -> Evd.evar_map -> - pinductive -> sorts_family list -> EConstr.constr -> - EConstr.unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b + pinductive -> sorts_family list -> constr -> + unsafe_judgment -> (sorts_family * sorts_family * arity_error) option -> 'b val error_not_a_type : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b val error_assumption : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.unsafe_judgment -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> 'b -val error_cannot_coerce : env -> Evd.evar_map -> EConstr.constr * EConstr.constr -> 'b +val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b (** {6 Implicit arguments synthesis errors } *) -val error_occur_check : env -> Evd.evar_map -> existential_key -> EConstr.constr -> 'b +val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_unsolvable_implicit : ?loc:Loc.t -> env -> Evd.evar_map -> existential_key -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map -> - ?reason:unification_error -> EConstr.constr * EConstr.constr -> 'b + ?reason:unification_error -> constr * constr -> 'b -val error_cannot_unify_local : env -> Evd.evar_map -> EConstr.constr * EConstr.constr * EConstr.constr -> 'b +val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map -> - EConstr.constr -> EConstr.constr list -> (env * type_error) option -> 'b + constr -> constr list -> (env * type_error) option -> 'b val error_wrong_abstraction_type : env -> Evd.evar_map -> - Name.t -> EConstr.constr -> EConstr.types -> EConstr.types -> 'b + Name.t -> constr -> types -> types -> 'b val error_abstraction_over_meta : env -> Evd.evar_map -> metavariable -> metavariable -> 'b val error_non_linear_unification : env -> Evd.evar_map -> - metavariable -> EConstr.constr -> 'b + metavariable -> constr -> 'b (** {6 Ml Case errors } *) val error_cant_find_case_type : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Pretyping errors } *) val error_unexpected_type : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> constr -> 'b val error_not_product : - ?loc:Loc.t -> env -> Evd.evar_map -> EConstr.constr -> 'b + ?loc:Loc.t -> env -> Evd.evar_map -> constr -> 'b (** {6 Error in conversion from AST to glob_constr } *) diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f76f608d0d..6b6800ac6a 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -61,7 +61,7 @@ type ltac_var_map = { ltac_genargs : unbound_ltac_var_map; } type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * Constr.constr +type pure_open_constr = evar_map * EConstr.constr (************************************************************************) (* This concerns Cases *) diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 825d73f1f1..47ad93d7e0 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -16,6 +16,7 @@ open Names open Term open Environ open Evd +open EConstr open Glob_term open Evarutil open Misctypes @@ -25,7 +26,7 @@ open Misctypes val search_guard : Loc.t -> env -> int list list -> rec_declaration -> int array -type typing_constraint = OfType of EConstr.types | IsType | WithoutTypeConstraint +type typing_constraint = OfType of types | IsType | WithoutTypeConstraint type var_map = Pattern.constr_under_binders Id.Map.t type uconstr_var_map = Glob_term.closed_glob_constr Id.Map.t @@ -47,7 +48,7 @@ val empty_lvar : ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr -type inference_hook = env -> evar_map -> evar -> evar_map * EConstr.constr +type inference_hook = env -> evar_map -> evar -> evar_map * constr type inference_flags = { use_typeclasses : bool; @@ -76,10 +77,10 @@ val allow_anonymous_refs : bool ref evar_map is modified explicitly or by side-effect. *) val understand_tcc : ?flags:inference_flags -> env -> evar_map -> - ?expected_type:typing_constraint -> glob_constr -> evar_map * EConstr.constr + ?expected_type:typing_constraint -> glob_constr -> evar_map * constr val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> - ?expected_type:typing_constraint -> glob_constr -> EConstr.constr + ?expected_type:typing_constraint -> glob_constr -> constr (** More general entry point with evars from ltac *) @@ -95,7 +96,7 @@ val understand_tcc_evars : ?flags:inference_flags -> env -> evar_map ref -> val understand_ltac : inference_flags -> env -> evar_map -> ltac_var_map -> - typing_constraint -> glob_constr -> evar_map * EConstr.constr + typing_constraint -> glob_constr -> pure_open_constr (** Standard call to get a constr from a glob_constr, resolving implicit arguments and coercions, and compiling pattern-matching; @@ -105,21 +106,21 @@ val understand_ltac : inference_flags -> unresolved evar remains, expanding evars. *) val understand : ?flags:inference_flags -> ?expected_type:typing_constraint -> - env -> evar_map -> glob_constr -> constr Evd.in_evar_universe_context + env -> evar_map -> glob_constr -> Constr.constr Evd.in_evar_universe_context (** Idem but returns the judgment of the understood term *) val understand_judgment : env -> evar_map -> - glob_constr -> EConstr.unsafe_judgment Evd.in_evar_universe_context + glob_constr -> unsafe_judgment Evd.in_evar_universe_context (** Idem but do not fail on unresolved evars (type cl*) val understand_judgment_tcc : env -> evar_map ref -> - glob_constr -> EConstr.unsafe_judgment + glob_constr -> unsafe_judgment val type_uconstr : ?flags:inference_flags -> ?expected_type:typing_constraint -> - Geninterp.interp_sign -> Glob_term.closed_glob_constr -> EConstr.constr Tactypes.delayed_open + Geninterp.interp_sign -> Glob_term.closed_glob_constr -> constr Tactypes.delayed_open (** Trying to solve remaining evars and remaining conversion problems possibly using type classes, heuristics, external tactic solver @@ -139,21 +140,21 @@ val check_evars_are_solved : (** [check_evars env initial_sigma extended_sigma c] fails if some new unresolved evar remains in [c] *) -val check_evars : env -> evar_map -> evar_map -> EConstr.constr -> unit +val check_evars : env -> evar_map -> evar_map -> constr -> unit (**/**) (** Internal of Pretyping... *) val pretype : int -> bool -> type_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> EConstr.unsafe_judgment + ltac_var_map -> glob_constr -> unsafe_judgment val pretype_type : int -> bool -> val_constraint -> env -> evar_map ref -> - ltac_var_map -> glob_constr -> EConstr.unsafe_type_judgment + ltac_var_map -> glob_constr -> unsafe_type_judgment val ise_pretype_gen : inference_flags -> env -> evar_map -> - ltac_var_map -> typing_constraint -> glob_constr -> evar_map * EConstr.constr + ltac_var_map -> typing_constraint -> glob_constr -> evar_map * constr (**/**) @@ -163,5 +164,5 @@ val interp_sort : ?loc:Loc.t -> evar_map -> glob_sort -> evar_map * sorts val interp_elimination_sort : glob_sort -> sorts_family val genarg_interp_hook : - (EConstr.types -> env -> evar_map -> unbound_ltac_var_map -> - Genarg.glob_generic_argument -> EConstr.constr * evar_map) Hook.t + (types -> env -> evar_map -> unbound_ltac_var_map -> + Genarg.glob_generic_argument -> constr * evar_map) Hook.t diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2b496f9267..4abfc26fc5 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1154,7 +1154,6 @@ let abstract_scheme env sigma (locc,a) (c, sigma) = mkLambda (na,ta,c), sigma else let c', sigma' = subst_closed_term_occ env sigma (AtOccs locc) a c in - let c' = EConstr.of_constr c' in mkLambda (na,ta,c'), sigma' let pattern_occs loccs_trm = { e_redfun = begin fun env sigma c -> diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 15b4e990d8..a4499015d2 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -10,6 +10,7 @@ open Names open Term open Environ open Evd +open EConstr open Reductionops open Pattern open Globnames @@ -17,7 +18,7 @@ open Locus open Univ type reduction_tactic_error = - InvalidAbstraction of env * evar_map * EConstr.constr * (env * Type_errors.type_error) + InvalidAbstraction of env * evar_map * constr * (env * Type_errors.type_error) exception ReductionTacticError of reduction_tactic_error @@ -58,10 +59,10 @@ val unfoldn : (occurrences * evaluable_global_reference) list -> reduction_function (** Fold *) -val fold_commands : EConstr.constr list -> reduction_function +val fold_commands : constr list -> reduction_function (** Pattern *) -val pattern_occs : (occurrences * EConstr.constr) list -> e_reduction_function +val pattern_occs : (occurrences * constr) list -> e_reduction_function (** Rem: Lazy strategies are defined in Reduction *) @@ -75,23 +76,23 @@ val cbv_norm_flags : CClosure.RedFlags.reds -> reduction_function (** [reduce_to_atomic_ind env sigma t] puts [t] in the form [t'=(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) -val reduce_to_atomic_ind : env -> evar_map -> EConstr.types -> pinductive * EConstr.types +val reduce_to_atomic_ind : env -> evar_map -> types -> pinductive * types (** [reduce_to_quantified_ind env sigma t] puts [t] in the form [t'=(x1:A1)..(xn:An)(I args)] with [I] an inductive definition; returns [I] and [t'] or fails with a user error *) -val reduce_to_quantified_ind : env -> evar_map -> EConstr.types -> pinductive * EConstr.types +val reduce_to_quantified_ind : env -> evar_map -> types -> pinductive * types (** [reduce_to_quantified_ref env sigma ref t] try to put [t] in the form [t'=(x1:A1)..(xn:An)(ref args)] and fails with user error if not possible *) val reduce_to_quantified_ref : - env -> evar_map -> global_reference -> EConstr.types -> EConstr.types + env -> evar_map -> global_reference -> types -> types val reduce_to_atomic_ref : - env -> evar_map -> global_reference -> EConstr.types -> EConstr.types + env -> evar_map -> global_reference -> types -> types val find_hnf_rectype : - env -> evar_map -> EConstr.types -> pinductive * EConstr.constr list + env -> evar_map -> types -> pinductive * constr list val contextually : bool -> occurrences * constr_pattern -> (patvar_map -> reduction_function) -> reduction_function diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 5bb865310c..20f27a15a2 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -100,7 +100,6 @@ let abstract_scheme env evd c l lname_typ = if occur_meta evd a then mkLambda_name env (na,ta,t), evd else let t', evd' = Find_subterm.subst_closed_term_occ env evd locc a t in - let t' = EConstr.of_constr t' in mkLambda_name env (na,ta,t'), evd') (c,evd) (List.rev l) @@ -1656,7 +1655,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = | NoOccurrences -> concl | occ -> let occ = if likefirst then LikeFirst else AtOccs occ in - EConstr.of_constr (replace_term_occ_modulo sigma occ test mkvarid concl) + replace_term_occ_modulo sigma occ test mkvarid concl in let lastlhyp = if List.is_empty depdecls then None else Some (NamedDecl.get_id (List.last depdecls)) in diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 58b82002da..26d4ac994b 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -8,11 +8,12 @@ open Names open Term +open EConstr open Constrexpr open Misctypes val lemInv_clause : - quantified_hypothesis -> EConstr.constr -> Id.t list -> unit Proofview.tactic + quantified_hypothesis -> constr -> Id.t list -> unit Proofview.tactic val add_inversion_lemma_exn : Id.t -> constr_expr -> glob_sort -> bool -> (Id.t -> unit Proofview.tactic) -> diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index e4f110722b..ba5452e33f 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -9,6 +9,7 @@ open Pp open Names open Term +open EConstr open Tacmach open Proof_type open Locus @@ -58,25 +59,25 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic (** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (Id.t -> tactic) -> tactic -val onNthHyp : int -> (EConstr.constr -> tactic) -> tactic +val onNthHyp : int -> (constr -> tactic) -> tactic val onNthDecl : int -> (Context.Named.Declaration.t -> tactic) -> tactic val onLastHypId : (Id.t -> tactic) -> tactic -val onLastHyp : (EConstr.constr -> tactic) -> tactic +val onLastHyp : (constr -> tactic) -> tactic val onLastDecl : (Context.Named.Declaration.t -> tactic) -> tactic val onNLastHypsId : int -> (Id.t list -> tactic) -> tactic -val onNLastHyps : int -> (constr list -> tactic) -> tactic +val onNLastHyps : int -> (Constr.constr list -> tactic) -> tactic val onNLastDecls : int -> (Context.Named.t -> tactic) -> tactic val lastHypId : goal sigma -> Id.t -val lastHyp : goal sigma -> EConstr.constr +val lastHyp : goal sigma -> constr val lastDecl : goal sigma -> Context.Named.Declaration.t val nLastHypsId : int -> goal sigma -> Id.t list -val nLastHyps : int -> goal sigma -> constr list +val nLastHyps : int -> goal sigma -> Constr.constr list val nLastDecls : int -> goal sigma -> Context.Named.t val afterHyp : Id.t -> goal sigma -> Context.Named.t -val ifOnHyp : (Id.t * EConstr.types -> bool) -> +val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> tactic) -> (Id.t -> tactic) -> Id.t -> tactic @@ -99,9 +100,9 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic type branch_args = private { ity : pinductive; (** the type we were eliminating on *) - largs : EConstr.constr list; (** its arguments *) + largs : constr list; (** its arguments *) branchnum : int; (** the branch number *) - pred : EConstr.constr; (** the predicate we used *) + pred : constr; (** the predicate we used *) nassums : int; (** number of assumptions/letin to be introduced *) branchsign : bool list; (** the signature of the branch. true=assumption, false=let-in *) @@ -134,7 +135,7 @@ val elimination_sort_of_hyp : Id.t -> goal sigma -> sorts_family val elimination_sort_of_clause : Id.t option -> goal sigma -> sorts_family val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic -val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic +val pf_constr_of_global : Globnames.global_reference -> (Constr.constr -> tactic) -> tactic val elim_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic val case_on_ba : (branch_assumptions -> tactic) -> branch_args -> tactic @@ -230,13 +231,13 @@ module New : sig val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t - val ifOnHyp : (identifier * EConstr.types -> bool) -> + val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> identifier -> unit Proofview.tactic val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic val onLastHypId : (identifier -> unit tactic) -> unit tactic - val onLastHyp : (EConstr.constr -> unit tactic) -> unit tactic + val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (Context.Named.Declaration.t -> unit tactic) -> unit tactic val onHyps : ([ `NF ], Context.Named.t) Proofview.Goal.enter -> @@ -253,18 +254,18 @@ module New : sig val elimination_then : (branch_args -> unit Proofview.tactic) -> - EConstr.constr -> unit Proofview.tactic + constr -> unit Proofview.tactic val case_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - EConstr.constr option -> pinductive -> EConstr.constr * EConstr.types -> unit Proofview.tactic + constr option -> pinductive -> constr * types -> unit Proofview.tactic val case_nodep_then_using : or_and_intro_pattern option -> (branch_args -> unit Proofview.tactic) -> - EConstr.constr option -> pinductive -> EConstr.constr * EConstr.types -> unit Proofview.tactic + constr option -> pinductive -> constr * types -> unit Proofview.tactic val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : Globnames.global_reference -> (constr -> unit Proofview.tactic) -> unit Proofview.tactic + val pf_constr_of_global : Globnames.global_reference -> (Constr.constr -> unit Proofview.tactic) -> unit Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f79f7f1a82..e4dd9eea26 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2821,7 +2821,6 @@ let generalize_goal_gen env sigma ids i ((occs,c,b),na) t cl = let dummy_prod = it_mkProd_or_LetIn mkProp decls in let newdecls,_ = decompose_prod_n_assum sigma i (subst_term_gen sigma EConstr.eq_constr_nounivs c dummy_prod) in let cl',sigma' = subst_closed_term_occ env sigma (AtOccs occs) c (it_mkProd_or_LetIn cl newdecls) in - let cl' = EConstr.of_constr cl' in let na = generalized_name sigma c t ids cl' na in let decl = match b with | None -> local_assum (na,t) -- cgit v1.2.3