1 files changed, 247 insertions, 152 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 2812e36ed..470e21c82 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -18,6 +18,9 @@
 
 open Pp
 open Mutils
+open Proofview
+open Goptions
+open Proofview.Notations
 
 (**
   * Debug flag 
@@ -37,6 +40,53 @@ let time str f x =
 		     flush stdout);
   res
 
+
+(* Limit the proof search *)
+
+let max_depth = max_int
+
+(* Search limit for provers over Q R *)
+let lra_proof_depth = ref max_depth
+
+ 
+(* Search limit for provers over Z *)
+let lia_enum  = ref true
+let lia_proof_depth = ref max_depth
+
+let get_lia_option () =
+ (!lia_enum,!lia_proof_depth)
+
+let get_lra_option () =
+ !lra_proof_depth
+
+
+ 
+let _ =
+ 
+ let int_opt l vref =
+  {
+   optsync = true;
+   optdepr = false;
+   optname = List.fold_right (^) l "";
+   optkey  = l ;
+   optread = (fun () -> Some !vref);
+   optwrite = (fun x -> vref := (match x with None -> max_depth | Some v -> v))
+  } in
+
+ let lia_enum_opt = 
+  {
+   optsync = true;
+   optdepr = false;
+   optname = "Lia Enum";
+   optkey  = ["Lia";"Enum"];
+   optread = (fun () -> !lia_enum);
+   optwrite = (fun x -> lia_enum := x)
+  } in
+ ignore (declare_int_option (int_opt ["Lra"; "Depth"] lra_proof_depth)) ;
+ ignore (declare_int_option (int_opt ["Lia"; "Depth"] lia_proof_depth)) ;
+ ignore (declare_bool_option lia_enum_opt)
+
+ 
 (**
   * Initialize a tag type to the Tag module declaration (see Mutils).
   *)
@@ -359,6 +409,7 @@ struct
   let coq_Qmake = lazy (constant "Qmake")
 
   let coq_Rcst = lazy (constant "Rcst")
+
   let coq_C0   = lazy (m_constant "C0")
   let coq_C1   = lazy (m_constant "C1")
   let coq_CQ   = lazy (m_constant "CQ")
@@ -1094,10 +1145,6 @@ struct
    | N (a) -> Mc.N(f2f a)
    | I(a,_,b)  -> Mc.I(f2f a,f2f b)
 
-  let is_prop t =
-   match t with
-    | Names.Anonymous -> true (* Not quite right *)
-    | Names.Name x    -> false
 
   let mkC f1 f2 = C(f1,f2)
   let mkD f1 f2 = D(f1,f2)
@@ -1121,6 +1168,11 @@ struct
         (A(at,tg,t), env,Tag.next tg)
       with e when Errors.noncritical e -> (X(t),env,tg) in
 
+    let is_prop term =
+     let ty   = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in
+     let sort = Typing.sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in
+     Term.is_prop_sort sort in
+     
     let rec xparse_formula env tg term =
      match kind_of_term term with
       | App(l,rst) ->
@@ -1140,13 +1192,15 @@ struct
                let g,env,tg = xparse_formula env tg b in
                mkformula_binary mkIff term f g,env,tg
            | _ -> parse_atom env tg term)
-      | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b) ->
+      | Prod(typ,a,b) when not (Termops.dependent (mkRel 1) b)->
           let f,env,tg = xparse_formula env tg a in
           let g,env,tg = xparse_formula env tg b in
           mkformula_binary mkI term f g,env,tg
       | _ when eq_constr term (Lazy.force coq_True) -> (TT,env,tg)
       | _ when eq_constr term (Lazy.force coq_False) -> (FF,env,tg)
-      | _  -> X(term),env,tg in
+      | _ when is_prop term -> X(term),env,tg
+      | _ -> raise ParseError
+    in
     xparse_formula env tg  ((*Reductionops.whd_zeta*) term)
 
   let dump_formula typ dump_atom f =
@@ -1377,50 +1431,57 @@ let rcst_domain_spec  = lazy {
  dump_proof = dump_psatz coq_Q dump_q
 }
 
+open Proofview.Notations
+
+ 
 (**
   * Instanciate the current Coq goal with a Micromega formula, a varmap, and a
   * witness.
   *)
 
-
-
-let micromega_order_change spec cert cert_typ env ff : Tacmach.tactic = 
+let micromega_order_change spec cert cert_typ env ff  (*: unit Proofview.tactic*) = 
  let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in 
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in
  let ff  = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in
  let vm = dump_varmap (spec.typ) env in
- (* todo : directly generate the proof term - or generalize befor conversion? *)
- Tacticals.tclTHENSEQ [
-  (fun gl -> 
-   Proofview.V82.of_tactic (Tactics.change_concl
-   (set
-     [
-      ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-      ("__varmap", vm, Term.mkApp
-       (Coqlib.gen_constant_in_modules "VarMap"
-	 [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); 
-      ("__wit", cert, cert_typ)
-     ]
-     (Tacmach.pf_concl gl))) gl);
-  Tactics.generalize env ;
-  Tacticals.tclTHENSEQ (List.map (fun id -> Proofview.V82.of_tactic (Tactics.introduction id)) ids) ; 
- ] 
-
+ (* todo : directly generate the proof term - or generalize before conversion? *)
+  Proofview.Goal.nf_enter { enter = begin fun gl -> 
+   let gl = Tacmach.New.of_old (fun x -> x) gl in
+   Tacticals.New.tclTHENLIST
+    [
+     Tactics.change_concl
+    (set
+      [
+       ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+       ("__varmap", vm, Term.mkApp
+        (Coqlib.gen_constant_in_modules "VarMap"
+	[["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|spec.typ|])); 
+       ("__wit", cert, cert_typ)
+      ]
+      (Tacmach.pf_concl gl))
+   ;
+   Tactics.new_generalize env ;
+   Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
+  ] 
+  end }
 
 
 (**
   * The datastructures that aggregate prover attributes.
   *)
 
-type ('a,'prf) prover = {
+type ('option,'a,'prf) prover = {
   name : string ; (* name of the prover *)
-  prover : 'a list -> 'prf option ; (* the prover itself *)
+ get_option : unit ->'option ; (* find the options of the prover *)              
+ prover : 'option * 'a list -> 'prf option ; (* the prover itself *)
   hyps : 'prf -> ISet.t ; (* extract the indexes of the hypotheses really used in the proof *)
   compact : 'prf -> (int -> int) -> 'prf ; (* remap the hyp indexes according to function *)
   pp_prf : out_channel -> 'prf -> unit ;(* pretting printing of proof *)
   pp_f   : out_channel -> 'a   -> unit (* pretty printing of the formulas (polynomials)*)
 }
 
+
+ 
 (**
   * Given a list of provers and a disjunction of atoms, find a proof of any of
   * the atoms.  Returns an (optional) pair of a proof and a prover
@@ -1430,7 +1491,7 @@ type ('a,'prf) prover = {
 let find_witness provers polys1 =
   let provers = List.map (fun p ->
     (fun l ->
-      match p.prover l with
+      match p.prover (p.get_option (),l) with
         | None -> None
         | Some prf -> Some(prf,p)) , p.name) provers in
   try_any provers (List.map fst polys1)
@@ -1485,7 +1546,7 @@ let compact_proofs (cnf_ff: 'cst cnf) res (cnf_ff': 'cst cnf) =
     let res = try prover.compact prf remap with x when Errors.noncritical x ->
       if debug then Printf.fprintf stdout "Proof compaction %s" (Printexc.to_string x) ;
       (* This should not happen -- this is the recovery plan... *)
-      match prover.prover (List.map fst new_cl) with
+      match prover.prover (prover.get_option () ,List.map fst new_cl) with
         | None -> failwith "proof compaction error"
         | Some p ->  p
     in
@@ -1646,58 +1707,76 @@ let micromega_gen
     (negate:'cst atom -> 'cst mc_cnf)
     (normalise:'cst atom -> 'cst mc_cnf)
     unsat deduce 
-    spec prover gl =
-  let concl = Tacmach.pf_concl gl in
-  let hyps  = Tacmach.pf_hyps_types gl in
-  try
-   let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
-   let env = Env.elements env in
-   let spec = Lazy.force spec in
-
+    spec prover =
+ Proofview.Goal.nf_enter { enter = begin fun gl -> 
+    let gl = Tacmach.New.of_old (fun x -> x) gl in
+    let concl = Tacmach.pf_concl gl in
+    let hyps  = Tacmach.pf_hyps_types gl in
+    try
+     let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+     let env = Env.elements env in
+     let spec = Lazy.force spec in
+     
      match micromega_tauto  negate normalise unsat deduce spec prover env hyps concl gl with
-       | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl
-       | Some (ids,ff',res') -> 
-	   (Tacticals.tclTHENSEQ
-	      [
-		Tactics.generalize (List.map Term.mkVar ids) ;
-		micromega_order_change  spec res' 
-		  (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
-	      ]) gl
-  with
-   | ParseError  -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
-   | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
-      Tacticals.tclFAIL 0 (Pp.str 
-      (" Skipping what remains of this tactic: the complexity of the goal requires "
-      ^ "the use of a specialized external tool called csdp. \n\n" 
-      ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
-      ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) gl
-
-
-
-let micromega_order_changer cert env ff gl =
-  let coeff = Lazy.force coq_Rcst in
-  let dump_coeff = dump_Rcst in
-  let typ  = Lazy.force coq_R in
-  let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in
+     | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness")
+     | Some (ids,ff',res') -> 
+      (Tacticals.New.tclTHENLIST
+	[
+	 Tactics.new_generalize (List.map Term.mkVar ids) ;
+	 micromega_order_change  spec res' 
+	  (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env ff'
+	])
+    with
+    | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
+    | Mfourier.TimeOut  -> Tacticals.New.tclFAIL 0 (Pp.str "Timeout")
+    | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+     Tacticals.New.tclFAIL 0 (Pp.str 
+                           (" Skipping what remains of this tactic: the complexity of the goal requires "
+                            ^ "the use of a specialized external tool called csdp. \n\n" 
+                            ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
+                            ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
+  end }
+
+let micromega_gen parse_arith 
+    (negate:'cst atom -> 'cst mc_cnf)
+    (normalise:'cst atom -> 'cst mc_cnf)
+    unsat deduce 
+    spec prover  =
+ (micromega_gen parse_arith negate normalise unsat deduce spec prover)
+ 
+       
 
+let micromega_order_changer cert env ff  = 
+ let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__z"^(string_of_int i)))) 0 env in 
+ let coeff = Lazy.force coq_Rcst in
+ let dump_coeff = dump_Rcst in
+ let typ  = Lazy.force coq_R in
+ let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in
+ 
  let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in
  let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in
  let vm = dump_varmap (typ) env in
-  Proofview.V82.of_tactic (Tactics.change_concl
-   (set
+ Proofview.Goal.nf_enter { enter = begin fun gl -> 
+    let gl = Tacmach.New.of_old (fun x -> x) gl in
+    Tacticals.New.tclTHENLIST
      [
-      ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
-      ("__varmap", vm, Term.mkApp
-       (Coqlib.gen_constant_in_modules "VarMap"
-	 [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
-      ("__wit", cert, cert_typ)
+     (Tactics.change_concl
+      (set
+        [
+         ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |]));
+         ("__varmap", vm, Term.mkApp
+          (Coqlib.gen_constant_in_modules "VarMap"
+	    [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|]));
+         ("__wit", cert, cert_typ)
+        ]
+        (Tacmach.pf_concl gl)));
+      Tactics.new_generalize env ;
+      Tacticals.New.tclTHENLIST (List.map (fun id ->  (Tactics.introduction id)) ids)
      ]
-     (Tacmach.pf_concl gl)
-   ))
-   gl
+  end }
 
 
-let micromega_genr prover gl =
+let micromega_genr prover =
   let parse_arith = parse_rarith in
   let negate = Mc.rnegate in
   let normalise = Mc.rnormalise in
@@ -1710,39 +1789,41 @@ let micromega_genr prover gl =
     proof_typ = Lazy.force coq_QWitness ;
     dump_proof = dump_psatz coq_Q dump_q
   } in
-    
-  let concl = Tacmach.pf_concl gl in
-  let hyps  = Tacmach.pf_hyps_types gl in
-  try
-   let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
-   let env = Env.elements env in
-   let spec = Lazy.force spec in
-
-   let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in
-   let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in
-
-     match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl with
-       | None -> Tacticals.tclFAIL 0 (Pp.str " Cannot find witness") gl
+  Proofview.Goal.nf_enter { enter = begin fun gl -> 
+     let gl = Tacmach.New.of_old (fun x -> x) gl in
+     let concl = Tacmach.pf_concl gl in
+     let hyps  = Tacmach.pf_hyps_types gl in
+     try
+      let (hyps,concl,env) = parse_goal gl parse_arith Env.empty hyps concl in
+       let env = Env.elements env in
+       let spec = Lazy.force spec in
+       
+       let hyps' = List.map (fun (n,f) -> (n, map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) f)) hyps in
+       let concl' = map_atoms (Micromega.map_Formula Micromega.q_of_Rcst) concl in
+       
+       match micromega_tauto  negate normalise unsat deduce spec prover env hyps' concl' gl with
+       | None -> Tacticals.New.tclFAIL 0 (Pp.str " Cannot find witness") 
        | Some (ids,ff',res') -> 
            let (ff,ids') = formula_hyps_concl 
 	     (List.filter (fun (n,_) -> List.mem n ids) hyps) concl in
-
-           (Tacticals.tclTHENSEQ
+           (Tacticals.New.tclTHENLIST
               [
-                Tactics.generalize (List.map Term.mkVar ids) ;
+                Tactics.new_generalize (List.map Term.mkVar ids) ;
                 micromega_order_changer res' env (abstract_wrt_formula ff' ff)
-              ]) gl
+              ])
   with
-   | ParseError  -> Tacticals.tclFAIL 0 (Pp.str "Bad logical fragment") gl
-   | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
-      Tacticals.tclFAIL 0 (Pp.str 
+  | Mfourier.TimeOut     -> Tacticals.New.tclFAIL 0 (Pp.str "TimeOut")
+  | ParseError  -> Tacticals.New.tclFAIL 0 (Pp.str "Bad logical fragment")
+  | CsdpNotFound -> flush stdout ; Pp.pp_flush () ;
+      Tacticals.New.tclFAIL 0 (Pp.str 
       (" Skipping what remains of this tactic: the complexity of the goal requires "
       ^ "the use of a specialized external tool called csdp. \n\n" 
       ^ "Unfortunately Coq isn't aware of the presence of any \"csdp\" executable in the path. \n\n"
-      ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp")) gl
-
+       ^ "Csdp packages are provided by some OS distributions; binaries and source code can be downloaded from https://projects.coin-or.org/Csdp"))
+    end }
 
 
+let micromega_genr prover  = (micromega_genr prover)
 
 
 let lift_ratproof  prover l =
@@ -1898,38 +1979,61 @@ let compact_pt pt f =
 
 let lift_pexpr_prover p l =  p (List.map (fun (e,o) -> Mc.denorm e , o) l)
 
-let linear_prover_Z = {
-  name    = "linear prover" ;
-  prover  = lift_ratproof (lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.z_spec)) ;
-  hyps    = hyps_of_pt ;
-  compact = compact_pt ;
-  pp_prf  = pp_proof_term;
-  pp_f    = fun o x -> pp_pol pp_z o (fst x)
-}
+module CacheZ = PHashtable(struct
+ type prover_option = bool * int
 
+ type t = prover_option * ((Mc.z Mc.pol * Mc.op1) list)
+  let equal = (=)
+  let hash  = Hashtbl.hash
+end)
+
+module CacheQ = PHashtable(struct
+  type t = int * ((Mc.q Mc.pol * Mc.op1) list)
+  let equal = (=)
+  let hash  = Hashtbl.hash
+end)
+
+let memo_zlinear_prover = CacheZ.memo "lia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.lia ce b) s)
+let memo_nlia = CacheZ.memo "nlia.cache" (fun ((ce,b),s) -> lift_pexpr_prover (Certificate.nlia ce b) s)
+let memo_nra = CacheQ.memo "nra.cache" (fun (o,s) -> lift_pexpr_prover (Certificate.nlinear_prover o) s)
+
+
+ 
 let linear_prover_Q = {
-  name    = "linear prover";
-  prover  = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ;
-  hyps    = hyps_of_cone ;
-  compact = compact_cone ;
-  pp_prf  = pp_psatz pp_q ;
-  pp_f   = fun o x -> pp_pol pp_q o  (fst x)
+ name    = "linear prover";
+ get_option = get_lra_option ; 
+ prover  = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ;
+ hyps    = hyps_of_cone ;
+ compact = compact_cone ;
+ pp_prf  = pp_psatz pp_q ;
+ pp_f   = fun o x -> pp_pol pp_q o  (fst x)
 }
 
 
 let linear_prover_R = {
   name    = "linear prover";
-  prover  = lift_pexpr_prover (Certificate.linear_prover_with_cert Certificate.q_spec) ;
+ get_option = get_lra_option ; 
+ prover  = (fun (o,l) -> lift_pexpr_prover (Certificate.linear_prover_with_cert o Certificate.q_spec) l) ;
   hyps    = hyps_of_cone ;
   compact = compact_cone ;
   pp_prf  = pp_psatz pp_q ;
   pp_f    =  fun o x -> pp_pol pp_q o (fst x)
 }
 
+let nlinear_prover_R = {
+  name    = "nra";
+ get_option = get_lra_option;
+ prover  = memo_nra ;
+  hyps    = hyps_of_cone ;
+  compact = compact_cone ;
+  pp_prf  = pp_psatz pp_q ;
+  pp_f    =  fun o x -> pp_pol pp_q o (fst x)
+}
 
 let non_linear_prover_Q str o = {
   name    = "real nonlinear prover";
-  prover  = call_csdpcert_q (str, o);
+ get_option = (fun () -> (str,o));
+ prover  = (fun (o,l) -> call_csdpcert_q o l);
   hyps    = hyps_of_cone;
   compact = compact_cone ;
   pp_prf  = pp_psatz pp_q ;
@@ -1938,7 +2042,8 @@ let non_linear_prover_Q str o = {
 
 let non_linear_prover_R str o = {
   name    = "real nonlinear prover";
-  prover  = call_csdpcert_q (str, o);
+ get_option = (fun () -> (str,o));
+ prover  = (fun (o,l) -> call_csdpcert_q o l);
   hyps    = hyps_of_cone;
   compact = compact_cone;
   pp_prf  = pp_psatz pp_q;
@@ -1947,30 +2052,19 @@ let non_linear_prover_R str o = {
 
 let non_linear_prover_Z str o  = {
   name    = "real nonlinear prover";
-  prover  = lift_ratproof (call_csdpcert_z (str, o));
+ get_option = (fun () -> (str,o));
+ prover  = (fun (o,l) -> lift_ratproof (call_csdpcert_z o) l);
   hyps    = hyps_of_pt;
   compact = compact_pt;
   pp_prf  = pp_proof_term;
   pp_f    =  fun o x -> pp_pol pp_z o (fst x)
 }
 
-module CacheZ = PHashtable(struct
-  type t = (Mc.z Mc.pol * Mc.op1) list
-  let equal = Pervasives.(=)
-  let hash  = Hashtbl.hash
-end)
-
-let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.lia)
-let memo_nlia = CacheZ.memo "nlia.cache" (lift_pexpr_prover Certificate.nlia)
-
-(*let memo_zlinear_prover = (lift_pexpr_prover Lia.lia)*)
-(*let memo_zlinear_prover = CacheZ.memo "lia.cache" (lift_pexpr_prover Certificate.zlinear_prover)*)
-
-
 
 let linear_Z =   {
   name    = "lia";
-  prover  = memo_zlinear_prover ;
+ get_option = get_lia_option;
+ prover  = memo_zlinear_prover ;
   hyps    = hyps_of_pt;
   compact = compact_pt;
   pp_prf  = pp_proof_term;
@@ -1979,7 +2073,8 @@ let linear_Z =   {
 
 let nlinear_Z =   {
   name    = "nlia";
-  prover  = memo_nlia ;
+ get_option = get_lia_option;
+ prover  = memo_nlia ;
   hyps    = hyps_of_pt;
   compact = compact_pt;
   pp_prf  = pp_proof_term;
@@ -2001,56 +2096,56 @@ let tauto_lia ff =
   * solvers
   *)
 
-let psatzl_Z gl =
+let psatzl_Z =
  micromega_gen parse_zarith  Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
-  [ linear_prover_Z ] gl
+  [ linear_Z ] 
 
-let psatzl_Q gl =
+let psatzl_Q =
  micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
-  [ linear_prover_Q ] gl
+  [ linear_prover_Q ] 
 
-let psatz_Q i gl =
+let psatz_Q i  =
  micromega_gen parse_qarith Mc.qnegate Mc.qnormalise Mc.qunsat Mc.qdeduce qq_domain_spec
-  [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ] gl
-
-
-let psatzl_R gl =
- micromega_genr [ linear_prover_R ] gl
+  [ non_linear_prover_Q "real_nonlinear_prover" (Some i) ]
 
+let psatzl_R  =
+ micromega_genr [ linear_prover_R ]
 
-let psatz_R i gl =
- micromega_genr  [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] gl
+let psatz_R i  =
+ micromega_genr  [ non_linear_prover_R "real_nonlinear_prover" (Some i) ] 
 
 
-let psatz_Z i gl =
+let psatz_Z i  =
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
-      [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] gl
+      [ non_linear_prover_Z "real_nonlinear_prover" (Some i) ] 
 
-let sos_Z gl =
+let sos_Z  =
  micromega_gen parse_zarith Mc.negate Mc.normalise  Mc.zunsat Mc.zdeduce zz_domain_spec
-  [ non_linear_prover_Z "pure_sos" None ] gl
+  [ non_linear_prover_Z "pure_sos" None ] 
 
-let sos_Q gl =
+let sos_Q  =
  micromega_gen parse_qarith Mc.qnegate Mc.qnormalise  Mc.qunsat Mc.qdeduce qq_domain_spec
-  [ non_linear_prover_Q "pure_sos" None ] gl
+  [ non_linear_prover_Q "pure_sos" None ] 
 
 
-let sos_R gl =
- micromega_genr  [ non_linear_prover_R "pure_sos" None ] gl
+let sos_R  =
+ micromega_genr  [ non_linear_prover_R "pure_sos" None ] 
 
 
-let xlia gl =
+let xlia  =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
-      [ linear_Z ] gl
+      [ linear_Z ] 
   with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
-let xnlia gl =
+let xnlia  =
   try 
     micromega_gen parse_zarith Mc.negate Mc.normalise Mc.zunsat Mc.zdeduce zz_domain_spec
-      [ nlinear_Z ] gl
+      [ nlinear_Z ] 
   with reraise -> (*Printexc.print_backtrace stdout ;*) raise reraise
 
+let nra  = 
+ micromega_genr  [ nlinear_prover_R ] 
 
 
 (* Local Variables: *)