aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml2
-rw-r--r--tactics/autorewrite.ml4
-rw-r--r--tactics/eauto.ml43
-rw-r--r--tactics/equality.ml9
-rw-r--r--tactics/evar_tactics.ml2
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/refine.ml13
-rw-r--r--tactics/setoid_replace.ml19
-rw-r--r--tactics/tacinterp.ml8
-rw-r--r--tactics/tactics.ml56
-rw-r--r--tactics/tactics.mli10
-rw-r--r--tactics/termdn.ml2
12 files changed, 72 insertions, 58 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index dd07c2b90..e6d1194a5 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -189,7 +189,7 @@ let make_exact_entry name (c,cty) =
{ hname=name; pri=0; pat=None; code=Give_exact c })
let dummy_goal =
- {it={evar_hyps=empty_named_context;evar_concl=mkProp;evar_body=Evar_empty};
+ {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty};
sigma=Evd.empty}
let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index b79e6c608..6cf0cc981 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -89,7 +89,7 @@ let autorewrite_in id tac_main lbas gl =
let to_be_cleared = ref false in
fun dir cstr gl ->
let last_hyp_id =
- match gl.Evd.it.Evd.evar_hyps with
+ match (Environ.named_context_of_val gl.Evd.it.Evd.evar_hyps) with
(last_hyp_id,_,_)::_ -> last_hyp_id
| _ -> (* even the hypothesis id is missing *)
error ("No such hypothesis : " ^ (string_of_id !id))
@@ -98,7 +98,7 @@ let autorewrite_in id tac_main lbas gl =
let gls = (fst gl').Evd.it in
match gls with
g::_ ->
- (match g.Evd.evar_hyps with
+ (match Environ.named_context_of_val g.Evd.evar_hyps with
(lastid,_,_)::_ ->
if last_hyp_id <> lastid then
begin
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 52f5f011a..e3cb25632 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -85,7 +85,8 @@ let e_constructor_tac boundopt i lbind gl =
end;
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
let apply_tac = e_resolve_with_bindings_tac (cons,lbind) in
- (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl
+ (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast
+; intros; apply_tac]) gl
let e_one_constructor i = e_constructor_tac None i
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 57d9ab58a..23e4d311c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -690,7 +690,7 @@ let try_delta_expand env sigma t =
match kind_of_term c with
| Construct _ -> whdt
| App (f,_) -> hd_rec f
- | Cast (c,_) -> hd_rec c
+ | Cast (c,_,_) -> hd_rec c
| _ -> t
in
hd_rec whdt
@@ -1036,7 +1036,7 @@ let unfold_body x gl =
let rfun _ _ c = replace_term xvar xval c in
tclTHENLIST
[tclMAP (fun h -> reduct_in_hyp rfun h) hl;
- reduct_in_concl rfun] gl
+ reduct_in_concl (rfun,DEFAULTcast)] gl
@@ -1088,8 +1088,9 @@ let subst_one x gl =
let introtac = function
(id,None,_) -> intro_using id
| (id,Some hval,htyp) ->
- forward true (Name id) (mkCast(replace_term varx rhs hval,
- replace_term varx rhs htyp)) in
+ forward true (Name id) (mkCast(replace_term varx rhs hval,DEFAULTcast,
+ replace_term varx rhs htyp))
+ in
let need_rewrite = dephyps <> [] || depconcl in
tclTHENLIST
((if need_rewrite then
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index a0be2149a..d1a2b40b1 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -34,7 +34,7 @@ let instantiate n rawc ido gl =
match ido with
ConclLocation () -> evar_list sigma gl.it.evar_concl
| HypLocation (id,hloc) ->
- let decl = lookup_named id gl.it.evar_hyps in
+ let decl = Environ.lookup_named_val id gl.it.evar_hyps in
match hloc with
InHyp ->
(match decl with
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 60d05ec70..481b78683 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -216,7 +216,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
errorlabstrm "lemma_inversion"
(str"Computed inversion goal was not closed in initial signature");
*)
- let invSign = named_context invEnv in
+ let invSign = named_context_val invEnv in
let pfs = mk_pftreestate (mk_goal invSign invGoal) in
let pfs = solve_pftreestate (tclTHEN intro (onLastHyp inv_op)) pfs in
let (pfterm,meta_types) = extract_open_pftreestate pfs in
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 493232d3c..a6b904c05 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -97,9 +97,9 @@ let replace_by_meta env = function
(* quand on introduit une mv on calcule son type *)
let ty = match kind_of_term c with
| Lambda (Name id,c1,c2) when isCast c2 ->
- mkNamedProd id c1 (snd (destCast c2))
+ let _,_,t = destCast c2 in mkNamedProd id c1 t
| Lambda (Anonymous,c1,c2) when isCast c2 ->
- mkArrow c1 (snd (destCast c2))
+ let _,_,t = destCast c2 in mkArrow c1 t
| _ -> (* (App _ | Case _) -> *)
Retyping.get_type_of_with_meta env Evd.empty mm c
(*
@@ -108,7 +108,7 @@ let replace_by_meta env = function
| _ -> invalid_arg "Tcc.replace_by_meta (TO DO)"
*)
in
- mkCast (m,ty),[n,ty],[Some th]
+ mkCast (m,DEFAULTcast, ty),[n,ty],[Some th]
exception NoMeta
@@ -138,9 +138,10 @@ let rec compute_metamap env c = match kind_of_term c with
| Meta n ->
TH (c,[],[None])
- | Cast (m,ty) when isMeta m ->
+ | Cast (m,_, ty) when isMeta m ->
TH (c,[destMeta m,ty],[None])
+
(* abstraction => il faut décomposer si le terme dessous n'est pas pur
* attention : dans ce cas il faut remplacer (Rel 1) par (Var x)
* où x est une variable FRAICHE *)
@@ -216,7 +217,7 @@ let rec compute_metamap env c = match kind_of_term c with
end
(* Cast. Est-ce bien exact ? *)
- | Cast (c,t) -> compute_metamap env c
+ | Cast (c,_,t) -> compute_metamap env c
(*let TH (c',mm,sgp) = compute_metamap sign c in
TH (mkCast (c',t),mm,sgp) *)
@@ -258,7 +259,7 @@ let rec tcc_aux subst (TH (c,mm,sgp) as _th) gl =
| Meta _ , _ ->
tclIDTAC gl
- | Cast (c,_), _ when isMeta c ->
+ | Cast (c,_,_), _ when isMeta c ->
tclIDTAC gl
(* terme pur => refine *)
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 5cd163364..316f3c276 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1464,7 +1464,7 @@ let mark_occur gl ~new_goals t in_c input_relation input_direction =
| (he::tl) as a->
let typnf = Reduction.whd_betadeltaiota env typ in
match kind_of_term typnf with
- Cast (typ,_) ->
+ Cast (typ,_,_) ->
find_non_dependent_function env c c_args_rev typ
f_args_rev a_rev a
| Prod (name,s,t) ->
@@ -1676,7 +1676,7 @@ let syntactic_but_representation_of_marked_but hole_relation hole_direction =
else
let c_is_proper =
let typ = mkApp (rel_out, [| c ; c |]) in
- mkCast (Evarutil.mk_new_meta (),typ)
+ mkCast (Evarutil.mk_new_meta (),DEFAULTcast, typ)
in
mkApp ((Lazy.force coq_ProperElementToKeep),
[| hole_relation ; hole_direction; precise_out ;
@@ -1759,7 +1759,8 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
let impl2 = mkProd (Anonymous, hyp1, lift 1 hyp2) in
let th' = mkApp (proj, [|impl2; impl1; th|]) in
Tactics.refine
- (mkApp (th', [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl in
+ (mkApp (th',[|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|]))
+ gl in
let if_output_relation_is_if gl =
let th =
apply_coq_setoid_rewrite input_relation output_relation c1 c2 hyp
@@ -1767,15 +1768,15 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
in
let new_but = Termops.replace_term c1 c2 but in
Tactics.refine
- (mkApp (th, [| mkCast (Evarutil.mk_new_meta(), new_but) |])) gl
- in
- if output_relation = (Lazy.force coq_iff_relation) then
+ (mkApp (th, [|mkCast (Evarutil.mk_new_meta(), DEFAULTcast, new_but)|]))
+ gl in
+ if output_relation = (Lazy.force coq_iff_relation) then
if_output_relation_is_iff gl
- else
+ else
if_output_relation_is_if gl
with
- Optimize ->
- !general_rewrite (input_direction = Left2Right) (snd hyp) gl
+ Optimize ->
+ !general_rewrite (input_direction = Left2Right) (snd hyp) gl
let analyse_hypothesis gl c =
let ctype = pf_type_of gl c in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 5948da2b8..177c3ffd8 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1191,7 +1191,9 @@ open Evd
let solvable_by_tactic env evi (ev,args) src =
match (!implicit_tactic, src) with
| Some tac, (ImplicitArg _ | QuestionMark)
- when evi.evar_hyps = Environ.named_context env ->
+ when
+ Environ.named_context_of_val evi.evar_hyps =
+ Environ.named_context env ->
let id = id_of_string "H" in
start_proof id IsLocal evi.evar_hyps evi.evar_concl (fun _ _ -> ());
begin
@@ -1510,7 +1512,7 @@ and interp_letin ist gl = function
with Not_found ->
try
let t = tactic_of_value v in
- let ndc = Environ.named_context env in
+ let ndc = Environ.named_context_val env in
start_proof id IsLocal ndc typ (fun _ _ -> ());
by t;
let (_,({const_entry_body = pft},_,_)) = cook_proof () in
@@ -1520,7 +1522,7 @@ and interp_letin ist gl = function
delete_proof (dummy_loc,id);
errorlabstrm "Tacinterp.interp_letin"
(str "Term or fully applied tactic expected in Let")
- in (id,VConstr (mkCast (csr,typ)))::(interp_letin ist gl tl)
+ in (id,VConstr (mkCast (csr,DEFAULTcast, typ)))::(interp_letin ist gl tl)
(* Interprets the Match Context expressions *)
and interp_match_context ist g lz lr lmr =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 5079a1010..d1a7507c7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -50,7 +50,7 @@ let rec nb_prod x =
match kind_of_term c with
Prod(_,_,t) -> count (n+1) t
| LetIn(_,a,_,t) -> count n (subst1 a t)
- | Cast(c,_) -> count n c
+ | Cast(c,_,_) -> count n c
| _ -> n
in count 0 x
@@ -144,8 +144,8 @@ type tactic_reduction = env -> evar_map -> constr -> constr
reduction function either to the conclusion or to a
certain hypothesis *)
-let reduct_in_concl redfun gl =
- convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) gl
+let reduct_in_concl (redfun,sty) gl =
+ convert_concl_no_check (pf_reduce redfun gl (pf_concl gl)) sty gl
let reduct_in_hyp redfun (id,_,(where,where')) gl =
let (_,c, ty) = pf_get_hyp gl id in
@@ -165,7 +165,7 @@ let reduct_in_hyp redfun (id,_,(where,where')) gl =
convert_hyp_no_check (id,Some b',ty') gl
let reduct_option redfun = function
- | Some id -> reduct_in_hyp redfun id
+ | Some id -> reduct_in_hyp (fst redfun) id
| None -> reduct_in_concl redfun
(* The following tactic determines whether the reduction
@@ -188,7 +188,8 @@ let change_on_subterm cv_pb t = function
| Some occl -> contextually false occl (change_and_check Reduction.CONV t)
let change_in_concl occl t =
- reduct_in_concl (change_on_subterm Reduction.CUMUL t occl)
+ reduct_in_concl ((change_on_subterm Reduction.CUMUL t occl),DEFAULTcast)
+
let change_in_hyp occl t =
reduct_in_hyp (change_on_subterm Reduction.CONV t occl)
@@ -205,22 +206,23 @@ let change occl c cls =
onClauses (change_option occl c) cls
(* Pour usage interne (le niveau User est pris en compte par reduce) *)
-let red_in_concl = reduct_in_concl red_product
+let red_in_concl = reduct_in_concl (red_product,DEFAULTcast)
let red_in_hyp = reduct_in_hyp red_product
-let red_option = reduct_option red_product
-let hnf_in_concl = reduct_in_concl hnf_constr
+let red_option = reduct_option (red_product,DEFAULTcast)
+let hnf_in_concl = reduct_in_concl (hnf_constr,DEFAULTcast)
let hnf_in_hyp = reduct_in_hyp hnf_constr
-let hnf_option = reduct_option hnf_constr
-let simpl_in_concl = reduct_in_concl nf
+let hnf_option = reduct_option (hnf_constr,DEFAULTcast)
+let simpl_in_concl = reduct_in_concl (nf,DEFAULTcast)
let simpl_in_hyp = reduct_in_hyp nf
-let simpl_option = reduct_option nf
-let normalise_in_concl = reduct_in_concl compute
+let simpl_option = reduct_option (nf,DEFAULTcast)
+let normalise_in_concl = reduct_in_concl (compute,DEFAULTcast)
let normalise_in_hyp = reduct_in_hyp compute
-let normalise_option = reduct_option compute
-let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname)
-let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
-let unfold_option loccname = reduct_option (unfoldn loccname)
-let pattern_option l = reduct_option (pattern_occs l)
+let normalise_option = reduct_option (compute,DEFAULTcast)
+let normalise_vm_in_concl = reduct_in_concl (Redexpr.cbv_vm,VMcast)
+let unfold_in_concl loccname = reduct_in_concl (unfoldn loccname,DEFAULTcast)
+let unfold_in_hyp loccname = reduct_in_hyp (unfoldn loccname)
+let unfold_option loccname = reduct_option (unfoldn loccname,DEFAULTcast)
+let pattern_option l = reduct_option (pattern_occs l,DEFAULTcast)
(* A function which reduces accordingly to a reduction expression,
as the command Eval does. *)
@@ -346,7 +348,9 @@ let pf_lookup_hypothesis_as_renamed_gen red h gl =
let rec aux ccl =
match pf_lookup_hypothesis_as_renamed env ccl h with
| None when red ->
- aux (Redexpr.reduction_of_red_expr (Red true) env (project gl) ccl)
+ aux
+ ((fst (Redexpr.reduction_of_red_expr (Red true)))
+ env (project gl) ccl)
| x -> x
in
try aux (pf_concl gl)
@@ -433,7 +437,7 @@ let rec intros_rmove = function
* of the type of a term. *)
let apply_type hdcty argl gl =
- refine (applist (mkCast (Evarutil.mk_new_meta(),hdcty),argl)) gl
+ refine (applist (mkCast (Evarutil.mk_new_meta(),DEFAULTcast, hdcty),argl)) gl
let apply_term hdc argl gl =
refine (applist (hdc,argl)) gl
@@ -443,7 +447,7 @@ let bring_hyps hyps =
else
(fun gl ->
let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in
- let f = mkCast (Evarutil.mk_new_meta(),newcl) in
+ let f = mkCast (Evarutil.mk_new_meta(),DEFAULTcast, newcl) in
refine_no_check (mkApp (f, instance_from_named_context hyps)) gl)
(* Resolution with missing arguments *)
@@ -749,7 +753,7 @@ let letin_tac with_eq name c occs gl =
let t = refresh_universes (pf_type_of gl c) in
let newcl = mkNamedLetIn id c t ccl in
tclTHENLIST
- [ convert_concl_no_check newcl;
+ [ convert_concl_no_check newcl DEFAULTcast;
intro_gen (IntroMustBe id) lastlhyp true;
if with_eq then tclIDTAC else thin_body [id];
tclMAP convert_hyp_no_check depdecls ] gl
@@ -882,7 +886,8 @@ let constructor_tac boundopt i lbind gl =
end;
let cons = mkConstruct (ith_constructor_of_inductive mind i) in
let apply_tac = apply_with_bindings (cons,lbind) in
- (tclTHENLIST [convert_concl_no_check redcl; intros; apply_tac]) gl
+ (tclTHENLIST
+ [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl
let one_constructor i = constructor_tac None i
@@ -1391,7 +1396,8 @@ let induction_tac varname typ ((elimc,lbindelimc),elimt) gl =
let c = mkVar varname in
let indclause = make_clenv_binding gl (c,typ) NoBindings in
let elimclause =
- make_clenv_binding gl (mkCast (elimc,elimt),elimt) lbindelimc in
+ make_clenv_binding gl
+ (mkCast (elimc,DEFAULTcast, elimt),elimt) lbindelimc in
elimination_clause_scheme true elimclause indclause gl
let make_up_names7 n ind (old_style,cname) =
@@ -1900,9 +1906,9 @@ let abstract_subproof name tac gls =
(fun (id,_,_ as d) (s1,s2) ->
if mem_named_context id current_sign &
interpretable_as_section_decl (Sign.lookup_named id current_sign) d
- then (s1,add_named_decl d s2)
+ then (s1,push_named_context_val d s2)
else (add_named_decl d s1,s2))
- global_sign (empty_named_context,empty_named_context) in
+ global_sign (empty_named_context,empty_named_context_val) in
let na = next_global_ident_away false name (pf_ids_of_hyps gls) in
let concl = it_mkNamedProd_or_LetIn (pf_concl gls) sign in
if occur_existential concl then
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 5b03a79dd..f3da4a8c9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -46,7 +46,7 @@ exception Bound
val introduction : identifier -> tactic
val refine : constr -> tactic
-val convert_concl : constr -> tactic
+val convert_concl : constr -> cast_kind -> tactic
val convert_hyp : named_declaration -> tactic
val thin : identifier list -> tactic
val mutual_fix :
@@ -110,8 +110,8 @@ val exact_proof : Topconstr.constr_expr -> tactic
type tactic_reduction = env -> evar_map -> constr -> constr
val reduct_in_hyp : tactic_reduction -> hyp_location -> tactic
-val reduct_option : tactic_reduction -> simple_clause -> tactic
-val reduct_in_concl : tactic_reduction -> tactic
+val reduct_option : tactic_reduction * cast_kind -> simple_clause -> tactic
+val reduct_in_concl : tactic_reduction * cast_kind -> tactic
val change_in_concl : constr occurrences option -> constr -> tactic
val change_in_hyp : constr occurrences option -> constr -> hyp_location ->
tactic
@@ -124,9 +124,10 @@ val hnf_option : simple_clause -> tactic
val simpl_in_concl : tactic
val simpl_in_hyp : hyp_location -> tactic
val simpl_option : simple_clause -> tactic
-val normalise_in_concl: tactic
+val normalise_in_concl : tactic
val normalise_in_hyp : hyp_location -> tactic
val normalise_option : simple_clause -> tactic
+val normalise_vm_in_concl : tactic
val unfold_in_concl : (int list * evaluable_global_reference) list -> tactic
val unfold_in_hyp :
(int list * evaluable_global_reference) list -> hyp_location -> tactic
@@ -250,3 +251,4 @@ val generalize_dep : constr -> tactic
val tclABSTRACT : identifier option -> tactic -> tactic
val admit_as_an_axiom : tactic
+
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 3ee0ee430..1c95f7fdc 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -28,7 +28,7 @@ type 'a t = (global_reference,constr_pattern,'a) Dn.t
let decomp =
let rec decrec acc c = match kind_of_term c with
| App (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
- | Cast (c1,_) -> decrec acc c1
+ | Cast (c1,_,_) -> decrec acc c1
| _ -> (c,acc)
in
decrec []
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 03:57:15 +0000