diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-05 15:15:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-10-09 16:04:42 +0200 |
| commit | e824d429363262a9ff9db117282fe15289b5ab59 (patch) | |
| tree | cd319518235243c63835cd646d4b0536f2a656bd /plugins/omega | |
| parent | 5eff644c658d1765ba73cd9e73c5bd7819c7d644 (diff) | |
A version of convert_concl and convert_hyp in new proof engine.
Not very optimized though (if we apply convert_hyp on any hyp, a new
evar will be generated for every different hyp...).
Diffstat (limited to 'plugins/omega')
| -rw-r--r-- | plugins/omega/coq_omega.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml index f8fd71ae2..847fda8cd 100644 --- a/plugins/omega/coq_omega.ml +++ b/plugins/omega/coq_omega.ml @@ -566,7 +566,7 @@ let abstract_path typ path t = let focused_simpl path gl = let newc = context (fun i t -> pf_nf gl t) (List.rev path) (pf_concl gl) in - convert_concl_no_check newc DEFAULTcast gl + Proofview.V82.of_tactic (convert_concl_no_check newc DEFAULTcast) gl let focused_simpl path = focused_simpl path @@ -1806,15 +1806,15 @@ let destructure_hyps = match destructurate_type (pf_nf typ) with | Kapp(Nat,_) -> (Tacticals.New.tclTHEN - (Proofview.V82.tactic (convert_hyp_no_check + (convert_hyp_no_check (i,body, - (mkApp (Lazy.force coq_neq, [| t1;t2|]))))) + (mkApp (Lazy.force coq_neq, [| t1;t2|])))) (loop lit)) | Kapp(Z,_) -> (Tacticals.New.tclTHEN - (Proofview.V82.tactic (convert_hyp_no_check + (convert_hyp_no_check (i,body, - (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))) + (mkApp (Lazy.force coq_Zne, [| t1;t2|])))) (loop lit)) | _ -> loop lit end |