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/omega | |
| 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/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index 4802608fda..f3bc791b8d 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -535,7 +535,7 @@ let focused_simpl path = let open Tacmach.New in Proofview.Goal.enter begin fun gl -> let newc = context (project gl) (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - convert_concl_no_check newc DEFAULTcast + convert_concl ~check:false newc DEFAULTcast end let focused_simpl path = focused_simpl path @@ -687,7 +687,7 @@ let simpl_coeffs path_init path_k = let n = Pervasives.(-) (List.length path_k) (List.length path_init) in let newc = context sigma (fun _ t -> loop n t) (List.rev path_init) (pf_concl gl) in - convert_concl_no_check newc DEFAULTcast + convert_concl ~check:false newc DEFAULTcast end let rec shuffle p (t1,t2) = @@ -1849,12 +1849,12 @@ let destructure_hyps = match destructurate_type env sigma typ with | Kapp(Nat,_) -> (tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) + (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_neq, [| t1;t2|])) decl)) (loop lit)) | Kapp(Z,_) -> (tclTHEN - (convert_hyp_no_check (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) + (Tactics.convert_hyp ~check:false (NamedDecl.set_type (mkApp (Lazy.force coq_Zne, [| t1;t2|])) decl)) (loop lit)) | _ -> loop lit |