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 /toplevel/auto_ind_decl.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 'toplevel/auto_ind_decl.ml')
-rw-r--r-- | toplevel/auto_ind_decl.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 0ef835689..9192db722 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -525,7 +525,7 @@ let compute_bl_tact ind lnamesparrec nparrec = intro_using freshz; intros; tclTRY ( - tclORELSE reflexivity (Equality.discr_tac None) + tclORELSE reflexivity (Equality.discr_tac false None) ); simpl_in_hyp ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp); @@ -643,9 +643,10 @@ let compute_lb_tact ind lnamesparrec nparrec = intro_using freshz; intros; tclTRY ( - tclORELSE reflexivity (Equality.discr_tac None) + tclORELSE reflexivity (Equality.discr_tac false None) ); - Equality.inj [] freshz; intros; simpl_in_concl; + Equality.inj [] false (mkVar freshz,Rawterm.NoBindings); + intros; simpl_in_concl; Auto.default_auto; tclREPEAT ( tclTHENSEQ [apply (andb_true_intro()); @@ -806,6 +807,6 @@ let compute_dec_tact ind lnamesparrec nparrec = Rawterm.NoBindings ) true); - Pfedit.by (Equality.discr_tac None) + Pfedit.by (Equality.discr_tac false None) |