diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-02 21:42:11 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-02 21:42:11 +0000 |
| commit | d51d98682fcff981a1e6b95574c25fc7edf97b3f (patch) | |
| tree | 0f6e2a769b3ebf4a93d103f0c5d3ae9acabd8281 /toplevel/auto_ind_decl.ml | |
| parent | 52ca74d1495249844e2ba1be2eaec662e3808074 (diff) | |
Making the behavior of "injection ... as ..." more natural:
- hypotheses are introduced in the left-to-right order
- intropatterns have to match the number of generated hypotheses, and,
if less, new introduction names are automatically generated
- clearing the hypothesis on which injection is applied, if any.
However, this is a source of incompatibilities (for a variant of
injection that is hopefully not used a lot). Compatibility can be
restored by "Unset Injection L2R Pattern Order".
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16556 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index 56bdc810d..82445a0fd 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -666,7 +666,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig = tclTRY ( tclORELSE reflexivity (Equality.discr_tac false None) ); - Equality.inj [] false (mkVar freshz,NoBindings); + Equality.inj None false (mkVar freshz,NoBindings); intros; simpl_in_concl; Auto.default_auto; tclREPEAT ( |