diff options
author | 2008-06-21 13:02:48 +0000 | |
---|---|---|
committer | 2008-06-21 13:02:48 +0000 | |
commit | 2d3d9d4c7a4276fbc6bdf553f082ac12a56824d3 (patch) | |
tree | 7775b2a32b1936ab6b9bef3962b7a2e413b38a28 /pretyping/termops.ml | |
parent | ae819de2775d1bc30c05ac9574f13ec31a7103a8 (diff) |
- Implantation de la suggestion 1873 sur discriminate. Au final,
discriminate/injection/simplify_eq acceptent maintenant un terme
comme argument. Les clauses "with" et les variantes "e" sont aussi
acceptées. Aussi, discriminate sans argument essaie maintenant
toutes les hyps quantifiées (au lieu de traiter seulement les buts
t1<>t2).
--This line, and those below, will be ignored--
M doc/refman/RefMan-tac.tex
M CHANGES
M pretyping/evd.ml
M pretyping/termops.ml
M pretyping/termops.mli
M pretyping/clenv.ml
M tactics/extratactics.ml4
M tactics/inv.ml
M tactics/equality.ml
M tactics/tactics.mli
M tactics/equality.mli
M tactics/tacticals.ml
M tactics/eqdecide.ml4
M tactics/tacinterp.ml
M tactics/tactics.ml
M tactics/extratactics.mli
M toplevel/auto_ind_decl.ml
M contrib/funind/invfun.ml
M test-suite/success/Discriminate.v
M test-suite/success/Injection.v
M proofs/clenvtac.mli
M proofs/clenvtac.ml
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11159 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/termops.ml')
-rw-r--r-- | pretyping/termops.ml | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 73c03097a..4246f0daa 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -275,6 +275,11 @@ let rec strip_head_cast c = match kind_of_term c with | Cast (c,_,_) -> strip_head_cast c | _ -> c +(* Get the last arg of an application *) +let last_arg c = match kind_of_term c with + | App (f,cl) -> array_last cl + | _ -> anomaly "last_arg" + (* [map_constr_with_named_binders g f l c] maps [f l] on the immediate subterms of [c]; it carries an extra data [l] (typically a name list) which is processed by [g na] (which typically cons [na] to |