diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:12:52 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:12:52 +0100 |
commit | eaff61e0a19fcf6ebc2a9a8ae17327413274c67b (patch) | |
tree | acbbc416ad78bf8520893405c04855c600909576 | |
parent | 073b92396a68be30f77c80960a58ca562bb01f49 (diff) | |
parent | 68935660fbfdec2e357e123ed999073ed3b8fc26 (diff) |
Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`
-rw-r--r-- | dev/doc/changes.md | 8 | ||||
-rw-r--r-- | engine/ftactic.mli | 4 | ||||
-rw-r--r-- | engine/proofview.ml | 4 | ||||
-rw-r--r-- | engine/proofview.mli | 39 | ||||
-rw-r--r-- | grammar/argextend.mlp | 1 | ||||
-rw-r--r-- | plugins/cc/cctac.ml | 2 | ||||
-rw-r--r-- | plugins/firstorder/ground.ml | 2 | ||||
-rw-r--r-- | plugins/romega/const_omega.ml | 4 | ||||
-rw-r--r-- | plugins/romega/const_omega.mli | 4 | ||||
-rw-r--r-- | plugins/ssr/ssrcommon.ml | 2 | ||||
-rw-r--r-- | proofs/clenv.mli | 8 | ||||
-rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
-rw-r--r-- | proofs/refine.ml | 2 | ||||
-rw-r--r-- | proofs/refine.mli | 2 | ||||
-rw-r--r-- | proofs/tacmach.ml | 6 | ||||
-rw-r--r-- | proofs/tacmach.mli | 48 | ||||
-rw-r--r-- | tactics/auto.ml | 4 | ||||
-rw-r--r-- | tactics/auto.mli | 4 | ||||
-rw-r--r-- | tactics/class_tactics.ml | 13 | ||||
-rw-r--r-- | tactics/contradiction.ml | 4 | ||||
-rw-r--r-- | tactics/eauto.ml | 2 | ||||
-rw-r--r-- | tactics/equality.ml | 15 | ||||
-rw-r--r-- | tactics/hipattern.mli | 4 | ||||
-rw-r--r-- | tactics/inv.ml | 2 | ||||
-rw-r--r-- | tactics/tacticals.ml | 7 | ||||
-rw-r--r-- | tactics/tacticals.mli | 10 | ||||
-rw-r--r-- | tactics/tactics.ml | 33 | ||||
-rw-r--r-- | tactics/tactics.mli | 4 |
28 files changed, 112 insertions, 128 deletions
diff --git a/dev/doc/changes.md b/dev/doc/changes.md index aef62b009..16a31790a 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -20,6 +20,14 @@ General deprecation removed. Please, make sure your plugin is warning-free in 8.7 before trying to port it over 8.8. +Proof engine + + Due to the introduction of `EConstr` in 8.7, it is not necessary to + track "goal evar normal form status" anymore, thus the type `'a + Proofview.Goal.t` loses its ghost argument. This may introduce some + minor incompatibilities at the typing level. Code-wise, things + should remain the same. + We removed the following functions: - `Universes.unsafe_constr_of_global`: use `Global.constr_of_global_in_context` diff --git a/engine/ftactic.mli b/engine/ftactic.mli index c108c0c2e..65ee929c8 100644 --- a/engine/ftactic.mli +++ b/engine/ftactic.mli @@ -39,10 +39,10 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic (** {5 Focussing} *) -val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t +val nf_enter : (Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal. The resulting tactic is focussed. *) -val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t +val enter : (Proofview.Goal.t -> 'a t) -> 'a t (** Enter a goal, without evar normalization. The resulting tactic is focussed. *) diff --git a/engine/proofview.ml b/engine/proofview.ml index 47b9b406d..c41b0b0dc 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1023,14 +1023,14 @@ let catchable_exception = function module Goal = struct - type 'a t = { + type t = { env : Environ.env; sigma : Evd.evar_map; concl : EConstr.constr ; self : Evar.t ; (* for compatibility with old-style definitions *) } - let assume (gl : 'a t) = (gl :> [ `NF ] t) + let assume (gl : t) = (gl : t) let env {env} = env let sigma {sigma} = sigma diff --git a/engine/proofview.mli b/engine/proofview.mli index b02fde3a8..721ce507d 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -461,56 +461,49 @@ end module Goal : sig - (** Type of goals. - - The first parameter type is a phantom argument indicating whether the data - contained in the goal has been normalized w.r.t. the current sigma. If it - is the case, it is flagged [ `NF ]. You may still access the un-normalized - data using {!assume} if you known you do not rely on the assumption of - being normalized, at your own risk. - - *) - type 'a t + (** Type of goals. *) + type t (** Assume that you do not need the goal to be normalized. *) - val assume : 'a t -> [ `NF ] t + val assume : t -> t + [@@ocaml.deprecated "Normalization is enforced by EConstr, [assume] is not needed anymore"] (** Normalises the argument goal. *) - val normalize : 'a t -> [ `NF ] t tactic + val normalize : t -> t tactic (** [concl], [hyps], [env] and [sigma] given a goal [gl] return respectively the conclusion of [gl], the hypotheses of [gl], the environment of [gl] (i.e. the global environment and the hypotheses) and the current evar map. *) - val concl : 'a t -> constr - val hyps : 'a t -> named_context - val env : 'a t -> Environ.env - val sigma : 'a t -> Evd.evar_map - val extra : 'a t -> Evd.Store.t + val concl : t -> constr + val hyps : t -> named_context + val env : t -> Environ.env + val sigma : t -> Evd.evar_map + val extra : t -> Evd.Store.t (** [nf_enter t] applies the goal-dependent tactic [t] in each goal independently, in the manner of {!tclINDEPENDENT} except that the current goal is also given as an argument to [t]. The goal is normalised with respect to evars. *) - val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic + val nf_enter : (t -> unit tactic) -> unit tactic (** Like {!nf_enter}, but does not normalize the goal beforehand. *) - val enter : ([ `LZ ] t -> unit tactic) -> unit tactic + val enter : (t -> unit tactic) -> unit tactic (** Like {!enter}, but assumes exactly one goal under focus, raising *) (** a fatal error otherwise. *) - val enter_one : ?__LOC__:string -> ([ `LZ ] t -> 'a tactic) -> 'a tactic + val enter_one : ?__LOC__:string -> (t -> 'a tactic) -> 'a tactic (** Recover the list of current goals under focus, without evar-normalization. FIXME: encapsulate the level in an existential type. *) - val goals : [ `LZ ] t tactic list tactic + val goals : t tactic list tactic (** [unsolved g] is [true] if [g] is still unsolved in the current proof state. *) - val unsolved : 'a t -> bool tactic + val unsolved : t -> bool tactic (** Compatibility: avoid if possible *) - val goal : [ `NF ] t -> Evar.t + val goal : t -> Evar.t end diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 9742a002d..01138702b 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -138,7 +138,6 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = <:expr< let f = $lid:f$ in fun ist v -> Ftactic.enter (fun gl -> - let gl = Proofview.Goal.assume gl in let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 8642df684..7f8f60e46 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -187,7 +187,7 @@ let make_prb gls depth additionnal_terms = let open Tacmach.New in let env=pf_env gls in let sigma=project gls in - let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in + let state = empty depth {it = Proofview.Goal.goal gls; sigma } in let pos_hyps = ref [] in let neg_hyps =ref [] in List.iter diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index d46201335..09147d606 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -37,7 +37,7 @@ let ground_tac solver startseq = let () = if Tacinterp.get_debug()=Tactic_debug.DebugOn 0 then - let gl = { Evd.it = Proofview.Goal.goal (Proofview.Goal.assume gl); sigma = project gl } in + let gl = { Evd.it = Proofview.Goal.goal gl; sigma = project gl } in Feedback.msg_debug (Printer.pr_goal gl) in tclORELSE (axiom_tac seq.gl seq) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 0d491d92b..0f5417e7d 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -223,7 +223,7 @@ let mk_N = function module type Int = sig val typ : constr Lazy.t - val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool + val is_int_typ : Proofview.Goal.t -> constr -> bool val plus : constr Lazy.t val mult : constr Lazy.t val opp : constr Lazy.t @@ -231,7 +231,7 @@ module type Int = sig val mk : Bigint.bigint -> constr val parse_term : constr -> parse_term - val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel + val parse_rel : Proofview.Goal.t -> constr -> parse_rel (* check whether t is built only with numbers and + * - *) val get_scalar : constr -> Bigint.bigint option end diff --git a/plugins/romega/const_omega.mli b/plugins/romega/const_omega.mli index 5ba063d9d..ecddc55de 100644 --- a/plugins/romega/const_omega.mli +++ b/plugins/romega/const_omega.mli @@ -105,7 +105,7 @@ module type Int = (* the coq type of the numbers *) val typ : constr Lazy.t (* Is a constr expands to the type of these numbers *) - val is_int_typ : [ `NF ] Proofview.Goal.t -> constr -> bool + val is_int_typ : Proofview.Goal.t -> constr -> bool (* the operations on the numbers *) val plus : constr Lazy.t val mult : constr Lazy.t @@ -116,7 +116,7 @@ module type Int = (* parsing a term (one level, except if a number is found) *) val parse_term : constr -> parse_term (* parsing a relation expression, including = < <= >= > *) - val parse_rel : [ `NF ] Proofview.Goal.t -> constr -> parse_rel + val parse_rel : Proofview.Goal.t -> constr -> parse_rel (* Is a particular term only made of numbers and + * - ? *) val get_scalar : constr -> Bigint.bigint option end diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index d25ecee06..9822da1c7 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -1061,7 +1061,7 @@ let () = CLexer.set_keyword_state frozen_lexer ;; (** Basic tactics *) let rec fst_prod red tac = Proofview.Goal.nf_enter begin fun gl -> - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in match EConstr.kind (Proofview.Goal.sigma gl) concl with | Prod (id,_,tgt) | LetIn(id,_,_,tgt) -> tac id | _ -> if red then Tacticals.New.tclZEROMSG (str"No product even after head-reduction.") diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 9a2026dd3..c894b9dc9 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -41,10 +41,10 @@ val clenv_nf_meta : clausenv -> EConstr.constr -> EConstr.constr (** type of a meta in clenv context *) val clenv_meta_type : clausenv -> metavariable -> types -val mk_clenv_from : 'a Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : - 'a Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv -val mk_clenv_type_of : 'a Proofview.Goal.t -> EConstr.constr -> clausenv + Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv +val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) @@ -66,7 +66,7 @@ val old_clenv_unique_resolver : ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv val clenv_unique_resolver : - ?flags:unify_flags -> clausenv -> 'a Proofview.Goal.t -> clausenv + ?flags:unify_flags -> clausenv -> Proofview.Goal.t -> clausenv val clenv_dependent : clausenv -> metavariable list diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 8bd5d98cb..373d60e69 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -141,7 +141,7 @@ let fail_quick_unif_flags = { let unify ?(flags=fail_quick_unif_flags) m = Proofview.Goal.enter begin fun gl -> let env = Tacmach.New.pf_env gl in - let n = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in + let n = Tacmach.New.pf_concl gl in let evd = clear_metas (Tacmach.New.project gl) in try let evd' = w_unify env evd CONV ~flags m n in diff --git a/proofs/refine.ml b/proofs/refine.ml index e3f650848..90276951b 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -70,7 +70,6 @@ let add_side_effects env effects = List.fold_left (fun env eff -> add_side_effect env eff) env effects let generic_refine ~typecheck f gl = - let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in @@ -159,7 +158,6 @@ let with_type env evd c t = evd , j'.Environ.uj_val let refine_casted ~typecheck f = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let f h = diff --git a/proofs/refine.mli b/proofs/refine.mli index cfdcde36e..1932a306c 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -33,7 +33,7 @@ val refine_one : typecheck:bool -> (Evd.evar_map -> Evd.evar_map * ('a * EConstr (** A variant of [refine] which assumes exactly one goal under focus *) val generic_refine : typecheck:bool -> ('a * EConstr.t) tactic -> - [ `NF ] Proofview.Goal.t -> 'a tactic + Proofview.Goal.t -> 'a tactic (** The general version of refine. *) (** {7 Helper functions} *) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index bdcb4868b..d3405b892 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -150,7 +150,6 @@ module New = struct let pf_global id gl = (** We only check for the existence of an [id] in [hyps] *) - let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in Constrintern.construct_reference hyps id @@ -167,13 +166,11 @@ module New = struct let pf_ids_of_hyps gl = (** We only get the identifiers in [hyps] *) - let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in ids_of_named_context hyps let pf_ids_set_of_hyps gl = (** We only get the identifiers in [hyps] *) - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in Environ.ids_of_named_context_val (Environ.named_context_val env) @@ -204,9 +201,8 @@ module New = struct let hyps = Proofview.Goal.hyps gl in List.hd hyps - let pf_nf_concl (gl : [ `LZ ] Proofview.Goal.t) = + let pf_nf_concl (gl : Proofview.Goal.t) = (** We normalize the conclusion just after *) - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = project gl in nf_evar sigma concl diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index e0fb8fbc5..8f69358d4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -92,46 +92,46 @@ val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig - val pf_apply : (env -> evar_map -> 'a) -> 'b Proofview.Goal.t -> 'a - val pf_global : Id.t -> 'a Proofview.Goal.t -> Globnames.global_reference + val pf_apply : (env -> evar_map -> 'a) -> Proofview.Goal.t -> 'a + val pf_global : Id.t -> Proofview.Goal.t -> Globnames.global_reference (** FIXME: encapsulate the level in an existential type. *) - val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a + val of_old : (Proof_type.goal Evd.sigma -> 'a) -> Proofview.Goal.t -> 'a - val project : 'a Proofview.Goal.t -> Evd.evar_map - val pf_env : 'a Proofview.Goal.t -> Environ.env - val pf_concl : 'a Proofview.Goal.t -> types + val project : Proofview.Goal.t -> Evd.evar_map + val pf_env : Proofview.Goal.t -> Environ.env + val pf_concl : Proofview.Goal.t -> types (** WRONG: To be avoided at all costs, it typechecks the term entirely but forgets the universe constraints necessary to retypecheck it *) - val pf_unsafe_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_unsafe_type_of : Proofview.Goal.t -> constr -> types (** This function does no type inference and expects an already well-typed term. It recomputes its type in the fastest way possible (no conversion is ever involved) *) - val pf_get_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_get_type_of : Proofview.Goal.t -> constr -> types (** This function entirely type-checks the term and computes its type and the implied universe constraints. *) - val pf_type_of : 'a Proofview.Goal.t -> constr -> evar_map * types - val pf_conv_x : 'a Proofview.Goal.t -> t -> t -> bool + val pf_type_of : Proofview.Goal.t -> constr -> evar_map * types + val pf_conv_x : Proofview.Goal.t -> t -> t -> bool - val pf_get_new_id : Id.t -> 'a Proofview.Goal.t -> Id.t - val pf_ids_of_hyps : 'a Proofview.Goal.t -> Id.t list - val pf_ids_set_of_hyps : 'a Proofview.Goal.t -> Id.Set.t - val pf_hyps_types : 'a Proofview.Goal.t -> (Id.t * types) list + val pf_get_new_id : Id.t -> Proofview.Goal.t -> Id.t + val pf_ids_of_hyps : Proofview.Goal.t -> Id.t list + val pf_ids_set_of_hyps : Proofview.Goal.t -> Id.Set.t + val pf_hyps_types : Proofview.Goal.t -> (Id.t * types) list - val pf_get_hyp : Id.t -> 'a Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : Id.t -> 'a Proofview.Goal.t -> types - val pf_last_hyp : 'a Proofview.Goal.t -> named_declaration + val pf_get_hyp : Id.t -> Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : Id.t -> Proofview.Goal.t -> types + val pf_last_hyp : Proofview.Goal.t -> named_declaration - val pf_nf_concl : [ `LZ ] Proofview.Goal.t -> types - val pf_reduce_to_quantified_ind : 'a Proofview.Goal.t -> types -> (inductive * EInstance.t) * types + val pf_nf_concl : Proofview.Goal.t -> types + val pf_reduce_to_quantified_ind : Proofview.Goal.t -> types -> (inductive * EInstance.t) * types - val pf_hnf_constr : 'a Proofview.Goal.t -> constr -> types - val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types + val pf_hnf_constr : Proofview.Goal.t -> constr -> types + val pf_hnf_type_of : Proofview.Goal.t -> constr -> types - val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr - val pf_compute : 'a Proofview.Goal.t -> constr -> constr + val pf_whd_all : Proofview.Goal.t -> constr -> constr + val pf_compute : Proofview.Goal.t -> constr -> constr - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr + val pf_nf_evar : Proofview.Goal.t -> constr -> constr end diff --git a/tactics/auto.ml b/tactics/auto.ml index e7e21b5f4..eec7a5f2a 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -32,7 +32,7 @@ open Hints let priority l = List.filter (fun (_, hint) -> Int.equal hint.pri 0) l let compute_secvars gl = - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in secvars_of_hyps hyps (* tell auto not to reuse already instantiated metas in unification (for @@ -316,7 +316,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let sigma = Tacmach.New.project gl in let env = Proofview.Goal.env gl in let nf c = Evarutil.nf_evar sigma c in - let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in + let decl = Tacmach.New.pf_last_hyp gl in let hyp = Context.Named.Declaration.map_constr nf decl in let hintl = make_resolve_hyp env sigma hyp in trivial_fail_db dbg mod_delta db_list diff --git a/tactics/auto.mli b/tactics/auto.mli index b9cd4932c..59809331e 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -16,14 +16,14 @@ open Decl_kinds open Hints open Tactypes -val compute_secvars : 'a Proofview.Goal.t -> Id.Pred.t +val compute_secvars : Proofview.Goal.t -> Id.Pred.t val default_search_depth : int ref val auto_flags_of_state : transparent_state -> Unification.unify_flags val connect_hint_clenv : polymorphic -> raw_hint -> clausenv -> - 'a Proofview.Goal.t -> clausenv * constr + Proofview.Goal.t -> clausenv * constr (** Try unification with the precompiled clause, then use registered Apply *) val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index cfadfc535..a95e6b941 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -996,7 +996,7 @@ module Search = struct Hint_db.transparent_state cached_hints == st then cached_hints else - let hints = make_hints {it = Goal.goal (Proofview.Goal.assume g); sigma = project g} + let hints = make_hints {it = Goal.goal g; sigma = project g} st only_classes sign in autogoal_cache := (cwd, only_classes, sign, hints); hints @@ -1041,7 +1041,6 @@ module Search = struct let fail_if_nonclass info = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in if is_class_type sigma (Proofview.Goal.concl gl) then Proofview.tclUNIT () @@ -1089,7 +1088,7 @@ module Search = struct pr_depth (idx :: info.search_depth) ++ str": " ++ Lazy.force pp ++ (if !foundone != true then - str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl)) + str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl) else mt ()) in let msg = @@ -1110,7 +1109,7 @@ module Search = struct if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth (succ j :: i :: info.search_depth) ++ str" : " ++ - pr_ev sigma' (Proofview.Goal.goal (Proofview.Goal.assume gl'))); + pr_ev sigma' (Proofview.Goal.goal gl')); let eq c1 c2 = EConstr.eq_constr sigma' c1 c2 in let hints' = if b && not (Context.Named.equal eq (Goal.hyps gl') (Goal.hyps gl)) @@ -1119,7 +1118,7 @@ module Search = struct make_autogoal_hints info.search_only_classes ~st gl' else info.search_hints in - let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal (Proofview.Goal.assume gl')) gls in + let dep' = info.search_dep || Proofview.unifiable sigma' (Goal.goal gl') gls in let info' = { search_depth = succ j :: i :: info.search_depth; last_tac = pp; @@ -1136,7 +1135,7 @@ module Search = struct (if !typeclasses_debug > 0 then Feedback.msg_debug (pr_depth (i :: info.search_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal (Proofview.Goal.assume gl)) + ++ str" on" ++ spc () ++ pr_ev sigma (Proofview.Goal.goal gl) ++ str", " ++ int j ++ str" subgoal(s)" ++ (Option.cata (fun k -> str " in addition to the first " ++ int k) (mt()) k))); @@ -1261,7 +1260,7 @@ module Search = struct if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then Tacticals.New.tclZEROMSG (str"Not a subgoal for a class") else - let dep = dep || Proofview.unifiable sigma (Goal.goal (Proofview.Goal.assume gl)) gls in + let dep = dep || Proofview.unifiable sigma (Goal.goal gl) gls in let info = make_autogoal ?st only_classes dep (cut_of_hints hints) i gl in search_tac hints depth 1 info diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 5e2006ccc..467754a84 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -53,7 +53,7 @@ let filter_hyp f tac = | d::rest when f (NamedDecl.get_type d) -> tac (NamedDecl.get_id d) | _::rest -> seek rest in Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in seek hyps end @@ -98,7 +98,7 @@ let contradiction_context = end) | _ -> seek_neg rest in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in seek_neg hyps end diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 6ea6155e0..785d2f515 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -32,7 +32,7 @@ let eauto_unif_flags = auto_flags_of_state full_transparent_state let e_give_exact ?(flags=eauto_unif_flags) c = Proofview.Goal.enter begin fun gl -> let t1 = Tacmach.New.pf_unsafe_type_of gl c in - let t2 = Tacmach.New.pf_concl (Proofview.Goal.assume gl) in + let t2 = Tacmach.New.pf_concl gl in let sigma = Tacmach.New.project gl in if occur_existential sigma t1 || occur_existential sigma t2 then Tacticals.New.tclTHEN (Clenvtac.unify ~flags t1) (exact_no_check c) diff --git a/tactics/equality.ml b/tactics/equality.ml index 450d68436..674d01777 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -266,7 +266,7 @@ let rewrite_elim with_evars frzevars cls c e = end let tclNOTSAMEGOAL tac = - let goal gl = Proofview.Goal.goal (Proofview.Goal.assume gl) in + let goal gl = Proofview.Goal.goal gl in Proofview.Goal.nf_enter begin fun gl -> let sigma = project gl in let ev = goal gl in @@ -324,7 +324,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim = in let typ = match cls with | None -> pf_concl gl - | Some id -> pf_get_hyp_typ id (Proofview.Goal.assume gl) + | Some id -> pf_get_hyp_typ id gl in let cs = instantiate_lemma typ in if firstonly then tclFIRST (List.map try_clause cs) @@ -970,7 +970,7 @@ let rec build_discriminator env sigma true_0 false_0 dirn c = function let gen_absurdity id = Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in + let hyp_typ = pf_get_hyp_typ id gl in if is_empty_type sigma hyp_typ then simplest_elim (mkVar id) @@ -1443,7 +1443,7 @@ let get_previous_hyp_position id gl = let hyp = Context.Named.Declaration.get_id d in if Id.equal hyp id then dest else aux (MoveAfter hyp) right in - aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + aux MoveLast (Proofview.Goal.hyps gl) let injEq flags ?(old=false) with_evars clear_flag ipats = (* Decide which compatibility mode to use *) @@ -1716,8 +1716,8 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in + let concl = Proofview.Goal.concl gl in (* The set of hypotheses using x *) let dephyps = List.rev (pi3 (List.fold_right (fun dcl (dest,deps,allhyps) -> @@ -1749,7 +1749,6 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = let subst_one_var dep_proof_ok x = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let decl = pf_get_hyp x gl in (* If x has a body, simply replace x with body and clear x *) if is_local_def decl then tclTHEN (unfold_body x) (clear [x]) else @@ -1790,7 +1789,6 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* First step: find hypotheses to treat in linear time *) let find_equations gl = - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let sigma = project gl in let find_eq_data_decompose = find_eq_data_decompose gl in @@ -1816,7 +1814,6 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* Second step: treat equations *) let process hyp = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let sigma = project gl in let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 237ed42d5..01d916053 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -120,11 +120,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : 'a Proofview.Goal.t -> constr -> +val find_eq_data_decompose : Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : Proofview.Goal.t -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) diff --git a/tactics/inv.ml b/tactics/inv.ml index cb0bbfd0e..5435b63ce 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -353,7 +353,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = Proofview.Goal.enter begin fun gl -> let sigma = project gl in (** We only look at the type of hypothesis "id" *) - let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in + let hyp = pf_nf_evar gl (pf_get_hyp_typ id gl) in let (t,t1,t2) = dest_nf_eq (pf_env gl) sigma hyp in match (EConstr.kind sigma t1, EConstr.kind sigma t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index cea6ccc30..e7da17cff 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -540,7 +540,6 @@ module New = struct let nthHypId m gl = (** We only use [id] *) - let gl = Proofview.Goal.assume gl in nthDecl m gl |> NamedDecl.get_id let nthHyp m gl = mkVar (nthHypId m gl) @@ -572,7 +571,7 @@ module New = struct let afterHyp id tac = Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let rem, _ = List.split_when (NamedDecl.get_id %> Id.equal id) hyps in tac rem end @@ -658,12 +657,12 @@ module New = struct let elimination_sort_of_goal gl = (** Retyping will expand evars anyway. *) - let c = Proofview.Goal.concl (Goal.assume gl) in + let c = Proofview.Goal.concl gl in pf_apply Retyping.get_sort_family_of gl c let elimination_sort_of_hyp id gl = (** Retyping will expand evars anyway. *) - let c = pf_get_hyp_typ id (Goal.assume gl) in + let c = pf_get_hyp_typ id gl in pf_apply Retyping.get_sort_family_of gl c let elimination_sort_of_clause id gl = match id with diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 55c519e24..c5d5c8c12 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -225,7 +225,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : 'a Proofview.Goal.t -> int -> named_context + val nLastDecls : Proofview.Goal.t -> int -> named_context val ifOnHyp : (Id.t * types -> bool) -> (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> @@ -236,7 +236,7 @@ module New : sig val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic - val onHyps : ([ `LZ ] Proofview.Goal.t -> named_context) -> + val onHyps : (Proofview.Goal.t -> named_context) -> (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic @@ -244,9 +244,9 @@ module New : sig val tryAllHypsAndConcl : (Id.t option -> unit tactic) -> unit tactic val onClause : (Id.t option -> unit tactic) -> clause -> unit tactic - val elimination_sort_of_goal : 'a Proofview.Goal.t -> Sorts.family - val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> Sorts.family - val elimination_sort_of_clause : Id.t option -> 'a Proofview.Goal.t -> Sorts.family + val elimination_sort_of_goal : Proofview.Goal.t -> Sorts.family + val elimination_sort_of_hyp : Id.t -> Proofview.Goal.t -> Sorts.family + val elimination_sort_of_clause : Id.t option -> Proofview.Goal.t -> Sorts.family val elimination_then : (branch_args -> unit Proofview.tactic) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index d5160fc9a..29a30b4a2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -151,7 +151,6 @@ let unsafe_intro env store decl b = let introduction ?(check=true) id = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let hyps = named_context_val (Proofview.Goal.env gl) in @@ -258,7 +257,6 @@ let clear_gen fail = function Proofview.Goal.enter begin fun gl -> let ids = List.fold_right Id.Set.add ids Id.Set.empty in (** clear_hyps_in_evi does not require nf terms *) - let gl = Proofview.Goal.assume gl in let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in @@ -322,7 +320,6 @@ let rename_hyp repl = | None -> Tacticals.New.tclZEROMSG (str "Not a one-to-one name mapping") | Some (src, dst) -> Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let hyps = Proofview.Goal.hyps gl in let concl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in @@ -814,7 +811,7 @@ let e_pf_change_decl (redfun : bool -> e_reduction_function) where decl env sigm let e_change_in_hyp redfun (id,where) = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let hyp = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + let hyp = Tacmach.New.pf_get_hyp id gl in let (sigma, c) = e_pf_change_decl redfun where hyp (Proofview.Goal.env gl) sigma in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (convert_hyp c) @@ -981,7 +978,7 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = Proofview.Goal.enter begin fun gl -> let sigma = Tacmach.New.project gl in let env = Tacmach.New.pf_env gl in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in match EConstr.kind sigma concl with | Prod (name,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalAssum (name,t)) name_flag gl in @@ -1052,7 +1049,7 @@ let intro_forthcoming_then_gen name_flag move_flag dep_flag n bound tac = let intro_replacing id = Proofview.Goal.enter begin fun gl -> let env, sigma = Proofview.Goal.(env gl, sigma gl) in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let next_hyp = get_next_hyp_position env sigma id hyps in Tacticals.New.tclTHENLIST [ clear_for_replacing [id]; @@ -1073,7 +1070,7 @@ let intros_possibly_replacing ids = let suboptimal = true in Proofview.Goal.enter begin fun gl -> let env, sigma = Proofview.Goal.(env gl, sigma gl) in - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN (Tacticals.New.tclMAP (fun id -> @@ -1087,7 +1084,7 @@ let intros_possibly_replacing ids = (* This version assumes that replacement is actually possible *) let intros_replacing ids = Proofview.Goal.enter begin fun gl -> - let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in + let hyps = Proofview.Goal.hyps gl in let env, sigma = Proofview.Goal.(env gl, sigma gl) in let posl = List.map (fun id -> (id, get_next_hyp_position env sigma id hyps)) ids in Tacticals.New.tclTHEN @@ -1150,7 +1147,7 @@ let intros_until_n = intros_until_n_gen true let tclCHECKVAR id = Proofview.Goal.enter begin fun gl -> - let _ = Tacmach.New.pf_get_hyp id (Proofview.Goal.assume gl) in + let _ = Tacmach.New.pf_get_hyp id gl in Proofview.tclUNIT () end @@ -1973,7 +1970,7 @@ let exact_check c = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in (** We do not need to normalize the goal because we just check convertibility *) - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let sigma, ct = Typing.type_of env sigma c in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) @@ -1982,7 +1979,7 @@ let exact_check c = let cast_no_check cast c = Proofview.Goal.enter begin fun gl -> - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in exact_no_check (mkCast (c, cast, concl)) end @@ -2066,7 +2063,7 @@ let clear_body ids = let open Context.Named.Declaration in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let concl = Proofview.Goal.concl gl in let sigma = Tacmach.New.project gl in let ctx = named_context env in let map = function @@ -2191,7 +2188,6 @@ let bring_hyps hyps = let revert hyps = Proofview.Goal.enter begin fun gl -> - let gl = Proofview.Goal.assume gl in let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in (bring_hyps ctx) <*> (clear hyps) end @@ -2619,7 +2615,7 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars if with_evars then MoveLast (* evars would depend on the whole context *) else ( let env, sigma = Proofview.Goal.(env gl, sigma gl) in - get_previous_hyp_position env sigma id (Proofview.Goal.hyps (Proofview.Goal.assume gl)) + get_previous_hyp_position env sigma id (Proofview.Goal.hyps gl) ) in let naming,ipat_tac = prepare_intros_opt with_evars (IntroIdentifier id) destopt ipat in @@ -2913,7 +2909,6 @@ end let new_generalize_gen_let lconstr = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let gl = Proofview.Goal.assume gl in let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in let ids = Tacmach.New.pf_ids_of_hyps gl in @@ -3063,7 +3058,7 @@ let unfold_body x = let open Context.Named.Declaration in Proofview.Goal.enter begin fun gl -> (** We normalize the given hypothesis immediately. *) - let env = Proofview.Goal.env (Proofview.Goal.assume gl) in + let env = Proofview.Goal.env gl in let xval = match Environ.lookup_named x env with | LocalAssum _ -> user_err ~hdr:"unfold_body" (Id.print x ++ str" is not a defined hypothesis.") @@ -3274,7 +3269,7 @@ let atomize_param_of_ind_then (indref,nparams,_) hyp0 tac = Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 (Proofview.Goal.assume gl) in + let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in let typ0 = reduce_to_quantified_ref indref tmptyp0 in let prods, indtyp = decompose_prod_assum sigma typ0 in @@ -4272,7 +4267,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let deps_cstr = List.fold_left (fun a decl -> if NamedDecl.is_local_assum decl then (mkVar (NamedDecl.get_id decl))::a else a) [] deps in - let (sigma, isrec, elim, indsign) = get_eliminator elim dep s (Proofview.Goal.assume gl) in + let (sigma, isrec, elim, indsign) = get_eliminator elim dep s gl in let branchletsigns = let f (_,is_not_let,_,_) = is_not_let in Array.map (fun (_,l) -> List.map f l) indsign in @@ -4297,7 +4292,7 @@ let apply_induction_in_context with_evars hyp0 inhyps elim indvars names induct_ let induction_with_atomization_of_ind_arg isrec with_evars elim names hyp0 inhyps = Proofview.Goal.enter begin fun gl -> - let elim_info = find_induction_type isrec elim hyp0 (Proofview.Goal.assume gl) in + let elim_info = find_induction_type isrec elim hyp0 gl in atomize_param_of_ind_then elim_info hyp0 (fun indvars -> apply_induction_in_context with_evars (Some hyp0) inhyps (pi3 elim_info) indvars names (fun elim -> induction_tac with_evars [] [hyp0] elim)) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index ca8e0f20c..74415f8d0 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -30,7 +30,7 @@ open Ltac_pretype (** {6 General functions. } *) -val is_quantified_hypothesis : Id.t -> 'a Proofview.Goal.t -> bool +val is_quantified_hypothesis : Id.t -> Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) @@ -76,7 +76,7 @@ val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> 'a Proofview.Goal.t -> int + bool -> quantified_hypothesis -> Proofview.Goal.t -> int val intros_until : quantified_hypothesis -> unit Proofview.tactic |