diff options
Diffstat (limited to 'contrib/fourier/fourierR.ml')
| -rw-r--r-- | contrib/fourier/fourierR.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index 74a58b11d4..c877dc47bb 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -18,8 +18,10 @@ open Term open Tactics open Clenv open Names +open Tacticals open Tacmach open Fourier +open Contradiction (****************************************************************************** Opérations sur les combinaisons linéaires affines. @@ -68,6 +70,7 @@ let flin_emult a f = ;; (*****************************************************************************) +open Vernacexpr let parse_ast = Pcoq.parse_string Pcoq.Constr.constr;; let parse s = Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);; let pf_parse_constr gl s = @@ -550,10 +553,11 @@ let rec fourier gl= ;; +(* let fourier_tac x gl = fourier gl ;; let v_fourier = add_tactic "Fourier" fourier_tac - +*) |