aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/g_class.ml42
-rw-r--r--plugins/ltac/g_rewrite.ml413
-rw-r--r--plugins/ltac/rewrite.ml6
-rw-r--r--tactics/auto.ml11
-rw-r--r--tactics/class_tactics.ml28
-rw-r--r--tactics/class_tactics.mli2
6 files changed, 37 insertions, 25 deletions
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 40f30c794..ff5e7d5ff 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -85,7 +85,7 @@ TACTIC EXTEND not_evar
END
TACTIC EXTEND is_ground
- [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ]
+ [ "is_ground" constr(ty) ] -> [ is_ground ty ]
END
TACTIC EXTEND autoapply
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c50100bf5..fdcaedab3 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -19,6 +19,7 @@ open Geninterp
open Extraargs
open Tacmach
open Tacticals
+open Proofview.Notations
open Rewrite
open Stdarg
open Pcoq.Vernac_
@@ -123,15 +124,19 @@ TACTIC EXTEND rewrite_strat
END
let clsubstitute o c =
+ Proofview.Goal.enter { enter = begin fun gl ->
let is_tac id = match fst (fst (snd c)) with GVar (_, id') when Id.equal id' id -> true | _ -> false in
- Tacticals.onAllHypsAndConcl
+ let hyps = Tacmach.New.pf_ids_of_hyps gl in
+ Tacticals.New.tclMAP
(fun cl ->
match cl with
- | Some id when is_tac id -> tclIDTAC
- | _ -> Proofview.V82.of_tactic (cl_rewrite_clause c o AllOccurrences cl))
+ | Some id when is_tac id -> Tacticals.New.tclIDTAC
+ | _ -> cl_rewrite_clause c o AllOccurrences cl)
+ (None :: List.map (fun id -> Some id) hyps)
+ end }
TACTIC EXTEND substitute
-| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ Proofview.V82.tactic (clsubstitute o c) ]
+| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
END
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index b84be4600..12a1566e2 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -2197,7 +2197,8 @@ let setoid_transitivity c =
(transitivity_red true c)
let setoid_symmetry_in id =
- Proofview.V82.tactic (fun gl ->
+ let open Tacmach.New in
+ Proofview.Goal.enter { enter = begin fun gl ->
let sigma = project gl in
let ctype = pf_unsafe_type_of gl (mkVar id) in
let binders,concl = decompose_prod_assum sigma ctype in
@@ -2211,11 +2212,10 @@ let setoid_symmetry_in id =
let he,c1,c2 = mkApp (equiv, Array.of_list others),c1,c2 in
let new_hyp' = mkApp (he, [| c2 ; c1 |]) in
let new_hyp = it_mkProd_or_LetIn new_hyp' binders in
- Proofview.V82.of_tactic
(tclTHENLAST
(Tactics.assert_after_replacing id new_hyp)
(tclTHENLIST [ intros; setoid_symmetry; apply (mkVar id); Tactics.assumption ]))
- gl)
+ end }
let _ = Hook.set Tactics.setoid_reflexivity setoid_reflexivity
let _ = Hook.set Tactics.setoid_symmetry setoid_symmetry
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 74cb7a364..42230dff1 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -380,7 +380,7 @@ and my_find_search_delta sigma db_list local_db secvars hdc concl =
and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=dbname})) =
let tactic = function
| Res_pf (c,cl) -> unify_resolve_gen poly flags (c,cl)
- | ERes_pf _ -> Proofview.V82.tactic (fun gl -> error "eres_pf")
+ | ERes_pf _ -> Proofview.Goal.enter { enter = fun gl -> Tacticals.New.tclZEROMSG (str "eres_pf") }
| Give_exact (c, cl) -> exact poly (c, cl)
| Res_pf_THEN_trivial_fail (c,cl) ->
Tacticals.New.tclTHEN
@@ -389,10 +389,11 @@ and tac_of_hint dbg db_list local_db concl (flags, ({pat=p; code=t;poly=poly;db=
with "debug auto" we don't display the details of inner trivial *)
(trivial_fail_db (no_dbg ()) (not (Option.is_empty flags)) db_list local_db)
| Unfold_nth c ->
- Proofview.V82.tactic (fun gl ->
- if exists_evaluable_reference (pf_env gl) c then
- tclPROGRESS (Proofview.V82.of_tactic (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)) gl
- else tclFAIL 0 (str"Unbound reference") gl)
+ Proofview.Goal.enter { enter = begin fun gl ->
+ if exists_evaluable_reference (Tacmach.New.pf_env gl) c then
+ Tacticals.New.tclPROGRESS (reduce (Unfold [AllOccurrences,c]) Locusops.onConcl)
+ else Tacticals.New.tclFAIL 0 (str"Unbound reference")
+ end }
| Extern tacast ->
conclPattern concl p tacast
in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index d70275dee..54e4405d1 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -221,18 +221,22 @@ let auto_unif_flags freeze st =
resolve_evars = false
}
-let e_give_exact flags poly (c,clenv) gl =
+let e_give_exact flags poly (c,clenv) =
+ let open Tacmach.New in
+ Proofview.Goal.s_enter { s_enter = begin fun gl ->
+ let sigma = project gl in
let (c, _, _) = c in
- let c, gl =
+ let c, sigma =
if poly then
let clenv', subst = Clenv.refresh_undefined_univs clenv in
- let evd = evars_reset_evd ~with_conv_pbs:true gl.sigma clenv'.evd in
+ let evd = evars_reset_evd ~with_conv_pbs:true sigma clenv'.evd in
let c = Vars.subst_univs_level_constr subst c in
- c, {gl with sigma = evd}
- else c, gl
+ c, evd
+ else c, sigma
in
- let t1 = pf_unsafe_type_of gl c in
- Proofview.V82.of_tactic (Clenvtac.unify ~flags t1 <*> exact_no_check c) gl
+ let (sigma, t1) = Typing.type_of (pf_env gl) sigma c in
+ Sigma.Unsafe.of_pair (Clenvtac.unify ~flags t1 <*> exact_no_check c, sigma)
+ end }
let unify_e_resolve poly flags = { enter = begin fun gls (c,_,clenv) ->
let clenv', c = connect_hint_clenv poly c clenv gls in
@@ -455,7 +459,7 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes sigma co
{ enter = fun gl -> unify_resolve_refine poly flags gl (c,None,clenv) } in
Tacticals.New.tclTHEN tac Proofview.shelve_unifiable
else
- Proofview.V82.tactic (e_give_exact flags poly (c,clenv))
+ e_give_exact flags poly (c,clenv)
| Res_pf_THEN_trivial_fail (term,cl) ->
let fst = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in
let snd = if complete then Tacticals.New.tclIDTAC
@@ -1613,9 +1617,11 @@ let not_evar c =
| Evar _ -> Tacticals.New.tclFAIL 0 (str"Evar")
| _ -> Proofview.tclUNIT ()
-let is_ground c gl =
- if Evarutil.is_ground_term (project gl) c then tclIDTAC gl
- else tclFAIL 0 (str"Not ground") gl
+let is_ground c =
+ let open Tacticals.New in
+ Proofview.tclEVARMAP >>= fun sigma ->
+ if Evarutil.is_ground_term sigma c then tclIDTAC
+ else tclFAIL 0 (str"Not ground")
let autoapply c i =
let open Proofview.Notations in
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli
index a38be5972..738cc0feb 100644
--- a/tactics/class_tactics.mli
+++ b/tactics/class_tactics.mli
@@ -33,7 +33,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic
val not_evar : constr -> unit Proofview.tactic
-val is_ground : constr -> tactic
+val is_ground : constr -> unit Proofview.tactic
val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 19:10:08 +0000