diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-22 09:56:54 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-02-22 09:56:54 +0000 |
| commit | fdbc16dff05e57389a17a360814011f40489b499 (patch) | |
| tree | e0897ce9789f608c839518161667edfc2e67fa90 /tactics | |
| parent | f070d33f9822dac079e58a9920c9c9e0cade12f6 (diff) | |
suppression de pop_named
meilleure discrimination dans les tactiques d'inversion
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2491 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/inv.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.ml | 17 |
3 files changed, 17 insertions, 10 deletions
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 |