Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et commandes vernaculaires (cf dev/changements.txt pour plus de précisions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2734 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 1 deletions

diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 74a58b11d..c877dc47b 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
-
+*)