diff options
| author | Hugo Herbelin | 2019-04-29 21:01:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-29 21:01:49 +0200 |
| commit | fcba5e87be13bc5a5374fe274476cd4d5c45f058 (patch) | |
| tree | 14707fa1bd939458f553b1baaf35becda2267675 /plugins/ltac | |
| parent | 69daead8ae18d55ee445a918865ea2adf59439eb (diff) | |
| parent | 7e8fbed8df5e3f819e4775df791fc85f235854fb (diff) | |
Merge PR #9983: Hypothesis conversion allocates a single evar
Reviewed-by: gares
Ack-by: herbelin
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_auto.mlg | 2 | ||||
| -rw-r--r-- | plugins/ltac/rewrite.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg index 523c7c8305..ec5e46d89b 100644 --- a/plugins/ltac/g_auto.mlg +++ b/plugins/ltac/g_auto.mlg @@ -184,7 +184,7 @@ END TACTIC EXTEND convert_concl_no_check -| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl_no_check x DEFAULTcast } +| ["convert_concl_no_check" constr(x) ] -> { Tactics.convert_concl ~check:false x DEFAULTcast } END { diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 2d40ba6562..99a9c1ab9a 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1596,7 +1596,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = tclTHENFIRST (assert_replacing id newt tac) (beta_hyp id) | Some id, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_hyp_no_check (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> + convert_hyp ~check:false (LocalAssum (make_annot id Sorts.Relevant, newt)) <*> beta_hyp id | None, Some p -> Proofview.Unsafe.tclEVARS undef <*> @@ -1610,7 +1610,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma ~progress strat clause = end | None, None -> Proofview.Unsafe.tclEVARS undef <*> - convert_concl_no_check newt DEFAULTcast + convert_concl ~check:false newt DEFAULTcast in Proofview.Goal.enter begin fun gl -> let concl = Proofview.Goal.concl gl in |