aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ltac/extratactics.ml46
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--plugins/funind/recdef.ml2
-rw-r--r--tactics/elim.ml19
-rw-r--r--tactics/elim.mli1
-rw-r--r--tactics/tacticals.ml3
-rw-r--r--tactics/tacticals.mli4
7 files changed, 20 insertions, 17 deletions
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index c39b1a0e9..faf545d4f 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -172,11 +172,11 @@ END
(* Decompose *)
TACTIC EXTEND decompose_sum
-| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or c ]
+| [ "decompose" "sum" constr(c) ] -> [ Elim.h_decompose_or (EConstr.of_constr c) ]
END
TACTIC EXTEND decompose_record
-| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and c ]
+| [ "decompose" "record" constr(c) ] -> [ Elim.h_decompose_and (EConstr.of_constr c) ]
END
(**********************************************************************)
@@ -1055,7 +1055,7 @@ let decompose l c =
end }
TACTIC EXTEND decompose
-| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l c ]
+| [ "decompose" "[" ne_constr_list(l) "]" constr(c) ] -> [ decompose l (EConstr.of_constr c) ]
END
(** library/keys *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 503cafdd5..940f1669a 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1626,7 +1626,7 @@ let prove_principle_for_gen
[
Proofview.V82.of_tactic (generalize [lemma]);
Proofview.V82.of_tactic (Simple.intro hid);
- Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid));
+ Proofview.V82.of_tactic (Elim.h_decompose_and (EConstr.mkVar hid));
(fun g ->
let new_hyps = pf_ids_of_hyps g in
tcc_list := List.rev (List.subtract Id.equal new_hyps (hid::hyps));
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d5ee42af8..74affa396 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1314,7 +1314,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
(fun g ->
let ids = pf_ids_of_hyps g in
tclTHEN
- (Proofview.V82.of_tactic (Elim.h_decompose_and (mkVar hid)))
+ (Proofview.V82.of_tactic (Elim.h_decompose_and (EConstr.mkVar hid)))
(fun g ->
let ids' = pf_ids_of_hyps g in
lid := List.rev (List.subtract Id.equal ids' ids);
diff --git a/tactics/elim.ml b/tactics/elim.ml
index e641f970a..ef848c2e1 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -10,6 +10,7 @@ open Util
open Names
open Term
open Termops
+open EConstr
open Inductiveops
open Hipattern
open Tacmach.New
@@ -55,7 +56,7 @@ Another example :
*)
let elimHypThen tac id =
- elimination_then tac (EConstr.mkVar id)
+ elimination_then tac (mkVar id)
let rec general_decompose_on_hyp recognizer =
ifOnHyp recognizer (general_decompose_aux recognizer) (fun _ -> Proofview.tclUNIT())
@@ -77,7 +78,6 @@ let tmphyp_name = Id.of_string "_TmpHyp"
let up_to_delta = ref false (* true *)
let general_decompose recognizer c =
- let c = EConstr.of_constr c in
Proofview.Goal.enter { enter = begin fun gl ->
let type_of = pf_unsafe_type_of gl in
let sigma = project gl in
@@ -105,17 +105,17 @@ let head_in indl t gl =
let decompose_these c l =
Proofview.Goal.enter { enter = begin fun gl ->
let indl = List.map (fun x -> x, Univ.Instance.empty) l in
- general_decompose (fun sigma (_,t) -> head_in indl (EConstr.of_constr t) gl) c
+ general_decompose (fun sigma (_,t) -> head_in indl t gl) c
end }
let decompose_and c =
general_decompose
- (fun sigma (_,t) -> is_record sigma (EConstr.of_constr t))
+ (fun sigma (_,t) -> is_record sigma t)
c
let decompose_or c =
general_decompose
- (fun sigma (_,t) -> is_disjunction sigma (EConstr.of_constr t))
+ (fun sigma (_,t) -> is_disjunction sigma t)
c
let h_decompose l c = decompose_these c l
@@ -127,7 +127,7 @@ let h_decompose_and = decompose_and
(* The tactic Double performs a double induction *)
let simple_elimination c =
- elimination_then (fun _ -> tclIDTAC) (EConstr.of_constr c)
+ elimination_then (fun _ -> tclIDTAC) c
let induction_trailer abs_i abs_j bargs =
tclTHEN
@@ -135,8 +135,9 @@ let induction_trailer abs_i abs_j bargs =
(onLastHypId
(fun id ->
Proofview.Goal.nf_enter { enter = begin fun gl ->
- let idty = pf_unsafe_type_of gl (EConstr.mkVar id) in
- let fvty = global_vars (pf_env gl) (project gl) (EConstr.of_constr idty) in
+ let idty = pf_unsafe_type_of gl (mkVar id) in
+ let idty = EConstr.of_constr idty in
+ let fvty = global_vars (pf_env gl) (project gl) idty in
let possible_bring_hyps =
(List.tl (nLastDecls gl (abs_j - abs_i))) @ bargs.Tacticals.assums
in
@@ -168,7 +169,7 @@ let double_ind h1 h2 =
(onLastHypId
(fun id ->
elimination_then
- (introElimAssumsThen (induction_trailer abs_i abs_j)) (EConstr.mkVar id))))
+ (introElimAssumsThen (induction_trailer abs_i abs_j)) (mkVar id))))
end }
let h_double_induction = double_ind
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 29c441463..dc1af79ba 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -8,6 +8,7 @@
open Names
open Term
+open EConstr
open Tacticals
open Misctypes
open Tactypes
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e15ee149d..e440f1dc5 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -128,7 +128,7 @@ let onClauseLR tac cl gls =
tclMAP tac (List.rev (Locusops.simple_clause_of hyps cl)) gls
let ifOnHyp pred tac1 tac2 id gl =
- if pred (id,pf_get_hyp_typ gl id) then
+ if pred (id,EConstr.of_constr (pf_get_hyp_typ gl id)) then
tac1 id gl
else
tac2 id gl
@@ -583,6 +583,7 @@ module New = struct
let ifOnHyp pred tac1 tac2 id =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let typ = Tacmach.New.pf_get_hyp_typ id gl in
+ let typ = EConstr.of_constr typ in
if pred (id,typ) then
tac1 id
else
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2c3e51280..e4f110722 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -76,7 +76,7 @@ val nLastDecls : int -> goal sigma -> Context.Named.t
val afterHyp : Id.t -> goal sigma -> Context.Named.t
-val ifOnHyp : (Id.t * types -> bool) ->
+val ifOnHyp : (Id.t * EConstr.types -> bool) ->
(Id.t -> tactic) -> (Id.t -> tactic) ->
Id.t -> tactic
@@ -230,7 +230,7 @@ module New : sig
val nLastDecls : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t
- val ifOnHyp : (identifier * types -> bool) ->
+ val ifOnHyp : (identifier * EConstr.types -> bool) ->
(identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
identifier -> unit Proofview.tactic
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 13:53:54 +0000