diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-30 09:12:39 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-30 10:28:54 +0100 |
| commit | 19e2576c979c57ad0827f6a4364713930e0c6d4f (patch) | |
| tree | dd4cddf6faec1a3c919cb047b0018850c0b09397 /plugins/fourier/fourierR.ml | |
| parent | 203b0eaac832af3b62e484c1aef89a02ffe8e29b (diff) | |
Simplifying code of fourier.
Diffstat (limited to 'plugins/fourier/fourierR.ml')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 9 |
1 files changed, 1 insertions, 8 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index e5c9b2707..b1f642c1d 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -413,13 +413,6 @@ let tac_zero_infeq_false gl (n,d) = (tac_zero_inf_pos gl (-n,d))) ;; -let create_meta () = mkMeta(Evarutil.new_meta());; - -let my_cut c gl= - let concl = pf_concl gl in - apply_type (mkProd(Anonymous,c,concl)) [create_meta()] gl -;; - let exact = exact_check;; let tac_use h = @@ -587,7 +580,7 @@ let rec fourier () = then tac_zero_inf_false gl (rational_to_fraction cres) else tac_zero_infeq_false gl (rational_to_fraction cres) in - tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq)) + tac:=(Tacticals.New.tclTHENS (cut ineq) [Tacticals.New.tclTHEN (change_concl (mkAppL [| get coq_not; ineq|] )) |