diff options
33 files changed, 423 insertions, 439 deletions
diff --git a/interp/genarg.mli b/interp/genarg.mli index ef7c3e864e..664ed43f06 100644 --- a/interp/genarg.mli +++ b/interp/genarg.mli @@ -195,11 +195,11 @@ val wit_casted_open_constr : (open_constr,tlevel) abstract_argument_type val rawwit_constr_with_bindings : (constr_expr with_bindings,rlevel) abstract_argument_type val globwit_constr_with_bindings : (rawconstr_and_expr with_bindings,glevel) abstract_argument_type -val wit_constr_with_bindings : (constr with_ebindings,tlevel) abstract_argument_type +val wit_constr_with_bindings : (constr with_bindings sigma,tlevel) abstract_argument_type val rawwit_bindings : (constr_expr bindings,rlevel) abstract_argument_type val globwit_bindings : (rawconstr_and_expr bindings,glevel) abstract_argument_type -val wit_bindings : (open_constr bindings,tlevel) abstract_argument_type +val wit_bindings : (constr bindings sigma,tlevel) abstract_argument_type val rawwit_red_expr : ((constr_expr,reference or_by_notation) red_expr_gen,rlevel) abstract_argument_type val globwit_red_expr : ((rawconstr_and_expr,evaluable_global_reference and_short_name or_var) red_expr_gen,glevel) abstract_argument_type diff --git a/lib/option.ml b/lib/option.ml index 2a530b89bd..942fff48ae 100644 --- a/lib/option.ml +++ b/lib/option.ml @@ -97,6 +97,12 @@ let fold_right f x a = | Some y -> f y a | _ -> a +(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *) +let fold_map f a x = + match x with + | Some y -> let a, z = f a y in a, Some z + | _ -> a, None + (** [cata f a x] is [a] if [x] is [None] and [f y] if [x] is [Some y]. *) let cata f a = function | Some c -> f c diff --git a/lib/option.mli b/lib/option.mli index 8002a7ea29..ef2e311a62 100644 --- a/lib/option.mli +++ b/lib/option.mli @@ -66,6 +66,9 @@ val fold_left2 : ('a -> 'b -> 'c -> 'a) -> 'a -> 'b option -> 'c option -> 'a (** [fold_right f x a] is [f y a] if [x] is [Some y], and [a] otherwise. *) val fold_right : ('a -> 'b -> 'b) -> 'a option -> 'b -> 'b +(** [fold_map f a x] is [a, f y] if [x] is [Some y], and [a] otherwise. *) +val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option + (** [cata e f x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) val cata : ('a -> 'b) -> 'b -> 'a option -> 'b diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index 1fde7b245a..fe7038d3a3 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -246,10 +246,10 @@ let rec pr_generic prc prlc prtac x = pr_red_expr (prc,prlc,pr_evaluable_reference) (out_gen wit_red_expr x) | OpenConstrArgType b -> prc (snd (out_gen (wit_open_constr_gen b) x)) | ConstrWithBindingsArgType -> - let (c,b) = out_gen wit_constr_with_bindings x in - pr_with_bindings prc prlc (c,out_bindings b) + let (c,b) = (out_gen wit_constr_with_bindings x).Evd.it in + pr_with_bindings prc prlc (c,b) | BindingsArgType -> - pr_bindings_no_with prc prlc (out_bindings (out_gen wit_bindings x)) + pr_bindings_no_with prc prlc (out_gen wit_bindings x).Evd.it | List0ArgType _ -> hov 0 (pr_sequence (pr_generic prc prlc prtac) (fold_list0 (fun a l -> a::l) x [])) @@ -288,7 +288,7 @@ let pr_raw_extend prc prlc prtac = let pr_glob_extend prc prlc prtac = pr_extend_gen (pr_glob_generic prc prlc prtac) let pr_extend prc prlc prtac = - pr_extend_gen (pr_generic (fun c -> prc (Evd.empty,c)) (fun c -> prlc (Evd.empty,c)) prtac) + pr_extend_gen (pr_generic prc prlc prtac) (**********************************************************************) (* The tactic printer *) @@ -1008,12 +1008,12 @@ let strip_prod_binders_rawterm n (ty,_) = | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty -let strip_prod_binders_constr n (sigma,ty) = +let strip_prod_binders_constr n ty = let rec strip_ty acc n ty = - if n=0 then (List.rev acc, (sigma,ty)) else + if n=0 then (List.rev acc, ty) else match Term.kind_of_term ty with Term.Prod(na,a,b) -> - strip_ty (([dummy_loc,na],(sigma,a))::acc) (n-1) b + strip_ty (([dummy_loc,na],a)::acc) (n-1) b | _ -> error "Cannot translate fix tactic: not enough products" in strip_ty [] n ty @@ -1059,8 +1059,8 @@ and pr_glob_match_rule env t = let typed_printers = (pr_glob_tactic_level, - pr_open_constr_env, - pr_open_lconstr_env, + pr_constr_env, + pr_lconstr_env, pr_lconstr_pattern, pr_evaluable_reference_env, pr_inductive, diff --git a/parsing/pptactic.mli b/parsing/pptactic.mli index 7fa33119d6..f84a2deb27 100644 --- a/parsing/pptactic.mli +++ b/parsing/pptactic.mli @@ -74,7 +74,7 @@ val pr_glob_extend: string -> glob_generic_argument list -> std_ppcmds val pr_extend : - (open_constr -> std_ppcmds) -> (open_constr -> std_ppcmds) -> + (Term.constr -> std_ppcmds) -> (Term.constr -> std_ppcmds) -> (tolerability -> glob_tactic_expr -> std_ppcmds) -> int -> string -> typed_generic_argument list -> std_ppcmds diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 64f9403a1c..ab6c42035f 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -36,7 +36,7 @@ let pr_with_bindings prc prlc (c,bl) = let pr_fun_ind_using prc prlc _ opt_c = match opt_c with | None -> mt () - | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc (p,b)) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings prc prlc b) (* Duplication of printing functions because "'a with_bindings" is (internally) not uniform in 'a: indeed constr_with_bindings at the @@ -46,12 +46,12 @@ let pr_fun_ind_using prc prlc _ opt_c = let pr_with_bindings_typed prc prlc (c,bl) = prc c ++ - hv 0 (pr_bindings (fun c -> prc (snd c)) (fun c -> prlc (snd c)) bl) + hv 0 (pr_bindings prc prlc bl) let pr_fun_ind_using_typed prc prlc _ opt_c = match opt_c with | None -> mt () - | Some (p,b) -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc (p,b)) + | Some b -> spc () ++ hov 2 (str "using" ++ spc () ++ pr_with_bindings_typed prc prlc b.Evd.it) ARGUMENT EXTEND fun_ind_using @@ -96,7 +96,7 @@ TACTIC EXTEND newfunind | [c] -> c | c::cl -> applist(c,cl) in - functional_induction true c princl pat ] + Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ] END (***** debug only ***) TACTIC EXTEND snewfunind @@ -107,7 +107,7 @@ TACTIC EXTEND snewfunind | [c] -> c | c::cl -> applist(c,cl) in - functional_induction false c princl pat ] + Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ] END diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index ca608ec0ba..8c22265d66 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -24,13 +24,13 @@ open Hiddentac let pr_binding prc = function - | loc, Rawterm.NamedHyp id, (_,c) -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) - | loc, Rawterm.AnonHyp n, (_,c) -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.NamedHyp id, c -> hov 1 (Ppconstr.pr_id id ++ str " := " ++ Pp.cut () ++ prc c) + | loc, Rawterm.AnonHyp n, c -> hov 1 (int n ++ str " := " ++ Pp.cut () ++ prc c) let pr_bindings prc prlc = function | Rawterm.ImplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ - Util.prlist_with_sep spc (fun (_,c) -> prc c) l + Util.prlist_with_sep spc prc l | Rawterm.ExplicitBindings l -> brk (1,1) ++ str "with" ++ brk (1,1) ++ Util.prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l @@ -424,7 +424,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,inj_open p)::bindings,id::avoid + (dummy_loc,Rawterm.NamedHyp id,p)::bindings,id::avoid ) ([],pf_ids_of_hyps g) princ_infos.params @@ -434,7 +434,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem List.rev (fst (List.fold_left2 (fun (bindings,avoid) (x,_,_) p -> let id = Namegen.next_ident_away (Nameops.out_name x) avoid in - (dummy_loc,Rawterm.NamedHyp id,inj_open (nf_zeta p))::bindings,id::avoid) + (dummy_loc,Rawterm.NamedHyp id,(nf_zeta p))::bindings,id::avoid) ([],avoid) princ_infos.predicates (lemmas))) diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 02d70da74c..60616845be 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -1224,7 +1224,7 @@ let replay_history tactic_normalisation = (clear [aux]); (intros_using [id]); (loop l) ]; - tclTHEN (exists_tac (inj_open eq1)) reflexivity ] + tclTHEN (exists_tac eq1) reflexivity ] | SPLIT_INEQ(e,(e1,act1),(e2,act2)) :: l -> let id1 = new_identifier () and id2 = new_identifier () in diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml index 0beb1e1aea..476724ba6d 100644 --- a/plugins/subtac/subtac_utils.ml +++ b/plugins/subtac/subtac_utils.ml @@ -248,7 +248,7 @@ let build_dependent_sum l = ([intros; (tclTHENSEQ [constructor_tac false (Some 1) 1 - (Rawterm.ImplicitBindings [inj_open (mkVar n)]); + (Rawterm.ImplicitBindings [mkVar n]); cont]); ]))) in diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index a65cc24ff6..99e3c4e1d6 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -354,7 +354,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv (***************************************************************) (* Bindings *) -type arg_bindings = open_constr explicit_bindings +type arg_bindings = constr explicit_bindings (* [clenv_independent clenv] * returns a list of metavariables which appear in the term cval, @@ -411,12 +411,11 @@ let clenv_unify_binding_type clenv c t u = | e when precatchable_exception e -> TypeNotProcessed, clenv, c -let clenv_assign_binding clenv k (sigma,c) = +let clenv_assign_binding clenv k c = let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in - let clenv' = { clenv with evd = Evd.merge clenv.evd sigma} in - let c_typ = nf_betaiota clenv'.evd (clenv_get_type_of clenv' c) in - let status,clenv'',c = clenv_unify_binding_type clenv' c c_typ k_typ in - { clenv'' with evd = meta_assign k (c,(UserGiven,status)) clenv''.evd } + let c_typ = nf_betaiota clenv.evd (clenv_get_type_of clenv c) in + let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in + { clenv' with evd = meta_assign k (c,(UserGiven,status)) clenv'.evd } let clenv_match_args bl clenv = if bl = [] then @@ -425,13 +424,13 @@ let clenv_match_args bl clenv = let mvs = clenv_independent clenv in check_bindings bl; List.fold_left - (fun clenv (loc,b,(sigma,c as sc)) -> + (fun clenv (loc,b,c) -> let k = meta_of_binder clenv loc mvs b in if meta_defined clenv.evd k then if eq_constr (fst (meta_fvalue clenv.evd k)).rebus c then clenv else error_already_defined b else - clenv_assign_binding clenv k sc) + clenv_assign_binding clenv k c) clenv bl let clenv_constrain_last_binding c clenv = @@ -439,7 +438,7 @@ let clenv_constrain_last_binding c clenv = let k = try list_last all_mvs with Failure _ -> anomaly "clenv_constrain_with_bindings" in - clenv_assign_binding clenv k (Evd.empty,c) + clenv_assign_binding clenv k c let clenv_constrain_dep_args hyps_only bl clenv = if bl = [] then diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 5571efbc57..4f7ac40920 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -86,7 +86,7 @@ val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv (***************************************************************) (* Bindings *) -type arg_bindings = open_constr explicit_bindings +type arg_bindings = constr explicit_bindings (* bindings where the key is the position in the template of the clenv (dependent or not). Positions can be negative meaning to @@ -107,10 +107,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (* the optional int tells how many prods of the lemma have to be used *) (* use all of them if None *) val make_clenv_binding_apply : - evar_info sigma -> int option -> constr * constr -> open_constr bindings -> + evar_info sigma -> int option -> constr * constr -> constr bindings -> clausenv val make_clenv_binding : - evar_info sigma -> constr * constr -> open_constr bindings -> clausenv + evar_info sigma -> constr * constr -> constr bindings -> clausenv (* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where [lmetas] is a list of metas to be applied to a proof of [t] so that diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index dc1784f40c..a33c81b097 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -1241,6 +1241,15 @@ let check_evars env initial_sigma evd c = | _ -> iter_constr proc_rec c in proc_rec c +(* This returns the evars of [sigma] that are not in [sigma0] and + [sigma] minus these evars *) + +let subtract_evars sigma0 sigma = + Evd.fold (fun evk ev (sigma,sigma' as acc) -> + if Evd.mem sigma0 evk || Evd.mem sigma' evk then acc else + (Evd.remove sigma evk,Evd.add sigma' evk ev)) + sigma (sigma,Evd.empty) + (* Operations on value/type constraints *) type type_constraint_type = (int * int) option * constr @@ -1376,4 +1385,3 @@ let pr_tycon_type env (abs, t) = let pr_tycon env = function None -> str "None" | Some t -> pr_tycon_type env t - diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 4bfef79983..205ca8bd64 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -90,6 +90,7 @@ val solve_simple_eqn : new unresolved evar remains in [c] *) val check_evars : env -> evar_map -> evar_map -> constr -> unit +val subtract_evars : evar_map -> evar_map -> evar_map * evar_map val define_evar_as_product : evar_map -> existential -> evar_map * types val define_evar_as_lambda : evar_map -> existential -> evar_map * types val define_evar_as_sort : evar_map -> existential -> evar_map * sorts diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index d5bc868894..b741c9a413 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -703,9 +703,9 @@ let plain_instance s c = empty map). *) -let instance s c = +let instance sigma s c = (* if s = [] then c else *) - local_strong whd_betaiota Evd.empty (plain_instance s c) + local_strong whd_betaiota sigma (plain_instance s c) (* pseudo-reduction rule: * [hnf_prod_app env s (Prod(_,B)) N --> B[N] @@ -902,21 +902,21 @@ let meta_value evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> - instance + instance evd (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) b.rebus | None -> mkMeta mv in valrec mv -let meta_instance env b = +let meta_instance sigma b = let c_sigma = List.map - (fun mv -> (mv,meta_value env mv)) (Metaset.elements b.freemetas) + (fun mv -> (mv,meta_value sigma mv)) (Metaset.elements b.freemetas) in - if c_sigma = [] then b.rebus else instance c_sigma b.rebus + if c_sigma = [] then b.rebus else instance sigma c_sigma b.rebus -let nf_meta env c = meta_instance env (mk_freelisted c) +let nf_meta sigma c = meta_instance sigma (mk_freelisted c) (* Instantiate metas that create beta/iota redexes *) @@ -924,7 +924,7 @@ let meta_value evd mv = let rec valrec mv = match meta_opt_fvalue evd mv with | Some (b,_) -> - instance + instance evd (List.map (fun mv' -> (mv',valrec mv')) (Metaset.elements b.freemetas)) b.rebus | None -> mkMeta mv diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 9e5ced8a28..0b9e69d95b 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -210,7 +210,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr val whd_meta : (metavariable * constr) list -> constr -> constr val plain_instance : (metavariable * constr) list -> constr -> constr -val instance : (metavariable * constr) list -> constr -> constr +val instance :evar_map -> (metavariable * constr) list -> constr -> constr val head_unfold_under_prod : transparent_state -> reduction_function (*s Heuristic for Conversion with Evar *) diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index ff7cf5acc3..9bc818e861 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -78,6 +78,7 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls = clenv.env clenv.evd else clenv.evd in + let clenv = { clenv with evd = evd' } in tclTHEN (tclEVARS evd') (refine (clenv_cast_meta clenv (clenv_value clenv))) diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml index e7bca648c8..bc29534081 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.ml @@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -74,7 +74,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -85,7 +85,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli index 5fa4a44ef7..b5c4a234d1 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.mli @@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation) and validation = (proof_tree list -> proof_tree) and tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -109,7 +109,7 @@ and tactic_expr = Tacexpr.gen_tactic_expr and atomic_tactic_expr = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, @@ -120,7 +120,7 @@ and atomic_tactic_expr = Tacexpr.gen_atomic_tactic_expr and tactic_arg = - (open_constr, + (constr, constr_pattern, evaluable_global_reference, inductive, diff --git a/proofs/refiner.mli b/proofs/refiner.mli index ff902d880b..e853c12b7c 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -185,6 +185,11 @@ val then_tactic_list : tactic_list -> tactic_list -> tactic_list val tactic_list_tactic : tactic_list -> tactic val goal_goal_list : 'a sigma -> 'a list sigma +(* [tclWITHHOLES solve_holes tac (sigma,c)] applies [tac] to [c] which + may have unresolved holes; if [solve_holes] these holes must be + resolved after application of the tactic; [sigma] must be an + extension of the sigma of the goal *) +val tclWITHHOLES : bool -> ('a -> tactic) -> evar_map -> 'a -> tactic (*s Functions for handling the state of the proof editor. *) diff --git a/tactics/auto.ml b/tactics/auto.ml index 6a08bda87a..59791f011d 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -756,7 +756,7 @@ let unify_resolve_nodelta (c,clenv) gl = let unify_resolve flags (c,clenv) gl = let clenv' = connect_clenv gl clenv in let _ = clenv_unique_resolver false ~flags clenv' gl in - h_apply true false [dummy_loc,(inj_open c,NoBindings)] gl + h_apply true false [dummy_loc,(c,NoBindings)] gl let unify_resolve_gen = function | None -> unify_resolve_nodelta @@ -932,7 +932,7 @@ let gen_trivial lems = function let inj_open c = (Evd.empty,c) let h_trivial lems l = - Refiner.abstract_tactic (TacTrivial (List.map inj_open lems,l)) + Refiner.abstract_tactic (TacTrivial (lems,l)) (gen_trivial lems l) (**************************************************************************) @@ -1062,7 +1062,7 @@ 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,List.map inj_open lems,l)) + Refiner.abstract_tactic (TacAuto (inj_or_var n,lems,l)) (gen_auto n lems l) (**************************************************************************) @@ -1091,7 +1091,7 @@ let dauto (n,p) lems = let default_dauto = dauto (None,None) [] let h_dauto (n,p) lems = - Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,List.map inj_open lems)) + Refiner.abstract_tactic (TacDAuto (inj_or_var n,p,lems)) (dauto (n,p) lems) (***************************************) diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 71817b2c70..9c38362a8c 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -17,4 +17,4 @@ open Genarg (*i*) val absurd : constr -> tactic -val contradiction : constr with_ebindings option -> tactic +val contradiction : constr with_bindings option -> tactic diff --git a/tactics/elim.ml b/tactics/elim.ml index 935431bf93..cac200f58d 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -139,13 +139,13 @@ let decompose_or c gls = let inj_open c = (Evd.empty,c) let h_decompose l c = - Refiner.abstract_tactic (TacDecompose (l,inj_open c)) (decompose_these c l) + Refiner.abstract_tactic (TacDecompose (l,c)) (decompose_these c l) let h_decompose_or c = - Refiner.abstract_tactic (TacDecomposeOr (inj_open c)) (decompose_or c) + Refiner.abstract_tactic (TacDecomposeOr c) (decompose_or c) let h_decompose_and c = - Refiner.abstract_tactic (TacDecomposeAnd (inj_open c)) (decompose_and c) + Refiner.abstract_tactic (TacDecomposeAnd c) (decompose_and c) (* The tactic Double performs a double induction *) diff --git a/tactics/equality.ml b/tactics/equality.ml index a82f506715..62581d74b2 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -240,19 +240,18 @@ let rewrite_side_tac tac sidetac = side_tac tac (Option.map fst sidetac) (* Main function for dispatching which kind of rewriting it is about *) let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac - ((c,l) : open_constr with_bindings) with_evars gl = + ((c,l) : constr with_bindings) with_evars gl = if occs <> all_occurrences then ( rewrite_side_tac (!general_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac gl) else let env = pf_env gl in - let sigma, c' = c in - let sigma = Evd.merge sigma (project gl) in - let ctype = get_type_of env sigma c' in + let sigma = project gl in + let ctype = get_type_of env sigma c in let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in match match_with_equality_type t with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) let lft2rgt = adjust_rewriting_direction args lft2rgt in - leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' (it_mkProd_or_LetIn t rels) + leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t rels) l with_evars dep_proof_ok gl hdcncl | None -> try @@ -264,7 +263,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs dep_proof_ok ?tac match match_with_equality_type t' with | Some (hdcncl,args) -> let lft2rgt = adjust_rewriting_direction args lft2rgt in - leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c' + leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars dep_proof_ok gl hdcncl | None -> raise e (* error "The provided term does not end with an equality or a declared rewrite relation." *) @@ -273,7 +272,7 @@ let general_rewrite_ebindings = general_rewrite_ebindings_clause None let general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,bl) = - general_rewrite_ebindings_clause None l2r occs dep_proof_ok ?tac (inj_open c,inj_ebindings bl) + general_rewrite_ebindings_clause None l2r occs dep_proof_ok ?tac (c,bl) let general_rewrite l2r occs dep_proof_ok ?tac c = general_rewrite_bindings l2r occs dep_proof_ok ?tac (c,NoBindings) false @@ -282,10 +281,10 @@ let general_rewrite_ebindings_in l2r occs dep_proof_ok ?tac id = general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac let general_rewrite_bindings_in l2r occs dep_proof_ok ?tac id (c,bl) = - general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (inj_open c,inj_ebindings bl) + general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,bl) let general_rewrite_in l2r occs dep_proof_ok ?tac id c = - general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (inj_open c,NoBindings) + general_rewrite_ebindings_clause (Some id) l2r occs dep_proof_ok ?tac (c,NoBindings) let general_multi_rewrite l2r with_evars ?tac c cl = let occs_of = on_snd (List.fold_left @@ -321,7 +320,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl = let do_hyps gl = (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) let ids = - let ids_in_c = Environ.global_vars_set (Global.env()) (snd (fst c)) in + let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in Idset.fold (fun id l -> list_remove id l) ids_in_c (pf_ids_of_hyps gl) in do_hyps_atleastonce ids gl in @@ -331,7 +330,10 @@ let general_multi_rewrite l2r with_evars ?tac c cl = do_hyps let general_multi_multi_rewrite with_evars l cl tac = - let do1 l2r c = general_multi_rewrite l2r with_evars ?tac c cl in + let do1 l2r c gl = + Refiner.tclWITHHOLES with_evars + (general_multi_rewrite l2r with_evars ?tac c.it) + (Evd.merge (project gl) c.sigma) cl gl in let rec doN l2r c = function | Precisely n when n <= 0 -> tclIDTAC | Precisely 1 -> do1 l2r c @@ -372,7 +374,7 @@ let multi_replace clause c2 c1 unsafe try_prove_eq_opt gl = tclTHENS (assert_as false None eq) [onLastHypId (fun id -> tclTHEN - (tclTRY (general_multi_rewrite false false (inj_open (mkVar id),NoBindings) clause)) + (tclTRY (general_multi_rewrite false false (mkVar id,NoBindings) clause)) (clear [id])); tclFIRST [assumption; @@ -1398,7 +1400,7 @@ let rewrite_multi_assumption_cond cond_eq_term cl gl = begin try let dir = cond_eq_term t gl in - general_multi_rewrite dir false (inj_open (mkVar id),NoBindings) cl gl + general_multi_rewrite dir false (mkVar id,NoBindings) cl gl with | Failure _ | UserError _ -> arec rest end in diff --git a/tactics/equality.mli b/tactics/equality.mli index b88f376ee2..9986d230bb 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -52,12 +52,12 @@ val rewriteRL : ?tac:(tactic * conditions) -> constr -> tactic val register_general_rewrite_clause : (identifier option -> orientation -> - occurrences -> open_constr with_bindings -> new_goals:constr list -> tactic) -> unit -val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> open_constr option) -> unit + occurrences -> constr with_bindings -> new_goals:constr list -> tactic) -> unit +val register_is_applied_rewrite_relation : (env -> evar_map -> rel_context -> constr -> constr option) -> unit val general_rewrite_ebindings_clause : identifier option -> orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) -> - open_constr with_bindings -> evars_flag -> tactic + constr with_bindings -> evars_flag -> tactic val general_rewrite_bindings_in : orientation -> occurrences -> dep_proof_flag -> ?tac:(tactic * conditions) -> @@ -67,9 +67,9 @@ val general_rewrite_in : identifier -> constr -> evars_flag -> tactic val general_multi_rewrite : - orientation -> evars_flag -> ?tac:(tactic * conditions) -> open_constr with_bindings -> clause -> tactic + orientation -> evars_flag -> ?tac:(tactic * conditions) -> constr with_bindings -> clause -> tactic val general_multi_multi_rewrite : - evars_flag -> (bool * multi * open_constr with_bindings) list -> clause -> + evars_flag -> (bool * multi * constr with_bindings sigma) list -> clause -> (tactic * conditions) option -> tactic val replace_in_clause_maybe_by : constr -> constr -> clause -> tactic option -> tactic @@ -78,22 +78,22 @@ val replace_in : identifier -> constr -> constr -> tactic val replace_by : constr -> constr -> tactic -> tactic val replace_in_by : identifier -> constr -> constr -> tactic -> tactic -val discr : evars_flag -> constr with_ebindings -> tactic +val discr : evars_flag -> constr with_bindings -> tactic val discrConcl : tactic val discrClause : evars_flag -> clause -> tactic val discrHyp : identifier -> tactic val discrEverywhere : evars_flag -> tactic val discr_tac : evars_flag -> - constr with_ebindings induction_arg option -> tactic + constr with_bindings induction_arg option -> tactic val inj : intro_pattern_expr located list -> evars_flag -> - constr with_ebindings -> tactic + constr with_bindings -> tactic val injClause : intro_pattern_expr located list -> evars_flag -> - constr with_ebindings induction_arg option -> tactic + constr with_bindings induction_arg option -> tactic val injHyp : identifier -> tactic val injConcl : tactic -val dEq : evars_flag -> constr with_ebindings induction_arg option -> tactic -val dEqThen : evars_flag -> (int -> tactic) -> constr with_ebindings induction_arg option -> tactic +val dEq : evars_flag -> constr with_bindings induction_arg option -> tactic +val dEqThen : evars_flag -> (int -> tactic) -> constr with_bindings induction_arg option -> tactic val make_iterated_tuple : env -> evar_map -> constr -> (constr * types) -> constr * constr * constr diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index b5d7d10d09..c0043db067 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -21,6 +21,7 @@ open Rawterm open Tactics open Util open Termops +open Evd (* Equality *) open Equality @@ -54,9 +55,13 @@ let induction_arg_of_quantified_hyp = function ElimOnAnonHyp and not as a "constr", and "id" is interpreted as a ElimOnIdent and not as "constr" *) +let elimOnConstrWithHoles tac with_evars c = + Refiner.tclWITHHOLES with_evars (tac with_evars) + c.sigma (Some (ElimOnConstr c.it)) + TACTIC EXTEND simplify_eq_main | [ "simplify_eq" constr_with_bindings(c) ] -> - [ dEq false (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles dEq false c ] END TACTIC EXTEND simplify_eq [ "simplify_eq" ] -> [ dEq false None ] @@ -65,7 +70,7 @@ TACTIC EXTEND simplify_eq END TACTIC EXTEND esimplify_eq_main | [ "esimplify_eq" constr_with_bindings(c) ] -> - [ dEq true (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles dEq true c ] END TACTIC EXTEND esimplify_eq | [ "esimplify_eq" ] -> [ dEq true None ] @@ -75,7 +80,7 @@ END TACTIC EXTEND discriminate_main | [ "discriminate" constr_with_bindings(c) ] -> - [ discr_tac false (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles discr_tac false c ] END TACTIC EXTEND discriminate | [ "discriminate" ] -> [ discr_tac false None ] @@ -84,7 +89,7 @@ TACTIC EXTEND discriminate END TACTIC EXTEND ediscriminate_main | [ "ediscriminate" constr_with_bindings(c) ] -> - [ discr_tac true (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles discr_tac true c ] END TACTIC EXTEND ediscriminate | [ "ediscriminate" ] -> [ discr_tac true None ] @@ -92,11 +97,12 @@ TACTIC EXTEND ediscriminate [ discr_tac true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_discrHyp id = h_discriminate_main (Term.mkVar id,NoBindings) +let h_discrHyp id gl = + h_discriminate_main {it = Term.mkVar id,NoBindings; sigma = Refiner.project gl} gl TACTIC EXTEND injection_main | [ "injection" constr_with_bindings(c) ] -> - [ injClause [] false (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles (injClause []) false c ] END TACTIC EXTEND injection | [ "injection" ] -> [ injClause [] false None ] @@ -105,7 +111,7 @@ TACTIC EXTEND injection END TACTIC EXTEND einjection_main | [ "einjection" constr_with_bindings(c) ] -> - [ injClause [] true (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles (injClause []) true c ] END TACTIC EXTEND einjection | [ "einjection" ] -> [ injClause [] true None ] @@ -113,7 +119,7 @@ TACTIC EXTEND einjection END TACTIC EXTEND injection_as_main | [ "injection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> - [ injClause ipat false (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles (injClause ipat) false c ] END TACTIC EXTEND injection_as | [ "injection" "as" simple_intropattern_list(ipat)] -> @@ -123,7 +129,7 @@ TACTIC EXTEND injection_as END TACTIC EXTEND einjection_as_main | [ "einjection" constr_with_bindings(c) "as" simple_intropattern_list(ipat)] -> - [ injClause ipat true (Some (ElimOnConstr c)) ] + [ elimOnConstrWithHoles (injClause ipat) true c ] END TACTIC EXTEND einjection_as | [ "einjection" "as" simple_intropattern_list(ipat)] -> @@ -132,7 +138,8 @@ TACTIC EXTEND einjection_as [ injClause ipat true (Some (induction_arg_of_quantified_hyp h)) ] END -let h_injHyp id = h_injection_main (Term.mkVar id,NoBindings) +let h_injHyp id gl = + h_injection_main { it = Term.mkVar id,NoBindings; sigma = Refiner.project gl } gl TACTIC EXTEND dependent_rewrite | [ "dependent" "rewrite" orient(b) constr(c) ] -> [ rewriteInConcl b c ] @@ -153,8 +160,13 @@ TACTIC EXTEND absurd [ "absurd" constr(c) ] -> [ absurd c ] END +let onSomeWithHoles tac = function + | None -> tac None + | Some c -> Refiner.tclWITHHOLES false tac c.sigma (Some c.it) + TACTIC EXTEND contradiction - [ "contradiction" constr_with_bindings_opt(c) ] -> [ contradiction c ] + [ "contradiction" constr_with_bindings_opt(c) ] -> + [ onSomeWithHoles contradiction c ] END (* AutoRewrite *) @@ -194,9 +206,10 @@ END open Extraargs -let rewrite_star clause orient occs c (tac : glob_tactic_expr option) = +let rewrite_star clause orient occs (sigma,c) (tac : glob_tactic_expr option) = let tac' = Option.map (fun t -> Tacinterp.eval_tactic t, FirstSolved) tac in - general_rewrite_ebindings_clause clause orient occs ?tac:tac' true (c,NoBindings) true + Refiner. tclWITHHOLES false + (general_rewrite_ebindings_clause clause orient occs ?tac:tac' true (c,NoBindings)) sigma true let occurrences_of = function | n::_ as nl when n < 0 -> (false,List.map abs nl) diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli index 7a5314c367..82006f6026 100644 --- a/tactics/extratactics.mli +++ b/tactics/extratactics.mli @@ -15,3 +15,4 @@ val h_injHyp : Names.identifier -> tactic val refine_tac : Evd.open_constr -> tactic +val onSomeWithHoles : ('a option -> tactic) -> 'a Evd.sigma option -> tactic diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index d642a38dbc..ba17ac30cd 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -19,26 +19,17 @@ open Tacexpr 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_wb 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 = abstract_tactic (TacIntroMove (x, y)) (intro_move x y) let h_intro x = h_intro_move (Some x) no_move 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 (inj_open c)) (exact_check c) +let h_exact c = abstract_tactic (TacExact c) (exact_check c) let h_exact_no_check c = - abstract_tactic (TacExactNoCheck (inj_open c)) (exact_no_check c) + abstract_tactic (TacExactNoCheck c) (exact_no_check c) let h_vm_cast_no_check c = - abstract_tactic (TacVmCastNoCheck (inj_open c)) (vm_cast_no_check c) + abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c) let h_apply simple ev cb = abstract_tactic (TacApply (simple,ev,List.map snd cb,None)) (apply_with_ebindings_gen simple ev cb) @@ -46,35 +37,35 @@ let h_apply_in simple ev cb (id,ipat as inhyp) = abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp)) (apply_in simple ev id cb ipat) let h_elim ev cb cbo = - abstract_tactic (TacElim (ev,inj_open_wb cb,Option.map inj_open_wb cbo)) + abstract_tactic (TacElim (ev,cb,cbo)) (elim ev cb cbo) -let h_elim_type c = abstract_tactic (TacElimType (inj_open c)) (elim_type c) -let h_case ev cb = abstract_tactic (TacCase (ev,inj_open_wb cb)) (general_case_analysis ev cb) -let h_case_type c = abstract_tactic (TacCaseType (inj_open c)) (case_type c) +let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c) +let h_case ev cb = abstract_tactic (TacCase (ev,cb)) (general_case_analysis ev cb) +let h_case_type c = abstract_tactic (TacCaseType c) (case_type c) let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n) let h_mutual_fix b id n l = abstract_tactic - (TacMutualFix (b,id,n,List.map (fun (id,n,c) -> (id,n,inj_open c)) l)) + (TacMutualFix (b,id,n,l)) (mutual_fix id n l 0) let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido) let h_mutual_cofix b id l = abstract_tactic - (TacMutualCofix (b,id,List.map (fun (id,c) -> (id,inj_open c)) l)) + (TacMutualCofix (b,id,l)) (mutual_cofix id l 0) -let h_cut c = abstract_tactic (TacCut (inj_open c)) (cut c) +let h_cut c = abstract_tactic (TacCut c) (cut c) let h_generalize_gen cl = - abstract_tactic (TacGeneralize (List.map (on_fst inj_occ) cl)) + abstract_tactic (TacGeneralize cl) (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) let h_generalize cl = h_generalize_gen (List.map (fun c -> ((all_occurrences_expr,c),Names.Anonymous)) cl) let h_generalize_dep c = - abstract_tactic (TacGeneralizeDep (inj_open c))(generalize_dep c) + abstract_tactic (TacGeneralizeDep c) (generalize_dep c) let h_let_tac b na c cl = let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in - abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl) + abstract_tactic (TacLetTac (na,c,cl,b)) (letin_tac with_eq na c None cl) (* Derived basic tactics *) let h_simple_induction_destruct isrec h = @@ -83,15 +74,14 @@ let h_simple_induction_destruct isrec h = let h_simple_induction = h_simple_induction_destruct true let h_simple_destruct = h_simple_induction_destruct false -let h_induction_destruct isrec ev (l,cl) = - abstract_tactic (TacInductionDestruct (isrec,ev,(List.map (fun (c,e,idl) -> - List.map inj_ia c,Option.map inj_open_wb e,idl) l,cl))) - (induction_destruct ev isrec (l,cl)) +let h_induction_destruct isrec ev lcl = + abstract_tactic (TacInductionDestruct (isrec,ev,lcl)) + (induction_destruct ev isrec lcl) let h_new_induction ev c e idl cl = h_induction_destruct ev true ([c,e,idl],cl) let h_new_destruct ev c e idl cl = h_induction_destruct ev false ([c,e,idl],cl) -let h_specialize n d = abstract_tactic (TacSpecialize (n,inj_open_wb d)) (specialize n d) -let h_lapply c = abstract_tactic (TacLApply (inj_open c)) (cut_and_apply c) +let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d) +let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) (* Context management *) let h_clear b l = abstract_tactic (TacClear (b,l)) @@ -113,26 +103,27 @@ let h_any_constructor t = *) let h_constructor ev n l = abstract_tactic (TacConstructor(ev,AI n,l))(constructor_tac ev None n l) -let h_one_constructor n = h_constructor false n NoBindings +let h_one_constructor n = + abstract_tactic (TacConstructor(false,AI n,NoBindings)) (one_constructor n NoBindings) let h_simplest_left = h_left false NoBindings let h_simplest_right = h_right false NoBindings (* Conversion *) let h_reduce r cl = - abstract_tactic (TacReduce (inj_red_expr r,cl)) (reduce r cl) + abstract_tactic (TacReduce (r,cl)) (reduce r cl) let h_change oc c cl = - abstract_tactic (TacChange (Option.map inj_occ oc,inj_open c,cl)) + abstract_tactic (TacChange (oc,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 (Option.map inj_open c)) + abstract_tactic (TacTransitivity c) (intros_transitivity c) -let h_simplest_apply c = h_apply false false [dummy_loc,(inj_open c,NoBindings)] -let h_simplest_eapply c = h_apply false true [dummy_loc,(inj_open c,NoBindings)] +let h_simplest_apply c = h_apply false false [dummy_loc,(c,NoBindings)] +let h_simplest_eapply c = h_apply false true [dummy_loc,(c,NoBindings)] let h_simplest_elim c = h_elim false (c,NoBindings) None let h_simplest_case c = h_case false (c,NoBindings) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 86a3376785..70eb8dfb30 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -38,15 +38,15 @@ val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic val h_apply : advanced_flag -> evars_flag -> - open_constr with_bindings located list -> tactic + constr with_bindings located list -> tactic val h_apply_in : advanced_flag -> evars_flag -> - open_constr with_bindings located list -> + constr with_bindings located list -> identifier * intro_pattern_expr located option -> tactic -val h_elim : evars_flag -> constr with_ebindings -> - constr with_ebindings option -> tactic +val h_elim : evars_flag -> constr with_bindings -> + constr with_bindings option -> tactic val h_elim_type : constr -> tactic -val h_case : evars_flag -> constr with_ebindings -> tactic +val h_case : evars_flag -> constr with_bindings -> tactic val h_case_type : constr -> tactic val h_mutual_fix : hidden_flag -> identifier -> int -> @@ -69,19 +69,19 @@ val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic val h_new_induction : evars_flag -> - constr with_ebindings induction_arg list -> constr with_ebindings option -> + constr with_bindings induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> Tacticals.clause option -> tactic val h_new_destruct : evars_flag -> - constr with_ebindings induction_arg list -> constr with_ebindings option -> + constr with_bindings induction_arg list -> constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> Tacticals.clause option -> tactic val h_induction_destruct : rec_flag -> evars_flag -> - (constr with_ebindings induction_arg list * constr with_ebindings option * + (constr with_bindings induction_arg list * constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) list * Tacticals.clause option -> tactic -val h_specialize : int option -> constr with_ebindings -> tactic +val h_specialize : int option -> constr with_bindings -> tactic val h_lapply : constr -> tactic (* Automation tactic : see Auto *) @@ -95,10 +95,10 @@ val h_rename : (identifier*identifier) list -> tactic val h_revert : identifier list -> tactic (* Constructors *) -val h_constructor : evars_flag -> int -> open_constr bindings -> tactic -val h_left : evars_flag -> open_constr bindings -> tactic -val h_right : evars_flag -> open_constr bindings -> tactic -val h_split : evars_flag -> open_constr bindings list -> tactic +val h_constructor : evars_flag -> int -> constr bindings -> tactic +val h_left : evars_flag -> constr bindings -> tactic +val h_right : evars_flag -> constr bindings -> tactic +val h_split : evars_flag -> constr bindings list -> tactic val h_one_constructor : int -> tactic val h_simplest_left : tactic diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index aea8c0ccf5..ce6abc93ec 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -158,7 +158,7 @@ let is_applied_rewrite_relation env sigma rels t = let evd, evar = Evarutil.new_evar sigma env' (new_Type ()) in let inst = mkApp (Lazy.force rewrite_relation_class, [| evar; mkApp (c, params) |]) in let _ = Typeclasses.resolve_one_typeclass env' evd inst in - Some (sigma, it_mkProd_or_LetIn t rels) + Some (it_mkProd_or_LetIn t rels) with _ -> None) | _ -> None @@ -759,6 +759,8 @@ module Strategies = choice tac (apply_lemma l l2r (false,[]))) fail cs + let inj_open c = (Evd.empty,c) + let old_hints (db : string) : strategy = let rules = Autorewrite.find_rewrites db in lemmas (List.map (fun hint -> (inj_open hint.Autorewrite.rew_lemma, hint.Autorewrite.rew_l2r)) rules) @@ -1378,17 +1380,16 @@ let unification_rewrite l2r c1 c2 cl car rel but gl = let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)} -let get_hyp gl evars (evm,c) clause l2r = +let get_hyp gl evars c clause l2r = let hi = decompose_applied_relation (pf_env gl) evars c l2r in let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl let general_rewrite_flags = { under_lambdas = false; on_morphisms = false } -let apply_lemma gl (evm,c) cl l2r occs = +let apply_lemma gl c cl l2r occs = let sigma = project gl in - let evars = Evd.merge sigma evm in - let hypinfo = ref (get_hyp gl evars (evm,c) cl l2r) in + let hypinfo = ref (get_hyp gl sigma c cl l2r) in let app = apply_rule hypinfo occs in let rec aux () = Strategies.choice app (subterm true general_rewrite_flags (fun env -> aux () env)) @@ -1397,7 +1398,10 @@ let apply_lemma gl (evm,c) cl l2r occs = let general_s_rewrite cl l2r occs (c,l) ~new_goals gl = let meta = Evarutil.new_meta() in let hypinfo, strat = apply_lemma gl c cl l2r occs in - try cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl gl + try + tclTHEN + (Refiner.tclEVARS hypinfo.cl.evd) + (cl_rewrite_clause_aux ~abs:hypinfo.abs strat meta cl) gl with Not_found -> let {l2r=l2r; c1=x; c2=y} = hypinfo in raise (Pretype_errors.PretypeError diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 13add4151f..8c5f85c213 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1169,18 +1169,19 @@ let coerce_to_ident fresh env = function destVar c | v -> raise (CannotCoerceTo "a fresh identifier") -let interp_ident_gen fresh ist gl id = - let env = pf_env gl in +let interp_ident_gen fresh ist env id = try try_interp_ltac_var (coerce_to_ident fresh env) ist (Some env) (dloc,id) with Not_found -> id let interp_ident = interp_ident_gen false let interp_fresh_ident = interp_ident_gen true +let pf_interp_ident id gl = interp_ident_gen false id (pf_env gl) +let pf_interp_fresh_ident id gl = interp_ident_gen true id (pf_env gl) (* Interprets an optional identifier which must be fresh *) -let interp_fresh_name ist gl = function +let interp_fresh_name ist env = function | Anonymous -> Anonymous - | Name id -> Name (interp_fresh_ident ist gl id) + | Name id -> Name (interp_fresh_ident ist env id) let coerce_to_intro_pattern env = function | VIntroPattern ipat -> ipat @@ -1367,7 +1368,7 @@ let rec extract_ids ids = function let default_fresh_id = id_of_string "H" -let interp_fresh_id ist gl l = +let interp_fresh_id ist env l = let ids = map_succeed (function ArgVar(_,id) -> id | _ -> failwith "") l in let avoid = (extract_ids ids ist.lfun) @ ist.avoid_ids in let id = @@ -1376,10 +1377,12 @@ let interp_fresh_id ist gl l = let s = String.concat "" (List.map (function | ArgArg s -> s - | ArgVar (_,id) -> string_of_id (interp_ident ist gl id)) l) in + | ArgVar (_,id) -> string_of_id (interp_ident ist env id)) l) in let s = if Lexer.is_keyword s then s^"0" else s in id_of_string s in - Tactics.fresh_id avoid id gl + Tactics.fresh_id_in_env avoid id env + +let pf_interp_fresh_id ist gl = interp_fresh_id ist (pf_env gl) (* To retype a list of key*constr with undefined key *) let retype_list sigma env lst = @@ -1446,7 +1449,7 @@ let solve_remaining_evars fail_evar use_classes env initial_sigma evd c = (* Side-effect *) !evdref,c -let interp_gen kind ist fail_evar use_classes sigma env (c,ce) = +let interp_gen kind ist fail_evar use_classes env sigma (c,ce) = let (ltacvars,unbndltacvars as vars),typs = extract_ltac_vars_data ist sigma env in let c = match ce with @@ -1465,90 +1468,58 @@ let interp_gen kind ist fail_evar use_classes sigma env (c,ce) = (evd,c) (* Interprets a constr; expects evars to be solved *) -let interp_constr_gen kind ist sigma env c = - snd (interp_gen kind ist true true sigma env c) +let interp_constr_gen kind ist env sigma c = + snd (interp_gen kind ist true true env sigma c) let interp_constr = interp_constr_gen (OfType None) let interp_type = interp_constr_gen IsType (* Interprets an open constr *) -let interp_open_constr_gen kind ist sigma env c = - interp_gen kind ist false false sigma env c +let interp_open_constr_gen kind ist = interp_gen kind ist false false let interp_open_constr ccl = interp_open_constr_gen (OfType ccl) (* Interprets a constr expression casted by the current goal *) let pf_interp_casted_constr ist gl c = - interp_constr_gen (OfType (Some (pf_concl gl))) ist (project gl) (pf_env gl) c - -(* Interprets an open constr expression *) -let pf_interp_open_constr casted ist gl cc = - let cl = if casted then Some (pf_concl gl) else None in - interp_open_constr cl ist (project gl) (pf_env gl) cc + interp_constr_gen (OfType (Some (pf_concl gl))) ist (pf_env gl) (project gl) c (* Interprets a constr expression *) let pf_interp_constr ist gl = - interp_constr ist (project gl) (pf_env gl) + interp_constr ist (pf_env gl) (project gl) let constr_list_of_VList env = function | VList l -> List.map (constr_of_value env) l | _ -> raise Not_found -let pf_interp_constr_in_compound_list inj_fun dest_fun interp_fun ist gl l = - let env = pf_env gl in - let try_expand_ltac_var x = +let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = + let try_expand_ltac_var sigma x = try match dest_fun x with - | RVar (_,id), _ -> - List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun)) + | RVar (_,id), _ -> + sigma, + List.map inj_fun (constr_list_of_VList env (List.assoc id ist.lfun)) | _ -> - raise Not_found + raise Not_found with Not_found -> (*all of dest_fun, List.assoc, constr_list_of_VList may raise Not_found*) - [interp_fun ist gl x] in - List.flatten (List.map try_expand_ltac_var l) + let sigma, c = interp_fun ist env sigma x in + sigma, [c] in + let sigma, l = list_fold_map try_expand_ltac_var sigma l in + sigma, List.flatten l -let pf_interp_constr_list = - pf_interp_constr_in_compound_list (fun x -> x) (fun x -> x) - (fun ist gl -> interp_constr ist (project gl) (pf_env gl)) - -(* -let pf_interp_constr_list_as_list ist gl (c,_ as x) = - match c with - | RVar (_,id) -> - (try constr_list_of_VList (pf_env gl) (List.assoc id ist.lfun) - with Not_found -> []) - | _ -> [interp_constr ist (project gl) (pf_env gl) x] - -let pf_interp_constr_list ist gl l = - List.flatten (List.map (pf_interp_constr_list_as_list ist gl) l) -*) +let interp_constr_list ist env sigma c = + snd (interp_constr_in_compound_list (fun x -> x) (fun x -> x) (fun ist env sigma c -> (Evd.empty, interp_constr ist env sigma c)) ist env sigma c) let inj_open c = (Evd.empty,c) -let pf_interp_open_constr_list = - pf_interp_constr_in_compound_list inj_open (fun x -> x) - (fun ist gl -> interp_open_constr None ist (project gl) (pf_env gl)) - -(* -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) -*) +let interp_open_constr_list = + interp_constr_in_compound_list (fun x -> x) (fun x -> x) + (interp_open_constr None) (* Interprets a type expression *) let pf_interp_type ist gl = - interp_type ist (project gl) (pf_env gl) + interp_type ist (pf_env gl) (project gl) (* Interprets a reduction expression *) let interp_unfold ist env (occs,qid) = @@ -1561,24 +1532,24 @@ let interp_pattern ist sigma env (occs,c) = (interp_occurrences ist occs, interp_constr ist sigma env c) let pf_interp_constr_with_occurrences ist gl = - interp_pattern ist (project gl) (pf_env gl) + interp_pattern ist (pf_env gl) (project gl) -let pf_interp_constr_with_occurrences_and_name_as_list = - pf_interp_constr_in_compound_list +let interp_constr_with_occurrences_and_name_as_list = + interp_constr_in_compound_list (fun c -> ((all_occurrences_expr,c),Anonymous)) (function ((occs,c),Anonymous) when occs = all_occurrences_expr -> c | _ -> raise Not_found) - (fun ist gl (occ_c,na) -> - (interp_pattern ist (project gl) (pf_env gl) occ_c, - interp_fresh_name ist gl na)) + (fun ist env sigma (occ_c,na) -> + sigma, (interp_pattern ist env sigma occ_c, + interp_fresh_name ist env na)) let interp_red_expr ist sigma env = function | Unfold l -> Unfold (List.map (interp_unfold ist env) l) - | Fold l -> Fold (List.map (interp_constr ist sigma env) l) + | Fold l -> Fold (List.map (interp_constr ist env sigma) l) | Cbv f -> Cbv (interp_flag ist env f) | Lazy f -> Lazy (interp_flag ist env f) - | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l) - | Simpl o -> Simpl (Option.map (interp_pattern ist sigma env) o) + | Pattern l -> Pattern (List.map (interp_pattern ist env sigma) l) + | Simpl o -> Simpl (Option.map (interp_pattern ist env sigma) o) | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl) @@ -1619,12 +1590,6 @@ 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 rec message_of_value = function | VVoid -> str "()" | VInteger n -> int n @@ -1661,7 +1626,7 @@ let rec interp_intro_pattern ist gl = function | loc, IntroIdentifier id -> loc, interp_intro_pattern_var loc ist (pf_env gl) id | loc, IntroFresh id -> - loc, IntroFresh (interp_fresh_ident ist gl id) + loc, IntroFresh (interp_fresh_ident ist (pf_env gl) id) | loc, (IntroWildcard | IntroAnonymous | IntroRewrite _ | IntroForthcoming _) as x -> x @@ -1717,37 +1682,53 @@ let interp_declared_or_quantified_hypothesis ist gl = function (coerce_to_decl_or_quant_hyp env) ist (Some env) (dloc,id) with Not_found -> NamedHyp id -let interp_binding ist gl (loc,b,c) = - (loc,interp_binding_name ist b,pf_interp_open_constr false ist gl c) - -let interp_bindings ist gl = function -| NoBindings -> NoBindings -| 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 interp_binding ist env sigma (loc,b,c) = + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (loc,interp_binding_name ist b,c) + +let interp_bindings ist env sigma = function +| NoBindings -> + sigma, NoBindings +| ImplicitBindings l -> + let sigma, l = interp_open_constr_list ist env sigma l in + sigma, ImplicitBindings l +| ExplicitBindings l -> + let sigma, l = list_fold_map (interp_binding ist env) sigma l in + sigma, ExplicitBindings l + +let interp_constr_with_bindings ist env sigma (c,bl) = + let sigma, bl = interp_bindings ist env sigma bl in + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (c,bl) + +let interp_open_constr_with_bindings ist env sigma (c,bl) = + let sigma, bl = interp_bindings ist env sigma bl in + let sigma, c = interp_open_constr None ist env sigma c in + sigma, (c, bl) let loc_of_bindings = function | NoBindings -> dummy_loc | ImplicitBindings l -> loc_of_rawconstr (fst (list_last l)) | ExplicitBindings l -> pi1 (list_last l) -let interp_open_constr_with_bindings_loc ist gl ((c,_),bl as cb) = +let interp_open_constr_with_bindings_loc ist env sigma ((c,_),bl as cb) = let loc1 = loc_of_rawconstr c in let loc2 = loc_of_bindings bl in let loc = if loc2 = dummy_loc then loc1 else join_loc loc1 loc2 in - (loc,interp_open_constr_with_bindings ist gl cb) + let sigma, cb = interp_open_constr_with_bindings ist env sigma cb in + sigma, (loc,cb) -let interp_induction_arg ist gl = function - | ElimOnConstr c -> ElimOnConstr (interp_constr_with_bindings ist gl c) - | ElimOnAnonHyp n as x -> x +let interp_induction_arg ist gl sigma arg = + let env = pf_env gl in + match arg with + | ElimOnConstr c -> + let sigma, c = interp_constr_with_bindings ist env sigma c in + sigma, ElimOnConstr c + | ElimOnAnonHyp n as x -> sigma, x | ElimOnIdent (loc,id) -> try - match List.assoc id ist.lfun with + sigma, + match List.assoc id ist.lfun with | VInteger n -> ElimOnAnonHyp n | VIntroPattern (IntroIdentifier id) -> ElimOnIdent (loc,id) | VConstr c -> ElimOnConstr (c,NoBindings) @@ -1756,15 +1737,18 @@ let interp_induction_arg ist gl = function strbrk " neither to a quantified hypothesis nor to a term.") with Not_found -> (* Interactive mode *) - if Tactics.is_quantified_hypothesis id gl then ElimOnIdent (loc,id) - else ElimOnConstr - (pf_interp_constr ist gl (RVar (loc,id),Some (CRef (Ident (loc,id)))), - NoBindings) + if Tactics.is_quantified_hypothesis id gl then + sigma, ElimOnIdent (loc,id) + else + let c = interp_constr ist env sigma (RVar (loc,id),Some (CRef (Ident (loc,id)))) in + sigma, ElimOnConstr (c,NoBindings) 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) +let pack_sigma (sigma,c) = {it=c;sigma=sigma} + (* Interprets an l-tac expression into a value *) let rec val_interp ist gl (tac:glob_tactic_expr) = @@ -1802,7 +1786,7 @@ and eval_tactic ist = function | TacProgress tac -> tclPROGRESS (interp_tactic ist tac) | TacAbstract (tac,ido) -> fun gl -> Tactics.tclABSTRACT - (Option.map (interp_ident ist gl) ido) (interp_tactic ist tac) gl + (Option.map (pf_interp_ident ist gl) ido) (interp_tactic ist tac) gl | TacThen (t1,tf,t,tl) -> tclTHENS3PARTS (interp_tactic ist t1) (Array.map (interp_tactic ist) tf) (interp_tactic ist t) (Array.map (interp_tactic ist) tl) @@ -1859,7 +1843,7 @@ and interp_tacarg ist gl = function | TacExternal (loc,com,req,la) -> interp_external loc ist gl com req (List.map (interp_tacarg ist gl) la) | TacFreshId l -> - let id = interp_fresh_id ist gl l in + let id = pf_interp_fresh_id ist gl l in VIntroPattern (IntroIdentifier id) | Tacexp t -> val_interp ist gl t | TacDynamic(_,t) -> @@ -2054,7 +2038,7 @@ and interp_genarg ist gl x = (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x)) | IdentArgType b -> in_gen (wit_ident_gen b) - (interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)) + (pf_interp_fresh_ident ist gl (out_gen (globwit_ident_gen b) x)) | VarArgType -> in_gen wit_var (interp_hyp ist gl (out_gen globwit_var x)) | RefArgType -> @@ -2076,14 +2060,16 @@ and interp_genarg ist gl x = in_gen wit_red_expr (pf_interp_red_expr ist gl (out_gen globwit_red_expr x)) | OpenConstrArgType casted -> in_gen (wit_open_constr_gen casted) - (pf_interp_open_constr casted ist gl + (interp_open_constr (if casted then Some (pf_concl gl) else None) + ist (pf_env gl) (project gl) (snd (out_gen (globwit_open_constr_gen casted) x))) | ConstrWithBindingsArgType -> in_gen wit_constr_with_bindings - (interp_constr_with_bindings ist gl (out_gen globwit_constr_with_bindings x)) + (pack_sigma (interp_constr_with_bindings ist (pf_env gl) (project gl) + (out_gen globwit_constr_with_bindings x))) | BindingsArgType -> in_gen wit_bindings - (interp_bindings ist gl (out_gen globwit_bindings x)) + (pack_sigma (interp_bindings ist (pf_env gl) (project gl) (out_gen globwit_bindings x))) | List0ArgType ConstrArgType -> interp_genarg_constr_list0 ist gl x | List1ArgType ConstrArgType -> interp_genarg_constr_list1 ist gl x | List0ArgType VarArgType -> interp_genarg_var_list0 ist gl x @@ -2104,12 +2090,12 @@ and interp_genarg ist gl x = and interp_genarg_constr_list0 ist gl x = let lc = out_gen (wit_list0 globwit_constr) x in - let lc = pf_interp_constr_list ist gl lc in + let lc = pf_apply (interp_constr_list ist) gl lc in in_gen (wit_list0 wit_constr) lc and interp_genarg_constr_list1 ist gl x = let lc = out_gen (wit_list1 globwit_constr) x in - let lc = pf_interp_constr_list ist gl lc in + let lc = pf_apply (interp_constr_list ist) gl lc in in_gen (wit_list1 wit_constr) lc and interp_genarg_var_list0 ist gl x = @@ -2227,59 +2213,68 @@ and interp_tactic ist tac gl = tactic_of_value ist (val_interp ist gl tac) gl (* Interprets a primitive tactic *) -and interp_atomic ist gl = function +and interp_atomic ist gl tac = + let env = pf_env gl and sigma = project gl in + match tac with (* Basic tactics *) | TacIntroPattern l -> h_intro_patterns (interp_intro_pattern_list_as_list ist gl l) | TacIntrosUntil hyp -> h_intros_until (interp_quantified_hypothesis ist hyp) | TacIntroMove (ido,hto) -> - h_intro_move (Option.map (interp_fresh_ident ist gl) ido) + h_intro_move (Option.map (interp_fresh_ident ist env) ido) (interp_move_location ist gl hto) | TacAssumption -> h_assumption | TacExact c -> h_exact (pf_interp_casted_constr ist gl c) | TacExactNoCheck c -> h_exact_no_check (pf_interp_constr ist gl c) | TacVmCastNoCheck c -> h_vm_cast_no_check (pf_interp_constr ist gl c) - | TacApply (a,ev,cb,None) -> - h_apply a ev (List.map (interp_open_constr_with_bindings_loc ist gl) cb) - | TacApply (a,ev,cb,Some cl) -> - h_apply_in a ev (List.map (interp_open_constr_with_bindings_loc ist gl) cb) - (interp_in_hyp_as ist gl cl) + | TacApply (a,ev,cb,cl) -> + let sigma, l = + list_fold_map (interp_open_constr_with_bindings_loc ist env) sigma cb + in + let tac = match cl with + | None -> h_apply a ev + | Some cl -> + (fun l -> h_apply_in a ev l (interp_in_hyp_as ist gl cl)) in + tclWITHHOLES ev tac sigma l | TacElim (ev,cb,cbo) -> - h_elim ev (interp_constr_with_bindings ist gl cb) - (Option.map (interp_constr_with_bindings ist gl) cbo) + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + tclWITHHOLES ev (h_elim ev cb) sigma cbo | TacElimType c -> h_elim_type (pf_interp_type ist gl c) - | TacCase (ev,cb) -> h_case ev (interp_constr_with_bindings ist gl cb) + | TacCase (ev,cb) -> + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + tclWITHHOLES ev (h_case ev) sigma cb | TacCaseType c -> h_case_type (pf_interp_type ist gl c) - | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist gl) idopt) n + | TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist env) idopt) n | TacMutualFix (b,id,n,l) -> - let f (id,n,c) = (interp_fresh_ident ist gl id,n,pf_interp_type ist gl c) - in h_mutual_fix b (interp_fresh_ident ist gl id) n (List.map f l) - | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist gl) idopt) + let f (id,n,c) = (interp_fresh_ident ist env id,n,pf_interp_type ist gl c) + in h_mutual_fix b (interp_fresh_ident ist env id) n (List.map f l) + | TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist env) idopt) | TacMutualCofix (b,id,l) -> - let f (id,c) = (interp_fresh_ident ist gl id,pf_interp_type ist gl c) in - h_mutual_cofix b (interp_fresh_ident ist gl id) (List.map f l) + let f (id,c) = (interp_fresh_ident ist env id,pf_interp_type ist gl c) in + h_mutual_cofix b (interp_fresh_ident ist env id) (List.map f l) | TacCut c -> h_cut (pf_interp_type ist gl c) | TacAssert (t,ipat,c) -> - let c = (if t=None then interp_constr else interp_type) ist (project gl) (pf_env gl) c in - abstract_tactic (TacAssert (t,ipat,inj_open c)) + let c = (if t=None then interp_constr else interp_type) ist env sigma c in + abstract_tactic (TacAssert (t,ipat,c)) (Tactics.forward (Option.map (interp_tactic ist) t) (Option.map (interp_intro_pattern ist gl) ipat) c) | TacGeneralize cl -> - h_generalize_gen - (pf_interp_constr_with_occurrences_and_name_as_list ist gl cl) + let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in + tclWITHHOLES false (h_generalize_gen) sigma cl | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) | TacLetTac (na,c,clp,b) -> let clp = interp_clause ist gl clp in - h_let_tac b (interp_fresh_name ist gl na) (pf_interp_constr ist gl c) clp + h_let_tac b (interp_fresh_name ist env na) (pf_interp_constr ist gl c) clp (* Automation tactics *) | TacTrivial (lems,l) -> - Auto.h_trivial (pf_interp_constr_list ist gl lems) + Auto.h_trivial (interp_constr_list ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) | TacAuto (n,lems,l) -> Auto.h_auto (Option.map (interp_int_or_var ist) n) - (pf_interp_constr_list ist gl lems) + (interp_constr_list ist env sigma lems) (Option.map (List.map (interp_hint_base ist)) l) | TacAutoTDB n -> Dhyp.h_auto_tdb n | TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id) @@ -2287,19 +2282,23 @@ and interp_atomic ist gl = function | TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2 | TacDAuto (n,p,lems) -> Auto.h_dauto (Option.map (interp_int_or_var ist) n,p) - (pf_interp_constr_list ist gl lems) + (interp_constr_list ist env sigma lems) (* Derived basic tactics *) | TacSimpleInductionDestruct (isrec,h) -> h_simple_induction_destruct isrec (interp_quantified_hypothesis ist h) | TacInductionDestruct (isrec,ev,(l,cls)) -> - h_induction_destruct ev isrec - (List.map (fun (lc,cbo,(ipato,ipats)) -> - (List.map (interp_induction_arg ist gl) lc, - Option.map (interp_constr_with_bindings ist gl) cbo, - (Option.map (interp_intro_pattern ist gl) ipato, - Option.map (interp_intro_pattern ist gl) ipats))) l, - Option.map (interp_clause ist gl) cls) + let sigma, l = + list_fold_map (fun sigma (lc,cbo,(ipato,ipats)) -> + let sigma,lc = + list_fold_map (interp_induction_arg ist gl) sigma lc in + let sigma,cbo = + Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in + (sigma,(lc,cbo, + (Option.map (interp_intro_pattern ist gl) ipato, + Option.map (interp_intro_pattern ist gl) ipats)))) sigma l in + let cls = Option.map (interp_clause ist gl) cls in + tclWITHHOLES ev (h_induction_destruct ev isrec) sigma (l,cls) | TacDoubleInduction (h1,h2) -> let h1 = interp_quantified_hypothesis ist h1 in let h2 = interp_quantified_hypothesis ist h2 in @@ -2309,8 +2308,9 @@ and interp_atomic ist gl = function | TacDecompose (l,c) -> let l = List.map (interp_inductive ist) l in Elim.h_decompose l (pf_interp_constr ist gl c) - | TacSpecialize (n,l) -> - h_specialize n (interp_constr_with_bindings ist gl l) + | TacSpecialize (n,cb) -> + let sigma, cb = interp_constr_with_bindings ist env sigma cb in + tclWITHHOLES false (h_specialize n) sigma cb | TacLApply c -> h_lapply (pf_interp_constr ist gl c) (* Context management *) @@ -2321,18 +2321,25 @@ and interp_atomic ist gl = function | TacRename l -> h_rename (List.map (fun (id1,id2) -> interp_hyp ist gl id1, - interp_fresh_ident ist gl (snd id2)) l) + interp_fresh_ident ist env (snd id2)) l) | TacRevert l -> h_revert (interp_hyp_list ist gl l) (* Constructors *) - | TacLeft (ev,bl) -> h_left ev (interp_bindings ist gl bl) - | TacRight (ev,bl) -> h_right ev (interp_bindings ist gl bl) - | TacSplit (ev,_,bll) -> h_split ev (List.map (interp_bindings ist gl) bll) + | TacLeft (ev,bl) -> + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_left ev) sigma bl + | TacRight (ev,bl) -> + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_right ev) sigma bl + | TacSplit (ev,_,bll) -> + let sigma, bll = list_fold_map (interp_bindings ist env) sigma bll in + tclWITHHOLES ev (h_split ev) sigma bll | TacAnyConstructor (ev,t) -> abstract_tactic (TacAnyConstructor (ev,t)) (Tactics.any_constructor ev (Option.map (interp_tactic ist) t)) | TacConstructor (ev,n,bl) -> - h_constructor ev (skip_metaid n) (interp_bindings ist gl bl) + let sigma, bl = interp_bindings ist env sigma bl in + tclWITHHOLES ev (h_constructor ev (skip_metaid n)) sigma bl (* Conversion *) | TacReduce (r,cl) -> @@ -2353,10 +2360,13 @@ and interp_atomic ist gl = function (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> - Equality.general_multi_multi_rewrite ev - (List.map (fun (b,m,c) -> (b,m,interp_open_constr_with_bindings ist gl c)) l) - (interp_clause ist gl cl) - (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) + let l = List.map (fun (b,m,c) -> + let sigma',c = interp_open_constr_with_bindings ist env sigma c in + let _,sigma' = Evarutil.subtract_evars sigma sigma' in + (b,m,{it=c;sigma=sigma'})) l in + let cl = interp_clause ist gl cl in + Equality.general_multi_multi_rewrite ev l cl + (Option.map (fun by -> tclCOMPLETE (interp_tactic ist by), Equality.Naive) by) | TacInversion (DepInversion (k,c,ids),hyp) -> Inv.dinv k (Option.map (pf_interp_constr ist gl) c) (Option.map (interp_intro_pattern ist gl) ids) @@ -2388,7 +2398,7 @@ and interp_atomic ist gl = function VIntroPattern (snd (interp_intro_pattern ist gl (out_gen globwit_intro_pattern x))) | IdentArgType b -> - value_of_ident (interp_fresh_ident ist gl + value_of_ident (interp_fresh_ident ist env (out_gen (globwit_ident_gen b) x)) | VarArgType -> mk_hyp_value ist gl (out_gen globwit_var x) @@ -2420,7 +2430,7 @@ and interp_atomic ist gl = function VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) | List0ArgType (IdentArgType b) -> let wit = wit_list0 (globwit_ident_gen b) in - let mk_ident x = value_of_ident (interp_fresh_ident ist gl x) in + let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in VList (List.map mk_ident (out_gen wit x)) | List0ArgType IntroPatternArgType -> let wit = wit_list0 globwit_intro_pattern in @@ -2440,7 +2450,7 @@ and interp_atomic ist gl = function VList (List.map (mk_int_or_var_value ist) (out_gen wit x)) | List1ArgType (IdentArgType b) -> let wit = wit_list1 (globwit_ident_gen b) in - let mk_ident x = value_of_ident (interp_fresh_ident ist gl x) in + let mk_ident x = value_of_ident (interp_fresh_ident ist env x) in VList (List.map mk_ident (out_gen wit x)) | List1ArgType IntroPatternArgType -> let wit = wit_list1 globwit_intro_pattern in diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index ce8cfa7dbc..fe4e9f6aab 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -134,8 +134,7 @@ val interp_tac_gen : (identifier * value) list -> identifier list -> val interp_hyp : interp_sign -> goal sigma -> identifier located -> identifier -val interp_bindings : interp_sign -> goal sigma -> rawconstr_and_expr Rawterm.bindings -> - Evd.open_constr Rawterm.bindings +val interp_bindings : interp_sign -> Environ.env -> Evd.evar_map -> rawconstr_and_expr Rawterm.bindings -> Evd.evar_map * constr Rawterm.bindings (* Initial call for interpretation *) val glob_tactic : raw_tactic_expr -> glob_tactic_expr diff --git a/tactics/tactics.ml b/tactics/tactics.ml index dc51c6d0c1..332e93c8c6 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -59,23 +59,6 @@ let rec nb_prod x = let inj_with_occurrences e = (all_occurrences_expr,e) -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 inj_ebindings = function - | NoBindings -> NoBindings - | ImplicitBindings l -> ImplicitBindings (List.map inj_open l) - | ExplicitBindings l -> - ExplicitBindings (List.map (fun (l,id,c) -> (l,id,inj_open c)) l) - let dloc = dummy_loc (* Option for 8.2 compatibility *) @@ -191,8 +174,11 @@ let rename_hyp = Tacmach.rename_hyp (* Fresh names *) (**************************************************************) +let fresh_id_in_env avoid id env = + next_ident_away_in_goal id (avoid@ids_of_named_context (named_context env)) + let fresh_id avoid id gl = - next_ident_away_in_goal id (avoid@(pf_ids_of_hyps gl)) + fresh_id_in_env avoid id (pf_env gl) (**************************************************************) (* Fixpoints and CoFixpoints *) @@ -776,7 +762,7 @@ let elimination_clause_scheme with_evars allow_K i elimclause indclause gl = type eliminator = { elimindex : int option; (* None = find it automatically *) - elimbody : constr with_ebindings + elimbody : constr with_bindings } let general_elim_clause_gen elimtac indclause elim gl = @@ -927,26 +913,6 @@ let descend_in_conjunctions sidecond_first with_evars tac exit c gl = (* Resolution tactics *) (****************************************************) -(* Resolution with missing arguments *) - -let check_evars sigma evm gl = - let origsigma = gl.sigma in - let rest = - Evd.fold (fun ev evi acc -> - if not (Evd.mem origsigma ev) && not (Evd.is_defined sigma ev) - then Evd.add acc ev evi else acc) - evm Evd.empty - in - if rest <> Evd.empty then - errorlabstrm "apply" (str"Uninstantiated existential "++ - str(plural (List.length (Evd.to_list rest)) "variable")++str": " ++ - fnl () ++ pr_evar_map rest);; - -let get_bindings_evars = function - | ImplicitBindings largs -> List.map fst largs - | ExplicitBindings lbind -> List.map (fun x -> fst (pi3 x)) lbind - | NoBindings -> [] - let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in @@ -954,17 +920,13 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = goal. If this fails, then the head constant will be unfolded step by step. *) let concl_nprod = nb_prod (pf_concl gl0) in - let evmc, c = c in - let evm = List.fold_left Evd.merge evmc (get_bindings_evars lbind) in let rec try_main_apply with_destruct c gl = let thm_ty0 = nf_betaiota (project gl) (pf_type_of gl c) in 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 res = Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in - if not with_evars then check_evars (fst res).sigma evm gl0; - res + Clenvtac.res_pf clause ~with_evars:with_evars ~flags:flags gl in try try_apply thm_ty0 concl_nprod with PretypeError _|RefinerError _|UserError _|Failure _ as exn -> @@ -987,33 +949,27 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = Stdpp.raise_with_loc loc exn in try_red_apply thm_ty0 in - if evm = Evd.empty then try_main_apply with_destruct c gl0 - else - tclTHEN - (tclEVARS (Evd.merge gl0.sigma evm)) - (try_main_apply with_destruct c) gl0 + try_main_apply with_destruct c gl0 let rec apply_with_ebindings_gen b e = function - | [] -> - tclIDTAC + | [] -> tclIDTAC | [cb] -> general_apply b b e cb | cb::cbl -> tclTHENLAST (general_apply b b e cb) (apply_with_ebindings_gen b e cbl) -let apply_with_ebindings cb = apply_with_ebindings_gen false false [dloc,cb] -let eapply_with_ebindings cb = apply_with_ebindings_gen false true [dloc,cb] +let apply_with_ebindings cb = + apply_with_ebindings_gen false false [dloc,cb] + +let eapply_with_ebindings cb = + apply_with_ebindings_gen false true [dloc,cb] -let apply_with_bindings (c,bl) = - apply_with_ebindings (inj_open c,inj_ebindings bl) +let apply_with_bindings cb = apply_with_ebindings_gen false false [dloc,cb] -let eapply_with_bindings (c,bl) = - apply_with_ebindings_gen false true [dloc,(inj_open c,inj_ebindings bl)] +let eapply_with_bindings cb = apply_with_ebindings_gen false true [dloc,cb] -let apply c = - apply_with_ebindings (inj_open c,NoBindings) +let apply c = apply_with_ebindings_gen false false [dloc,(c,NoBindings)] -let eapply c = - eapply_with_ebindings (inj_open c,NoBindings) +let eapply c = apply_with_ebindings_gen false true [dloc,(c,NoBindings)] let apply_list = function | c::l -> apply_with_bindings (c,ImplicitBindings l) @@ -1055,25 +1011,19 @@ let apply_in_once_main flags innerclause (d,lbind) gl = aux (make_clenv_binding gl (d,thm) lbind) let apply_in_once sidecond_first with_delta with_destruct with_evars id - (loc,((sigma,d),lbind)) gl0 = + (loc,(d,lbind)) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in - let sigma = List.fold_left Evd.merge sigma (get_bindings_evars lbind) in let t' = pf_get_hyp_typ gl0 id in let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in let rec aux with_destruct c gl = try let clause = apply_in_once_main flags innerclause (c,lbind) gl in - let res = clenv_refine_in ~sidecond_first with_evars id clause gl in - if not with_evars then check_evars (fst res).sigma sigma gl0; - res + clenv_refine_in ~sidecond_first with_evars id clause gl with exn when with_destruct -> descend_in_conjunctions sidecond_first true aux (fun _ -> raise exn) c gl in - if sigma = Evd.empty then aux with_destruct d gl0 - else - tclTHEN (tclEVARS (Evd.merge gl0.sigma sigma)) (aux with_destruct d) gl0 - + aux with_destruct d gl0 (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1176,13 +1126,12 @@ let rec intros_clearing = function (* Modifying/Adding an hypothesis *) let specialize mopt (c,lbind) g = - let evars, term = - if lbind = NoBindings then None, c + let term = + if lbind = NoBindings then c else let clause = make_clenv_binding g (c,pf_type_of g c) lbind in let clause = clenv_unify_meta_types clause in - let (thd,tstack) = - whd_stack clause.evd (clenv_value clause) in + let (thd,tstack) = whd_stack clause.evd (clenv_value clause) in let nargs = List.length tstack in let tstack = match mopt with | Some m -> @@ -1193,24 +1142,21 @@ let specialize mopt (c,lbind) g = | t::l -> if occur_meta t then [] else t :: chk l in chk tstack in - let term = applist(thd,tstack) in + let term = applist(thd,List.map (nf_evar clause.evd) tstack) in if occur_meta term then errorlabstrm "" (str "Cannot infer an instance for " ++ pr_name (meta_name clause.evd (List.hd (collect_metas term))) ++ str "."); - Some clause.evd, term + term in - tclTHEN - (match evars with Some e -> tclEVARS e | _ -> tclIDTAC) - (match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with + match kind_of_term (fst(decompose_app (snd(decompose_lam_assum c)))) with | Var id when List.mem id (pf_ids_of_hyps g) -> tclTHENFIRST (fun g -> internal_cut_replace id (pf_type_of g term) g) - (exact_no_check term) + (exact_no_check term) g | _ -> tclTHENLAST (fun g -> cut (pf_type_of g term) g) - (exact_no_check term)) - g + (exact_no_check term) g (* Keeping only a few hypotheses *) @@ -1248,12 +1194,11 @@ let constructor_tac with_evars expctdnumopt i lbind gl = Array.length (snd (Global.lookup_inductive mind)).mind_consnames in check_number_of_constructors expctdnumopt i nconstr; let cons = mkConstruct (ith_constructor_of_inductive mind i) in - let apply_tac = - general_apply true false with_evars (dloc,(inj_open cons,lbind)) in + let apply_tac = general_apply true false with_evars (dloc,(cons,lbind)) in (tclTHENLIST [convert_concl_no_check redcl DEFAULTcast; intros; apply_tac]) gl -let one_constructor i = constructor_tac false None i +let one_constructor i lbind = constructor_tac false None i lbind (* Try to apply the constructor of the inductive definition followed by a tactic t given as an argument. @@ -1273,18 +1218,17 @@ let any_constructor with_evars tacopt gl = let left_with_ebindings with_evars = constructor_tac with_evars (Some 2) 1 let right_with_ebindings with_evars = constructor_tac with_evars (Some 2) 2 -let split_with_ebindings with_evars = - tclMAP (constructor_tac with_evars (Some 1) 1) - -let left l = left_with_ebindings false (inj_ebindings l) -let simplest_left = left NoBindings +let split_with_ebindings with_evars l = + tclMAP (constructor_tac with_evars (Some 1) 1) l -let right l = right_with_ebindings false (inj_ebindings l) -let simplest_right = right NoBindings +let left = left_with_ebindings false +let simplest_left = left NoBindings -let split l = split_with_ebindings false [inj_ebindings l] -let simplest_split = split NoBindings +let right = right_with_ebindings false +let simplest_right = right NoBindings +let split = constructor_tac false (Some 1) 1 +let simplest_split = split NoBindings (*****************************) (* Decomposing introductions *) @@ -1328,7 +1272,7 @@ let intro_or_and_pattern loc b ll l' tac id gl = let rewrite_hyp l2r id gl = let rew_on l2r = - !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) in + !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) in let clear_var_and_eq c = tclTRY (tclTHEN (clear [id]) (tclTRY (clear [destVar c]))) in let t = pf_whd_betadeltaiota gl (pf_type_of gl (mkVar id)) in @@ -1431,7 +1375,7 @@ let prepare_intros s ipat gl = match ipat with | IntroWildcard -> let id = make_id s gl in id, clear_wildcards [dloc,id] | IntroRewrite l2r -> let id = make_id s gl in - id, !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allHypsAndConcl + id, !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl | IntroOrAndPattern ll -> make_id s gl, onLastHypId (intro_or_and_pattern loc true ll [] @@ -1465,7 +1409,7 @@ let assert_tac na = assert_as true (ipat_of_name na) let as_tac id ipat = match ipat with | Some (loc,IntroRewrite l2r) -> - !forward_general_multi_rewrite l2r false (inj_open (mkVar id),NoBindings) allHypsAndConcl + !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl | Some (loc,IntroOrAndPattern ll) -> intro_or_and_pattern loc true ll [] (intros_patterns true [] [] no_move) id @@ -1497,10 +1441,11 @@ let general_apply_in sidecond_first with_delta with_destruct with_evars lemmas) (as_tac id ipat) -let apply_in simple with_evars = general_apply_in false simple simple with_evars +let apply_in simple with_evars id lemmas ipat = + general_apply_in false simple simple with_evars id lemmas ipat let simple_apply_in id c = - apply_in false false id [dloc,((Evd.empty,c),NoBindings)] None + general_apply_in false false false false id [dloc,(c,NoBindings)] None (**************************) (* Generalize tactics *) @@ -2137,7 +2082,7 @@ let cook_sign hyp0_opt indvars env = (* [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) type elim_scheme = { - elimc: constr with_ebindings option; + elimc: constr with_bindings option; elimt: types; indref: global_reference option; index: int; (* index of the elimination type in the scheme *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index b894628c3c..d2cbeb8560 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -30,10 +30,6 @@ open Rawterm open Termops (*i*) -val inj_open : constr -> open_constr -val inj_red_expr : red_expr -> (open_constr, evaluable_global_reference) red_expr_gen -val inj_ebindings : constr bindings -> open_constr bindings - (* Main tactics. *) (*s General functions. *) @@ -60,6 +56,7 @@ val cofix : identifier option -> tactic (*s Introduction tactics. *) +val fresh_id_in_env : identifier list -> identifier -> env -> identifier val fresh_id : identifier list -> identifier -> goal sigma -> identifier val find_intro_names : rel_context -> goal sigma -> identifier list @@ -103,8 +100,8 @@ val try_intros_until : or a term with bindings *) val onInductionArg : - (constr with_ebindings -> tactic) -> - constr with_ebindings induction_arg -> tactic + (constr with_bindings -> tactic) -> + constr with_bindings induction_arg -> tactic (*s Introduction tactics with eliminations. *) @@ -163,7 +160,7 @@ val clear : identifier list -> tactic val clear_body : identifier list -> tactic val keep : identifier list -> tactic -val specialize : int option -> constr with_ebindings -> tactic +val specialize : int option -> constr with_bindings -> tactic val move_hyp : bool -> identifier -> identifier move_location -> tactic val rename_hyp : (identifier * identifier) list -> tactic @@ -180,21 +177,20 @@ val apply : constr -> tactic val eapply : constr -> tactic val apply_with_ebindings_gen : - advanced_flag -> evars_flag -> open_constr with_ebindings located list -> - tactic + advanced_flag -> evars_flag -> constr with_bindings located list -> tactic val apply_with_bindings : constr with_bindings -> tactic val eapply_with_bindings : constr with_bindings -> tactic -val apply_with_ebindings : open_constr with_ebindings -> tactic -val eapply_with_ebindings : open_constr with_ebindings -> tactic +val apply_with_ebindings : constr with_bindings -> tactic +val eapply_with_ebindings : constr with_bindings -> tactic val cut_and_apply : constr -> tactic val apply_in : - advanced_flag -> evars_flag -> identifier -> - open_constr with_ebindings located list -> - intro_pattern_expr located option -> tactic + advanced_flag -> evars_flag -> identifier -> + constr with_bindings located list -> + intro_pattern_expr located option -> tactic val simple_apply_in : identifier -> constr -> tactic @@ -227,7 +223,7 @@ val simple_apply_in : identifier -> constr -> tactic (* [rel_contexts] and [rel_declaration] actually contain triples, and lists are actually in reverse order to fit [compose_prod]. *) type elim_scheme = { - elimc: constr with_ebindings option; + elimc: constr with_bindings option; elimt: types; indref: global_reference option; index: int; (* index of the elimination type in the scheme *) @@ -248,13 +244,13 @@ type elim_scheme = { } -val compute_elim_sig : ?elimc: constr with_ebindings -> types -> elim_scheme +val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme val rebuild_elimtype_from_scheme: elim_scheme -> types (* elim principle with the index of its inductive arg *) type eliminator = { elimindex : int option; (* None = find it automatically *) - elimbody : constr with_ebindings + elimbody : constr with_bindings } val elimination_clause_scheme : evars_flag -> @@ -267,38 +263,38 @@ val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) -> 'a -> eliminator -> tactic val general_elim : evars_flag -> - constr with_ebindings -> eliminator -> ?allow_K:bool -> tactic + constr with_bindings -> eliminator -> ?allow_K:bool -> tactic val general_elim_in : evars_flag -> - identifier -> constr with_ebindings -> eliminator -> tactic + identifier -> constr with_bindings -> eliminator -> tactic -val default_elim : evars_flag -> constr with_ebindings -> tactic +val default_elim : evars_flag -> constr with_bindings -> tactic val simplest_elim : constr -> tactic val elim : - evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic + evars_flag -> constr with_bindings -> constr with_bindings option -> tactic val simple_induct : quantified_hypothesis -> tactic -val new_induct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> +val new_induct : evars_flag -> constr with_bindings induction_arg list -> + constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> clause option -> tactic (*s Case analysis tactics. *) -val general_case_analysis : evars_flag -> constr with_ebindings -> tactic +val general_case_analysis : evars_flag -> constr with_bindings -> tactic val simplest_case : constr -> tactic val simple_destruct : quantified_hypothesis -> tactic -val new_destruct : evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> +val new_destruct : evars_flag -> constr with_bindings induction_arg list -> + constr with_bindings option -> intro_pattern_expr located option * intro_pattern_expr located option -> clause option -> tactic (*s Generic case analysis / induction tactics. *) val induction_destruct : rec_flag -> evars_flag -> - (constr with_ebindings induction_arg list * - constr with_ebindings option * + (constr with_bindings induction_arg list * + constr with_bindings option * (intro_pattern_expr located option * intro_pattern_expr located option)) list * clause option -> tactic @@ -321,17 +317,17 @@ val dorE : bool -> clause ->tactic (*s Introduction tactics. *) val constructor_tac : evars_flag -> int option -> int -> - open_constr bindings -> tactic + constr bindings -> tactic val any_constructor : evars_flag -> tactic option -> tactic -val one_constructor : int -> open_constr bindings -> tactic +val one_constructor : int -> constr bindings -> tactic val left : constr bindings -> tactic val right : constr bindings -> tactic val split : constr bindings -> tactic -val left_with_ebindings : evars_flag -> open_constr bindings -> tactic -val right_with_ebindings : evars_flag -> open_constr bindings -> tactic -val split_with_ebindings : evars_flag -> open_constr bindings list -> tactic +val left_with_ebindings : evars_flag -> constr bindings -> tactic +val right_with_ebindings : evars_flag -> constr bindings -> tactic +val split_with_ebindings : evars_flag -> constr bindings list -> tactic val simplest_left : tactic val simplest_right : tactic @@ -388,4 +384,4 @@ val specialize_hypothesis : identifier -> tactic val dependent_pattern : ?pattern_term:bool -> constr -> tactic val register_general_multi_rewrite : - (bool -> evars_flag -> open_constr with_bindings -> clause -> tactic) -> unit + (bool -> evars_flag -> constr with_bindings -> clause -> tactic) -> unit |