aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml14
-rw-r--r--tactics/contradiction.mli3
-rw-r--r--tactics/elim.ml8
-rw-r--r--tactics/equality.mli10
-rw-r--r--tactics/extraargs.mli14
-rw-r--r--tactics/extratactics.ml42
-rw-r--r--tactics/extratactics.mli8
-rw-r--r--tactics/hiddentac.ml64
-rw-r--r--tactics/hiddentac.mli23
-rw-r--r--tactics/inv.ml2
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/setoid_replace.ml8
-rw-r--r--tactics/tacinterp.ml32
-rw-r--r--tactics/tacinterp.mli10
-rw-r--r--tactics/tactics.ml21
-rw-r--r--tactics/tactics.mli43
16 files changed, 163 insertions, 101 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index d1caa9862..f0e9842fa 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -216,12 +216,12 @@ let make_apply_entry env sigma (eapply,verbose) (c,cty) =
(hd,
{ pri = nb_hyp cty + nmiss;
pat = Some pat;
- code = ERes_pf(c,{ce with templenv=empty_env}) })
+ code = ERes_pf(c,{ce with env=empty_env}) })
end else
(hd,
{ pri = nb_hyp cty;
pat = Some pat;
- code = Res_pf(c,{ce with templenv=empty_env}) })
+ code = Res_pf(c,{ce with env=empty_env}) })
| _ -> failwith "make_apply_entry"
(* eap is (e,v) with e=true if eapply and v=true if verbose
@@ -270,7 +270,7 @@ let make_trivial env sigma c =
let ce = mk_clenv_from dummy_goal (c,t) in
(hd, { pri=1;
pat = Some (Pattern.pattern_of_constr (clenv_type ce));
- code=Res_pf_THEN_trivial_fail(c,{ce with templenv=empty_env}) })
+ code=Res_pf_THEN_trivial_fail(c,{ce with env=empty_env}) })
open Vernacexpr
@@ -673,8 +673,11 @@ let gen_trivial lems = function
| None -> full_trivial lems
| Some l -> trivial lems l
+let inj_open c = (Evd.empty,c)
+
let h_trivial lems l =
- Refiner.abstract_tactic (TacTrivial (lems,l)) (gen_trivial lems l)
+ Refiner.abstract_tactic (TacTrivial (List.map inj_open lems,l))
+ (gen_trivial lems l)
(**************************************************************************)
(* The classical Auto tactic *)
@@ -784,7 +787,8 @@ let gen_auto n lems dbnames =
let inj_or_var = option_map (fun n -> ArgArg n)
let h_auto n lems l =
- Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l)
+ Refiner.abstract_tactic (TacAuto (inj_or_var n,List.map inj_open lems,l))
+ (gen_auto n lems l)
(**************************************************************************)
(* The "destructing Auto" from Eduardo *)
diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli
index 145411aa1..71817b2c7 100644
--- a/tactics/contradiction.mli
+++ b/tactics/contradiction.mli
@@ -13,7 +13,8 @@ open Names
open Term
open Proof_type
open Rawterm
+open Genarg
(*i*)
val absurd : constr -> tactic
-val contradiction : constr with_bindings option -> tactic
+val contradiction : constr with_ebindings option -> tactic
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 90b3c66b2..43ea91f5a 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -136,14 +136,16 @@ let decompose_or c gls =
(fun (_,t) -> is_disjunction t)
c gls
+let inj_open c = (Evd.empty,c)
+
let h_decompose l c =
- Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l)
+ Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l)
let h_decompose_or c =
- Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c)
+ Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c)
let h_decompose_and c =
- Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c)
+ Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c)
(* The tactic Double performs a double induction *)
diff --git a/tactics/equality.mli b/tactics/equality.mli
index e7726eac3..9254e5f0d 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -26,7 +26,7 @@ open Genarg
(*i*)
val general_rewrite_bindings :
- bool -> constr with_bindings -> evars_flag -> tactic
+ bool -> constr with_ebindings -> evars_flag -> tactic
val general_rewrite :
bool -> constr -> tactic
@@ -42,16 +42,16 @@ val rewriteRL : constr -> tactic
(* Warning: old [general_rewrite_in] is now [general_rewrite_bindings_in] *)
val general_rewrite_bindings_in :
- bool -> identifier -> constr with_bindings -> evars_flag -> tactic
+ bool -> identifier -> constr with_ebindings -> evars_flag -> tactic
val general_rewrite_in :
bool -> identifier -> constr -> evars_flag -> tactic
val general_multi_rewrite :
- bool -> evars_flag -> constr with_bindings -> clause -> tactic
+ bool -> evars_flag -> constr with_ebindings -> clause -> tactic
-val conditional_rewrite : bool -> tactic -> constr with_bindings -> tactic
+val conditional_rewrite : bool -> tactic -> constr with_ebindings -> tactic
val conditional_rewrite_in :
- bool -> identifier -> tactic -> constr with_bindings -> tactic
+ bool -> identifier -> tactic -> constr with_ebindings -> tactic
val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic
val replace : constr -> constr -> tactic
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index a1da9d2b3..2f891a61f 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -16,18 +16,18 @@ open Topconstr
open Rawterm
val rawwit_orient : bool raw_abstract_argument_type
-val wit_orient : bool closed_abstract_argument_type
+val wit_orient : bool typed_abstract_argument_type
val orient : bool Pcoq.Gram.Entry.e
val rawwit_morphism_signature :
Setoid_replace.morphism_signature raw_abstract_argument_type
val wit_morphism_signature :
- Setoid_replace.morphism_signature closed_abstract_argument_type
+ Setoid_replace.morphism_signature typed_abstract_argument_type
val morphism_signature :
Setoid_replace.morphism_signature Pcoq.Gram.Entry.e
val rawwit_raw : constr_expr raw_abstract_argument_type
-val wit_raw : rawconstr closed_abstract_argument_type
+val wit_raw : rawconstr typed_abstract_argument_type
val raw : constr_expr Pcoq.Gram.Entry.e
type 'id gen_place= ('id * hyp_location_flag,unit) location
@@ -36,20 +36,20 @@ type loc_place = identifier Util.located gen_place
type place = identifier gen_place
val rawwit_hloc : loc_place raw_abstract_argument_type
-val wit_hloc : place closed_abstract_argument_type
+val wit_hloc : place typed_abstract_argument_type
val hloc : loc_place Pcoq.Gram.Entry.e
val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.Entry.e
val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type
-val wit_in_arg_hyp : (Names.identifier list option * bool) closed_abstract_argument_type
+val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type
val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause
val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause
val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e
val rawwit_by_arg_tac : raw_tactic_expr option raw_abstract_argument_type
-val wit_by_arg_tac : glob_tactic_expr option closed_abstract_argument_type
+val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type
@@ -57,4 +57,4 @@ val wit_by_arg_tac : glob_tactic_expr option closed_abstract_argument_type
val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e
val rawwit_retroknowledge_field : Retroknowledge.field raw_abstract_argument_type
-val wit_retroknowledge_field : Retroknowledge.field closed_abstract_argument_type
+val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index d51d17aaf..ea33ead5d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -323,7 +323,7 @@ let step left x tac =
let l =
List.map (fun lem ->
tclTHENLAST
- (apply_with_bindings (lem, ImplicitBindings [x]))
+ (apply_with_bindings (lem, ImplicitBindings [Evd.empty,x]))
tac)
!(if left then transitivity_left_table else transitivity_right_table)
in
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index 23d4a275d..341716c01 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -8,17 +8,11 @@
(*i $Id$ i*)
-open Util
-open Names
-open Term
open Proof_type
open Rawterm
-open Tacexpr
-open Topconstr
-open Genarg
val h_discrHyp : quantified_hypothesis -> tactic
val h_injHyp : quantified_hypothesis -> tactic
-val refine_tac : Genarg.open_constr -> tactic
+val refine_tac : Evd.open_constr -> tactic
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index b8c8e6d18..85a85083e 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -20,6 +20,13 @@ open Tactics
open Util
let inj_id id = (dummy_loc,id)
+let inj_open c = (Evd.empty,c)
+let inj_open_wb (c,b) = ((Evd.empty,c),b)
+let inj_ia = function
+ | ElimOnConstr c -> ElimOnConstr (inj_open c)
+ | ElimOnIdent id -> ElimOnIdent id
+ | ElimOnAnonHyp n -> ElimOnAnonHyp n
+let inj_occ (occ,c) = (occ,inj_open c)
(* Basic tactics *)
let h_intro_move x y =
@@ -27,27 +34,39 @@ let h_intro_move x y =
let h_intro x = h_intro_move (Some x) None
let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x)
let h_assumption = abstract_tactic TacAssumption assumption
-let h_exact c = abstract_tactic (TacExact c) (exact_check c)
-let h_exact_no_check c = abstract_tactic (TacExactNoCheck c) (exact_no_check c)
+let h_exact c = abstract_tactic (TacExact (inj_open c)) (exact_check c)
+let h_exact_no_check c =
+ abstract_tactic (TacExactNoCheck (inj_open c)) (exact_no_check c)
let h_vm_cast_no_check c =
- abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c)
-let h_apply ev cb = abstract_tactic (TacApply (ev,cb)) (apply_with_bindings_gen ev cb)
-let h_elim cb cbo = abstract_tactic (TacElim (cb,cbo)) (elim cb cbo)
-let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c)
-let h_case cb = abstract_tactic (TacCase cb) (general_case_analysis cb)
-let h_case_type c = abstract_tactic (TacCaseType c) (case_type c)
+ abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c)
+let h_apply ev cb =
+ abstract_tactic (TacApply (ev,inj_open_wb cb))
+ (apply_with_bindings_gen ev cb)
+let h_elim cb cbo =
+ abstract_tactic (TacElim (inj_open_wb cb,option_map inj_open_wb cbo))
+ (elim cb cbo)
+let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c)
+let h_case cb = abstract_tactic (TacCase (inj_open_wb cb)) (general_case_analysis cb)
+let h_case_type c = abstract_tactic (TacCaseType (inj_open c)) (case_type c)
let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n)
let h_mutual_fix id n l =
- abstract_tactic (TacMutualFix (id,n,l)) (mutual_fix id n l)
+ abstract_tactic
+ (TacMutualFix (id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l))
+ (mutual_fix id n l)
let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido)
let h_mutual_cofix id l =
- abstract_tactic (TacMutualCofix (id,l)) (mutual_cofix id l)
+ abstract_tactic
+ (TacMutualCofix (id,List.map (fun (id,c) -> (id,inj_open c)) l))
+ (mutual_cofix id l)
-let h_cut c = abstract_tactic (TacCut c) (cut c)
-let h_generalize cl = abstract_tactic (TacGeneralize cl) (generalize cl)
-let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
+let h_cut c = abstract_tactic (TacCut (inj_open c)) (cut c)
+let h_generalize cl =
+ abstract_tactic (TacGeneralize (List.map inj_open cl))
+ (generalize cl)
+let h_generalize_dep c =
+ abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c)
let h_let_tac na c cl =
- abstract_tactic (TacLetTac (na,c,cl)) (letin_tac true na c cl)
+ abstract_tactic (TacLetTac (na,inj_open c,cl)) (letin_tac true na c cl)
let h_instantiate n c ido =
(Evar_tactics.instantiate n c ido)
(* abstract_tactic (TacInstantiate (n,c,cls))
@@ -59,11 +78,13 @@ let h_simple_induction h =
let h_simple_destruct h =
abstract_tactic (TacSimpleDestruct h) (simple_destruct h)
let h_new_induction c e idl =
- abstract_tactic (TacNewInduction (c,e,idl)) (new_induct c e idl)
+ abstract_tactic (TacNewInduction (List.map inj_ia c,option_map inj_open_wb e,idl))
+ (new_induct c e idl)
let h_new_destruct c e idl =
- abstract_tactic (TacNewDestruct (c,e,idl)) (new_destruct c e idl)
-let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (new_hyp n d)
-let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c)
+ abstract_tactic (TacNewDestruct (List.map inj_ia c,option_map inj_open_wb e,idl))
+ (new_destruct c e idl)
+let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (new_hyp n d)
+let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c)
(* Context management *)
let h_clear b l = abstract_tactic (TacClear (b,l))
@@ -89,16 +110,17 @@ let h_simplest_left = h_left NoBindings
let h_simplest_right = h_right NoBindings
(* Conversion *)
-let h_reduce r cl = abstract_tactic (TacReduce (r,cl)) (reduce r cl)
+let h_reduce r cl =
+ abstract_tactic (TacReduce (inj_red_expr r,cl)) (reduce r cl)
let h_change oc c cl =
- abstract_tactic (TacChange (oc,c,cl))
+ abstract_tactic (TacChange (option_map inj_occ oc,inj_open c,cl))
(change (option_map Redexpr.out_with_occurrences oc) c cl)
(* Equivalence relations *)
let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity
let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c)
let h_transitivity c =
- abstract_tactic (TacTransitivity c) (intros_transitivity c)
+ abstract_tactic (TacTransitivity (inj_open c)) (intros_transitivity c)
let h_simplest_apply c = h_apply false (c,NoBindings)
let h_simplest_eapply c = h_apply true (c,NoBindings)
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 767f217b9..9c92ddcf2 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -16,6 +16,7 @@ open Tacmach
open Genarg
open Tacexpr
open Rawterm
+open Evd
(*i*)
(* Tactics for the interpreter. They left a trace in the proof tree
@@ -32,12 +33,12 @@ val h_exact : constr -> tactic
val h_exact_no_check : constr -> tactic
val h_vm_cast_no_check : constr -> tactic
-val h_apply : evars_flag -> constr with_bindings -> tactic
+val h_apply : evars_flag -> constr with_ebindings -> tactic
-val h_elim : constr with_bindings ->
- constr with_bindings option -> tactic
+val h_elim : constr with_ebindings ->
+ constr with_ebindings option -> tactic
val h_elim_type : constr -> tactic
-val h_case : constr with_bindings -> tactic
+val h_case : constr with_ebindings -> tactic
val h_case_type : constr -> tactic
val h_mutual_fix : identifier -> int ->
@@ -58,12 +59,12 @@ val h_instantiate : int -> Rawterm.rawconstr ->
val h_simple_induction : quantified_hypothesis -> tactic
val h_simple_destruct : quantified_hypothesis -> tactic
val h_new_induction :
- constr induction_arg list -> constr with_bindings option ->
+ constr induction_arg list -> constr with_ebindings option ->
intro_pattern_expr -> tactic
val h_new_destruct :
- constr induction_arg list -> constr with_bindings option ->
+ constr induction_arg list -> constr with_ebindings option ->
intro_pattern_expr -> tactic
-val h_specialize : int option -> constr with_bindings -> tactic
+val h_specialize : int option -> constr with_ebindings -> tactic
val h_lapply : constr -> tactic
(* Automation tactic : see Auto *)
@@ -77,10 +78,10 @@ val h_rename : identifier -> identifier -> tactic
(* Constructors *)
-val h_constructor : int -> constr bindings -> tactic
-val h_left : constr bindings -> tactic
-val h_right : constr bindings -> tactic
-val h_split : constr bindings -> tactic
+val h_constructor : int -> open_constr bindings -> tactic
+val h_left : open_constr bindings -> tactic
+val h_right : open_constr bindings -> tactic
+val h_split : open_constr bindings -> tactic
val h_one_constructor : int -> tactic
val h_simplest_left : tactic
diff --git a/tactics/inv.ml b/tactics/inv.ml
index b799c939f..47b8ca64b 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -47,7 +47,7 @@ let collect_meta_variables c =
let check_no_metas clenv ccl =
if occur_meta ccl then
let metas = List.filter (fun na -> na<>Anonymous)
- (List.map (Evd.meta_name clenv.env) (collect_meta_variables ccl)) in
+ (List.map (Evd.meta_name clenv.evd) (collect_meta_variables ccl)) in
errorlabstrm "inversion"
(str ("Cannot find an instantiation for variable"^
(if List.length metas = 1 then " " else "s ")) ++
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index a0ff76968..1b308e298 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -292,7 +292,7 @@ let add_inversion_lemma_exn na com comsort bool tac =
let lemInv id c gls =
try
let clause = mk_clenv_type_of gls c in
- let clause = clenv_constrain_with_bindings [(-1,mkVar id)] clause in
+ let clause = clenv_constrain_with_bindings [(-1,(Evd.empty,mkVar id))] clause in
Clenvtac.res_pf clause ~allow_K:true gls
with
| UserError (a,b) ->
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 170f2948d..8fc95b408 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1734,14 +1734,14 @@ let unification_rewrite c1 c2 cl but gl =
(* ~mod_delta:false to allow to mark occurences that must not be
rewritten simply by replacing them with let-defined definitions
in the context *)
- w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.env
+ w_unify_to_subterm ~mod_delta:false (pf_env gl) (c1,but) cl.evd
with
Pretype_errors.PretypeError _ ->
(* ~mod_delta:true to make Ring work (since it really
exploits conversion) *)
- w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.env
+ w_unify_to_subterm ~mod_delta:true (pf_env gl) (c1,but) cl.evd
in
- let cl' = {cl with env = env' } in
+ let cl' = {cl with evd = env' } in
let c2 = Clenv.clenv_nf_meta cl' c2 in
check_evar_map_of_evars_defs env' ;
env',Clenv.clenv_value cl', c1, c2
@@ -1983,7 +1983,7 @@ let setoid_transitivity c gl =
| _ -> assert false
in
apply_with_bindings
- (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, c ]) gl
+ (trans, Rawterm.ExplicitBindings [ dummy_loc, binder, (Evd.empty,c) ]) gl
with
Optimize -> transitivity c gl
;;
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4dfcebbe7..aba013c1c 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -288,7 +288,7 @@ type glob_sign = {
type interp_genarg_type =
(glob_sign -> raw_generic_argument -> glob_generic_argument) *
(interp_sign -> goal sigma -> glob_generic_argument ->
- closed_generic_argument) *
+ typed_generic_argument) *
(substitution -> glob_generic_argument -> glob_generic_argument)
let extragenargtab =
@@ -1367,6 +1367,21 @@ let pf_interp_constr_list_as_list ist gl (c,_ as x) =
let pf_interp_constr_list ist gl l =
List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l)
+let inj_open c = (Evd.empty,c)
+
+let pf_interp_open_constr_list_as_list ist gl (c,_ as x) =
+ match c with
+ | RVar (_,id) ->
+ (try List.map inj_open
+ (constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun))
+ with Not_found ->
+ [interp_open_constr None ist (project gl) (pf_env gl) x])
+ | _ ->
+ [interp_open_constr None ist (project gl) (pf_env gl) x]
+
+let pf_interp_open_constr_list ist gl l =
+ List.flatten (List.map (pf_interp_open_constr_list_as_list ist gl) l)
+
(* Interprets a type expression *)
let pf_interp_type ist gl =
interp_type ist (project gl) (pf_env gl)
@@ -1446,6 +1461,12 @@ let interp_constr_may_eval ist gl c =
csr
end
+let inj_may_eval = function
+ | ConstrTerm c -> ConstrTerm (inj_open c)
+ | ConstrEval (r,c) -> ConstrEval (Tactics.inj_red_expr r,inj_open c)
+ | ConstrContext (id,c) -> ConstrContext (id,inj_open c)
+ | ConstrTypeOf c -> ConstrTypeOf (inj_open c)
+
let message_of_value = function
| VVoid -> str "()"
| VInteger n -> int n
@@ -1517,16 +1538,19 @@ let interp_induction_arg ist gl = function
(pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))))
let interp_binding ist gl (loc,b,c) =
- (loc,interp_quantified_hypothesis ist b,pf_interp_constr ist gl c)
+ (loc,interp_quantified_hypothesis ist b,pf_interp_open_constr false ist gl c)
let interp_bindings ist gl = function
| NoBindings -> NoBindings
-| ImplicitBindings l -> ImplicitBindings (pf_interp_constr_list ist gl l)
+| ImplicitBindings l -> ImplicitBindings (pf_interp_open_constr_list ist gl l)
| ExplicitBindings l -> ExplicitBindings (List.map (interp_binding ist gl) l)
let interp_constr_with_bindings ist gl (c,bl) =
(pf_interp_constr ist gl c, interp_bindings ist gl bl)
+let interp_open_constr_with_bindings ist gl (c,bl) =
+ (pf_interp_open_constr false ist gl c, interp_bindings ist gl bl)
+
let mk_constr_value ist gl c = VConstr (pf_interp_constr ist gl c)
let mk_hyp_value ist gl c = VConstr (mkVar (interp_hyp ist gl c))
let mk_int_or_var_value ist c = VInteger (interp_int_or_var ist c)
@@ -2047,7 +2071,7 @@ and interp_atomic ist gl = function
| TacCut c -> h_cut (pf_interp_type ist gl c)
| TacAssert (t,ipat,c) ->
let c = (if t=None then pf_interp_constr else pf_interp_type) ist gl c in
- abstract_tactic (TacAssert (t,ipat,c))
+ abstract_tactic (TacAssert (t,ipat,inj_open c))
(Tactics.forward (option_map (interp_tactic ist) t)
(interp_intro_pattern ist gl ipat) c)
| TacGeneralize cl -> h_generalize (pf_interp_constr_list ist gl cl)
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index ca9b076d9..b4a715983 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -66,11 +66,11 @@ val add_primitive_tactic : string -> glob_tactic_expr -> unit
(* Tactic extensions *)
val add_tactic :
- string -> (closed_generic_argument list -> tactic) -> unit
+ string -> (typed_generic_argument list -> tactic) -> unit
val overwriting_add_tactic :
- string -> (closed_generic_argument list -> tactic) -> unit
+ string -> (typed_generic_argument list -> tactic) -> unit
val lookup_tactic :
- string -> (closed_generic_argument list) -> tactic
+ string -> (typed_generic_argument list) -> tactic
(* Adds an interpretation function for extra generic arguments *)
type glob_sign = {
@@ -83,12 +83,12 @@ val add_interp_genarg :
string ->
(glob_sign -> raw_generic_argument -> glob_generic_argument) *
(interp_sign -> goal sigma -> glob_generic_argument ->
- closed_generic_argument) *
+ typed_generic_argument) *
(substitution -> glob_generic_argument -> glob_generic_argument)
-> unit
val interp_genarg :
- interp_sign -> goal sigma -> glob_generic_argument -> closed_generic_argument
+ interp_sign -> goal sigma -> glob_generic_argument -> typed_generic_argument
val intern_genarg :
glob_sign -> raw_generic_argument -> glob_generic_argument
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e71911f6b..b042a8422 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -505,7 +505,7 @@ let cut_in_parallel l =
prec (List.rev l)
let error_uninstantiated_metas t clenv =
- let na = meta_name clenv.env (List.hd (Metaset.elements (metavars_of t))) in
+ let na = meta_name clenv.evd (List.hd (Metaset.elements (metavars_of t))) in
let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta"
in errorlabstrm "" (str "cannot find an instance for " ++ pr_id id)
@@ -516,7 +516,7 @@ let clenv_refine_in with_evars id clenv gl =
error_uninstantiated_metas new_hyp_typ clenv;
let new_hyp_prf = clenv_value clenv in
tclTHEN
- (tclEVARS (evars_of clenv.env))
+ (tclEVARS (evars_of clenv.evd))
(cut_replacing id new_hyp_typ
(fun x gl -> refine_no_check new_hyp_prf gl)) gl
@@ -558,8 +558,19 @@ let eapply_with_bindings = apply_with_bindings_gen true
let apply c = apply_with_bindings (c,NoBindings)
+let inj_open c = (Evd.empty,c)
+
+let inj_occ (occ,c) = (occ,inj_open c)
+
+let inj_red_expr = function
+ | Simpl lo -> Simpl (option_map inj_occ lo)
+ | Fold l -> Fold (List.map inj_open l)
+ | Pattern l -> Pattern (List.map inj_occ l)
+ | (ExtraRedExpr _ | CbvVm | Red _ | Hnf | Cbv _ | Lazy _ | Unfold _ as c)
+ -> c
+
let apply_list = function
- | c::l -> apply_with_bindings (c,ImplicitBindings l)
+ | c::l -> apply_with_bindings (c,ImplicitBindings (List.map inj_open l))
| _ -> assert false
(* Resolution with no reduction on the type *)
@@ -710,7 +721,7 @@ let new_hyp mopt (c,lbind) g =
| Some m -> if m < nargs then list_firstn m tstack else tstack
| None -> tstack)
in
- (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.env))
+ (tclTHENLAST (tclTHEN (tclEVARS (evars_of clause.evd))
(cut (pf_type_of g cut_pf)))
((tclORELSE (apply cut_pf) (exact_no_check cut_pf)))) g
@@ -1530,7 +1541,7 @@ let cook_sign hyp0_opt indvars_init env =
(* [rel_contexts] and [rel_declaration] actually contain triples, and
lists are actually in reverse order to fit [compose_prod]. *)
type elim_scheme = {
- elimc: (Term.constr * constr Rawterm.bindings) option;
+ elimc: constr with_ebindings option;
elimt: types;
indref: global_reference option;
params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 52c5ba883..6b0f8413a 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -28,12 +28,15 @@ open Nametab
open Rawterm
(*i*)
+val inj_open : constr -> open_constr
+val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen
+
(* Main tactics. *)
(*s General functions. *)
val type_clenv_binding : goal sigma ->
- constr * constr -> constr bindings -> constr
+ constr * constr -> open_constr bindings -> constr
val string_of_inductive : constr -> string
val head_constr : constr -> constr list
@@ -152,7 +155,7 @@ val clear : identifier list -> tactic
val clear_body : identifier list -> tactic
val keep : identifier list -> tactic
-val new_hyp : int option -> constr with_bindings -> tactic
+val new_hyp : int option -> constr with_ebindings -> tactic
val move_hyp : bool -> identifier -> identifier -> tactic
val rename_hyp : identifier -> identifier -> tactic
@@ -166,13 +169,13 @@ val bring_hyps : named_context -> tactic
val apply : constr -> tactic
val apply_without_reduce : constr -> tactic
val apply_list : constr list -> tactic
-val apply_with_bindings_gen : evars_flag -> constr with_bindings -> tactic
-val apply_with_bindings : constr with_bindings -> tactic
-val eapply_with_bindings : constr with_bindings -> tactic
+val apply_with_bindings_gen : evars_flag -> constr with_ebindings -> tactic
+val apply_with_bindings : constr with_ebindings -> tactic
+val eapply_with_bindings : constr with_ebindings -> tactic
val cut_and_apply : constr -> tactic
-val apply_in : evars_flag -> identifier -> constr with_bindings list -> tactic
+val apply_in : evars_flag -> identifier -> constr with_ebindings list -> tactic
(*s Elimination tactics. *)
@@ -203,7 +206,7 @@ val apply_in : evars_flag -> identifier -> constr with_bindings list -> tactic
(* [rel_contexts] and [rel_declaration] actually contain triples, and
lists are actually in reverse order to fit [compose_prod]. *)
type elim_scheme = {
- elimc: (Term.constr * constr Rawterm.bindings) option;
+ elimc: constr with_ebindings option;
elimt: types;
indref: global_reference option;
params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
@@ -223,28 +226,28 @@ type elim_scheme = {
}
-val compute_elim_sig : ?elimc: (Term.constr * constr Rawterm.bindings) -> types -> elim_scheme
+val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme
val general_elim :
- constr with_bindings -> constr with_bindings -> ?allow_K:bool -> tactic
+ constr with_ebindings -> constr with_ebindings -> ?allow_K:bool -> tactic
val general_elim_in : evars_flag ->
- identifier -> constr with_bindings -> constr with_bindings -> tactic
+ identifier -> constr with_ebindings -> constr with_ebindings -> tactic
-val default_elim : constr with_bindings -> tactic
+val default_elim : constr with_ebindings -> tactic
val simplest_elim : constr -> tactic
-val elim : constr with_bindings -> constr with_bindings option -> tactic
+val elim : constr with_ebindings -> constr with_ebindings option -> tactic
val simple_induct : quantified_hypothesis -> tactic
-val new_induct : constr induction_arg list -> constr with_bindings option ->
+val new_induct : constr induction_arg list -> constr with_ebindings option ->
intro_pattern_expr -> tactic
(*s Case analysis tactics. *)
-val general_case_analysis : constr with_bindings -> tactic
+val general_case_analysis : constr with_ebindings -> tactic
val simplest_case : constr -> tactic
val simple_destruct : quantified_hypothesis -> tactic
-val new_destruct : constr induction_arg list -> constr with_bindings option ->
+val new_destruct : constr induction_arg list -> constr with_ebindings option ->
intro_pattern_expr -> tactic
(*s Eliminations giving the type instead of the proof. *)
@@ -265,14 +268,14 @@ val dorE : bool -> clause ->tactic
(*s Introduction tactics. *)
val constructor_tac : int option -> int ->
- constr bindings -> tactic
-val one_constructor : int -> constr bindings -> tactic
+ open_constr bindings -> tactic
+val one_constructor : int -> open_constr bindings -> tactic
val any_constructor : tactic option -> tactic
-val left : constr bindings -> tactic
+val left : open_constr bindings -> tactic
val simplest_left : tactic
-val right : constr bindings -> tactic
+val right : open_constr bindings -> tactic
val simplest_right : tactic
-val split : constr bindings -> tactic
+val split : open_constr bindings -> tactic
val simplest_split : tactic
(*s Logical connective tactics. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 17:50:01 +0000