diff options
Diffstat (limited to 'toplevel')
| -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 56bdc810d5..82445a0fde 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 ( |