diff options
| -rw-r--r-- | proofs/proofview.ml | 9 | ||||
| -rw-r--r-- | proofs/proofview.mli | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 53 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
5 files changed, 68 insertions, 4 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 8a4531c12..506d04f38 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -930,6 +930,15 @@ struct let h = (evd, evk :: evs) in (h, ev) + let new_evar_instance (evd, evs) ctx typ inst = + let src = (Loc.ghost, Evar_kinds.GoalEvar) in + let (evd, ev) = Evarutil.new_evar_instance ctx evd ~src typ inst in + let evd = Typeclasses.mark_unresolvables + ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in + let (evk, _) = Term.destEvar ev in + let h = (evd, evk :: evs) in + (h, ev) + let fresh_constructor_instance (evd,evs) env construct = let (evd,pconstruct) = Evd.fresh_constructor_instance env evd construct in (evd,evs) , pconstruct diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 357b1f4d7..b4a4a7197 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -427,6 +427,10 @@ module Refine : sig val new_evar : handle -> Environ.env -> Constr.types -> handle * Constr.t (** Create a new hole that will be added to the goals to solve. *) + val new_evar_instance : handle -> Environ.named_context_val -> + Constr.types -> Constr.t list -> handle * Constr.t + (** Create a new hole with the given signature and instance. *) + val fresh_constructor_instance : handle -> Environ.env -> Names.constructor -> handle * Constr.pconstructor (** Creates a constructor with fresh universe variables. *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 16e785180..ccea38caa 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1928,8 +1928,8 @@ and interp_atomic ist tac : unit Proofview.tactic = if b then Tactics.keep l gl else Tactics.clear l gl end | TacClearBody l -> - Proofview.V82.tactic begin fun gl -> - Tactics.clear_body (interp_hyp_list ist (pf_env gl) l) gl + Proofview.Goal.raw_enter begin fun gl -> + Tactics.clear_body (interp_hyp_list ist (Tacmach.New.pf_env gl) l) end | TacMove (dep,id1,id2) -> Proofview.V82.tactic begin fun gl -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 932bfc5fe..6800ca71e 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1467,7 +1467,58 @@ let assumption = let clear ids = (* avant seul dyn_clear n'echouait pas en [] *) if List.is_empty ids then tclIDTAC else thin ids -let clear_body = thin_body +let on_the_bodies = function +| [] -> assert false +| [id] -> str " depends on the body of " ++ pr_id id +| l -> str " depends on the bodies of " ++ pr_sequence pr_id l + +let check_is_type env ty msg = + Proofview.tclEVARMAP >>= fun sigma -> + let evdref = ref sigma in + try + let _ = Typing.sort_of env evdref ty in + Proofview.V82.tclEVARS !evdref + with e when Errors.noncritical e -> + msg e + +let clear_body ids = + Proofview.Goal.raw_enter begin fun gl -> + let env = Proofview.Goal.env gl in + let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in + let ctx = named_context env in + let map (id, body, t as decl) = match body with + | None -> + let () = if List.mem_f Id.equal id ids then + errorlabstrm "" (str "Hypothesis " ++ pr_id id ++ str " is not a local definition") + in + decl + | Some _ -> + if List.mem_f Id.equal id ids then (id, None, t) else decl + in + let ctx = List.map map ctx in + let base_env = reset_context env in + let env = push_named_context ctx base_env in + let check_hyps = + let check env (id, _, t as decl) = + let msg _ = Tacticals.New.tclZEROMSG + (str "Hypothesis " ++ pr_id id ++ on_the_bodies ids) + in + check_is_type env t msg <*> Proofview.tclUNIT (push_named decl env) + in + let checks = Proofview.Monad.List.fold_left check base_env (List.rev ctx) in + Proofview.tclIGNORE checks + in + let check_concl = + let msg _ = Tacticals.New.tclZEROMSG + (str "Conclusion" ++ on_the_bodies ids) + in + check_is_type env concl msg + in + check_hyps <*> check_concl <*> + Proofview.Refine.refine ~unsafe:true begin fun h -> + Proofview.Refine.new_evar h env concl + end + end let clear_wildcards ids = Proofview.V82.tactic (tclMAP (fun (loc,id) gl -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d7a88787b..349e828a1 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -163,7 +163,7 @@ val unfold_constr : global_reference -> tactic (** {6 Modification of the local context. } *) val clear : Id.t list -> tactic -val clear_body : Id.t list -> tactic +val clear_body : Id.t list -> unit Proofview.tactic val keep : Id.t list -> tactic val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic |