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/ssr | |
| 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/ssr')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 4 | ||||
| -rw-r--r-- | plugins/ssr/ssrtacticals.ml | 2 |
2 files changed, 2 insertions, 4 deletions
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index a05b1e3d81..a4caeb403c 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -426,7 +426,7 @@ let mk_anon_id t gl_ids = (set s i (Char.chr (Char.code (get s i) + 1)); s) in Id.of_string_soft (Bytes.to_string (loop (n - 1))) -let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast +let convert_concl_no_check t = Tactics.convert_concl ~check:false t DEFAULTcast let convert_concl t = Tactics.convert_concl t DEFAULTcast let rename_hd_prod orig_name_ref gl = @@ -1409,8 +1409,6 @@ let tclINTRO_ANON ?seed () = | Some seed -> tclINTRO ~id:(Seed seed) ~conclusion:return let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> - let convert_concl_no_check t = - Tactics.convert_concl_no_check t DEFAULTcast in let concl = Goal.concl gl in let sigma = Goal.sigma gl in match EConstr.kind sigma concl with diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index bbe7bde78b..17e4114958 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -110,7 +110,7 @@ let endclausestac id_map clseq gl_id cl0 gl = | _ -> EConstr.map (project gl) unmark c in let utac hyp = Proofview.V82.of_tactic - (Tactics.convert_hyp_no_check (NamedDecl.map_constr unmark hyp)) in + (Tactics.convert_hyp ~check:false (NamedDecl.map_constr unmark hyp)) in let utacs = List.map utac (pf_hyps gl) in let ugtac gl' = Proofview.V82.of_tactic |