- 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

1 files changed, 1 insertions, 0 deletions

diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 0cf0a5545..4dd59fcf6 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -27,6 +27,7 @@ val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 
 val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+val clenv_value_cast_meta : clausenv -> constr
 
 (* Compatibility, use res_pf ?with_evars:true instead *)
 val e_res_pf : clausenv -> tactic