diff options
| -rw-r--r-- | engine/proofview.ml | 3 | ||||
| -rw-r--r-- | engine/proofview.mli | 8 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 10 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 6 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 12 |
6 files changed, 17 insertions, 24 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 0a18cf191..71e9acc88 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -999,9 +999,6 @@ module Goal = struct let concl { concl=concl } = concl let extra { sigma=sigma; self=self } = goal_extra sigma self - let raw_concl { concl=concl } = concl - - let gmake_with info env sigma goal = { env = Environ.reset_with_named_context (Evd.evar_filtered_hyps info) env ; sigma = sigma ; diff --git a/engine/proofview.mli b/engine/proofview.mli index 025e3de20..4f662b294 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -485,16 +485,12 @@ module Goal : sig 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 : ([ `NF ], 'r) t -> constr - val hyps : ([ `NF ], 'r) t -> named_context + val concl : ('a, 'r) t -> constr + val hyps : ('a, 'r) t -> named_context val env : ('a, 'r) t -> Environ.env val sigma : ('a, 'r) t -> 'r Sigma.t val extra : ('a, 'r) t -> Evd.Store.t - (** Returns the goal's conclusion even if the goal is not - normalised. *) - val raw_concl : ('a, 'r) t -> constr - type ('a, 'b) enter = { enter : 'r. ('a, 'r) t -> 'b } diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 3b23a6ab4..1992cec65 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -107,19 +107,19 @@ module New : sig val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env - val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types + val pf_concl : ('a, 'r) Proofview.Goal.t -> types val pf_unsafe_type_of : ('a, 'r) Proofview.Goal.t -> constr -> types val pf_type_of : ('a, 'r) Proofview.Goal.t -> constr -> evar_map * types val pf_conv_x : ('a, 'r) Proofview.Goal.t -> t -> t -> bool - val pf_get_new_id : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> identifier + val pf_get_new_id : identifier -> ('a, 'r) Proofview.Goal.t -> identifier val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list - val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration - val pf_get_hyp_typ : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types - val pf_last_hyp : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration + val pf_get_hyp : identifier -> ('a, 'r) Proofview.Goal.t -> named_declaration + val pf_get_hyp_typ : identifier -> ('a, 'r) Proofview.Goal.t -> types + val pf_last_hyp : ('a, 'r) Proofview.Goal.t -> named_declaration val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 65ba0aad0..c46817f50 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -121,11 +121,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 : ([ `NF ], 'r) Proofview.Goal.t -> constr -> +val find_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr -> coq_eq_data * Univ.universe_instance * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : ('a, 'r) Proofview.Goal.t -> constr -> coq_eq_data * Univ.universe_instance * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) @@ -146,7 +146,7 @@ val is_matching_sigma : evar_map -> constr -> bool val match_eqdec : evar_map -> constr -> bool * constr * constr * constr * constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (constr * constr * constr) +val dest_nf_eq : ('a, 'r) Proofview.Goal.t -> constr -> (constr * constr * constr) (** Match a negation *) val is_matching_not : evar_map -> constr -> bool diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index e9f623100..4bb745875 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -229,7 +229,7 @@ module New : sig val tclTIMEOUT : int -> unit tactic -> unit tactic val tclTIME : string option -> 'a tactic -> 'a tactic - val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context + val nLastDecls : ('a, 'r) Proofview.Goal.t -> int -> named_context val ifOnHyp : (identifier * types -> bool) -> (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4bf848a9c..de3572155 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -208,7 +208,7 @@ let convert_concl ?(check=true) ty k = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let store = Proofview.Goal.extra gl in - let conclty = Proofview.Goal.raw_concl gl in + let conclty = Proofview.Goal.concl gl in Refine.refine ~unsafe:true { run = begin fun sigma -> let Sigma ((), sigma, p) = if check then begin @@ -228,7 +228,7 @@ let convert_hyp ?(check=true) d = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let ty = Proofview.Goal.raw_concl gl in + let ty = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let sign = convert_hyp check (named_context_val env) sigma d in let env = reset_with_named_context sign env in @@ -328,7 +328,7 @@ let move_hyp id dest = Proofview.Goal.enter { enter = begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in - let ty = Proofview.Goal.raw_concl gl in + let ty = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let sign = named_context_val env in let sign' = move_hyp_in_named_context sigma id dest sign in @@ -756,7 +756,7 @@ let e_reduct_option ?(check=false) redfun = function let e_change_in_concl (redfun,sty) = Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.raw_concl gl) in + let Sigma (c, sigma, p) = redfun.e_redfun (Proofview.Goal.env gl) sigma (Proofview.Goal.concl gl) in Sigma (convert_concl_no_check c sty, sigma, p) end } @@ -4340,7 +4340,7 @@ let pose_induction_arg_then isrec with_evars (is_arg_pure_hyp,from_prefix) elim Proofview.Goal.s_enter { s_enter = begin fun gl -> let sigma = Proofview.Goal.sigma gl in let env = Proofview.Goal.env gl in - let ccl = Proofview.Goal.raw_concl gl in + let ccl = Proofview.Goal.concl gl in let store = Proofview.Goal.extra gl in let check = check_enough_applied env sigma elim in let Sigma (c, sigma', p) = use_bindings env sigma elim false (c0,lbind) t0 in @@ -4409,7 +4409,7 @@ let induction_gen clear_flag isrec with_evars elim let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let evd = Sigma.to_evar_map sigma in - let ccl = Proofview.Goal.raw_concl gl in + let ccl = Proofview.Goal.concl gl in let cls = Option.default allHypsAndConcl cls in let t = typ_of env sigma c in let is_arg_pure_hyp = |