diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-12-22 19:45:04 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-10-26 15:34:50 +0200 |
| commit | 91e9e1c26b7f2b874df83600b2bc8d23df9ed48b (patch) | |
| tree | 770c08abffe9c2ea689cfa0f2e49cf9da445888c /vernac/auto_ind_decl.ml | |
| parent | 925c434592597a34cd7ef4efb5e18a43e197bd96 (diff) | |
Passing around the flag for injection so that tactics calling inj at
ML level can set the flags themselves.
In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".
This fixes bug #5281.
Diffstat (limited to 'vernac/auto_ind_decl.ml')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 503508fc0..7af391758 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -91,6 +91,15 @@ let destruct_on_using c id = let destruct_on_as c l = destruct false None c (Some (Loc.tag l)) None +let inj_flags = Some { + Equality.keep_proof_equalities = true; (* necessary *) + injection_in_context = true; (* does not matter here *) + Equality.injection_pattern_l2r_order = true; (* does not matter here *) + } + +let my_discr_tac = Equality.discr_tac false None +let my_inj_tac x = Equality.inj inj_flags None false None (EConstr.mkVar x,NoBindings) + (* reconstruct the inductive with the correct de Bruijn indexes *) let mkFullInd (ind,u) n = let mib = Global.lookup_mind (fst ind) in @@ -595,7 +604,7 @@ let compute_bl_tact mode bl_scheme_key ind lnamesparrec nparrec = intro_using freshz; intros; Tacticals.New.tclTRY ( - Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) + Tacticals.New.tclORELSE reflexivity my_discr_tac ); simpl_in_hyp (freshz,Locus.InHyp); (* @@ -739,9 +748,9 @@ let compute_lb_tact mode lb_scheme_key ind lnamesparrec nparrec = intro_using freshz; intros; Tacticals.New.tclTRY ( - Tacticals.New.tclORELSE reflexivity (Equality.discr_tac false None) + Tacticals.New.tclORELSE reflexivity my_discr_tac ); - Equality.inj None false None (EConstr.mkVar freshz,NoBindings); + my_inj_tac freshz; intros; simpl_in_concl; Auto.default_auto; Tacticals.New.tclREPEAT ( @@ -936,7 +945,7 @@ let compute_dec_tact ind lnamesparrec nparrec = NoBindings ) true; - Equality.discr_tac false None + my_discr_tac ] end ] |