Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v

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

23 files changed, 1111 insertions, 194 deletions

diff --git a/contrib/correctness/Correctness.v b/contrib/correctness/Correctness.v
index 0c47512ed7..5cc7b6aa74 100644
--- a/contrib/correctness/Correctness.v
+++ b/contrib/correctness/Correctness.v
@@ -12,8 +12,6 @@
 
 (* Correctness is base on the tactic Refine (developped on purpose) *)
 
-Require Export Refine.
-
 Require Export Tuples.
 
 Require Export ProgInt.
@@ -22,4 +20,6 @@ Require Export ProgWf.
 
 Require Export Arrays.
 
+(*
 Token "'".
+*)
diff --git a/contrib/correctness/psyntax.ml4 b/contrib/correctness/psyntax.ml4
index 0791dab78d..bbca106086 100644
--- a/contrib/correctness/psyntax.ml4
+++ b/contrib/correctness/psyntax.ml4
@@ -26,6 +26,7 @@ open Ptype
 open Past
 open Penv
 open Pmonad
+open Vernacexpr
 
 
 (* We define new entries for programs, with the use of this module
@@ -479,13 +480,17 @@ GEXTEND Gram
   END
 ;;
 
+let wit_prog, rawwit_prog = Genarg.create_arg "PROGRAMS-PROG"
+let wit_typev, rawwit_typev = Genarg.create_arg "PROGRAMS-TYPEV"
+(*
 let (in_prog,out_prog) = Dyn.create "PROGRAMS-PROG"
 let (in_typev,out_typev) = Dyn.create "PROGRAMS-TYPEV"
-
+*)
 open Pp
 open Util
 open Himsg
 open Vernacinterp
+open Vernacexpr
 open Declare
 
 let is_assumed global ids =
@@ -497,15 +502,18 @@ let is_assumed global ids =
 	     prlist_with_sep (fun () -> (str ", ")) pr_id ids ++
 	     str " are assumed")
 
+open Genarg
+
 let add = vinterp_add
 
 let _ = add "CORRECTNESS"
      (function
-	 [ VARG_STRING s; VARG_DYN d ] -> 
-	   fun () -> Ptactic.correctness s (out_prog d) None
-       | [ VARG_STRING s; VARG_DYN d; VARG_TACTIC t ] ->
-	   let tac = Tacinterp.interp t in
-	   fun () -> Ptactic.correctness s (out_prog d) (Some tac)
+	 [ s; p; t ] ->
+	   let str = out_gen rawwit_pre_ident s in
+	   let pgm = out_gen rawwit_prog p in
+	   let tac = out_gen (wit_opt rawwit_tactic) t in
+	   fun () ->
+	     Ptactic.correctness str pgm (option_app Tacinterp.interp tac)
        | _ -> assert false)
 
 let _ = 
@@ -522,28 +530,28 @@ let _ =
 		Penv.empty ())
        | _ -> assert false)
 
-let id_of_varg = function VARG_IDENTIFIER id -> id | _ -> assert false
-    
+open Extend
+
 let _ = 
   add "PROGVARIABLE"
     (function
-       | [ VARG_VARGLIST l; VARG_DYN d ] ->
+       | [ ids; v ] ->
 	   (fun () ->
-	      let ids = List.map id_of_varg l in
+ 	      let ids = out_gen (wit_list1 rawwit_ident) ids in
 	      List.iter
 		(fun id -> if Penv.is_global id then
 		   Util.errorlabstrm "PROGVARIABLE"
 		     (str"Clash with previous constant " ++ pr_id id))
 		ids;
-	      let v = out_typev d in
+              let v = out_gen rawwit_typev v in
 	      Pdb.check_type_v (all_refs ()) v;
 	      let env = empty in
 	      let ren = update empty_ren "" [] in
 	      let v = Ptyping.cic_type_v env ren v in
 	      if not (is_mutable v) then begin
-		let c =
+		let c = 
 		  Safe_typing.ParameterEntry (trad_ml_type_v ren env v),
-		  Declare.NeverDischarge in
+		  Nametab.NeverDischarge in
 		List.iter 
 		  (fun id -> ignore (Declare.declare_constant id c)) ids;
 		if_verbose (is_assumed false) ids
@@ -555,28 +563,27 @@ let _ =
        | _ -> assert false)
 
 open Vernac
+open Coqast
 
 GEXTEND Gram
-  Pcoq.Vernac_.vernac:
-  [ [ IDENT "Global"; "Variable"; 
-      l = LIST1 ident SEP ","; ":"; t = type_v; "." ->
-	let idl = List.map Ast.nvar l in
-	let d = Ast.dynamic (in_typev t) in
-	  <:ast< (PROGVARIABLE (VERNACARGLIST ($LIST $idl)) (VERNACDYN $d)) >>
-
-    | IDENT "Show"; IDENT "Programs"; "." ->
-	<:ast< (SHOWPROGRAMS) >>
-
-    | IDENT "Correctness"; s = IDENT; p = Programs.program; "." ->
-	let d = Ast.dynamic (in_prog p) in
-	let str = Ast.string s in
-	<:ast< (CORRECTNESS $str (VERNACDYN $d)) >>
-
-    | IDENT "Correctness"; s = IDENT; p = Programs.program; ";";
-      tac = Tactic.tactic; "." ->
-	let d = Ast.dynamic (in_prog p) in
-	let str = Ast.string s in
-	<:ast< (CORRECTNESS $str (VERNACDYN $d) (TACTIC $tac)) >> ] ];
+  GLOBAL:  Pcoq.Vernac_.command;
+
+  Pcoq.Vernac_.command:
+  [ [ (s,l) = aux -> VernacExtend (s,l) ] ];
+  aux:
+  [ [ IDENT "Global"; "Variable"; l = LIST1 Pcoq.Prim.ident SEP ","; ":"; t = type_v ->
+	("PROGVARIABLE",
+	  [in_gen (wit_list1 rawwit_ident) l;in_gen rawwit_typev t])
+
+    | IDENT "Show"; IDENT "Programs" ->
+	("SHOWPROGRAMS",[])
+
+    | IDENT "Correctness"; s = IDENT; p = Programs.program; 
+      t = OPT [ ";"; tac = Tactic.tactic -> tac ] ->
+	let str = in_gen rawwit_pre_ident s in
+	let d = in_gen rawwit_prog p in
+	let tac = in_gen (wit_opt rawwit_tactic) t in
+	("CORRECTNESS",[str;d;tac]) ] ];
  END
 ;;
 
diff --git a/contrib/extraction/g_extraction.ml4 b/contrib/extraction/g_extraction.ml4
new file mode 100644
index 0000000000..1fe4ee7058
--- /dev/null
+++ b/contrib/extraction/g_extraction.ml4
@@ -0,0 +1,90 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* ML names *)
+
+open Vernacexpr
+open Pcoq
+open Genarg
+
+let wit_mlname, rawwit_mlname = Genarg.create_arg "mlname"
+let mlname = create_generic_entry "mlname" rawwit_mlname
+let _ = Tacinterp.add_genarg_interp "mlname"
+  (fun ist x ->
+    (in_gen wit_mlname
+      (out_gen wit_string
+	(Tacinterp.genarg_interp ist
+	  (in_gen rawwit_string
+	    (out_gen rawwit_mlname x))))))
+
+GEXTEND Gram
+  GLOBAL: mlname;
+  mlname:
+  [ [ id = IDENT -> id
+    | s = STRING -> s ] ]
+  ;
+END
+
+(* Extraction commands *)
+
+open Table
+open Extract_env
+open Pcoq.Constr
+open Pcoq.Prim
+
+VERNAC COMMAND EXTEND Extraction
+(* Extraction in the Coq toplevel *)
+| [ "Extraction" constr(c) ] -> [ extraction c ]
+| [ "Recursive" "Extraction" ne_qualid_list(l) ] -> [ extraction_rec l ]
+
+(* Monolithic extraction to a file *)
+| [ "Extraction" string(f) ne_qualid_list(l) ] 
+  -> [ extraction_file f l ]
+
+(* Modular extraction (one Coq module = one ML module) *)
+| [ "Extraction" "Module" ident(m) ]
+  -> [ extraction_module m ]
+| [ "Recursive" "Extraction" "Module" ident(m) ]
+  -> [ recursive_extraction_module m ]
+
+(* Target Language *)
+
+| [ "Extraction" "Language" "Ocaml" ] 
+  -> [ extraction_language Ocaml ]
+| [ "Extraction" "Language" "Haskell" ] 
+  -> [ extraction_language Haskell ]
+| [ "Extraction" "Language" "Toplevel" ] 
+  -> [ extraction_language Toplevel ]
+
+(* Custom inlining directives *)
+| [ "Extraction" "Inline" ne_qualid_list(l) ] 
+  -> [ extraction_inline true l ]
+
+| [ "Extraction" "NoInline" ne_qualid_list(l) ] 
+  -> [ extraction_inline false l ]
+
+| [ "Print" "Extraction" "Inline" ]
+  -> [ print_extraction_inline () ]
+
+| [ "Reset" "Extraction" "Inline" ]
+  -> [ reset_extraction_inline () ]
+
+(* Overriding of a Coq object by an ML one *)
+| [ "Extract" "Constant" qualid(x) "=>" mlname(y) ]
+  -> [ extract_constant_inline false x y ]
+
+| [ "Extract" "Inlined" "Constant" qualid(x) "=>" mlname(y) ]
+  -> [ extract_constant_inline true x y ]
+
+| [ "Extract" "Inductive" qualid(x) "=>" mlname(id) "[" mlname_list(idl) "]" ]
+  -> [ extract_inductive x (id,idl) ]
+
+
+END
diff --git a/contrib/field/Field.v b/contrib/field/Field.v
index 69687c1009..df2a44f3e7 100644
--- a/contrib/field/Field.v
+++ b/contrib/field/Field.v
@@ -12,31 +12,4 @@ Require Export Field_Compl.
 Require Export Field_Theory.
 Require Export Field_Tactic.
 
-Declare ML Module "field".
-
-Grammar vernac opt_arg_list : ast list :=
-| noal [] -> []
-| minus [ "minus" ":=" constrarg($aminus) opt_arg_list($l) ] ->
-  [ "minus" $aminus ($LIST $l) ]
-| div [ "div" ":=" constrarg($adiv) opt_arg_list($l) ] ->
-  [ "div" $adiv ($LIST $l) ]
-
-with extra_args : ast list :=
-| nea [] -> []
-| with_a [ "with" opt_arg_list($l)] -> [ ($LIST $l) ]
-
-with vernac : ast := 
-  addfield [ "Add" "Field" 
-      	     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
-      	     constrarg($azero) constrarg($aopp) constrarg($aeq)
-             constrarg($ainv) constrarg($rth) constrarg($ainv_l) extra_args($l)
-             "." ]
-    -> [(AddField $a $aplus $amult $aone $azero $aopp $aeq $ainv $rth
-                  $ainv_l ($LIST $l))].
-
-Grammar tactic simple_tactic: ast :=
-  | field [ "Field" constrarg_list($arg) ] -> [(Field ($LIST $arg))].
-
-Syntax tactic level 0:
-  | field [ <<(Field ($LIST $lc))>> ] -> ["Field" [1 1] (LISTSPC ($LIST $lc))]
-  | field_e [(Field)] -> ["Field"].
+(* Command declarations are moved to the ML side *)
diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v
index 7be170ebb7..e893c9f36c 100644
--- a/contrib/field/Field_Tactic.v
+++ b/contrib/field/Field_Tactic.v
@@ -271,7 +271,7 @@ Tactic Definition Field_Gen_Aux FT :=
     Let mul = (GiveMult '(EAplus trm1 trm2)) In
     Cut [ft:=FT][vm:=lvar](interp_ExprA ft vm trm1)==(interp_ExprA ft vm trm2);
     [Compute;Auto
-    |Intros;(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc);
+    |Intros ft vm;(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc);
      (Multiply mul);[(ApplySimplif ApplyMultiply);
        (ApplySimplif (ApplyInverse mul));
        (Let id = GrepMult In Clear id);WeakReduce;Clear ft vm;
diff --git a/contrib/field/Field_Theory.v b/contrib/field/Field_Theory.v
index 54cc9609e9..fcd864f366 100644
--- a/contrib/field/Field_Theory.v
+++ b/contrib/field/Field_Theory.v
@@ -41,7 +41,7 @@ Inductive ExprA : Set :=
 
 Lemma eqExprA_O:(e1,e2:ExprA){e1=e2}+{~e1=e2}.
 Proof.
-  Double Induction 1 2;Try Intros;
+  Double Induction e1 e2;Try Intros;
    Try (Left;Reflexivity) Orelse Try (Right;Discriminate).
   Elim (H1 e0);Intro y;Elim (H2 e);Intro y0;
     Try (Left; Rewrite y; Rewrite y0;Auto)
diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 1edf302e07..137d125287 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -19,6 +19,8 @@ open Term
 open Typing
 open Util
 open Vernacinterp
+open Vernacexpr
+open Tacexpr
 
 (* Interpretation of constr's *)
 let constr_of com = Astterm.interp_constr Evd.empty (Global.env()) com
@@ -86,30 +88,43 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth
   end
 
 (* Vernac command declaration *)
-let _ =
-  let rec opt_arg (aminus_o,adiv_o) = function
-    | (VARG_STRING "minus")::(VARG_CONSTR aminus)::l ->
-      (match aminus_o with
-      |	None -> opt_arg ((Some aminus),adiv_o) l
-      |	_ -> anomaly "AddField")
-    | (VARG_STRING "div")::(VARG_CONSTR adiv)::l ->
-      (match adiv_o with
-      |	None -> opt_arg (aminus_o,(Some adiv)) l
-      |	_ -> anomaly "AddField")
-    | _ -> (aminus_o,adiv_o) in
-  vinterp_add "AddField"
-    (function 
-       | (VARG_CONSTR a)::(VARG_CONSTR aplus)::(VARG_CONSTR amult)
-	 ::(VARG_CONSTR aone)::(VARG_CONSTR azero)::(VARG_CONSTR aopp)
-	 ::(VARG_CONSTR aeq)::(VARG_CONSTR ainv)::(VARG_CONSTR rth)
-         ::(VARG_CONSTR ainv_l)::l ->
-         (fun () ->
-           let (aminus_o,adiv_o) = opt_arg (None,None) l in
-           add_field (constr_of a) (constr_of aplus) (constr_of amult)
-             (constr_of aone) (constr_of azero) (constr_of aopp)
-             (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
-             (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l))
-       | _ -> anomaly "AddField")
+open Extend
+open Pcoq
+open Genarg
+
+let wit_minus_div_arg, rawwit_minus_div_arg = Genarg.create_arg "minus_div_arg"
+let minus_div_arg = create_generic_entry "minus_div_arg" rawwit_minus_div_arg
+let _ = Tacinterp.add_genarg_interp "minus_div_arg"
+  (fun ist x ->
+    (in_gen wit_minus_div_arg
+      (out_gen (wit_pair (wit_opt wit_constr) (wit_opt wit_constr))
+	(Tacinterp.genarg_interp ist
+	  (in_gen (wit_pair (wit_opt rawwit_constr) (wit_opt rawwit_constr))
+	    (out_gen rawwit_minus_div_arg x))))))
+
+open Pcoq.Constr
+GEXTEND Gram
+  GLOBAL: minus_div_arg;
+  minus_arg: [ [ IDENT "minus"; ":="; aminus = constr -> aminus ] ];
+  div_arg: [ [ IDENT "div"; ":="; adiv = constr -> adiv ] ];
+  minus_div_arg:
+    [ [ "with"; m = minus_arg; d = OPT div_arg -> Some m, d
+      | "with"; d = div_arg; m = OPT minus_arg -> m, Some d
+      | -> None, None ] ];
+END
+
+VERNAC COMMAND EXTEND Field
+  [ "Add" "Field" 
+      constr(a) constr(aplus) constr(amult) constr(aone)
+      constr(azero) constr(aopp) constr(aeq)
+      constr(ainv) constr(rth) constr(ainv_l) minus_div_arg(md) ]
+    -> [ let (aminus_o, adiv_o) = md in
+         add_field
+           (constr_of a) (constr_of aplus) (constr_of amult)
+           (constr_of aone) (constr_of azero) (constr_of aopp)
+           (constr_of aeq) (constr_of ainv) (constr_of_opt a aminus_o)
+           (constr_of_opt a adiv_o) (constr_of rth) (constr_of ainv_l) ]
+END
 
 (* Guesses the type and calls Field_Gen with the right theory *)
 let field g =
@@ -117,12 +132,12 @@ let field g =
   and env = pf_env g in
   let ist = { evc=evc; env=env; lfun=[]; lmatch=[];
               goalopt=Some g; debug=get_debug () } in
-  let typ = constr_of_Constr (interp_tacarg ist
+  let typ = constr_of_VConstr (val_interp ist
     <:tactic<
       Match Context With
       | [|- (eq ?1 ? ?)] -> ?1
       | [|- (eqT ?1 ? ?)] -> ?1>>) in
-  let th = VArg (Constr (lookup typ)) in
+  let th = VConstr (lookup typ) in
   (tac_interp [(id_of_string "FT",th)] [] (get_debug ())
     <:tactic<
       Match Context With
@@ -148,21 +163,16 @@ let guess_theory env evc = function
 let field_term l g =
   let env = (pf_env g)
   and evc = (project g) in
-  let th = constrIn (guess_theory env evc l)
-  and nl = List.map constrIn (Quote.sort_subterm g l) in
+  let th = valueIn (VConstr (guess_theory env evc l))
+  and nl = List.map (fun x -> valueIn (VConstr x)) (Quote.sort_subterm g l) in
   (List.fold_right
     (fun c a ->
      let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in
-     tclTHENSI tac [a]) nl tclIDTAC) g
-
-(* Gives the constr list from the tactic_arg list *)
-let targ_constr =
-   List.map
-     (fun e ->
-        match e with
-        | Constr c -> c
-        | _ -> anomaly "Field: must be a constr")
+     Tacticals.tclTHENFIRSTn tac [|a|]) nl Tacticals.tclIDTAC) g
 
 (* Declaration of Field *)
-let _ = hide_tactic "Field"
-        (fun l -> if l = [] then field else field_term (targ_constr l))
+
+TACTIC EXTEND Field
+| [ "Field" ] -> [ field ]
+| [ "Field" ne_constr_list(l) ] -> [ field_term l ]
+END
diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v
index 32c61b6d2d..b02688de63 100644
--- a/contrib/fourier/Fourier.v
+++ b/contrib/fourier/Fourier.v
@@ -20,11 +20,6 @@ Require Export Fourier_util.
 Require Export Field.
 Require Export DiscrR.
 
-Grammar tactic simple_tactic:ast:=
-  fourier
-  ["FourierZ" constrarg_list($arg)] ->
-  [(Fourier ($LIST $arg))].
-
 Tactic Definition Fourier  :=
   Abstract (FourierZ;Field;DiscrR).
 
diff --git a/contrib/fourier/g_fourier.ml4 b/contrib/fourier/g_fourier.ml4
new file mode 100644
index 0000000000..79c85aeb2b
--- /dev/null
+++ b/contrib/fourier/g_fourier.ml4
@@ -0,0 +1,17 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open FourierR
+
+TACTIC EXTEND Fourier
+  [ "FourierZ" (* constr_list(l) *) ] -> [ fourier (* l *) ]
+END
diff --git a/contrib/jprover/jprover.ml4 b/contrib/jprover/jprover.ml4
new file mode 100644
index 0000000000..5fce08d386
--- /dev/null
+++ b/contrib/jprover/jprover.ml4
@@ -0,0 +1,565 @@
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+open Jlogic
+
+module JA = Jall
+module JT = Jterm
+module T = Tactics
+module TCL = Tacticals
+module TM = Tacmach
+module N = Names
+module PT = Proof_type
+module HT = Hiddentac
+module PA = Pattern
+module HP = Hipattern
+module TR = Term
+module PR = Printer
+module RO = Reductionops
+module UT = Util
+module RA = Rawterm
+
+module J=JA.JProver(JLogic)         (* the JProver *)
+
+(*i
+module NO = Nameops
+module TO = Termops
+module RE = Reduction
+module CL = Coqlib
+module ID = Inductiveops
+module CV = Clenv
+module RF = Refiner
+i*)
+
+(* Interface to JProver: *)
+(* type JLogic.inf_step = rule * (string * Jterm.term) * (string * Jterm.term) *)
+type jp_inf_step = JLogic.inf_step
+type jp_inference = JLogic.inference    (* simply a list of [inf_step] *)
+
+(* Definitions for rebuilding proof tree from JProver: *)
+(* leaf, one-branch, two-branch, two-branch, true, false *)
+type jpbranch = JP0 | JP1 | JP2 | JP2' | JPT | JPF
+type jptree = | JPempty                                 (* empty tree *)
+              | JPAx of jp_inf_step                     (* Axiom node *)
+              | JPA of jp_inf_step * jptree
+              | JPB of jp_inf_step * jptree * jptree
+
+(* Private debugging tools: *)
+(*i*)
+let mbreak s = Format.print_flush (); print_string ("-break at: "^s);
+               Format.print_flush (); let _ = input_char stdin in ()
+(*i*)
+let jp_error re = raise (JT.RefineError ("jprover", JT.StringError re))
+
+(* print Coq constructor *)
+let print_constr ct = Pp.ppnl (PR.prterm ct); Format.print_flush ()
+
+let rec print_constr_list = function
+  |  [] -> ()
+  |  ct::r -> print_constr ct; print_constr_list r
+
+let print_constr_pair op c1 c2 =
+    print_string (op^"(");
+    print_constr c1;
+    print_string ",";
+    print_constr c2;
+    print_string ")\n"
+
+
+(* Parsing modules for Coq:         *)
+(* [is_coq_???] : testing functions *)
+(* [dest_coq_???] : destructors     *)
+
+let is_coq_true ct = (HP.is_unit_type ct) && not (HP.is_equation ct)
+
+let is_coq_false = HP.is_empty_type
+
+(* return two subterms *)
+let dest_coq_and ct =
+    match (HP.match_with_conjunction ct) with
+      | Some (hdapp,args) ->
+(*i            print_constr hdapp; print_constr_list args; i*)
+            begin
+               match args with
+                   | s1::s2::[] ->
+(*i                       print_constr_pair "and" s1 s2; i*)
+                       (s1,s2)
+                   | _ -> jp_error "dest_coq_and"
+            end
+      | None -> jp_error "dest_coq_and"
+
+let is_coq_or = HP.is_disjunction
+
+(* return two subterms *)
+let dest_coq_or ct =
+    match (HP.match_with_disjunction ct) with
+      | Some (hdapp,args) ->
+(*i            print_constr hdapp; print_constr_list args; i*)
+            begin
+               match args with
+                   | s1::s2::[] ->
+(*i                       print_constr_pair "or" s1 s2; i*)
+                       (s1,s2)
+                   | _ -> jp_error "dest_coq_or"
+            end
+      | None -> jp_error "dest_coq_or"
+
+let is_coq_not = HP.is_nottype
+
+let dest_coq_not ct =
+    match (HP.match_with_nottype ct) with
+      | Some (hdapp,arg) ->
+(*i            print_constr hdapp; print_constr args; i*)
+(*i            print_string "not ";
+            print_constr arg; i*)
+            arg
+      | None -> jp_error "dest_coq_not"
+
+
+let is_coq_impl ct =
+  match TR.kind_of_term ct with
+    | TR.Prod (_,_,b) -> (not (Termops.dependent (TR.mkRel 1) b))
+    | _  -> false
+
+
+let dest_coq_impl c =
+  match TR.kind_of_term c with
+    | TR.Prod (_,b,c) ->
+(*i            print_constr_pair "impl" b c; i*)
+            (b, c)
+    | _ -> jp_error "dest_coq_impl"
+
+(* provide new variables for renaming of universal variables *)
+let new_counter =
+  let ctr = ref 0 in
+    fun () -> incr ctr;!ctr
+
+(* provide new symbol name for unknown Coq constructors *)
+let new_ecounter =
+  let ectr = ref 0 in
+    fun () -> incr ectr;!ectr
+
+(* provide new variables for address naming *)
+let new_acounter =
+  let actr = ref 0 in
+    fun () -> incr actr;!actr
+
+let is_coq_forall ct =
+  match TR.kind_of_term (RO.whd_betaiota ct) with
+    | TR.Prod (_,_,b) -> Termops.dependent (TR.mkRel 1) b
+    | _  -> false
+
+(* return the bounded variable (as a string) and the bounded term *)
+let dest_coq_forall ct =
+  match TR.kind_of_term (RO.whd_betaiota ct) with
+    | TR.Prod (_,_,b) ->
+        let x ="jp_"^(string_of_int (new_counter())) in
+        let v = TR.mkVar (N.id_of_string x) in
+        let c = TR.subst1 v b in    (* substitute de Bruijn variable by [v] *)
+(*i        print_constr_pair "forall" v c; i*)
+        (x, c)
+    | _  -> jp_error "dest_coq_forall"
+
+
+(* Apply [ct] to [t]: *)
+let sAPP ct t =
+  match TR.kind_of_term (RO.whd_betaiota ct) with
+    | TR.Prod (_,_,b) ->
+        let c = TR.subst1 t b in
+            c
+    | _  -> jp_error "sAPP"
+
+
+let is_coq_exists ct =
+  if not (HP.is_conjunction ct) then false
+  else let (hdapp,args) = TR.decompose_app ct in
+     match args with
+      | _::la::[] ->
+           begin
+            try
+              match TR.destLambda la with
+                | (N.Name _,_,_) -> true
+                | _ -> false
+            with _ -> false
+           end
+      | _ -> false
+
+(* return the bounded variable (as a string) and the bounded term *)
+let dest_coq_exists ct =
+  let (hdapp,args) = TR.decompose_app ct in
+     match args with
+      | _::la::[] ->
+           begin
+            try
+             match TR.destLambda la with
+                    | (N.Name x,t1,t2) ->
+                         let v = TR.mkVar x in
+                         let t3 = TR.subst1 v t2 in
+(*i                            print_constr_pair "exists" v t3; i*)
+                            (N.string_of_id x, t3)
+                    | _ -> jp_error "dest_coq_exists"
+            with _ -> jp_error "dest_coq_exists"
+           end
+      | _ -> jp_error "dest_coq_exists"
+
+
+let is_coq_and ct =
+  if (HP.is_conjunction ct) && not (is_coq_exists ct)
+  && not (is_coq_true ct) then true
+  else false
+
+
+(* Parsing modules: *)
+
+let jtbl = Hashtbl.create 53        (* associate for unknown Coq constr. *)
+let rtbl = Hashtbl.create 53        (* reverse table of [jtbl] *)
+
+let dest_coq_symb ct =
+    N.string_of_id (TR.destVar ct)
+
+(* provide new names for unknown Coq constr. *)
+(* [ct] is the unknown constr., string [s] is appended to the name encoding *)
+let create_coq_name ct s =
+    try
+       Hashtbl.find jtbl ct
+    with Not_found ->
+       let t = ("jp_"^s^(string_of_int (new_ecounter()))) in
+          Hashtbl.add jtbl ct t;
+          Hashtbl.add rtbl t ct;
+          t
+
+let dest_coq_app ct s =
+    let (hd, args) = TR.decompose_app ct in
+(*i        print_constr hd;
+        print_constr_list args; i*)
+       if TR.isVar hd then
+          (dest_coq_symb hd, args)
+       else                         (* unknown constr *)
+          (create_coq_name hd s, args)
+
+let rec parsing2 c =        (* for function symbols, variables, constants *)
+    if (TR.isApp c) then    (* function symbol? *)
+        let (f,args) = dest_coq_app c "fun_" in
+            JT.fun_ f (List.map parsing2 args)
+    else if TR.isVar c then (* identifiable variable or constant *)
+            JT.var_ (dest_coq_symb c)
+    else                    (* unknown constr *)
+            JT.var_ (create_coq_name c "var_")
+
+(* the main parsing function *)
+let rec parsing c =
+    let ct = Reduction.whd_betadeltaiota (Global.env ()) c in
+(*    let ct = Reduction.whd_betaiotazeta (Global.env ()) c in *)
+    if is_coq_true ct then
+       JT.true_
+    else if is_coq_false ct then
+       JT.false_
+    else if is_coq_not ct then
+        JT.not_ (parsing (dest_coq_not ct))
+    else if is_coq_impl ct then
+        let (t1,t2) = dest_coq_impl ct in
+            JT.imp_ (parsing t1) (parsing t2)
+    else if is_coq_or ct then
+        let (t1,t2) = dest_coq_or ct in
+            JT.or_ (parsing t1) (parsing t2)
+    else if is_coq_and ct then
+        let (t1,t2) = dest_coq_and ct in
+            JT.and_ (parsing t1) (parsing t2)
+    else if is_coq_forall ct then
+        let (v,t) = dest_coq_forall ct in
+            JT.forall v (parsing t)
+    else if is_coq_exists ct then
+        let (v,t) = dest_coq_exists ct in
+            JT.exists v (parsing t)
+    else if TR.isApp ct then            (* predicate symbol with arguments *)
+        let (p,args) = dest_coq_app ct "P_" in
+            JT.pred_ p (List.map parsing2 args)
+    else if TR.isVar ct then            (* predicate symbol without arguments *)
+        let p = dest_coq_symb ct in
+            JT.pred_ p []
+    else                                (* unknown predicate *)
+        JT.pred_ (create_coq_name ct "Q_") []
+
+(*i
+        print_string "??";print_constr ct;
+        JT.const_ ("err_"^(string_of_int (new_ecounter())))
+i*)
+
+
+(* Translate JProver terms into Coq constructors: *)
+(* The idea is to retrieve it from [rtbl] if it exists indeed, otherwise
+   create one. *)
+let rec constr_of_jterm t =
+  if (JT.is_var_term t) then            (* a variable *)
+     let v = JT.dest_var t in
+     try
+        Hashtbl.find rtbl v
+     with Not_found -> TR.mkVar (N.id_of_string v)
+  else if (JT.is_fun_term t) then       (* a function symbol *)
+     let (f,ts) = JT.dest_fun t in
+     let f' = try Hashtbl.find rtbl f with Not_found -> TR.mkVar (N.id_of_string f) in
+        TR.mkApp (f', Array.of_list (List.map constr_of_jterm ts))
+  else jp_error "constr_of_jterm"
+
+
+(* Coq tactics for Sequent Calculus LJ: *)
+(* Note that for left-rule a name indicating the being applied rule
+   in Coq's Hints is required; for right-rule a name is also needed
+   if it will pass some subterm to the left-hand side.
+   However, all of these can be computed by the path [id] of the being
+   applied rule.
+*)
+
+let assoc_addr = Hashtbl.create 97
+
+let short_addr s =
+  let ad =
+    try
+       Hashtbl.find assoc_addr s
+    with Not_found ->
+       let t = ("jp_H"^(string_of_int (new_acounter()))) in
+          Hashtbl.add assoc_addr s t;
+          t
+  in
+    N.id_of_string ad
+
+(* and-right *)
+let dyn_andr =
+  T.split RA.NoBindings
+
+(* For example, the following implements the [and-left] rule: *)
+let dyn_andl id =   (* [id1]: left child; [id2]: right child *)
+  let id1 = (short_addr (id^"_1")) and id2 = (short_addr (id^"_2")) in
+    (TCL.tclTHEN (T.simplest_elim (TR.mkVar (short_addr id))) (T.intros_using [id1;id2]))
+
+let dyn_orr1 =
+  T.left RA.NoBindings
+
+let dyn_orr2 =
+  T.right RA.NoBindings
+
+let dyn_orl id =
+  let id1 = (short_addr (id^"_1")) and id2 = (short_addr (id^"_2")) in
+    (TCL.tclTHENS (T.simplest_elim (TR.mkVar (short_addr id)))
+                  [T.intro_using id1; T.intro_using id2])
+
+let dyn_negr id =
+  let id1 = id^"_1_1" in
+     HT.h_intro (short_addr id1)
+
+let dyn_negl id =
+  T.simplest_elim (TR.mkVar (short_addr id))
+
+let dyn_impr id =
+  let id1 = id^"_1_1" in
+     HT.h_intro (short_addr id1)
+
+let dyn_impl id gl =
+  let t = TM.pf_get_hyp_typ gl (short_addr id) in
+    let ct = Reduction.whd_betadeltaiota (Global.env ()) t in   (* unfolding *)
+    let (_,b) = dest_coq_impl ct in
+      let id2 = (short_addr (id^"_1_2")) in
+         (TCL.tclTHENLAST
+            (TCL.tclTHENS (T.cut b) [T.intro_using id2;TCL.tclIDTAC])
+         (T.apply_term (TR.mkVar (short_addr id))
+                       [TR.mkMeta (Clenv.new_meta())])) gl
+
+let dyn_allr c =       (* [c] must be an eigenvariable which replaces [v] *)
+  HT.h_intro (N.id_of_string c)
+
+(* [id2] is the path of the instantiated term for [id]*)
+let dyn_alll id id2 t gl =
+  let id' = short_addr id in
+  let id2' = short_addr id2 in
+  let ct = TM.pf_get_hyp_typ gl id' in
+    let ct' = Reduction.whd_betadeltaiota (Global.env ()) ct in   (* unfolding *)
+    let ta = sAPP ct' t in
+       TCL.tclTHENS (T.cut ta) [T.intro_using id2'; T.apply (TR.mkVar id')] gl
+
+let dyn_exl id id2 c = (* [c] must be an eigenvariable *)
+  (TCL.tclTHEN (T.simplest_elim (TR.mkVar (short_addr id)))
+               (T.intros_using [(N.id_of_string c);(short_addr id2)]))
+
+let dyn_exr t =
+  T.one_constructor 1 (RA.ImplicitBindings [t])
+
+let dyn_falsel = dyn_negl
+
+let dyn_truer =
+  T.one_constructor 1 RA.NoBindings
+
+(* Do the proof by the guidance of JProver. *)
+
+let do_one_step inf =
+  let (rule, (s1, t1), ((s2, t2) as k)) = inf in
+   begin
+(*i   if not (Jterm.is_xnil_term t2) then
+   begin
+      print_string "1: "; JT.print_term stdout t2; print_string "\n";
+      print_string "2: "; print_constr (constr_of_jterm t2); print_string "\n";
+   end;
+i*)
+   match rule with
+     | Andl -> dyn_andl s1
+     | Andr -> dyn_andr
+     | Orl  -> dyn_orl s1
+     | Orr1 -> dyn_orr1
+     | Orr2 -> dyn_orr2
+     | Impr -> dyn_impr s1
+     | Impl -> dyn_impl s1
+     | Negr -> dyn_negr s1
+     | Negl -> dyn_negl s1
+     | Allr -> dyn_allr (JT.dest_var t2)
+     | Alll -> dyn_alll s1 s2 (constr_of_jterm t2)
+     | Exr  -> dyn_exr (constr_of_jterm t2)
+     | Exl  -> dyn_exl s1 s2 (JT.dest_var t2)
+     | Ax -> T.assumption (*i TCL.tclIDTAC i*)
+     | Truer -> dyn_truer
+     | Falsel -> dyn_falsel s1
+     | _ -> jp_error "do_one_step"
+            (* this is impossible *)
+    end
+;;
+
+(* Parameter [tr] is the reconstucted proof tree from output of JProver. *)
+let do_coq_proof tr =
+ let rec rec_do trs =
+    match trs with
+     | JPempty -> TCL.tclIDTAC
+     | JPAx h -> do_one_step h
+     | JPA (h, t) -> TCL.tclTHEN (do_one_step h) (rec_do t)
+     | JPB (h, left, right) -> TCL.tclTHENS (do_one_step h) [rec_do left; rec_do right]
+ in
+    rec_do tr
+
+
+(* Rebuild the proof tree from the output of JProver: *)
+
+(* Since some universal variables are not necessarily first-order,
+   lazy substitution may happen. They are recorded in [rtbl]. *)
+let reg_unif_subst t1 t2 =
+  let (v,_,_) = JT.dest_all t1 in
+    Hashtbl.add rtbl v (TR.mkVar (N.id_of_string (JT.dest_var t2)))
+
+let count_jpbranch one_inf =
+    let (rule, (_, t1), (_, t2)) = one_inf in
+      begin
+      match rule with
+        | Ax -> JP0
+        | Orr1 | Orr2 | Negl | Impr | Alll | Exr | Exl -> JP1
+        | Andr | Orl -> JP2
+        | Negr -> if (JT.is_true_term t1) then JPT else JP1
+        | Andl -> if (JT.is_false_term t1) then JPF else JP1
+        | Impl -> JP2'  (* reverse the sons of [Impl] since [dyn_impl] reverses them *)
+        | Allr -> reg_unif_subst t1 t2; JP1
+        | _ -> jp_error "count_jpbranch"
+      end
+
+let replace_by r = function
+  (rule, a, b) -> (r, a, b)
+
+let rec build_jptree inf =
+    match inf with
+     |  [] -> ([], JPempty)
+     |  h::r ->
+        begin
+          match count_jpbranch h with
+           | JP0 -> (r,JPAx h)
+           | JP1 -> let (r1,left) = build_jptree r in
+                    (r1, JPA(h, left))
+           | JP2 -> let (r1,left) = build_jptree r in
+                    let (r2,right) = build_jptree r1 in
+                    (r2, JPB(h, left, right))
+           | JP2' -> let (r1,left) = build_jptree r in      (* for [Impl] *)
+                    let (r2,right) = build_jptree r1 in
+                    (r2, JPB(h, right, left))
+           | JPT -> let (r1,left) = build_jptree r in       (* right True *)
+                    (r1, JPAx (replace_by Truer h))
+           | JPF -> let (r1,left) = build_jptree r in       (* left False *)
+                    (r1, JPAx (replace_by Falsel h))
+        end
+
+
+(* The main function: *)
+(* [limits] is the multiplicity limit. *)
+let jp limits gls =
+   let concl = TM.pf_concl gls in
+   let ct = concl in
+(*i     print_constr ct; i*)
+     Hashtbl.clear jtbl;    (* empty the hash tables *)
+     Hashtbl.clear rtbl;
+     Hashtbl.clear assoc_addr;
+     let t = parsing ct in
+(*i     JT.print_term stdout t; i*)
+        try
+        let p = (J.prover limits [] t) in
+(*i            print_string "\n";
+            JLogic.print_inf p; i*)
+            let (il,tr) = build_jptree p in
+               if (il = []) then
+               begin
+                  print_string "Proof is built.\n";
+                  do_coq_proof tr gls
+               end
+               else UT.error "Cannot reconstruct proof tree from JProver."
+        with e -> print_string "JProver fails to prove this:\n";
+                  JT.print_error_msg e;
+                  UT.error "JProver terminated."
+
+(* an unfailed generalization procedure *)
+let non_dep_gen b gls =
+  let concl = TM.pf_concl gls in
+      if (not (Termops.dependent b concl)) then
+         T.generalize [b] gls
+      else
+         TCL.tclIDTAC gls
+
+let rec unfail_gen = function
+  | [] -> TCL.tclIDTAC
+  | h::r ->
+     TCL.tclTHEN
+        (TCL.tclORELSE (non_dep_gen h) (TCL.tclIDTAC))
+        (unfail_gen r)
+
+(*
+(* no argument, which stands for no multiplicity limit *)
+let jp gls =
+  let ls = List.map (fst) (TM.pf_hyps_types gls) in
+(*i     T.generalize (List.map TR.mkVar ls) gls i*)
+    (* generalize the context *)
+    TCL.tclTHEN (TCL.tclTRY T.red_in_concl)
+                (TCL.tclTHEN (unfail_gen (List.map TR.mkVar ls))
+                             (jp None)) gls
+*)
+(*
+let dyn_jp l gls =
+  assert (l = []);
+  jp
+*)
+
+(* one optional integer argument for the multiplicity *)
+let jpn n gls =
+  let ls = List.map (fst) (TM.pf_hyps_types gls) in
+  TCL.tclTHEN (TCL.tclTRY T.red_in_concl)
+              (TCL.tclTHEN (unfail_gen (List.map TR.mkVar ls))
+                         (jp n)) gls
+(*
+let dyn_jpn l gls =
+  match l with
+   | [PT.Integer n] -> jpn n
+   | _ -> jp_error "Impossible!!!"
+
+
+let h_jp = TM.hide_tactic "Jp" dyn_jp
+
+let h_jpn = TM.hide_tactic "Jpn" dyn_jpn
+*)
+
+TACTIC EXTEND Jprover
+  [ "Jp" natural_opt(n) ] -> [ jpn n ]
+END
+
+(*
+TACTIC EXTEND Andl
+  [ "Andl" ident(id)] -> [ ... (Andl id) ... ].
+END
+*)
diff --git a/contrib/omega/Omega.v b/contrib/omega/Omega.v
index 6c4a6191b5..7da167623c 100755
--- a/contrib/omega/Omega.v
+++ b/contrib/omega/Omega.v
@@ -19,11 +19,6 @@ Require Export ZArith.
 (* The constant minus is required in coq_omega.ml *)
 Require Export Minus.
 
-Declare ML Module "omega".
-Declare ML Module "coq_omega".
-
-Require Export OmegaSyntax.
-
 Hint eq_nat_Omega : zarith := Extern 10 (eq nat ? ?) Abstract Omega.
 Hint le_Omega : zarith := Extern 10 (le ? ?) Abstract Omega.
 Hint lt_Omega : zarith := Extern 10 (lt ? ?) Abstract Omega.
diff --git a/contrib/omega/g_omega.ml4 b/contrib/omega/g_omega.ml4
new file mode 100644
index 0000000000..f0c00d3f80
--- /dev/null
+++ b/contrib/omega/g_omega.ml4
@@ -0,0 +1,24 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(**************************************************************************)
+(*                                                                        *)
+(* Omega: a solver of quantifier-free problems in Presburger Arithmetic   *)
+(*                                                                        *)
+(* Pierre Crégut (CNET, Lannion, France)                                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Coq_omega
+
+TACTIC EXTEND Omega
+  [ "Omega" ] -> [ omega_solver ]
+END
diff --git a/contrib/ring/ArithRing.v b/contrib/ring/ArithRing.v
index b9883d5cd4..e89017daf7 100644
--- a/contrib/ring/ArithRing.v
+++ b/contrib/ring/ArithRing.v
@@ -34,7 +34,7 @@ Hints Resolve nateq_prop eq2eqT : arithring.
 
 Definition NatTheory : (Semi_Ring_Theory plus mult (1) (0) nateq).
   Split; Intros; Auto with arith arithring.
-  Apply eq2eqT; Apply simpl_plus_l with n.
+  Apply eq2eqT; Apply simpl_plus_l with n:=n.
   Apply eqT2eq; Trivial.
 Defined.
 
diff --git a/contrib/ring/Quote.v b/contrib/ring/Quote.v
index 1565e522b4..e2bd0c5378 100644
--- a/contrib/ring/Quote.v
+++ b/contrib/ring/Quote.v
@@ -83,10 +83,3 @@ Save.
 End variables_map.
 
 Unset Implicit Arguments.
-
-Declare ML Module "quote".
-
-Grammar tactic simple_tactic : ast := 
-  quote [ "Quote" identarg($f) ] -> [(Quote $f)]
-| quote_lc [ "Quote" identarg($f) "[" ne_identarg_list($lc) "]"] ->  
-                   [ (Quote $f ($LIST $lc)) ].
diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v
index 93c6eaf539..fa2ba1ca0c 100644
--- a/contrib/ring/Ring.v
+++ b/contrib/ring/Ring.v
@@ -14,55 +14,6 @@ Require Export Quote.
 Require Export Ring_normalize.
 Require Export Ring_abstract.
 
-Declare ML Module "ring".
-
-Grammar tactic simple_tactic : ast :=
-  ring [ "Ring" constrarg_list($arg) ] -> [(Ring ($LIST $arg))].
-
-Syntax tactic level 0:
-  ring [ << (Ring ($LIST $lc)) >> ] -> [ "Ring" [1 1] (LISTSPC ($LIST $lc)) ] 
-| ring_e [ << (Ring) >> ] -> ["Ring"].
- 
-Grammar vernac vernac : ast := 
-  addring [ "Add" "Ring" 
-     constrarg($a) constrarg($aplus) constrarg($amult) constrarg($aone)
-     constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($t)
-     "[" ne_constrarg_list($l) "]" "." ] 
-  -> [(AddRing $a $aplus $amult $aone $azero $aopp $aeq $t
-     ($LIST $l))]
-
-| addsemiring [ "Add" "Semi" "Ring" 
-      	       	 constrarg($a) constrarg($aplus) constrarg($amult) 
-                 constrarg($aone) constrarg($azero) constrarg($aeq) 
-                 constrarg($t) 
-      	       	 "[" ne_constrarg_list($l) "]" "." ] 
-  -> [(AddSemiRing $a $aplus $amult $aone $azero $aeq $t
-      	   ($LIST $l))]
-| addabstractring [ "Add" "Abstract" "Ring" 
-      	     constrarg($a) constrarg($aplus) constrarg($amult)
-             constrarg($aone) constrarg($azero) constrarg($aopp)
-             constrarg($aeq) constrarg($t) "." ] 
-  -> [(AddAbstractRing $a $aplus $amult $aone $azero $aopp $aeq $t)]
-
-| addabstractsemiring [ "Add" "Abstract" "Semi" "Ring" 
-      	       	 constrarg($a) constrarg($aplus) constrarg($amult) 
-                 constrarg($aone) constrarg($azero) constrarg($aeq) 
-                 constrarg($t) "." ] 
-  -> [(AddAbstractSemiRing $a $aplus $amult $aone $azero $aeq $t )]
-| addsetoidring [ "Add" "Setoid" "Ring"
-      	    constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus) constrarg($amult) 
-	    constrarg($aone) constrarg($azero) constrarg($aopp) constrarg($aeq) constrarg($pm)
-	    constrarg($mm) constrarg($om) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
-  -> [(AddSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aopp $aeq $pm $mm $om $t
-      	 ($LIST $l))]
-| addsetoidsemiring [ "Add" "Semi" "Setoid" "Ring" 
-      	  constrarg($a) constrarg($aequiv) constrarg($asetth) constrarg($aplus)
-	  constrarg($amult) constrarg($aone) constrarg($azero) constrarg($aeq) 
-          constrarg($pm) constrarg($mm) constrarg($t) "[" ne_constrarg_list($l) "]" "." ] 
-  -> [(AddSemiRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
-      	   ($LIST $l))]
-.
-
 (* As an example, we provide an instantation for bool. *)
 (* Other instatiations are given in ArithRing and ZArithRing in the
    same directory *)
diff --git a/contrib/ring/Ring_abstract.v b/contrib/ring/Ring_abstract.v
index bd1fc79b66..f2fe16f3a1 100644
--- a/contrib/ring/Ring_abstract.v
+++ b/contrib/ring/Ring_abstract.v
@@ -459,7 +459,7 @@ Save.
 
 Hint rew_isacs_aux : core := Extern 10 (eqT A ? ?) Rewrite isacs_aux_ok.
 
-Tactic Definition Solve1 := 
+Tactic Definition Solve1 v v0 H H0 := 
   Simpl; Elim (varlist_lt v v0); Simpl; Rewrite isacs_aux_ok;
     [Rewrite H; Simpl; Auto
     |Simpl in H0; Rewrite H0; Auto ].
@@ -475,7 +475,7 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum)
 
   Auto.
 
-  Solve1.
+  Solve1 v v0 H H0.
 
   Simpl; Generalize (varlist_eq_prop v v0).
   Elim (varlist_eq v v0); Simpl.
@@ -491,7 +491,7 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum)
   Rewrite (Th_plus_zero_left T).
   Reflexivity.
 
-  Solve1.
+  Solve1 v v0 H H0.
 
   Induction y; Intros.
 
@@ -509,13 +509,13 @@ Lemma signed_sum_merge_ok : (x,y:signed_sum)
   Rewrite (Th_plus_zero_left T).
   Reflexivity.
 
-  Solve1.
+  Solve1 v v0 H H0.
 
-  Solve1.
+  Solve1 v v0 H H0.
 
 Save.
 
-Tactic Definition Solve2 :=
+Tactic Definition Solve2 l v H :=
  	Elim (varlist_lt l v); Simpl; Rewrite isacs_aux_ok;
   	[ Auto
   	| Rewrite H; Auto ].
@@ -529,7 +529,7 @@ Proof.
   Trivial.
 
   Simpl; Intros.
-  Solve2.
+  Solve2 l v H.
 
   Simpl; Intros.
   Generalize (varlist_eq_prop l v).
@@ -542,7 +542,7 @@ Proof.
   Rewrite (Th_plus_zero_left T).
   Reflexivity.
 
-  Solve2.
+  Solve2 l v H.
 
 Save.
 
@@ -567,9 +567,9 @@ Proof.
   Auto.
 
   Simpl; Intros.
-  Solve2.
+  Solve2 l v H.
 
-  Simpl; Intros; Solve2.
+  Simpl; Intros; Solve2 l v H.
 
 Save.
 
diff --git a/contrib/ring/Setoid_ring.v b/contrib/ring/Setoid_ring.v
index 59ccc43d32..5a25fbc1fe 100644
--- a/contrib/ring/Setoid_ring.v
+++ b/contrib/ring/Setoid_ring.v
@@ -2,6 +2,7 @@ Require Export Setoid_ring_theory.
 Require Export Quote.
 Require Export Setoid_ring_normalize.
 
+(*
 Declare ML Module "ring".
 
 Grammar tactic simple_tactic : ast :=
@@ -25,3 +26,4 @@ Grammar vernac vernac : ast :=
   -> [(AddSemiSetoidRing $a $aequiv $asetth $aplus $amult $aone $azero $aeq $pm $mm $t
       	   ($LIST $l))]
 .
+*)
diff --git a/contrib/ring/g_quote.ml4 b/contrib/ring/g_quote.ml4
new file mode 100644
index 0000000000..fdbfb4a724
--- /dev/null
+++ b/contrib/ring/g_quote.ml4
@@ -0,0 +1,18 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Quote
+
+TACTIC EXTEND Quote
+  [ "Quote" ident(f) ] -> [ quote f [] ]
+| [ "Quote" ident(f) "[" ne_ident_list(lc) "]"] -> [ quote f lc ]
+END
diff --git a/contrib/ring/g_ring.ml4 b/contrib/ring/g_ring.ml4
new file mode 100644
index 0000000000..e971815b54
--- /dev/null
+++ b/contrib/ring/g_ring.ml4
@@ -0,0 +1,135 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Quote
+open Ring
+
+TACTIC EXTEND Ring
+  [ "Ring" constr_list(l) ] -> [ polynom l ]
+END
+
+(* The vernac commands "Add Ring" and co *)
+
+let cset_of_comarg_list l = 
+  List.fold_right ConstrSet.add (List.map constr_of l) ConstrSet.empty
+
+VERNAC COMMAND EXTEND AddRing
+  [ "Add" "Ring" 
+          constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
+          constr(aopp) constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] 
+  -> [ add_theory true false false
+			 (constr_of a)
+			 None
+			 None
+			 None
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (Some (constr_of aopp))
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l) ]
+
+| [ "Add" "Semi" "Ring" 
+      	  constr(a) constr(aplus) constr(amult) constr(aone) constr(azero)
+          constr(aeq) constr(t) "[" ne_constr_list(l) "]" ] 
+  -> [ add_theory false false false
+			 (constr_of a)
+			 None
+			 None
+			 None
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 None
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l) ]
+
+| [ "Add" "Abstract" "Ring" 
+    	  constr(a) constr(aplus) constr(amult) constr(aone)
+          constr(azero) constr(aopp) constr(aeq) constr(t) ] 
+  -> [ add_theory true true false
+			 (constr_of a)
+			 None
+			 None
+			 None
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (Some (constr_of aopp))
+			 (constr_of aeq)
+			 (constr_of t)
+			 ConstrSet.empty ]
+
+| [ "Add" "Abstract" "Semi" "Ring" 
+          constr(a) constr(aplus) constr(amult) constr(aone)
+          constr(azero) constr(aeq) constr(t) ] 
+  -> [ add_theory false true false
+			 (constr_of a)
+			 None
+			 None
+			 None
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 None
+			 (constr_of aeq)
+			 (constr_of t)
+			 ConstrSet.empty ]
+
+| [ "Add" "Setoid" "Ring"
+      	  constr(a) constr(aequiv) constr(asetth) constr(aplus) constr(amult) 
+	  constr(aone) constr(azero) constr(aopp) constr(aeq) constr(pm)
+	  constr(mm) constr(om) constr(t) "[" ne_constr_list(l) "]" ] 
+  -> [ add_theory true false true
+			 (constr_of a)
+			 (Some (constr_of aequiv))
+			 (Some (constr_of asetth))
+			 (Some {
+			    plusm = (constr_of pm);
+			    multm = (constr_of mm);
+			    oppm = Some (constr_of om) })
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 (Some (constr_of aopp))
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l) ]
+
+| [ "Add" "Semi" "Setoid" "Ring" 
+          constr(a) constr(aequiv) constr(asetth) constr(aplus)
+	  constr(amult) constr(aone) constr(azero) constr(aeq) 
+          constr(pm) constr(mm) constr(t) "[" ne_constr_list(l) "]" ] 
+  -> [ add_theory false false true
+			 (constr_of a)
+			 (Some (constr_of aequiv))
+			 (Some (constr_of asetth))
+			 (Some {
+			    plusm = (constr_of pm);
+			    multm = (constr_of mm);
+			    oppm = None })
+			 (constr_of aplus)
+			 (constr_of amult)
+			 (constr_of aone)
+			 (constr_of azero)
+			 None
+			 (constr_of aeq)
+			 (constr_of t)
+			 (cset_of_comarg_list l) ]
+END
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 6bfc3f187a..ba02b232e0 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -8,10 +8,3 @@
 
 Require Omega.
 Require ReflOmegaCore.
-
-Grammar tactic simple_tactic : ast :=
-  romega [ "ROmega" ] -> [(ReflOmega)].
-
-Syntax tactic level 0:
-  romega [ (ReflOmega) ] -> ["ROmega"].   
-     
diff --git a/contrib/romega/g_romega.ml4 b/contrib/romega/g_romega.ml4
new file mode 100644
index 0000000000..b5203dcb72
--- /dev/null
+++ b/contrib/romega/g_romega.ml4
@@ -0,0 +1,17 @@
+(*************************************************************************
+
+   PROJET RNRT Calife - 2001
+   Author: Pierre Crégut - France Télécom R&D
+   Licence : LGPL version 2.1
+
+ *************************************************************************)
+
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Refl_omega
+
+TACTIC EXTEND ROmega
+  [ "ROmega" ] -> [ omega_solver ]
+END
diff --git a/contrib/xml/xmlcommand.ml4 b/contrib/xml/xmlcommand.ml4
index b794b28936..3c06c00dae 100644
--- a/contrib/xml/xmlcommand.ml4
+++ b/contrib/xml/xmlcommand.ml4
@@ -78,15 +78,16 @@ let extract_nparams pack =
 (* than that could exists in cooked form with the same name in a super        *)
 (* section of the actual section                                              *)
 let could_have_namesakes o sp =      (* namesake = omonimo in italian *)
+ let module N = Nametab in
  let module D = Declare in
   let tag = Libobject.object_tag o in
    print_if_verbose ("Object tag: " ^ tag ^ "\n") ;
    match tag with
       "CONSTANT" ->
         (match D.constant_strength sp with
-          | D.DischargeAt _  -> false (* a local definition *)
-          | D.NotDeclare     -> false (* not a definition *)
-          | D.NeverDischarge -> true  (* a non-local one    *)
+          | N.DischargeAt _  -> false (* a local definition *)
+          | N.NotDeclare     -> false (* not a definition *)
+          | N.NeverDischarge -> true  (* a non-local one    *)
         )
     | "PARAMETER"                 (* axioms and                               *)
     | "INDUCTIVE"       -> true   (* mutual inductive types are never local   *)
@@ -703,7 +704,7 @@ let pp_cmds_of_inner_types inner_types target_uri =
 (* Note: it is printed only (and directly) the most cooked available      *)
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
-let print qid fn =
+let print (_,qid as locqid) fn =
  let module D = Declarations in
  let module G = Global in
  let module N = Names in
@@ -711,7 +712,7 @@ let print qid fn =
  let module T = Term in
  let module X = Xml in
   let (_,id) = Nt.repr_qualid qid in
-  let glob_ref = Nametab.locate qid in
+  let glob_ref = Nametab.global locqid in
   let env = (Safe_typing.env_of_safe_env (G.safe_env ())) in
   reset_ids () ;
   let inner_types = ref [] in
@@ -976,7 +977,7 @@ let print_closed_section s ls dn =
 (* and terms of the module d                                                 *)
 (* Note: the terms are printed in their uncooked form plus the informations  *)
 (* on the parameters of their most cooked form                               *)
-let printModule qid dn =
+let printModule (loc,qid) dn =
  let module L = Library in
  let module N = Nametab in
  let module X = Xml in
diff --git a/contrib/xml/xmlentries.ml4 b/contrib/xml/xmlentries.ml4
new file mode 100644
index 0000000000..d812697023
--- /dev/null
+++ b/contrib/xml/xmlentries.ml4
@@ -0,0 +1,131 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+(******************************************************************************)
+(*                                                                            *)
+(*                               PROJECT HELM                                 *)
+(*                                                                            *)
+(*                     A module to print Coq objects in XML                   *)
+(*                                                                            *)
+(*                Claudio Sacerdoti Coen <sacerdot@cs.unibo.it>               *)
+(*                                 06/12/2000                                 *)
+(*                                                                            *)
+(* This module adds to the vernacular interpreter the functions that fullfill *)
+(* the new commands defined in Xml.v                                          *)
+(*                                                                            *)
+(******************************************************************************)
+(*i camlp4deps: "parsing/grammar.cma" i*)
+
+(* $Id$ *)
+
+open Util;;
+open Vernacinterp;;
+
+open Extend;;
+open Genarg;;
+open Pp;;
+open Pcoq;;
+
+(* File name *)
+
+let wit_filename, rawwit_filename = Genarg.create_arg "filename"
+let filename = Pcoq.create_generic_entry "filename" rawwit_filename
+let _ = Tacinterp.add_genarg_interp "filename"
+  (fun ist x ->
+    (in_gen wit_filename
+      (out_gen (wit_opt wit_string)
+	(Tacinterp.genarg_interp ist
+	  (in_gen (wit_opt rawwit_string)
+	    (out_gen rawwit_filename x))))))
+
+GEXTEND Gram
+  GLOBAL: filename;
+  filename: [ [ IDENT "File"; fn = STRING -> Some fn | -> None ] ];
+END
+
+let pr_filename = function Some fn -> str " File" ++ str fn | None -> mt ()
+
+let _ = 
+  Pptactic.declare_extra_genarg_pprule 
+    (rawwit_filename, pr_filename)
+    (wit_filename, pr_filename)
+
+(* Disk name *)
+
+let wit_diskname, rawwit_diskname = Genarg.create_arg "diskname"
+let diskname = create_generic_entry "diskname" rawwit_diskname
+let _ = Tacinterp.add_genarg_interp "diskname"
+  (fun ist x ->
+    (in_gen wit_diskname
+      (out_gen (wit_opt wit_string)
+	(Tacinterp.genarg_interp ist
+	  (in_gen (wit_opt rawwit_string)
+	    (out_gen rawwit_diskname x))))))
+
+GEXTEND Gram
+  GLOBAL: diskname;
+  diskname: [ [ IDENT "Disk"; fn = STRING -> Some fn | -> None ] ];
+END
+
+open Pp
+
+let pr_diskname = function Some fn -> str " Disk" ++ str fn | None -> mt ()
+
+let _ = 
+  Pptactic.declare_extra_genarg_pprule 
+    (rawwit_diskname, pr_diskname)
+    (wit_diskname, pr_diskname)
+
+VERNAC COMMAND EXTEND Xml
+| [ "Print" "XML" filename(fn) qualid(id) ] -> [ Xmlcommand.print id fn ]
+
+| [ "Show" "XML" filename(fn) "Proof" ] -> [ Xmlcommand.show fn ]
+
+| [ "Print" "XML" "All" ] -> [ Xmlcommand.printAll () ]
+
+| [ "Print" "XML" "Module" diskname(dn) qualid(id) ] ->
+    [ Xmlcommand.printModule id dn ]
+
+| [ "Print" "XML" "Section" diskname(dn) ident(id) ] ->
+    [ Xmlcommand.printSection id dn ]
+END
+(*
+vinterp_add "Print"
+ (function
+     [VARG_QUALID id] ->
+        (fun () -> Xmlcommand.print id None)
+   | [VARG_QUALID id ; VARG_STRING fn] ->
+        (fun () -> Xmlcommand.print id (Some fn))
+   | _ -> anomaly "This should be trapped");;
+
+vinterp_add "Show"
+ (function
+     [] ->
+        (fun () -> Xmlcommand.show None)
+   | [VARG_STRING fn] ->
+        (fun () -> Xmlcommand.show (Some fn))
+   | _ -> anomaly "This should be trapped");;
+
+vinterp_add "XmlPrintAll"
+ (function
+     [] -> (fun () -> Xmlcommand.printAll ())
+   | _  -> anomaly "This should be trapped");;
+
+vinterp_add "XmlPrintModule"
+ (function
+     [VARG_QUALID id] -> (fun () -> Xmlcommand.printModule id None)
+   | [VARG_QUALID id ; VARG_STRING dn] ->
+        (fun () -> Xmlcommand.printModule id (Some dn))
+   | _  -> anomaly "This should be trapped");;
+
+vinterp_add "XmlPrintSection"
+ (function
+     [VARG_IDENTIFIER id] -> (fun () -> Xmlcommand.printSection id None)
+   | [VARG_IDENTIFIER id ; VARG_STRING dn] ->
+        (fun () -> Xmlcommand.printSection id (Some dn))
+   | _  -> anomaly "This should be trapped");;
+*)