aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--proofs/clenv.ml4
-rw-r--r--proofs/clenv.mli4
-rw-r--r--proofs/tacmach.ml13
-rw-r--r--proofs/tacmach.mli10
-rw-r--r--tactics/equality.ml102
-rw-r--r--tactics/equality.mli10
-rw-r--r--tactics/extratactics.ml48
-rw-r--r--tactics/hipattern.ml44
-rw-r--r--tactics/hipattern.mli4
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/tactics.ml135
-rw-r--r--tactics/tactics.mli1
12 files changed, 159 insertions, 138 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 966d247e0..444043dbe 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -496,8 +496,8 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function
let make_clenv_binding_env_apply env sigma n =
make_clenv_binding_gen true n env sigma
-let make_clenv_binding_apply gls n = make_clenv_binding_gen true n (pf_env gls) gls.sigma
-let make_clenv_binding gls = make_clenv_binding_gen false None (pf_env gls) gls.sigma
+let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma
+let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma
(****************************************************************)
(* Pretty-print *)
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index 7731c4ca2..9a985a842 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -100,10 +100,10 @@ val make_clenv_binding_env_apply :
clausenv
val make_clenv_binding_apply :
- Goal.goal sigma -> int option -> constr * constr -> constr bindings ->
+ env -> evar_map -> int option -> constr * constr -> constr bindings ->
clausenv
val make_clenv_binding :
- Goal.goal sigma -> constr * constr -> constr bindings -> clausenv
+ env -> evar_map -> constr * constr -> constr bindings -> clausenv
(** if the clause is a product, add an extra meta for this product *)
exception NotExtensibleClause
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index a9146a96a..943974489 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -221,6 +221,7 @@ module New = struct
let pf_type_of gl t =
pf_apply type_of gl t
+ let pf_conv_x gl t1 t2 = pf_apply is_conv gl t1 t2
let pf_ids_of_hyps gl =
(** We only get the identifiers in [hyps] *)
@@ -253,11 +254,21 @@ module New = struct
let hyps = Proofview.Goal.hyps gl in
List.hd hyps
- let pf_nf_concl gl =
+ let pf_nf_concl (gl : [ `LZ ] 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 = Proofview.Goal.sigma gl in
nf_evar sigma concl
+ let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
+
+ let pf_get_type_of gl t = pf_apply Retyping.get_type_of gl t
+
+ let pf_reduce_to_quantified_ind gl t =
+ pf_apply reduce_to_quantified_ind gl t
+
+ let pf_hnf_type_of gl t =
+ pf_whd_betadeltaiota gl (pf_get_type_of gl t)
+
end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 9a53560b6..bf0ce04a1 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -134,15 +134,19 @@ module New : sig
val pf_global : identifier -> 'a Proofview.Goal.t -> constr
val of_old : (Proof_type.goal Evd.sigma -> 'a) -> [ `NF ] Proofview.Goal.t -> 'a
- val pf_type_of : 'b Proofview.Goal.t -> Term.constr -> Term.types
+ val pf_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+ val pf_get_type_of : 'a Proofview.Goal.t -> Term.constr -> Term.types
+ val pf_conv_x : 'a Proofview.Goal.t -> Term.constr -> Term.constr -> bool
val pf_get_new_id : identifier -> [ `NF ] Proofview.Goal.t -> identifier
- val pf_ids_of_hyps : 'b Proofview.Goal.t -> identifier list
- val pf_hyps_types : 'b Proofview.Goal.t -> (identifier * types) list
+ val pf_ids_of_hyps : 'a Proofview.Goal.t -> identifier list
+ val pf_hyps_types : 'a Proofview.Goal.t -> (identifier * types) list
val pf_get_hyp : identifier -> [ `NF ] Proofview.Goal.t -> named_declaration
val pf_get_hyp_typ : identifier -> [ `NF ] Proofview.Goal.t -> types
val pf_last_hyp : [ `NF ] 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 * types
+ val pf_hnf_type_of : 'a Proofview.Goal.t -> constr -> types
end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a0a5dddb8..b16f956d0 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -134,7 +134,7 @@ let side_tac tac sidetac =
| Some sidetac -> Tacticals.New.tclTHENSFIRSTn tac [|Proofview.tclUNIT ()|] sidetac
let instantiate_lemma_all frzevars env gl c ty l l2r concl =
- let eqclause = Clenv.make_clenv_binding gl (c,ty) l in
+ let eqclause = pf_apply Clenv.make_clenv_binding gl (c,ty) l in
let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
@@ -154,7 +154,7 @@ let instantiate_lemma_all frzevars env gl c ty l l2r concl =
let instantiate_lemma env gl c ty l l2r concl =
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
- let eqclause = Clenv.make_clenv_binding gl (c,t) l in
+ let eqclause = pf_apply Clenv.make_clenv_binding gl (c,t) l in
[eqclause]
let rewrite_conv_closed_unif_flags = {
@@ -880,13 +880,11 @@ let onEquality with_evars tac (c,lbindc) =
try (* type_of can raise exceptions *)
let t = type_of c in
let t' = try snd (reduce_to_quantified_ind t) with UserError _ -> t in
- let eq_clause = Tacmach.New.of_old (fun gl -> make_clenv_binding gl (c,t') lbindc) gl in
+ let eq_clause = Tacmach.New.pf_apply make_clenv_binding gl (c,t') lbindc in
begin try (* clenv_pose_dependent_evars can raise exceptions *)
let eq_clause' = clenv_pose_dependent_evars with_evars eq_clause in
let eqn = clenv_type eq_clause' in
- let (eq,eq_args) =
- Tacmach.New.of_old (fun gl -> find_this_eq_data_decompose gl eqn) gl
- in
+ let (eq,eq_args) = find_this_eq_data_decompose gl eqn in
Tacticals.New.tclTHEN
(Proofview.V82.tactic (Refiner.tclEVARS eq_clause'.evd))
(tac (eq,eqn,eq_args) eq_clause')
@@ -1319,7 +1317,7 @@ let swap_equality_args = function
| PolymorphicLeibnizEq (t,e1,e2) -> [t;e2;e1]
| HeterogenousEq (t1,e1,t2,e2) -> [t2;e2;t1;e1]
-let swap_equands gls eqn =
+let swap_equands eqn =
let (lbeq,eq_args) = find_eq_data eqn in
applist(lbeq.eq,swap_equality_args eq_args)
@@ -1416,69 +1414,80 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
exception NothingToRewrite
-let cutSubstInConcl_RL eqn gls =
- let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gls eqn in
- let body,expected_goal = pf_apply subst_tuple_term gls e2 e1 (pf_concl gls) in
+let cutSubstInConcl_RL eqn =
+ Proofview.Goal.enter begin fun gl ->
+ let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in
+ let concl = Proofview.Goal.concl gl in
+ let body,expected_goal = Tacmach.New.pf_apply subst_tuple_term gl e2 e1 concl in
if not (dependent (mkRel 1) body) then raise NothingToRewrite;
- tclTHENFIRST
+ Proofview.V82.tactic (fun gl -> tclTHENFIRST
(bareRevSubstInConcl lbeq body eq)
- (convert_concl expected_goal DEFAULTcast) gls
+ (convert_concl expected_goal DEFAULTcast) gl)
+ end
(* |- (P e1)
BY CutSubstInConcl_LR (eq T e1 e2)
|- (P e2)
|- (eq T e1 e2)
*)
-let cutSubstInConcl_LR eqn gls =
- (tclTHENS (cutSubstInConcl_RL (swap_equands gls eqn))
+let cutSubstInConcl_LR eqn =
+ Proofview.V82.tactic (fun gl ->
+ (tclTHENS (Proofview.V82.of_tactic (cutSubstInConcl_RL (swap_equands eqn)))
([tclIDTAC;
- swapEquandsInConcl])) gls
+ swapEquandsInConcl])) gl)
let cutSubstInConcl l2r =if l2r then cutSubstInConcl_LR else cutSubstInConcl_RL
-let cutSubstInHyp_LR eqn id gls =
- let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gls eqn in
- let idtyp = pf_get_hyp_typ gls id in
- let body,expected_goal = pf_apply subst_tuple_term gls e1 e2 idtyp in
+let cutSubstInHyp_LR eqn id =
+ Proofview.Goal.enter begin fun gl ->
+ let (lbeq,(t,e1,e2 as eq)) = find_eq_data_decompose gl eqn in
+ let idtyp = Tacmach.New.pf_get_hyp_typ id gl in
+ let body,expected_goal = Tacmach.New.pf_apply subst_tuple_term gl e1 e2 idtyp in
if not (dependent (mkRel 1) body) then raise NothingToRewrite;
- cut_replacing id expected_goal
+ Proofview.V82.tactic (fun gl -> cut_replacing id expected_goal
(tclTHENFIRST
(bareRevSubstInConcl lbeq body eq)
- (refine_no_check (mkVar id))) gls
+ (refine_no_check (mkVar id))) gl)
+ end
-let cutSubstInHyp_RL eqn id gls =
- (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id)
+let cutSubstInHyp_RL eqn id =
+ Proofview.V82.tactic (fun gl ->
+ (tclTHENS (Proofview.V82.of_tactic (cutSubstInHyp_LR (swap_equands eqn) id))
([tclIDTAC;
- swapEquandsInConcl])) gls
+ swapEquandsInConcl])) gl)
let cutSubstInHyp l2r = if l2r then cutSubstInHyp_LR else cutSubstInHyp_RL
-let try_rewrite tac gls =
- try
- tac gls
- with
+let try_rewrite tac =
+ Proofview.tclORELSE tac begin function
| ConstrMatching.PatternMatchingFailure ->
- errorlabstrm "try_rewrite" (str "Not a primitive equality here.")
+ Tactics.New.tclZEROMSG (str "Not a primitive equality here.")
| e when catchable_exception e ->
- errorlabstrm "try_rewrite"
+ Tactics.New.tclZEROMSG
(strbrk "Cannot find a well-typed generalization of the goal that makes the proof progress.")
| NothingToRewrite ->
- errorlabstrm "try_rewrite"
+ Tactics.New.tclZEROMSG
(strbrk "Nothing to rewrite.")
+ | e -> Proofview.tclZERO e
+ end
-let cutSubstClause l2r eqn cls gls =
+let cutSubstClause l2r eqn cls =
match cls with
- | None -> cutSubstInConcl l2r eqn gls
- | Some id -> cutSubstInHyp l2r eqn id gls
+ | None -> cutSubstInConcl l2r eqn
+ | Some id -> cutSubstInHyp l2r eqn id
let cutRewriteClause l2r eqn cls = try_rewrite (cutSubstClause l2r eqn cls)
let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
-let substClause l2r c cls gls =
- let eq = pf_apply get_type_of gls c in
+let substClause l2r c cls =
+ let open Tacmach.New in
+ let open Tacticals.New in
+ Proofview.Goal.raw_enter begin fun gl ->
+ let eq = pf_apply get_type_of gl c in
tclTHENS (cutSubstClause l2r eq cls)
- [tclIDTAC; exact_no_check c] gls
+ [Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)]
+ end
let rewriteClause l2r c cls = try_rewrite (substClause l2r c cls)
let rewriteInHyp l2r c id = rewriteClause l2r c (Some id)
@@ -1591,7 +1600,7 @@ let subst_one_var dep_proof_ok x =
(* x is a variable: *)
let varx = mkVar x in
(* Find a non-recursive definition for x *)
- let found gl =
+ let res =
try
let test hyp _ = is_eq_x gl varx hyp in
Context.fold_named_context test ~init:() hyps;
@@ -1599,8 +1608,7 @@ let subst_one_var dep_proof_ok x =
(str "Cannot find any non-recursive equality over " ++ pr_id x ++
str".")
with FoundHyp res -> res in
- let (hyp,rhs,dir) = Tacmach.New.of_old found gl in
- subst_one dep_proof_ok x (hyp,rhs,dir)
+ subst_one dep_proof_ok x res
end
let subst_gen dep_proof_ok ids =
@@ -1625,7 +1633,7 @@ let default_subst_tactic_flags () =
let subst_all ?(flags=default_subst_tactic_flags ()) () =
Proofview.Goal.enter begin fun gl ->
- let find_eq_data_decompose = Tacmach.New.of_old find_eq_data_decompose gl in
+ let find_eq_data_decompose = find_eq_data_decompose gl in
let test (_,c) =
try
let lbeq,(_,x,y) = find_eq_data_decompose c in
@@ -1649,27 +1657,23 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () =
let cond_eq_term_left c t gl =
try
let (_,x,_) = snd (find_eq_data_decompose gl t) in
- if pf_conv_x gl c x then true else failwith "not convertible"
+ if Tacmach.New.pf_conv_x gl c x then true else failwith "not convertible"
with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
let cond_eq_term_right c t gl =
try
let (_,_,x) = snd (find_eq_data_decompose gl t) in
- if pf_conv_x gl c x then false else failwith "not convertible"
+ if Tacmach.New.pf_conv_x gl c x then false else failwith "not convertible"
with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
let cond_eq_term c t gl =
try
let (_,x,y) = snd (find_eq_data_decompose gl t) in
- if pf_conv_x gl c x then true
- else if pf_conv_x gl c y then false
+ if Tacmach.New.pf_conv_x gl c x then true
+ else if Tacmach.New.pf_conv_x gl c y then false
else failwith "not convertible"
with ConstrMatching.PatternMatchingFailure -> failwith "not an equality"
-let cond_eq_term_left c t = Tacmach.New.of_old (cond_eq_term_left c t)
-let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t)
-let cond_eq_term c t = Tacmach.New.of_old (cond_eq_term c t)
-
let rewrite_multi_assumption_cond cond_eq_term cl =
let rec arec hyps gl = match hyps with
| [] -> error "No such assumption."
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 681b366db..d5aa2d248 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -94,15 +94,15 @@ val make_iterated_tuple :
env -> evar_map -> constr -> (constr * types) -> constr * constr * constr
(* The family cutRewriteIn expect an equality statement *)
-val cutRewriteInHyp : bool -> types -> Id.t -> tactic
-val cutRewriteInConcl : bool -> constr -> tactic
+val cutRewriteInHyp : bool -> types -> Id.t -> unit Proofview.tactic
+val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic
(* The family rewriteIn expect the proof of an equality *)
-val rewriteInHyp : bool -> constr -> Id.t -> tactic
-val rewriteInConcl : bool -> constr -> tactic
+val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic
+val rewriteInConcl : bool -> constr -> unit Proofview.tactic
(* Expect the proof of an equality; fails with raw internal errors *)
-val substClause : bool -> constr -> Id.t option -> tactic
+val substClause : bool -> constr -> Id.t option -> unit Proofview.tactic
val discriminable : env -> evar_map -> constr -> constr -> bool
val injectable : env -> evar_map -> constr -> constr -> bool
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index a397976ea..9ed937447 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -165,15 +165,15 @@ let injHyp id =
injection_main { it = Term.mkVar id,NoBindings; sigma = sigma; }
TACTIC EXTEND dependent_rewrite
-| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ Proofview.V82.tactic (rewriteInConcl b c) ]
+| [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ]
| [ "dependent" "rewrite" orient(b) constr(c) "in" hyp(id) ]
- -> [ Proofview.V82.tactic (rewriteInHyp b c id) ]
+ -> [ rewriteInHyp b c id ]
END
TACTIC EXTEND cut_rewrite
-| [ "cutrewrite" orient(b) constr(eqn) ] -> [ Proofview.V82.tactic (cutRewriteInConcl b eqn) ]
+| [ "cutrewrite" orient(b) constr(eqn) ] -> [ cutRewriteInConcl b eqn ]
| [ "cutrewrite" orient(b) constr(eqn) "in" hyp(id) ]
- -> [ Proofview.V82.tactic (cutRewriteInHyp b eqn id) ]
+ -> [ cutRewriteInHyp b eqn id ]
END
(**********************************************************************)
diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index 80720cfaf..cc3c4c297 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -396,10 +396,10 @@ let find_eq_data eqn = (* fails with PatternMatchingFailure *)
let extract_eq_args gl = function
| MonomorphicLeibnizEq (e1,e2) ->
- let t = Tacmach.pf_type_of gl e1 in (t,e1,e2)
+ let t = Tacmach.New.pf_type_of gl e1 in (t,e1,e2)
| PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2)
| HeterogenousEq (t1,e1,t2,e2) ->
- if Tacmach.pf_conv_x gl t1 t2 then (t1,e1,e2)
+ if Tacmach.New.pf_conv_x gl t1 t2 then (t1,e1,e2)
else raise PatternMatchingFailure
let find_eq_data_decompose gl eqn =
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 4735b26b3..f8a4d35a8 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 : Proof_type.goal sigma -> constr ->
+val find_eq_data_decompose : 'a Proofview.Goal.t -> constr ->
coq_eq_data * (types * constr * constr)
(** Idem but fails with an error message instead of PatternMatchingFailure *)
-val find_this_eq_data_decompose : Proof_type.goal sigma -> constr ->
+val find_this_eq_data_decompose : 'a Proofview.Goal.t -> constr ->
coq_eq_data * (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 06853e137..d2dd64e52 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -300,7 +300,7 @@ let remember_first_eq id x = if !x == MoveLast then x := MoveAfter id
let projectAndApply thin id eqname names depids =
let subst_hyp l2r id =
- tclTHEN (tclTRY(rewriteInConcl l2r (mkVar id)))
+ tclTHEN (tclTRY(Proofview.V82.of_tactic (rewriteInConcl l2r (mkVar id))))
(if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
in
let substHypIfVariable tac id =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 718c039fa..c61192031 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -695,10 +695,10 @@ let resolve_classes gl =
(**************************)
let cut c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
- let concl = Proofview.Goal.concl gl in
+ let concl = Tacmach.New.pf_nf_concl gl in
let is_sort =
try
(** Backward compat: ensure that [c] is well-typed. *)
@@ -836,13 +836,13 @@ let general_elim_clause_gen elimtac indclause elim gl =
let elimt = pf_type_of gl elimc in
let i =
match elim.elimindex with None -> index_of_ind_arg elimt | Some i -> i in
- let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in
+ let elimclause = pf_apply make_clenv_binding gl (elimc,elimt) lbindelimc in
elimtac i elimclause indclause gl
let general_elim_clause elimtac (c,lbindc) elim gl =
let ct = pf_type_of gl c in
let t = try snd (pf_reduce_to_quantified_ind gl ct) with UserError _ -> ct in
- let indclause = make_clenv_binding gl (c,t) lbindc in
+ let indclause = pf_apply make_clenv_binding gl (c,t) lbindc in
general_elim_clause_gen elimtac indclause elim gl
let general_elim with_evars c e =
@@ -1035,7 +1035,7 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 =
let try_apply thm_ty nprod =
let n = nb_prod thm_ty - nprod in
if n<0 then error "Applied theorem has not enough premisses.";
- let clause = make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
+ let clause = pf_apply make_clenv_binding_apply gl (Some n) (c,thm_ty) lbind in
Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl
in
try try_apply thm_ty0 concl_nprod
@@ -1116,7 +1116,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
try aux (clenv_push_prod clause)
with NotExtensibleClause -> raise e
in
- aux (make_clenv_binding gl (d,thm) lbind)
+ aux (pf_apply make_clenv_binding gl (d,thm) lbind)
let apply_in_once sidecond_first with_delta with_destruct with_evars id
(loc,(d,lbind)) gl0 =
@@ -1225,13 +1225,13 @@ let clear ids = (* avant seul dyn_clear n'echouait pas en [] *)
let clear_body = thin_body
let clear_wildcards ids =
- tclMAP (fun (loc,id) gl ->
+ Proofview.V82.tactic (tclMAP (fun (loc,id) gl ->
try with_check (Tacmach.thin_no_check [id]) gl
with ClearDependencyError (id,err) ->
(* Intercept standard [thin] error message *)
Loc.raise loc
(error_clear_dependency (pf_env gl) (Id.of_string "_") err))
- ids
+ ids)
(* Takes a list of booleans, and introduces all the variables
* quantified in the goal which are associated with a value
@@ -1252,7 +1252,7 @@ let specialize mopt (c,lbind) g =
let evd = Typeclasses.resolve_typeclasses (pf_env g) (project g) in
tclEVARS evd, nf_evar evd c
else
- let clause = make_clenv_binding g (c,pf_type_of g c) lbind in
+ let clause = pf_apply make_clenv_binding g (c,pf_type_of g c) lbind in
let flags = { default_unify_flags with resolve_evars = true } in
let clause = clenv_unify_meta_types ~flags clause in
let (thd,tstack) = whd_nored_stack clause.evd (clenv_value clause) in
@@ -1314,8 +1314,8 @@ let check_number_of_constructors expctdnumopt i nconstr =
if i > nconstr then error "Not enough constructors."
let constructor_tac with_evars expctdnumopt i lbind =
- Proofview.Goal.enter begin fun gl ->
- let cl = Proofview.Goal.concl gl in
+ Proofview.Goal.raw_enter begin fun gl ->
+ let cl = Tacmach.New.pf_nf_concl gl in
let reduce_to_quantified_ind =
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
in
@@ -1346,8 +1346,8 @@ let rec tclANY tac = function
let any_constructor with_evars tacopt =
let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in
- Proofview.Goal.enter begin fun gl ->
- let cl = Proofview.Goal.concl gl in
+ Proofview.Goal.raw_enter begin fun gl ->
+ let cl = Tacmach.New.pf_nf_concl gl in
let reduce_to_quantified_ind =
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
in
@@ -1414,22 +1414,23 @@ let my_find_eq_data_decompose gl t =
known equalities will be dynamically registered *)
-> raise ConstrMatching.PatternMatchingFailure
-let intro_decomp_eq loc b l l' thin tac id gl =
+let intro_decomp_eq loc b l l' thin tac id =
+ Proofview.Goal.raw_enter begin fun gl ->
let c = mkVar id in
- let _,t = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
+ let t = Tacmach.New.pf_type_of gl c in
+ let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
let eq,eq_args = my_find_eq_data_decompose gl t in
- let eq_clause = make_clenv_binding gl (c,t) NoBindings in
- Proofview.V82.of_tactic (!intro_decomp_eq_function
+ let eq_clause = Tacmach.New.pf_apply make_clenv_binding gl (c,t) NoBindings in
+ !intro_decomp_eq_function
(fun n -> tac ((dloc,id)::thin) (adjust_intro_patterns n l @ l'))
- (eq,t,eq_args) eq_clause) gl
+ (eq,t,eq_args) eq_clause
+ end
let intro_or_and_pattern loc b ll l' thin tac id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let c = mkVar id in
- let (ind,t) =
- Tacmach.New.of_old (fun gl ->
- pf_reduce_to_quantified_ind gl (pf_type_of gl c)) gl
- in
+ let t = Tacmach.New.pf_type_of gl c in
+ let (ind,t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
let nv = mis_constr_nargs ind in
let bracketed = b || not (List.is_empty l') in
let adjust n l = if bracketed then adjust_intro_patterns n l else l in
@@ -1448,7 +1449,7 @@ let rewrite_hyp l2r id =
Hook.get forward_subst_one true x (id,rhs,l2r) in
let clear_var_and_eq c =
tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_type_of gl in
let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
@@ -1533,8 +1534,8 @@ let rec intros_patterns b avoid ids thin destopt tac = function
(fun thin -> intros_patterns b avoid ids thin destopt tac))
| (loc, IntroInjection l) :: l' ->
intro_then_force (fun id ->
- (Proofview.V82.tactic (intro_decomp_eq loc b l l' thin
- (fun thin -> intros_patterns b avoid ids thin destopt tac) id)))
+ intro_decomp_eq loc b l l' thin
+ (fun thin -> intros_patterns b avoid ids thin destopt tac) id)
| (loc, IntroRewrite l2r) :: l ->
intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l))
MoveLast true false
@@ -1545,7 +1546,7 @@ let rec intros_patterns b avoid ids thin destopt tac = function
| [] -> tac ids thin
let intros_pattern destopt =
- intros_patterns false [] [] [] destopt (fun _ l -> Proofview.V82.tactic (clear_wildcards l))
+ intros_patterns false [] [] [] destopt (fun _ l -> clear_wildcards l)
let intro_pattern destopt pat =
intros_pattern destopt [dloc,pat]
@@ -1558,11 +1559,11 @@ let intro_patterns = function
(* Other cut tactics *)
(**************************)
-let make_id s = fresh_id [] (default_id_of_sort s)
+let make_id s = new_fresh_id [] (default_id_of_sort s)
let prepare_intros s ipat gl =
- let make_id s = Tacmach.New.of_old (make_id s) gl in
- let fresh_id l id = Tacmach.New.of_old (fresh_id l id) gl in
+ let make_id s = make_id s gl in
+ let fresh_id l id = new_fresh_id l id gl in
match ipat with
| None ->
make_id s , Proofview.tclUNIT ()
@@ -1575,7 +1576,7 @@ let prepare_intros s ipat gl =
fresh_id [] id , Proofview.tclUNIT ()
| IntroWildcard ->
let id = make_id s in
- id , Proofview.V82.tactic (clear_wildcards [dloc,id])
+ id , clear_wildcards [dloc,id]
| IntroRewrite l2r ->
let id = make_id s in
id , Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
@@ -1583,13 +1584,12 @@ let prepare_intros s ipat gl =
make_id s ,
Tacticals.New.onLastHypId
(intro_or_and_pattern loc true ll [] []
- (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
+ (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> clear_wildcards l)))
| IntroInjection l ->
make_id s ,
- Proofview.V82.tactic (onLastHypId
+ Tacticals.New.onLastHypId
(intro_decomp_eq loc true l [] []
- (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l))))
- )
+ (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> clear_wildcards l)))
| IntroForthcoming _ -> user_err_loc
(loc,"",str "Introduction pattern for one hypothesis expected")
@@ -1610,8 +1610,8 @@ let clear_if_overwritten c ipats =
| _ -> tclIDTAC
let assert_as first ipat c =
- Proofview.Goal.enter begin fun gl ->
- let hnf_type_of = Tacmach.New.of_old pf_hnf_type_of gl in
+ Proofview.Goal.raw_enter begin fun gl ->
+ let hnf_type_of = Tacmach.New.pf_hnf_type_of gl in
match kind_of_term (hnf_type_of c) with
| Sort s ->
let (id,tac) = prepare_intros s ipat gl in
@@ -1631,12 +1631,12 @@ let as_tac id ipat = match ipat with
Hook.get forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl
| Some (loc,IntroOrAndPattern ll) ->
intro_or_and_pattern loc true ll [] []
- (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l)))
+ (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> clear_wildcards l))
id
| Some (loc,IntroInjection l) ->
- Proofview.V82.tactic (intro_decomp_eq loc true l [] []
- (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> Proofview.V82.tactic (clear_wildcards l)))
- id)
+ intro_decomp_eq loc true l [] []
+ (fun thin -> intros_patterns true [] [] thin MoveLast (fun _ l -> clear_wildcards l))
+ id
| Some (loc,
(IntroIdentifier _ | IntroAnonymous | IntroFresh _ |
IntroWildcard | IntroForthcoming _)) ->
@@ -1955,8 +1955,8 @@ let letin_tac_gen with_eq name (sigmac,c) test ty occs =
let (newcl,eq_tac) = match with_eq with
| Some (lr,(loc,ido)) ->
let heq = match ido with
- | IntroAnonymous -> Tacmach.New.of_old (fresh_id [id] (add_prefix "Heq" id)) gl
- | IntroFresh heq_base -> Tacmach.New.of_old (fresh_id [id] heq_base) gl
+ | IntroAnonymous -> new_fresh_id [id] (add_prefix "Heq" id) gl
+ | IntroFresh heq_base -> new_fresh_id [id] heq_base gl
| IntroIdentifier id -> id
| _ -> Errors.error "Expect an introduction pattern naming one hypothesis." in
let eqdata = build_coq_eq_data () in
@@ -1983,7 +1983,7 @@ let letin_tac with_eq name c ty occs =
letin_tac_gen with_eq name (sigma,c) (make_eq_test c) ty (occs,true)
let letin_pat_tac with_eq name c ty occs =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
letin_tac_gen with_eq name c
@@ -1995,7 +1995,7 @@ let letin_pat_tac with_eq name c ty occs =
let forward usetac ipat c =
match usetac with
| None ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let type_of = Tacmach.New.pf_type_of gl in
begin try (* type_of can raise an exception *)
let t = type_of c in
@@ -2084,18 +2084,18 @@ let check_unused_names names =
++ str": " ++ prlist_with_sep spc Miscprint.pr_intro_pattern names)
let rec consume_pattern avoid id isdep gl = function
- | [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), [])
+ | [] -> ((dloc, IntroIdentifier (new_fresh_id avoid id gl)), [])
| (loc,IntroAnonymous)::names ->
let avoid = avoid@explicit_intro_names names in
- ((loc,IntroIdentifier (fresh_id avoid id gl)), names)
+ ((loc,IntroIdentifier (new_fresh_id avoid id gl)), names)
| (loc,IntroForthcoming true)::names when not isdep ->
consume_pattern avoid id isdep gl names
| (loc,IntroForthcoming _)::names as fullpat ->
let avoid = avoid@explicit_intro_names names in
- ((loc,IntroIdentifier (fresh_id avoid id gl)), fullpat)
+ ((loc,IntroIdentifier (new_fresh_id avoid id gl)), fullpat)
| (loc,IntroFresh id')::names ->
let avoid = avoid@explicit_intro_names names in
- ((loc,IntroIdentifier (fresh_id avoid id' gl)), names)
+ ((loc,IntroIdentifier (new_fresh_id avoid id' gl)), names)
| pat::names -> (pat,names)
let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) =
@@ -2154,32 +2154,32 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
match ra with
| (RecArg,deprec,recvarname) ::
(IndArg,depind,hyprecname) :: ra' ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let (recpat,names) = match names with
| [loc,IntroIdentifier id as pat] ->
let id' = next_ident_away (add_prefix "IH" id) avoid in
(pat, [dloc, IntroIdentifier id'])
- | _ -> Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname deprec gl names) gl in
+ | _ -> consume_pattern avoid recvarname deprec gl names in
let dest = get_recarg_dest dests in
safe_dest_intros_patterns avoid thin dest [recpat] (fun ids thin ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
let (hyprec,names) =
- Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname depind gl names) gl
+ consume_pattern avoid hyprecname depind gl names
in
safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin ->
peel_tac ra' (update_dest dests ids') names thin)
end)
end
| (IndArg,dep,hyprecname) :: ra' ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.raw_enter begin fun gl ->
(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
- let (pat,names) = Tacmach.New.of_old (fun gl -> consume_pattern avoid hyprecname dep gl names) gl in
+ let (pat,names) = consume_pattern avoid hyprecname dep gl names in
safe_dest_intros_patterns avoid thin MoveLast [pat] (fun ids thin ->
peel_tac ra' (update_dest dests ids) names thin)
end
| (RecArg,dep,recvarname) :: ra' ->
- Proofview.Goal.enter begin fun gl ->
- let (pat,names) = Tacmach.New.of_old (fun gl -> consume_pattern avoid recvarname dep gl names) gl in
+ Proofview.Goal.raw_enter begin fun gl ->
+ let (pat,names) = consume_pattern avoid recvarname dep gl names in
let dest = get_recarg_dest dests in
safe_dest_intros_patterns avoid thin dest [pat] (fun ids thin ->
peel_tac ra' dests names thin)
@@ -2193,7 +2193,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
peel_tac ra' dests names thin)
| [] ->
check_unused_names names;
- Tacticals.New.tclTHEN (Proofview.V82.tactic (clear_wildcards thin)) (tac dests)
+ Tacticals.New.tclTHEN (clear_wildcards thin) (tac dests)
in
peel_tac ra dests names []
@@ -2230,7 +2230,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
| Var id when not (List.exists (occur_var env id) avoid) ->
atomize_one (i-1) ((mkVar id)::avoid)
| Var id ->
- let x = Tacmach.New.of_old (fresh_id [] id) gl in
+ let x = new_fresh_id [] id gl in
Tacticals.New.tclTHEN
(letin_tac None (Name x) (mkVar id) None allHypsAndConcl)
(atomize_one (i-1) ((mkVar x)::avoid))
@@ -2238,7 +2238,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
let type_of = Tacmach.New.pf_type_of gl in
let id = id_of_name_using_hdchar (Global.env()) (type_of c)
Anonymous in
- let x = Tacmach.New.of_old (fresh_id [] id) gl in
+ let x = new_fresh_id [] id gl in
Tacticals.New.tclTHEN
(letin_tac None (Name x) c None allHypsAndConcl)
(atomize_one (i-1) ((mkVar x)::avoid))
@@ -3102,7 +3102,7 @@ let get_eliminator elim gl = match elim with
| ElimUsing (elim,indsign) ->
(* bugged, should be computed *) true, elim, indsign
| ElimOver (isrec,id) ->
- let (elimc,elimt),_ as elims = guess_elim isrec id gl in
+ let (elimc,elimt),_ as elims = Tacmach.New.of_old (guess_elim isrec id) gl in
isrec, ({elimindex = None; elimbody = elimc}, elimt),
fst (compute_elim_signature elims id)
@@ -3153,7 +3153,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
let {elimbody=(elimc,lbindelimc)},elimt = elim in
(* elimclause contains this: (elimc ?i ?j ?k...?l) *)
let elimclause =
- make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
+ pf_apply make_clenv_binding gl (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
(* elimclause' is built from elimclause by instanciating all args and params. *)
let elimclause' = recolle_clenv nparams indvars elimclause gl in
(* one last resolution (useless?) *)
@@ -3165,7 +3165,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names tac =
Proofview.Goal.enter begin fun gl ->
- let (isrec, elim, indsign) = Tacmach.New.of_old (get_eliminator elim) gl in
+ let (isrec, elim, indsign) = get_eliminator elim gl in
let names = compute_induction_names (Array.length indsign) names in
(if isrec then Tacticals.New.tclTHENFIRSTn else Tacticals.New.tclTHENLASTn)
(Tacticals.New.tclTHEN
@@ -3252,10 +3252,10 @@ let induction_from_context_l with_evars elim_info lid names =
hypothesis on which the induction is made *)
let induction_tac with_evars elim (varname,lbind) typ gl =
let ({elimindex=i;elimbody=(elimc,lbindelimc)},elimt) = elim in
- let indclause = make_clenv_binding gl (mkVar varname,typ) lbind in
+ let indclause = pf_apply make_clenv_binding gl (mkVar varname,typ) lbind in
let i = match i with None -> index_of_ind_arg elimt | Some i -> i in
let elimclause =
- make_clenv_binding gl
+ pf_apply make_clenv_binding gl
(mkCast (elimc,DEFAULTcast,elimt),elimt) lbindelimc in
elimination_clause_scheme with_evars i elimclause indclause gl
@@ -3615,9 +3615,8 @@ let dImp cls =
let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
let maybe_betadeltaiota_concl allowred gl =
- let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
+ let concl = Tacmach.New.pf_nf_concl gl in
let sigma = Proofview.Goal.sigma gl in
- let concl = nf_evar sigma concl in
if not allowred then concl
else
let env = Proofview.Goal.env gl in
@@ -3928,4 +3927,6 @@ module New = struct
)
end
+ let tclZEROMSG = tclZEROMSG
+
end
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 9f4f0e9ce..f3c5e7d26 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -417,4 +417,5 @@ module New : sig
open Proofview
val exact_proof : Constrexpr.constr_expr -> unit tactic
+ val tclZEROMSG : Pp.std_ppcmds -> unit tactic
end
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 17:10:07 +0000