diff options
| -rw-r--r-- | kernel/environ.ml | 1 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 | ||||
| -rw-r--r-- | kernel/safe_typing.ml | 5 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 1 | ||||
| -rw-r--r-- | kernel/sign.ml | 4 | ||||
| -rw-r--r-- | kernel/sign.mli | 1 | ||||
| -rw-r--r-- | library/global.ml | 1 | ||||
| -rw-r--r-- | library/global.mli | 1 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/inv.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 17 |
12 files changed, 18 insertions, 26 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 2cff2f716..7113b4040 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -101,7 +101,6 @@ let named_context_app f env = env_named_context = f env.env_named_context } let push_named d = named_context_app (Sign.add_named_decl d) -let pop_named id = named_context_app (Sign.pop_named_decl id) let reset_context env = { env with diff --git a/kernel/environ.mli b/kernel/environ.mli index a7670f46e..98f6380c0 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -53,7 +53,6 @@ val fold_rel_context : (***********************************************************************) (* Context of variables (section variables and goal assumptions) *) val push_named : named_declaration -> env -> env -val pop_named : identifier -> env -> env (* Looks up in the context of local vars referred by names ([named_context]) *) (* raises [Not_found] if the identifier is not found *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index f284d774d..ad36e2941 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -123,11 +123,6 @@ let add_mind sp mie env = let add_constraints = Environ.add_constraints -let rec pop_named_decls idl env = - match idl with - | [] -> env - | id::l -> pop_named_decls l (Environ.pop_named id env) - let export = export let import = import diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 853bc7ccd..071a67224 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -32,7 +32,6 @@ val push_named_assum : val push_named_def : identifier * constr * types option -> safe_environment -> Univ.constraints * safe_environment -val pop_named_decls : identifier list -> safe_environment -> safe_environment (* Adding global axioms or definitions *) type constant_entry = { diff --git a/kernel/sign.ml b/kernel/sign.ml index e1c9fbe4b..8c05d15ca 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -35,10 +35,6 @@ let add_named_decl (id,_,_ as d) sign = let named_context_length = List.length -let pop_named_decl id = function - | (id',_,_) :: sign -> assert (id = id'); sign - | [] -> assert false - let instance_from_named_context sign = let rec inst_rec = function | (id,None,_) :: sign -> mkVar id :: inst_rec sign diff --git a/kernel/sign.mli b/kernel/sign.mli index a35f61d22..6ba3e4fff 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -20,7 +20,6 @@ type section_context = named_context val empty_named_context : named_context val add_named_decl : named_declaration -> named_context -> named_context -val pop_named_decl : identifier -> named_context -> named_context val lookup_named : identifier -> named_context -> named_declaration val named_context_length : named_context -> int diff --git a/library/global.ml b/library/global.ml index b929ad78f..db0e5f470 100644 --- a/library/global.ml +++ b/library/global.ml @@ -45,7 +45,6 @@ let push_named_def d = let (cst,env) = push_named_def d !global_env in global_env := env; cst -let pop_named_decls ids = global_env := pop_named_decls ids !global_env let add_constant sp ce = global_env := add_constant sp ce !global_env let add_mind sp mie = global_env := add_mind sp mie !global_env diff --git a/library/global.mli b/library/global.mli index 48b647c6a..48e90d12e 100644 --- a/library/global.mli +++ b/library/global.mli @@ -30,7 +30,6 @@ val named_context : unit -> Sign.named_context (* Extending env with variables, constants and inductives *) val push_named_assum : (identifier * types) -> Univ.constraints val push_named_def : (identifier * constr * types option) -> Univ.constraints -val pop_named_decls : identifier list -> unit val add_constant : constant -> global_declaration -> unit val add_mind : mutual_inductive -> mutual_inductive_entry -> unit diff --git a/proofs/logic.ml b/proofs/logic.ml index 85c0a0297..cf6df42ce 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -748,7 +748,7 @@ let pr_prim_rule = function | {name=Intro_after;newids=[id]} -> str"intro after " ++ pr_id id - | {name=Intro_replacing;newids=[id]} -> + | {name=Intro_replacing;hypspecs=[id]} -> (str"intro replacing " ++ pr_id id) | {name=Cut b;terms=[t];newids=[id]} -> diff --git a/tactics/equality.ml b/tactics/equality.ml index ee2c9c450..ca049a454 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -814,7 +814,7 @@ let inj id gls = mkVar id]) in let ty = - try pf_type_of gls pf + try pf_nf gls (pf_type_of gls pf) with | UserError("refiner__fail",_) -> errorlabstrm "InjClause" @@ -878,7 +878,7 @@ let decompEqThen ntac id gls = let pf = applist(lbeq.congr (), [t;resty;injfun;t1;t2; mkVar id]) in - let ty = pf_type_of gls pf in + let ty = pf_nf gls (pf_type_of gls pf) in ((tclTHENS (cut ty) ([tclIDTAC;refine pf])))) (List.rev injectors)) diff --git a/tactics/inv.ml b/tactics/inv.ml index b372b8bdf..63c6eac3e 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -368,9 +368,11 @@ let raw_inversion inv_kind indbinding id status gl = make_inv_predicate env sigma indt id status (pf_concl gl) in let (cut_concl,case_tac) = if status <> NoDep & (dependent c (pf_concl gl)) then - applist(elim_predicate,realargs@[c]),case_then_using + Reduction.beta_appvect elim_predicate (Array.of_list (realargs@[c])), + case_then_using else - applist(elim_predicate,realargs),case_nodep_then_using + Reduction.beta_appvect elim_predicate (Array.of_list realargs), + case_nodep_then_using in (tclTHENS (true_cut_anon cut_concl) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 5623e3899..435e569d9 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -498,10 +498,13 @@ let apply_type hdcty argl gl = let apply_term hdc argl gl = refine (applist (hdc,argl)) gl -let bring_hyps hyps gl = - let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in - let f = mkCast (mkMeta (new_meta()),newcl) in - refine (mkApp (f, instance_from_named_context hyps)) gl +let bring_hyps hyps = + if hyps = [] then Refiner.tclIDTAC + else + (fun gl -> + let newcl = List.fold_right mkNamedProd_or_LetIn hyps (pf_concl gl) in + let f = mkCast (mkMeta (new_meta()),newcl) in + refine (mkApp (f, instance_from_named_context hyps)) gl) (* Resolution with missing arguments *) @@ -876,8 +879,10 @@ let dyn_assumption = function let clear ids gl = thin ids gl let dyn_clear = function | [Clause ids] -> - let out = function InHyp id -> id | _ -> assert false in - clear (List.map out ids) + if ids=[] then tclIDTAC + else + let out = function InHyp id -> id | _ -> assert false in + clear (List.map out ids) | l -> bad_tactic_args "clear" l let clear_body = thin_body |