diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-21 13:02:48 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-21 13:02:48 +0000 |
| commit | 2d3d9d4c7a4276fbc6bdf553f082ac12a56824d3 (patch) | |
| tree | 7775b2a32b1936ab6b9bef3962b7a2e413b38a28 /proofs | |
| 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 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 3 | ||||
| -rw-r--r-- | proofs/clenvtac.mli | 1 |
2 files changed, 4 insertions, 0 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 22dcca289..624b671d3 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -60,6 +60,9 @@ let clenv_cast_meta clenv = in crec +let clenv_value_cast_meta clenv = + clenv_cast_meta clenv (clenv_value clenv) + let clenv_pose_dependent_evars with_evars clenv = let dep_mvs = clenv_dependent false clenv in if dep_mvs <> [] & not with_evars then 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 |