Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

43 files changed, 819 insertions, 814 deletions

diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index 48444509..0c906712 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modutil.ml 10665 2008-03-14 12:10:09Z soubiran $ i*)
+(*i $Id: modutil.ml 11262 2008-07-24 20:59:29Z letouzey $ i*)
 
 open Names
 open Declarations
@@ -347,6 +347,73 @@ and optim_me to_appear s = function
       MEapply (optim_me to_appear s me, optim_me to_appear s me')
   | MEfunctor (mbid,mt,me) -> MEfunctor (mbid,mt, optim_me to_appear s me)
 
-let optimize_struct to_appear struc = 
-  let subst = ref (Refmap.empty : ml_ast Refmap.t) in 
-  List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
+(* After these optimisations, some dependencies may not be needed anymore. 
+   For monolithic extraction, we recompute a minimal set of dependencies. *)
+
+exception NoDepCheck
+
+let base_r = function
+  | ConstRef c as r -> r
+  | IndRef (kn,_) -> IndRef (kn,0)
+  | ConstructRef ((kn,_),_) -> IndRef (kn,0)
+  | _ -> assert false
+
+let reset_needed, add_needed, found_needed, is_needed =
+  let needed = ref Refset.empty in
+  ((fun l -> needed := Refset.empty),
+   (fun r -> needed := Refset.add (base_r r) !needed),
+   (fun r -> needed := Refset.remove (base_r r) !needed),
+   (fun r -> Refset.mem (base_r r) !needed))
+
+let declared_refs = function
+  | Dind (kn,_) -> [|IndRef (kn,0)|]
+  | Dtype (r,_,_) -> [|r|]
+  | Dterm (r,_,_) -> [|r|]
+  | Dfix (rv,_,_) -> rv
+
+(* Computes the dependencies of a declaration, except in case 
+   of custom extraction. *)
+
+let compute_deps_decl = function
+  | Dind (kn,ind) ->
+      (* Todo Later : avoid dependencies when Extract Inductive *)
+      ind_iter_references add_needed add_needed add_needed kn ind
+  | Dtype (r,ids,t) ->
+      if not (is_custom r) then type_iter_references add_needed t
+  | Dterm (r,u,t) ->
+      type_iter_references add_needed t;
+      if not (is_custom r) then
+	ast_iter_references add_needed add_needed add_needed u
+  | Dfix _ as d ->
+      (* Todo Later : avoid dependencies when Extract Constant *)
+      decl_iter_references add_needed add_needed add_needed d
+
+let rec depcheck_se = function
+  | [] -> []
+  | ((l,SEdecl d) as t)::se ->
+      let se' = depcheck_se se in
+      let rv = declared_refs d in
+      if not (array_exists is_needed rv) then
+	(Array.iter remove_info_axiom rv; se')
+      else
+	(Array.iter found_needed rv; compute_deps_decl d; t::se')
+  | _ -> raise NoDepCheck
+
+let rec depcheck_struct = function
+  | [] -> []
+  | (mp,lse)::struc ->
+      let struc' = depcheck_struct struc in
+      let lse' = depcheck_se lse in
+      (mp,lse')::struc'
+
+let optimize_struct to_appear struc =
+  let subst = ref (Refmap.empty : ml_ast Refmap.t) in
+  let opt_struc =
+    List.map (fun (mp,lse) -> (mp, optim_se true to_appear subst lse)) struc
+  in
+  try
+    if modular () then raise NoDepCheck;
+    reset_needed ();
+    List.iter add_needed to_appear;
+    depcheck_struct opt_struc
+  with NoDepCheck -> opt_struc
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index abf461c1..10f669e1 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.ml 10348 2007-12-06 17:36:14Z aspiwack $ i*)
+(*i $Id: table.ml 11262 2008-07-24 20:59:29Z letouzey $ i*)
 
 open Names
 open Term
@@ -175,6 +175,7 @@ let info_axioms = ref Refset.empty
 let log_axioms = ref Refset.empty
 let init_axioms () = info_axioms := Refset.empty; log_axioms := Refset.empty
 let add_info_axiom r = info_axioms := Refset.add r !info_axioms
+let remove_info_axiom r = info_axioms := Refset.remove r !info_axioms
 let add_log_axiom r = log_axioms := Refset.add r !log_axioms
 
 (*s Extraction mode: modular or monolithic *)
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index ca02cb4d..4dbccd08 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: table.mli 10245 2007-10-21 13:41:53Z letouzey $ i*)
+(*i $Id: table.mli 11262 2008-07-24 20:59:29Z letouzey $ i*)
 
 open Names
 open Libnames
@@ -77,6 +77,7 @@ val is_projection : global_reference -> bool
 val projection_arity : global_reference -> int
 
 val add_info_axiom : global_reference -> unit
+val remove_info_axiom : global_reference -> unit
 val add_log_axiom : global_reference -> unit
 
 val reset_tables : unit -> unit
diff --git a/contrib/firstorder/sequent.ml b/contrib/firstorder/sequent.ml
index c832d30f..e931f8fd 100644
--- a/contrib/firstorder/sequent.ml
+++ b/contrib/firstorder/sequent.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: sequent.ml 10824 2008-04-21 13:57:03Z msozeau $ *)
+(* $Id: sequent.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Term
 open Util
@@ -281,7 +281,7 @@ let create_with_auto_hints l depth gl=
 	searchtable_map dbname
       with Not_found-> 
 	error ("Firstorder: "^dbname^" : No such Hint database") in
-      Hint_db.iter g (snd hdb) in
+      Hint_db.iter g hdb in
     List.iter h l;
     !seqref
 
diff --git a/contrib/funind/functional_principles_proofs.ml b/contrib/funind/functional_principles_proofs.ml
index 3d80bd00..bd335d30 100644
--- a/contrib/funind/functional_principles_proofs.ml
+++ b/contrib/funind/functional_principles_proofs.ml
@@ -136,7 +136,7 @@ let change_hyp_with_using msg hyp_id t tac : tactic =
   fun g -> 
     let prov_id = pf_get_new_id hyp_id g in 
     tclTHENS
-      ((* observe_tac msg *) (forward (Some  (tclCOMPLETE tac)) (Genarg.IntroIdentifier prov_id) t))
+      ((* observe_tac msg *) (forward (Some  (tclCOMPLETE tac)) (dummy_loc,Genarg.IntroIdentifier prov_id) t))
       [tclTHENLIST 
       [	
 	(* observe_tac "change_hyp_with_using thin" *) (thin [hyp_id]);
@@ -388,7 +388,7 @@ let clean_hyp_with_heq ptes_infos eq_hyps hyp_id env sigma =
 		     in
 (* 		     observe_tac "rec hyp " *)
 		       (tclTHENS
-		       (assert_as true (Genarg.IntroIdentifier rec_pte_id) t_x)
+		       (assert_as true (dummy_loc, Genarg.IntroIdentifier rec_pte_id) t_x)
 		       [
 			 (* observe_tac "prove rec hyp" *) (prove_rec_hyp eq_hyps);
 (* 			observe_tac "prove rec hyp" *)
@@ -571,7 +571,7 @@ let instanciate_hyps_with_args (do_prove:identifier list -> tactic) hyps args_id
 	fun g -> 
 	  let prov_hid = pf_get_new_id hid g in
 	  tclTHENLIST[
-	    forward None (Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
+	    forward None (dummy_loc,Genarg.IntroIdentifier prov_hid) (mkApp(mkVar hid,args));
 	    thin [hid];
 	    h_rename [prov_hid,hid]
 	  ] g
@@ -1399,7 +1399,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
 				      false
 				      (true,5)
 				      [Lazy.force refl_equal]
-				      [empty_transparent_state, Auto.Hint_db.empty]
+				      [Auto.Hint_db.empty false]
 				  )
 			   )
 			)
@@ -1497,7 +1497,7 @@ let prove_principle_for_gen
 	    (tclTHEN
 	       (forward 
 		  (Some ((fun g -> (* observe_tac "prove wf" *) (tclCOMPLETE (wf_tac is_mes)) g)))
-		  (Genarg.IntroIdentifier wf_thm_id)
+		  (dummy_loc,Genarg.IntroIdentifier wf_thm_id)
 		  (mkApp (delayed_force well_founded,[|input_type;relation|])))
 	       (
 		 (* observe_tac  *)
@@ -1561,7 +1561,7 @@ let prove_principle_for_gen
 	);
       (* observe_tac "" *) (forward
 	 (Some (prove_rec_arg_acc))
-	 (Genarg.IntroIdentifier acc_rec_arg_id)
+	 (dummy_loc,Genarg.IntroIdentifier acc_rec_arg_id)
  	 (mkApp (delayed_force acc_rel,[|input_type;relation;mkVar rec_arg_id|]))
       );
 (*       observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
diff --git a/contrib/funind/g_indfun.ml4 b/contrib/funind/g_indfun.ml4
index dae76f2d..d435f513 100644
--- a/contrib/funind/g_indfun.ml4
+++ b/contrib/funind/g_indfun.ml4
@@ -90,11 +90,6 @@ END
 TACTIC EXTEND newfunind
    ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> 
      [ 
-       let pat = 
-	 match pat with 
-	   | None -> IntroAnonymous
-	   | Some pat -> pat
-       in
        let c = match cl with 
 	 | [] -> assert false
 	 | [c] -> c 
@@ -106,11 +101,6 @@ END
 TACTIC EXTEND snewfunind
    ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] -> 
      [ 
-       let pat = 
-	 match pat with 
-	   | None -> IntroAnonymous
-	   | Some pat -> pat
-       in
        let c = match cl with 
 	 | [] -> assert false
 	 | [c] -> c 
@@ -319,7 +309,7 @@ let poseq_unsafe idunsafe cstr gl =
   tclTHEN
     (Tactics.letin_tac None (Name idunsafe) cstr allClauses)
     (tclTHENFIRST 
-      (Tactics.assert_as true IntroAnonymous (mkEq typ (mkVar idunsafe) cstr)) 
+      (Tactics.assert_as true (Util.dummy_loc,IntroAnonymous) (mkEq typ (mkVar idunsafe) cstr)) 
       Tactics.reflexivity)
     gl
   
@@ -396,7 +386,7 @@ let finduction (oid:identifier option) (heuristic: fapp_info list -> fapp_info l
 	      fun gl -> 
 		  (functional_induction 
 		    true (applist (info.fname, List.rev !list_constr_largs)) 
-		    None IntroAnonymous) gl)) 
+		    None None) gl)) 
 	  nexttac)) ordered_info_list in
   (* we try each (f t u v) until one does not fail *)
   (* TODO: try also to mix functional schemes *)
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml
index a6cbb321..79ef0097 100644
--- a/contrib/funind/indfun.ml
+++ b/contrib/funind/indfun.ml
@@ -120,7 +120,7 @@ let functional_induction with_clean c princl pat =
 	 princ_infos
 	 args_as_induction_constr
 	 princ'
-	 pat
+	 (None,pat)
          None)
       subst_and_reduce
       g
diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 63d44916..f62d70ab 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -280,13 +280,13 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       List.map
 	(fun (_,_,br_type) ->
 	   List.map
-	     (fun id -> Genarg.IntroIdentifier id)
+	     (fun id -> dummy_loc, Genarg.IntroIdentifier id)
 	     (generate_fresh_id (id_of_string "y") ids (List.length (fst (decompose_prod_assum br_type))))
 	)
 	branches
     in
     (* before building the full intro pattern for the principle *)
-    let pat = Genarg.IntroOrAndPattern intro_pats in
+    let pat = Some (dummy_loc,Genarg.IntroOrAndPattern intro_pats) in
     let eq_ind = Coqlib.build_coq_eq () in
     let eq_construct = mkConstruct((destInd eq_ind),1) in
     (* The next to referencies will be used to find out which constructor to apply in each branch *)
@@ -297,7 +297,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       (* We get the identifiers of this branch *)
       let this_branche_ids =
 	List.fold_right
-	  (fun pat acc ->
+	  (fun (_,pat) acc ->
 	     match pat with
 	       | Genarg.IntroIdentifier id -> Idset.add id acc
 	       | _ -> anomaly "Not an identifier"
@@ -447,7 +447,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem
       [ observe_tac "intro args_names" (tclMAP h_intro args_names);
 	observe_tac "principle" (forward
 	  (Some (h_exact f_principle))
-	  (Genarg.IntroIdentifier principle_id)
+	  (dummy_loc,Genarg.IntroIdentifier principle_id)
 	  princ_type);
 	tclTHEN_i
 	  (observe_tac "functional_induction" (
@@ -948,7 +948,7 @@ let functional_inversion kn hid fconst f_correct : tactic =
 	    h_generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])];
 	    thin [hid];
 	    h_intro hid;
-	    Inv.inv FullInversion Genarg.IntroAnonymous (Rawterm.NamedHyp hid);
+	    Inv.inv FullInversion None (Rawterm.NamedHyp hid);
 	    (fun g ->
 	       let new_ids = List.filter (fun id -> not (Idset.mem id old_ids)) (pf_ids_of_hyps g) in 
 	       tclMAP (revert_graph kn pre_tac)  (hid::new_ids)  g
diff --git a/contrib/funind/recdef.ml b/contrib/funind/recdef.ml
index c9bf2f1f..5bd7a6b2 100644
--- a/contrib/funind/recdef.ml
+++ b/contrib/funind/recdef.ml
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: recdef.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: recdef.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Term
 open Termops
@@ -1157,7 +1157,7 @@ let rec introduce_all_values_eq cont_tac functional termine
       [] ->
        let heq2 = next_global_ident_away true heq_id ids in
 	tclTHENLIST
-	  [forward None (IntroIdentifier heq2)
+	  [forward None (dummy_loc,IntroIdentifier heq2)
              (mkApp(mkVar heq1, [|f_S(f_S(mkVar pmax))|]));
            simpl_iter (onHyp heq2);
            unfold_in_hyp [((true,[1]), evaluable_of_global_reference 
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml
index 6ec0fac4..767a7dd6 100644
--- a/contrib/interface/blast.ml
+++ b/contrib/interface/blast.ml
@@ -161,21 +161,22 @@ let rec e_trivial_fail_db db_list local_db goal =
 	  let d = pf_last_hyp g' in
 	  let hintl = make_resolve_hyp (pf_env g') (project g') d in
           (e_trivial_fail_db db_list
-	     (add_hint_list hintl local_db) g'))) ::
+	     (Hint_db.add_list hintl local_db) g'))) ::
     (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) )
   in 
   tclFIRST (List.map tclCOMPLETE tacl) goal 
 
 and e_my_find_search db_list local_db hdc concl = 
   let hdc = head_of_constr_reference hdc in
-  let flags = Auto.auto_unif_flags in
   let hintl =
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x))
-	(Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> List.map (fun x -> ({flags with Unification.modulo_delta = st}, x)) 
-	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in 
   let tac_of_hint = 
     fun (st, ({pri=b; pat = p; code=t} as _patac)) -> 
@@ -279,7 +280,7 @@ module MySearchProblem = struct
 	     let hintl = 
 	       make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
 	     in
-             let ldb = add_hint_list hintl (List.hd s.localdb) in
+             let ldb = Hint_db.add_list hintl (List.hd s.localdb) in
 	     { depth = s.depth; tacres = res; 
 	       last_tactic = pp; dblist = s.dblist;
 	       localdb = ldb :: List.tl s.localdb })
@@ -375,7 +376,7 @@ let rec trivial_fail_db db_list local_db gl =
     tclTHEN intro 
       (fun g'->
 	 let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g')
-	 in trivial_fail_db db_list (add_hint_list hintl local_db) g')
+	 in trivial_fail_db db_list (Hint_db.add_list hintl local_db) g')
   in
   tclFIRST 
     (assumption::intro_tac::
@@ -383,14 +384,15 @@ let rec trivial_fail_db db_list local_db gl =
 	(trivial_resolve db_list local_db (pf_concl gl)))) gl
 
 and my_find_search db_list local_db hdc concl =
-  let flags = Auto.auto_unif_flags in
   let tacl = 
     if occur_existential concl then 
-      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x) 
-	(Hint_db.map_all hdc db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_all hdc db)) (local_db::db_list)
     else 
-      list_map_append (fun (st, db) -> List.map (fun x -> {flags with Unification.modulo_delta = st}, x)
-	(Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
+      list_map_append (fun db -> 
+	let flags = {Auto.auto_unif_flags with Unification.modulo_delta = Hint_db.transparent_state db} in
+	  List.map (fun x -> flags, x) (Hint_db.map_auto (hdc,concl) db)) (local_db::db_list)
   in
   List.map 
     (fun (st, {pri=b; pat=p; code=t} as _patac) -> 
@@ -477,7 +479,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal =
 	   with Failure _ -> [] 
 	 in
          (free_try
-	  (search_gen decomp n db_list (add_hint_list hintl local_db) [d])
+	  (search_gen decomp n db_list (Hint_db.add_list hintl local_db) [d])
 	  g'))
   in
   let rec_tacs = 
diff --git a/contrib/interface/depends.ml b/contrib/interface/depends.ml
index dd40c5cc..203bc9e3 100644
--- a/contrib/interface/depends.ml
+++ b/contrib/interface/depends.ml
@@ -57,8 +57,7 @@ let explore_tree pfs =
   and explain_prim = function
     | Refine c -> "Refine " ^ (string_of_ppcmds (Printer.prterm c))
     | Intro identifier -> "Intro"
-    | Intro_replacing identifier -> "Intro_replacing"
-    | Cut (bool, identifier, types) -> "Cut"
+    | Cut (bool, _, identifier, types) -> "Cut"
     | FixRule (identifier, int, l) -> "FixRule"
     | Cofix (identifier, l) -> "Cofix"
     | Convert_concl (types, cast_kind) -> "Convert_concl"
@@ -269,7 +268,7 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
 	     igtal
 	     acc)
     | TacMatch (_, tac, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match not implemented yet"
-    | TacMatchContext (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
+    | TacMatchGoal (_, _, tacexpr_mrl) -> failwith "depends_of_tacexpr of a Match Context not implemented yet"
     | TacFun tacfa -> depends_of_tac_fun_ast tacfa acc
     | TacArg tacarg -> depends_of_tac_arg tacarg acc
   and depends_of_atomic_tacexpr atexpr acc = let depends_of_'constr_with_bindings = depends_of_'a_with_bindings depends_of_'constr in match atexpr with
@@ -281,7 +280,8 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacExact          c
     | TacExactNoCheck   c
     | TacVmCastNoCheck  c  -> depends_of_'constr c acc
-    | TacApply (_, _, cb) -> depends_of_'constr_with_bindings cb acc
+    | TacApply (_, _, [cb]) -> depends_of_'constr_with_bindings cb acc
+    | TacApply (_, _, _) -> failwith "TODO"
     | TacElim (_, cwb, cwbo) ->
 	depends_of_'constr_with_bindings cwb
 	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
@@ -302,14 +302,13 @@ let rec depends_of_gen_tactic_expr depends_of_'constr depends_of_'ind depends_of
     | TacLetTac (_,c,_,_) -> depends_of_'constr c acc
 
     (* Derived basic tactics *)
-    | TacSimpleInduction _
-    | TacSimpleDestruct  _
+    | TacSimpleInductionDestruct _
     | TacDoubleInduction _ -> acc
-    | TacNewInduction (_, cwbial, cwbo, _, _)
-    | TacNewDestruct (_, cwbial, cwbo, _, _) ->
+    | TacInductionDestruct (_, _, [cwbial, cwbo, _, _]) ->
 	list_union_map (depends_of_'a_induction_arg depends_of_'constr_with_bindings)
 	  cwbial
 	  (Option.fold_right depends_of_'constr_with_bindings cwbo acc)
+    | TacInductionDestruct (_, _, _) -> failwith "TODO"
     | TacDecomposeAnd c
     | TacDecomposeOr  c -> depends_of_'constr c acc
     | TacDecompose (il, c) -> depends_of_'constr c (list_union_map depends_of_'ind il acc)
@@ -410,8 +409,7 @@ let depends_of_compound_rule cr acc = match cr with
 and depends_of_prim_rule pr acc = match pr with
   | Refine c                     -> depends_of_constr c acc
   | Intro id                     -> acc
-  | Intro_replacing id           -> acc
-  | Cut (_, _, t)                -> depends_of_constr t acc (* TODO: check what 2nd argument contains *)
+  | Cut (_, _, _, t)             -> depends_of_constr t acc (* TODO: check what 3nd argument contains *)
   | FixRule (_, _, l)            -> list_union_map (o depends_of_constr trd_of_3) l acc (* TODO: check what the arguments contain *)
   | Cofix (_, l)                 -> list_union_map (o depends_of_constr snd) l acc (* TODO: check what the arguments contain *)
   | Convert_concl (t, _)         -> depends_of_constr t acc
diff --git a/contrib/interface/pbp.ml b/contrib/interface/pbp.ml
index 06b957d9..65eadf13 100644
--- a/contrib/interface/pbp.ml
+++ b/contrib/interface/pbp.ml
@@ -48,7 +48,7 @@ type pbp_atom =
   | PbpTryClear of identifier list
   | PbpGeneralize of identifier * identifier list
   | PbpLApply of identifier (* = CutAndApply *)
-  | PbpIntros of intro_pattern_expr list
+  | PbpIntros of intro_pattern_expr located list
   | PbpSplit
   (* Existential *)
   | PbpExists of identifier
@@ -93,7 +93,7 @@ type pbp_rule = (identifier list *
                     pbp_sequence option;;
 
 
-let make_named_intro id = PbpIntros [IntroIdentifier id];;
+let make_named_intro id = PbpIntros [zz,IntroIdentifier id];;
 
 let make_clears str_list = PbpThen [PbpTryClear str_list]
 
@@ -171,7 +171,7 @@ let make_pbp_atomic_tactic = function
   | PbpRight -> TacAtom (zz, TacRight (false,NoBindings))
   | PbpIntros l -> TacAtom (zz, TacIntroPattern l)
   | PbpLApply h -> TacAtom (zz, TacLApply (make_var h))
-  | PbpApply h -> TacAtom (zz, TacApply (true,false,(make_var h,NoBindings)))
+  | PbpApply h -> TacAtom (zz, TacApply (true,false,[make_var h,NoBindings]))
   | PbpElim (hyp_name, names) ->
       let bind = List.map (fun s ->(zz,NamedHyp s,make_pbp_pattern s)) names in
       TacAtom
@@ -255,9 +255,9 @@ fun avoid c path -> match kind_of_term c, path with
 	or_and_tree_to_intro_pattern (id2::avoid) cont_expr path in
       let patt_list = 
 	if a = 1 then
-	  [cont_patt; IntroIdentifier id2]
+	  [zz,cont_patt; zz,IntroIdentifier id2]
 	else
-	  [IntroIdentifier id2; cont_patt] in
+	  [zz,IntroIdentifier id2; zz,cont_patt] in
       	(IntroOrAndPattern[patt_list], avoid_names, id, c, path, rank, 
 	 total_branches)
   | (App(oper, [|c1; c2|]), 2::3::path)
@@ -268,7 +268,7 @@ fun avoid c path -> match kind_of_term c, path with
 	     let id1 = next_global_ident x avoid in
 	     let cont_patt, avoid_names, id, c, path, rank, total_branches =
 	       or_and_tree_to_intro_pattern (id1::avoid) body path in
-	     (IntroOrAndPattern[[IntroIdentifier id1; cont_patt]],
+	     (IntroOrAndPattern[[zz,IntroIdentifier id1; zz,cont_patt]],
 	      avoid_names, id, c, path, rank, total_branches)
 	 | _ -> assert false)
   | (App(oper, [|c1; c2|]), 2::a::path)
@@ -282,9 +282,9 @@ fun avoid c path -> match kind_of_term c, path with
       let new_rank = if a = 1 then rank else rank+1 in
       let patt_list =
 	if a = 1 then
-	  [[cont_patt];[IntroIdentifier id2]]
+	  [[zz,cont_patt];[zz,IntroIdentifier id2]]
 	else
-	  [[IntroIdentifier id2];[cont_patt]] in
+	  [[zz,IntroIdentifier id2];[zz,cont_patt]] in
 	(IntroOrAndPattern patt_list, 
 	 avoid_names, id, c, path, new_rank, total_branches+1)
   | (_, path) -> let id = next_global_ident hyp_radix avoid in
@@ -305,13 +305,13 @@ let (imply_intro3: pbp_rule) = function
       let intro_patt, avoid_names, id, c, p, rank, total_branches =
 	or_and_tree_to_intro_pattern avoid prem path in
 	if total_branches = 1 then
-	  Some(chain_tactics [PbpIntros [intro_patt]]
+	  Some(chain_tactics [PbpIntros [zz,intro_patt]]
 		 (f avoid_names clear_names clear_flag (Some id)
 		    (kind_of_term c) path))
 	else
 	  Some
 	    (PbpThens
-	       ([PbpIntros [intro_patt]],
+	       ([PbpIntros [zz,intro_patt]],
 	    	auxiliary_goals clear_names clear_flag id
 		  (rank - 1)
 		  ((f avoid_names clear_names clear_flag (Some id)
@@ -667,7 +667,7 @@ let rec cleanup_clears str_list = function
 
 let rec optim3_aux str_list = function
     (PbpGeneralize (h,l1))::
-    (PbpIntros [IntroIdentifier s])::(PbpGeneralize (h',l2))::others
+    (PbpIntros [zz,IntroIdentifier s])::(PbpGeneralize (h',l2))::others
       when s=h' ->
       optim3_aux (s::str_list) (PbpGeneralize (h,l1@l2)::others)
   | (PbpTryClear names)::other ->
diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml
index 953fb5e7..4b9c1332 100644
--- a/contrib/interface/showproof.ml
+++ b/contrib/interface/showproof.ml
@@ -1197,12 +1197,12 @@ let rec natural_ntree ig ntree =
 	  | TacAssumption -> natural_trivial ig lh g gs ltree
 	  | TacClear _ -> natural_clear ig lh g gs ltree
 (* Besoin de l'argument de la tactique *)
-	  | TacSimpleInduction (NamedHyp id) -> 
+	  | TacSimpleInductionDestruct (true,NamedHyp id) -> 
               natural_induction ig lh g gs ge id ltree false
 	  | TacExtend (_,"InductionIntro",[a]) -> 
               let id=(out_gen wit_ident a) in
               natural_induction ig lh g gs ge id ltree true
-	  | TacApply (_,false,(c,_)) -> natural_apply ig lh g gs (snd c) ltree
+	  | TacApply (_,false,[c,_]) -> natural_apply ig lh g gs (snd c) ltree
 	  | TacExact c -> natural_exact ig lh g gs (snd c) ltree
 	  | TacCut c -> natural_cut ig lh g gs (snd c) ltree
 	  | TacExtend (_,"CutIntro",[a]) ->
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7d1f57fe..da4908e5 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -615,8 +615,7 @@ let get_flag r =
   (* Rem: EVAR flag obsolčte *)
   conv_flags, red_ids
 
-let rec xlate_intro_pattern =
- function
+let rec xlate_intro_pattern (loc,pat) = match pat with
   | IntroOrAndPattern [] -> assert false
   | IntroOrAndPattern (fp::ll) ->
       CT_disj_pattern
@@ -684,8 +683,8 @@ let xlate_one_unfold_block = function
 ;;
 
 let xlate_with_names = function
-    IntroAnonymous -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
-  | fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
+    None -> CT_coerce_ID_OPT_to_INTRO_PATT_OPT ctv_ID_OPT_NONE
+  | Some fp -> CT_coerce_INTRO_PATT_to_INTRO_PATT_OPT (xlate_intro_pattern fp)
 
 let rawwit_main_tactic = Pcoq.rawwit_tactic Pcoq.tactic_main_level
 
@@ -829,11 +828,11 @@ and xlate_tactic =
                          | [] -> assert false
                          | fst::others ->
                              CT_match_tac_rules(fst, others))
-   | TacMatchContext (_,_,[]) | TacMatchContext (true,_,_) -> failwith ""
-   | TacMatchContext (false,false,rule1::rules) ->
+   | TacMatchGoal (_,_,[]) | TacMatchGoal (true,_,_) -> failwith ""
+   | TacMatchGoal (false,false,rule1::rules) ->
          CT_match_context(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
-   | TacMatchContext (false,true,rule1::rules) ->
+   | TacMatchGoal (false,true,rule1::rules) ->
          CT_match_context_reverse(xlate_context_rule rule1,
                           List.map xlate_context_rule rules)
    | TacLetIn (false, l, t) ->
@@ -926,23 +925,26 @@ and xlate_tac =
     | TacExtend (_,"contradiction",[]) -> CT_contradiction
     | TacDoubleInduction (n1, n2) ->
 	CT_tac_double (xlate_quantified_hypothesis n1, xlate_quantified_hypothesis n2)
-    | TacExtend (_,"discriminate", [idopt]) ->
+    | TacExtend (_,"discriminate", []) ->
+     CT_discriminate_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
+    | TacExtend (_,"discriminate", [id]) ->
      CT_discriminate_eq
          (xlate_quantified_hypothesis_opt
-	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
-    | TacExtend (_,"simplify_eq", [idopt]) ->
-	let idopt1 = out_gen (wit_opt rawwit_quant_hyp) idopt in
-	let idopt2 = match idopt1 with
-	    None -> CT_coerce_ID_OPT_to_ID_OR_INT_OPT
-		(CT_coerce_NONE_to_ID_OPT CT_none)
-	  | Some v ->
-	      CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
-	      	(xlate_quantified_hypothesis v) in
-	  CT_simplify_eq idopt2
-    | TacExtend (_,"injection", [idopt]) ->
+	    (Some (out_gen rawwit_quant_hyp id)))
+    | TacExtend (_,"simplify_eq", []) ->
+	  CT_simplify_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT
+		(CT_coerce_NONE_to_ID_OPT CT_none))
+    | TacExtend (_,"simplify_eq", [id]) ->
+	let id1 = out_gen rawwit_quant_hyp id in
+	let id2 = CT_coerce_ID_OR_INT_to_ID_OR_INT_OPT
+	      	(xlate_quantified_hypothesis id1) in
+	  CT_simplify_eq id2
+    | TacExtend (_,"injection", []) ->
+     CT_injection_eq (CT_coerce_ID_OPT_to_ID_OR_INT_OPT ctv_ID_OPT_NONE)
+    | TacExtend (_,"injection", [id]) ->
      CT_injection_eq
          (xlate_quantified_hypothesis_opt
-	    (out_gen (wit_opt rawwit_quant_hyp) idopt))
+	    (Some (out_gen rawwit_quant_hyp id)))
     | TacExtend (_,"injection_as", [idopt;ipat]) ->
 	xlate_error "TODO: injection as"
     | TacFix (idopt, n) ->
@@ -967,19 +969,22 @@ and xlate_tac =
 	CT_intros_until (CT_coerce_ID_to_ID_OR_INT (xlate_ident id))
     | TacIntrosUntil (AnonHyp n) -> 
 	CT_intros_until (CT_coerce_INT_to_ID_OR_INT (CT_int n))
-    | TacIntroMove (Some id1, Some (_,id2)) ->
-     CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_ident id2)
-    | TacIntroMove (None, Some (_,id2)) ->
-	CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_ident id2)
-    | TacMove (true, id1, id2) ->
+    | TacIntroMove (Some id1, MoveAfter id2) ->
+     CT_intro_after(CT_coerce_ID_to_ID_OPT (xlate_ident id1),xlate_hyp id2)
+    | TacIntroMove (None, MoveAfter id2) ->
+	CT_intro_after(CT_coerce_NONE_to_ID_OPT CT_none, xlate_hyp id2)
+    | TacMove (true, id1, MoveAfter id2) ->
 	CT_move_after(xlate_hyp id1, xlate_hyp id2)
     | TacMove (false, id1, id2) -> xlate_error "Non dep Move is only internal"
+    | TacMove _ -> xlate_error "TODO: move before, at top, at bottom"
     | TacIntroPattern patt_list ->
 	CT_intros
 	  (CT_intro_patt_list (List.map xlate_intro_pattern patt_list))
-    | TacIntroMove (Some id, None) ->
+    | TacIntroMove (Some id, MoveToEnd true) ->
      CT_intros (CT_intro_patt_list[CT_coerce_ID_to_INTRO_PATT(xlate_ident id)])
-    | TacIntroMove (None, None) ->  CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
+    | TacIntroMove (None, MoveToEnd true) ->
+	CT_intro (CT_coerce_NONE_to_ID_OPT CT_none)
+    | TacIntroMove _ -> xlate_error "TODO"
     | TacLeft (false,bindl) -> CT_left (xlate_bindings bindl)
     | TacRight (false,bindl) -> CT_right (xlate_bindings bindl)
     | TacSplit (false,false,bindl) -> CT_split (xlate_bindings bindl)
@@ -1150,11 +1155,12 @@ and xlate_tac =
 	xlate_error "TODO: trivial using"
     | TacReduce (red, l) ->
      CT_reduce (xlate_red_tactic red, xlate_clause l)
-    | TacApply (true,false,(c,bindl)) ->
+    | TacApply (true,false,[c,bindl]) ->
      CT_apply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (true,true,(c,bindl)) ->
+    | TacApply (true,true,[c,bindl]) ->
      CT_eapply (xlate_formula c, xlate_bindings bindl)
-    | TacApply (false,_,_) -> xlate_error "TODO: simple (e)apply"
+    | TacApply (_,_,_) ->
+	xlate_error "TODO: simple (e)apply and iterated apply"
     | TacConstructor (false,n_or_meta, bindl) ->
 	let n = match n_or_meta with AI n -> n | MetaId _ -> xlate_error ""
 	in CT_constructor (CT_int n, xlate_bindings bindl)
@@ -1178,10 +1184,12 @@ and xlate_tac =
     | TacCase (false,(c1,sl)) ->
      CT_casetac (xlate_formula c1, xlate_bindings sl)
     | TacElim (true,_,_) | TacCase (true,_)
-    | TacNewDestruct (true,_,_,_,_) | TacNewInduction (true,_,_,_,_) ->
+    | TacInductionDestruct (_,true,_) ->
 	xlate_error "TODO: eelim, ecase, edestruct, einduction"
-    | TacSimpleInduction h -> CT_induction (xlate_quantified_hypothesis h)
-    | TacSimpleDestruct h -> CT_destruct (xlate_quantified_hypothesis h)
+    | TacSimpleInductionDestruct (true,h) ->
+	CT_induction (xlate_quantified_hypothesis h)
+    | TacSimpleInductionDestruct (false,h) ->
+	CT_destruct (xlate_quantified_hypothesis h)
     | TacCut c -> CT_cut (xlate_formula c)
     | TacLApply c -> CT_use (xlate_formula c)
     | TacDecompose ([],c) ->
@@ -1222,19 +1230,16 @@ and xlate_tac =
 	CT_dauto(xlate_int_or_var_opt_to_int_opt a, xlate_int_opt b)
     | TacDAuto (a, b, _) ->
 	xlate_error "TODO: dauto using"
-    | TacNewDestruct(false,a,b,c,None) ->
+    | TacInductionDestruct(true,false,[a,b,(None,c),None]) ->
 	CT_new_destruct
 	  (List.map  xlate_int_or_constr a, xlate_using b, 
 	   xlate_with_names c)
-    | TacNewInduction(false,a,b,c,None) ->
+    | TacInductionDestruct(false,false,[a,b,(None,c),None]) ->
 	CT_new_induction
 	  (List.map xlate_int_or_constr a, xlate_using b,
 	   xlate_with_names c)
-    | TacNewDestruct(false,a,b,c,_) -> xlate_error "TODO: destruct in"
-    | TacNewInduction(false,a,b,c,_) ->xlate_error "TODO: induction in"
-    (*| TacInstantiate (a, b, cl) -> 
-        CT_instantiate(CT_int a, xlate_formula b,
-		       assert false) *)
+    | TacInductionDestruct(_,false,_) -> 
+	xlate_error "TODO: clause 'in' and full 'as' of destruct/induction"
     | TacLetTac (na, c, cl, true) when cl = nowhere -> 
         CT_pose(xlate_id_opt_aux na, xlate_formula c)
     | TacLetTac (na, c, cl, true) ->
@@ -1243,13 +1248,13 @@ and xlate_tac =
 		     but the structures are different *)
 		  xlate_clause cl)
     | TacLetTac (na, c, cl, false) -> xlate_error "TODO: remember"
-    | TacAssert (None, IntroIdentifier id, c) -> 
+    | TacAssert (None, (_,IntroIdentifier id), c) -> 
         CT_assert(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (None, IntroAnonymous, c) -> 
+    | TacAssert (None, (_,IntroAnonymous), c) -> 
         CT_assert(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
-    | TacAssert (Some (TacId []), IntroIdentifier id, c) -> 
+    | TacAssert (Some (TacId []), (_,IntroIdentifier id), c) -> 
         CT_truecut(xlate_id_opt ((0,0),Name id), xlate_formula c)
-    | TacAssert (Some (TacId []), IntroAnonymous, c) -> 
+    | TacAssert (Some (TacId []), (_,IntroAnonymous), c) -> 
         CT_truecut(xlate_id_opt ((0,0),Anonymous), xlate_formula c)
     | TacAssert _ ->
 	xlate_error "TODO: assert with 'as' and 'by' and pose proof with 'as'"
diff --git a/contrib/micromega/Micromegatac.v b/contrib/micromega/Psatz.v
index 13c7eace..b2dd9910 100644
--- a/contrib/micromega/Micromegatac.v
+++ b/contrib/micromega/Psatz.v
@@ -23,57 +23,53 @@ Require Export RingMicromega.
 Require Import VarMap.
 Require Tauto.
 
-Ltac micromegac dom d :=
+Ltac xpsatz dom d :=
   let tac := lazymatch dom with
   | Z => 
-    micromegap d ;
+    (sos_Z || psatz_Z d) ;
     intros __wit __varmap __ff ; 
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; 
     apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | R =>
-    rmicromegap d ;
+    (sos_R || psatz_R d) ;
     intros __wit __varmap __ff ; 
     change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; 
     apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
+  | Q =>
+      (sos_Q || psatz_Q d) ;
+    intros __wit __varmap __ff ; 
+    change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; 
+    apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | _ => fail "Unsupported domain"
   end in tac.
 
-Tactic Notation "micromega" constr(dom) int_or_var(n) := micromegac dom n.
-Tactic Notation "micromega" constr(dom) := micromegac dom ltac:-1.
+Tactic Notation "psatz" constr(dom) int_or_var(n) := xpsatz dom n.
+Tactic Notation "psatz" constr(dom) := xpsatz dom ltac:-1.
 
-Ltac zfarkas :=  omicronp ;
-  intros __wit __varmap __ff ; 
-  change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; 
-  apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
-
-Ltac omicron dom :=
+Ltac psatzl dom :=
   let tac := lazymatch dom with
   | Z =>
-    zomicronp ;
+    psatzl_Z ;
     intros __wit __varmap __ff ;
     change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; 
     apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | Q =>
-    qomicronp ; 
+    psatzl_Q ; 
     intros __wit __varmap __ff ; 
     change (Tauto.eval_f (Qeval_formula (@find Q 0%Q __varmap)) __ff) ; 
     apply (QTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | R => 
-    romicronp ;
+    psatzl_R ;
     intros __wit __varmap __ff ;
     change (Tauto.eval_f (Reval_formula (@find R 0%R __varmap)) __ff) ; 
     apply (RTautoChecker_sound __ff __wit); vm_compute ; reflexivity
   | _ => fail "Unsupported domain"
   end in tac.
 
-Ltac sos dom :=
-  let tac := lazymatch dom with
-  | Z =>
-    sosp ;
-    intros __wit __varmap __ff ;
-    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; 
-    apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity
-  | _ => fail "Unsupported domain"
-  end in tac.
 
 
+Ltac lia := 
+  xlia ;
+  intros __wit __varmap __ff ;
+    change (Tauto.eval_f (Zeval_formula (@find Z Z0 __varmap)) __ff) ; 
+      apply (ZTautoChecker_sound __ff __wit); vm_compute ; reflexivity.
diff --git a/contrib/micromega/QMicromega.v b/contrib/micromega/QMicromega.v
index 9e95f6c4..c054f218 100644
--- a/contrib/micromega/QMicromega.v
+++ b/contrib/micromega/QMicromega.v
@@ -16,38 +16,11 @@ Require Import OrderedRing.
 Require Import RingMicromega.
 Require Import Refl.
 Require Import QArith.
-Require Import Qring.
-
-(* Qsrt has been removed from the library ? *)
-Definition Qsrt : ring_theory 0 1 Qplus Qmult Qminus Qopp Qeq.
-Proof.
-  constructor.
-  exact Qplus_0_l.
-  exact Qplus_comm.
-  exact Qplus_assoc.
-  exact Qmult_1_l.
-  exact Qmult_comm.
-  exact Qmult_assoc.
-  exact Qmult_plus_distr_l.
-  reflexivity.
-  exact Qplus_opp_r.
-Qed.
-
-
-Add Ring Qring : Qsrt.
-
-Lemma Qmult_neutral : forall x , 0 * x == 0.
-Proof.
-  intros.
-  compute.
-  reflexivity.
-Qed.
-
-(* Is there any qarith database ? *)
+Require Import Qfield.
 
 Lemma Qsor : SOR 0 1 Qplus Qmult Qminus Qopp Qeq  Qle Qlt.
 Proof.
-  constructor; intros ; subst ; try (intuition (subst; auto  with qarith)).
+  constructor; intros ; subst ; try (intuition (subst; auto with qarith)).
   apply Q_Setoid.
   rewrite H ; rewrite H0 ; reflexivity.
   rewrite H ; rewrite H0 ; reflexivity.
@@ -67,45 +40,12 @@ Proof.
   destruct(Q_dec n m) as [[H1 |H1] | H1 ] ; tauto.
   apply (Qplus_le_compat  p p n m  (Qle_refl p) H).
   generalize (Qmult_lt_compat_r 0 n m H0 H).
-  rewrite Qmult_neutral.
+  rewrite Qmult_0_l.
   auto.
   compute in H.
   discriminate.
 Qed.
 
-Definition Qeq_bool (p q : Q) : bool := Zeq_bool (Qnum p * ' Qden q)%Z  (Qnum q * ' Qden p)%Z.
-
-Definition Qle_bool (x y : Q) : bool := Zle_bool (Qnum x * ' Qden y)%Z (Qnum y * ' Qden x)%Z.
-
-Require ZMicromega.
-
-Lemma Qeq_bool_ok : forall x y, Qeq_bool x y = true -> x == y.
-Proof.
-  intros.
-  unfold Qeq_bool in H.
-  unfold Qeq.
-  apply (Zeqb_ok  _ _ H).
-Qed.
-
-
-Lemma Qeq_bool_neq : forall x y, Qeq_bool x y = false -> ~ x == y.
-Proof.
-  unfold Qeq_bool,Qeq.
-  red ; intros ; subst.
-  rewrite H0 in H.
-  apply  (ZMicromega.Zeq_bool_neq _ _ H).
-  reflexivity.
-Qed.
-
-Lemma Qle_bool_imp_le : forall x y : Q, Qle_bool x y = true -> x <= y.
-Proof.
-  unfold Qle_bool, Qle.
-  intros.
-  apply Zle_bool_imp_le ; auto.
-Qed.
-  
-
-
 
 Lemma QSORaddon :
   SORaddon 0 1 Qplus Qmult Qminus Qopp  Qeq  Qle (* ring elements *)
@@ -115,7 +55,7 @@ Lemma QSORaddon :
 Proof.
   constructor.
   constructor ; intros ; try reflexivity.
-  apply Qeq_bool_ok ; auto.
+  apply Qeq_bool_eq; auto.
   constructor.
   reflexivity.
   intros x y.
@@ -173,9 +113,9 @@ match o with
 | OpEq =>  Qeq
 | OpNEq => fun x y  => ~ x == y
 | OpLe => Qle
-| OpGe => Qge
+| OpGe => fun x y => Qle y x
 | OpLt => Qlt
-| OpGt => Qgt
+| OpGt => fun x y => Qlt y x
 end.
 
 Definition Qeval_formula (e:PolEnv Q) (ff : Formula Q) :=
diff --git a/contrib/micromega/RMicromega.v b/contrib/micromega/RMicromega.v
index ef28db32..7c6969c2 100644
--- a/contrib/micromega/RMicromega.v
+++ b/contrib/micromega/RMicromega.v
@@ -76,12 +76,12 @@ Proof.
   apply mult_IZR.
   apply Ropp_Ropp_IZR.
   apply IZR_eq.
-  apply Zeqb_ok ; auto.
+  apply Zeq_bool_eq ; auto.
   apply R_power_theory.
   intros x y.
   intro.
   apply IZR_neq.
-  apply ZMicromega.Zeq_bool_neq ; auto.
+  apply Zeq_bool_neq ; auto.
   intros. apply IZR_le.  apply Zle_bool_imp_le. auto.
 Qed.
 
@@ -97,9 +97,34 @@ Definition INZ (n:N) : R :=
 Definition Reval_expr := eval_pexpr  Rplus Rmult Rminus Ropp IZR Nnat.nat_of_N pow.
 
 
-Definition Reval_formula :=
+Definition Reval_op2 (o:Op2) : R -> R -> Prop :=
+    match o with
+      | OpEq =>  @eq R
+      | OpNEq => fun x y  => ~ x = y
+      | OpLe => Rle
+      | OpGe => Rge
+      | OpLt => Rlt
+      | OpGt => Rgt
+    end.
+
+
+Definition Reval_formula (e: PolEnv R) (ff : Formula Z) :=
+  let (lhs,o,rhs) := ff in Reval_op2 o (Reval_expr e lhs) (Reval_expr e rhs).
+
+Definition Reval_formula' :=
   eval_formula  Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow.
 
+Lemma Reval_formula_compat : forall env f, Reval_formula env f <-> Reval_formula' env f.
+Proof.
+  intros.
+  unfold Reval_formula.
+  destruct f.
+  unfold Reval_formula'.
+  unfold Reval_expr.
+  split ; destruct Fop ; simpl ; auto.
+  apply Rge_le.
+  apply Rle_ge.
+Qed.
 
 Definition Reval_nformula :=
   eval_nformula 0 Rplus Rmult Rminus Ropp (@eq R) Rle Rlt IZR Nnat.nat_of_N pow.
@@ -139,8 +164,9 @@ Proof.
   unfold RTautoChecker.
   apply (tauto_checker_sound  Reval_formula Reval_nformula).
   apply Reval_nformula_dec.
-  intros. unfold Reval_formula. now apply (cnf_normalise_correct Rsor).
-  intros. unfold Reval_formula. now apply (cnf_negate_correct Rsor).
+  intros. rewrite Reval_formula_compat.
+  unfold Reval_formula'. now apply (cnf_normalise_correct Rsor).
+  intros. rewrite Reval_formula_compat. unfold Reval_formula. now apply (cnf_negate_correct Rsor).
   intros t w0.
   apply RWeakChecker_sound.
 Qed.
diff --git a/contrib/micromega/ZMicromega.v b/contrib/micromega/ZMicromega.v
index 94c83f73..0855925a 100644
--- a/contrib/micromega/ZMicromega.v
+++ b/contrib/micromega/ZMicromega.v
@@ -39,15 +39,6 @@ Proof.
   apply Zmult_lt_0_compat ; auto.
 Qed.
 
-Lemma Zeq_bool_neq : forall x y, Zeq_bool x y = false -> x <> y.
-Proof.
-  red ; intros.
-  subst.
-  unfold Zeq_bool in H.
-  rewrite Zcompare_refl  in H.
-  discriminate.
-Qed.
-
 Lemma ZSORaddon :
   SORaddon 0 1 Zplus Zmult Zminus Zopp  (@eq Z) Zle (* ring elements *)
   0%Z 1%Z Zplus Zmult Zminus Zopp (* coefficients *)
@@ -56,7 +47,7 @@ Lemma ZSORaddon :
 Proof.
   constructor.
   constructor ; intros ; try reflexivity.
-  apply Zeqb_ok ; auto.
+  apply Zeq_bool_eq ; auto.
   constructor.
   reflexivity.
   intros x y.
diff --git a/contrib/micromega/certificate.ml b/contrib/micromega/certificate.ml
index 88e882e6..f4efcd08 100644
--- a/contrib/micromega/certificate.ml
+++ b/contrib/micromega/certificate.ml
@@ -108,7 +108,7 @@ struct
   if compare_num v (Int 0) <> 0
   then 
    if Monomial.compare Monomial.const k = 0
-   then 	Printf.fprintf o "%s " (string_of_num v)
+   then         Printf.fprintf o "%s " (string_of_num v)
    else Printf.fprintf o "%s*%a " (string_of_num v) Monomial.pp k) p  
 
  (* Get the coefficient of monomial mn *)
@@ -304,8 +304,8 @@ let factorise_linear_cone c =
       (match pending with
        | None -> rebuild_cone l (Some e) 
        | Some p -> (match factorise p e with
-	  | None -> Mc.S_Add(p, rebuild_cone l (Some e))
-	  | Some f -> rebuild_cone l (Some f) )
+          | None -> Mc.S_Add(p, rebuild_cone l (Some e))
+          | Some f -> rebuild_cone l (Some f) )
       ) in
 
   (rebuild_cone (List.sort Pervasives.compare (cone_list c [])) None)
@@ -387,10 +387,10 @@ let build_linear_system l =
   (* I need at least something strictly positive *)
  let strict = {
   coeffs = Vect.from_list ((Big_int unit_big_int)::
-			    (List.map (fun (x,y) -> 
-			     match y with Mc.Strict -> 
-			      Big_int unit_big_int 
-			      | _ -> Big_int zero_big_int) l));
+                            (List.map (fun (x,y) -> 
+                             match y with Mc.Strict -> 
+                              Big_int unit_big_int 
+                              | _ -> Big_int zero_big_int) l));
   op = Ge ; cst = Big_int unit_big_int } in
   (* Add the positivity constraint *)
   {coeffs = Vect.from_list ([Big_int unit_big_int]) ; 
@@ -414,22 +414,22 @@ let make_certificate n_spec cert li =
       in
       let rec scalar_product cert l =
        match cert with
-	| [] -> Mc.S_Z
-	| c::cert -> match l with
-	   | [] -> failwith "make_certificate(1)"
-	   | i::l ->  
-	      let r = scalar_product cert l in
-	       match compare_big_int c  zero_big_int with
-		| -1 -> Mc.S_Add (
-		   Mc.S_Ideal (Mc.PEc ( bint_to_cst c), Mc.S_In (Ml2C.nat i)), 
-		   r)
-		| 0  -> r
-		| _ ->  Mc.S_Add (
-		   Mc.S_Mult (Mc.S_Pos (bint_to_cst c), Mc.S_In (Ml2C.nat i)),
-		   r) in
+        | [] -> Mc.S_Z
+        | c::cert -> match l with
+           | [] -> failwith "make_certificate(1)"
+           | i::l ->  
+              let r = scalar_product cert l in
+               match compare_big_int c  zero_big_int with
+                | -1 -> Mc.S_Add (
+                   Mc.S_Ideal (Mc.PEc ( bint_to_cst c), Mc.S_In (Ml2C.nat i)), 
+                   r)
+                | 0  -> r
+                | _ ->  Mc.S_Add (
+                   Mc.S_Mult (Mc.S_Pos (bint_to_cst c), Mc.S_In (Ml2C.nat i)),
+                   r) in
        
       Some ((factorise_linear_cone 
-	      (simplify_cone n_spec (Mc.S_Add (cst, scalar_product cert' li)))))
+              (simplify_cone n_spec (Mc.S_Add (cst, scalar_product cert' li)))))
 
 
 exception Found of Monomial.t
@@ -444,7 +444,7 @@ let raw_certificate l =
   with x -> 
    if debug 
    then (Printf.printf "raw certificate %s" (Printexc.to_string x);   
-	 flush stdout) ;
+         flush stdout) ;
    None
 
 
@@ -462,9 +462,9 @@ let linear_prover n_spec l  =
   (fun (x,_) -> if snd' x = Mc.NonEqual then true else false) li in
  let l' = List.map 
   (fun (c,i) -> let (Mc.Pair(x,y)) = c in 
-		 match y with 
-		   Mc.NonEqual -> failwith "cannot happen" 
-		  |  y -> ((dev_form n_spec x, y),i)) l' in
+                 match y with 
+                   Mc.NonEqual -> failwith "cannot happen" 
+                  |  y -> ((dev_form n_spec x, y),i)) l' in
   
   simple_linear_prover n_spec l' 
 
@@ -513,106 +513,228 @@ let rec remove_assoc p x l =
 
 let eq x y = Vect.compare x y = 0
 
-(* Beurk... this code is a shame *)
+let  remove e  l  = List.fold_left (fun l x -> if eq x e then l else x::l) [] l
 
-let rec zlinear_prover sys = xzlinear_prover [] sys
 
-and xzlinear_prover enum l :  (Mc.proofTerm option) = 
- match linear_prover z_spec l with
-  | Some prf ->  Some (Mc.RatProof prf)
-  | None     ->  
+(* The prover is (probably) incomplete --
+   only searching for naive cutting planes *)
+
+let candidates sys = 
+ let ll = List.fold_right (
+  fun (Mc.Pair(e,k)) r -> 
+   match k with 
+    | Mc.NonStrict -> (dev_form z_spec e , Ge)::r
+    | Mc.Equal     ->  (dev_form z_spec e , Eq)::r 
+       (* we already know the bound -- don't compute it again *)
+    | _     -> failwith "Cannot happen candidates") sys [] in
+
+ let (sys,var_mn) = make_linear_system ll in
+ let vars = mapi (fun _ i -> Vect.set i (Int 1) Vect.null) var_mn in
+  (List.fold_left (fun l cstr ->   
+   let gcd = Big_int (Vect.gcd cstr.coeffs) in
+    if gcd =/ (Int 1) && cstr.op = Eq 
+    then l 
+    else  (Vect.mul (Int 1 // gcd) cstr.coeffs)::l) [] sys) @ vars
+
+
+let rec xzlinear_prover planes sys = 
+ match linear_prover z_spec sys with
+  | Some prf -> Some (Mc.RatProof prf)
+  | None     -> (* find the candidate with the smallest range *)
+     (* Grrr - linear_prover is also calling 'make_linear_system' *)
      let ll = List.fold_right (fun (Mc.Pair(e,k)) r -> match k with 
        Mc.NonEqual -> r  
       | k -> (dev_form z_spec e , 
-	     match k with
-	      | Mc.Strict | Mc.NonStrict -> Ge 
-		 (* Loss of precision -- weakness of fourier*)
-	      | Mc.Equal              -> Eq
-	      | Mc.NonEqual -> failwith "Cannot happen") :: r) l [] in
-
-     let (sys,var) = make_linear_system ll in
-     let res = 
-      match Fourier.find_Q_interval sys with
-       | Some(i,x,j) -> if i =/ j 
-	 then Some(i,Vect.set x (Int 1) Vect.null,i) else None 
-       | None -> None in
-     let res = match res with
-      | None ->
-	 begin
-	  let candidates = List.fold_right 
-	   (fun cstr acc -> 
-	    let gcd = Big_int (Vect.gcd cstr.coeffs) in
-	    let vect = Vect.mul (Int 1 // gcd) cstr.coeffs in
-	     if mem eq vect enum then acc
-	     else ((vect,Fourier.optimise vect sys)::acc)) sys [] in
-	  let candidates = List.fold_left (fun l (x,i) -> 
-	   match i with 
-	     None -> (x,Empty)::l 
-	    | Some i ->  (x,i)::l) [] (candidates) in
-	   match List.fold_left (fun (x1,i1) (x2,i2) -> 
-	    if smaller_itv i1 i2 
-	    then (x1,i1) else (x2,i2)) (Vect.null,Itv(None,None)) candidates 
-	   with
-	    | (i,Empty) -> None
-	    | (x,Itv(Some i, Some j))  -> Some(i,x,j)
-	    | (x,Point n) ->  Some(n,x,n)
-	    |   x        ->   match Fourier.find_Q_interval sys with
-		 | None -> None
-		 | Some(i,x,j) -> 
-		    if i =/ j 
-		    then Some(i,Vect.set x (Int 1) Vect.null,i) 
-		    else None 
-	 end
-      |   _ -> res in
-
-      match res with 
+             match k with
+               Mc.NonStrict -> Ge 
+              | Mc.Equal              -> Eq
+              | Mc.Strict | Mc.NonEqual -> failwith "Cannot happen") :: r) sys [] in
+     let (ll,var) = make_linear_system ll in
+     let candidates = List.fold_left (fun  acc vect -> 
+      match Fourier.optimise vect ll with
+       | None -> acc
+       | Some i -> 
+(*	  Printf.printf "%s in %s\n" (Vect.string vect) (string_of_intrvl i) ; *)
+	  flush stdout ; 
+	  (vect,i) ::acc)  [] planes in
+
+     let smallest_interval = 
+      match List.fold_left (fun (x1,i1) (x2,i2) -> 
+       if smaller_itv i1 i2 
+       then (x1,i1) else (x2,i2)) (Vect.null,Itv(None,None)) candidates 
+      with
+       | (x,Itv(Some i, Some j))  -> Some(i,x,j)
+       | (x,Point n) ->  Some(n,x,n)
+       |   x        ->   None (* This might be a cutting plane *)
+      in
+      match smallest_interval with
        | Some (lb,e,ub) -> 
-	  let (lbn,lbd) = 
-	   (Ml2C.bigint (sub_big_int (numerator lb)  unit_big_int),
-	   Ml2C.bigint (denominator lb)) in
-	  let (ubn,ubd) = 
-	   (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) , 
-	   Ml2C.bigint (denominator ub)) in
-	  let expr = list_to_polynomial var (Vect.to_list e) in
-	   (match 
-	     (*x <= ub ->  x  > ub *)
-	     linear_prover  z_spec 
-	      (Mc.Pair(pplus (pmult (pconst ubd) expr) (popp (pconst  ubn)),
-		      Mc.NonStrict) :: l),
-	    (* lb <= x  -> lb > x *)
-	    linear_prover z_spec 
-	     (Mc.Pair( pplus  (popp (pmult  (pconst lbd) expr)) (pconst lbn) ,  
-		     Mc.NonStrict)::l) 
-	    with
-	     | Some cub , Some clb  ->   
-		(match zlinear_enum (e::enum)   expr 
-		  (ceiling_num lb)  (floor_num ub) l 
-		 with
-		 | None -> None
-		 | Some prf -> 
-		    Some (Mc.EnumProof(Ml2C.q lb,expr,Ml2C.q ub,clb,cub,prf)))
-	     | _ -> None
-	   )
+          let (lbn,lbd) = 
+           (Ml2C.bigint (sub_big_int (numerator lb)  unit_big_int),
+           Ml2C.bigint (denominator lb)) in
+          let (ubn,ubd) = 
+           (Ml2C.bigint (add_big_int unit_big_int (numerator ub)) , 
+           Ml2C.bigint (denominator ub)) in
+          let expr = list_to_polynomial var (Vect.to_list e) in
+           (match 
+             (*x <= ub ->  x  > ub *)
+             linear_prover  z_spec 
+              (Mc.Pair(pplus (pmult (pconst ubd) expr) (popp (pconst  ubn)),
+                      Mc.NonStrict) :: sys),
+            (* lb <= x  -> lb > x *)
+            linear_prover z_spec 
+             (Mc.Pair( pplus  (popp (pmult  (pconst lbd) expr)) (pconst lbn) ,  
+                     Mc.NonStrict)::sys) 
+            with
+             | Some cub , Some clb  ->   
+                (match zlinear_enum  (remove e planes)   expr 
+                  (ceiling_num lb)  (floor_num ub) sys 
+                 with
+                  | None -> None
+                  | Some prf -> 
+                     Some (Mc.EnumProof(Ml2C.q lb,expr,Ml2C.q ub,clb,cub,prf)))
+             | _ -> None
+           )
        |  _ -> None
-and xzlinear_enum enum expr clb cub l = 
+and zlinear_enum  planes expr clb cub l = 
  if clb >/  cub
  then Some Mc.Nil
  else 
   let pexpr = pplus (popp (pconst (Ml2C.bigint (numerator clb)))) expr in
   let sys' = (Mc.Pair(pexpr, Mc.Equal))::l in
-   match xzlinear_prover enum sys' with
+   (*let enum =  *)
+   match xzlinear_prover planes sys' with
     | None -> if debug then print_string "zlp?"; None
     | Some prf -> if debug then print_string "zlp!";
-    match zlinear_enum enum expr (clb +/ (Int 1)) cub l with
+    match zlinear_enum planes expr (clb +/ (Int 1)) cub l with
      | None -> None
      | Some prfl -> Some (Mc.Cons(prf,prfl))
 
-and zlinear_enum enum expr clb cub l = 
- let res = xzlinear_enum enum expr clb cub l in
-  if debug then Printf.printf "zlinear_enum %s %s -> %s\n" 
-   (string_of_num clb) 
-   (string_of_num cub) 
-   (match res with
-    | None -> "None"
-    | Some r -> "Some") ; res
+let zlinear_prover sys =  
+ let candidates = candidates sys in
+ (*  Printf.printf "candidates %d" (List.length candidates) ; *) 
+ xzlinear_prover candidates sys
+
+open Sos
+
+let rec scale_term t = 
+ match t with
+  | Zero    -> unit_big_int , Zero
+  | Const n ->  (denominator n) , Const (Big_int (numerator n))
+  | Var n   -> unit_big_int , Var n
+  | Inv _   -> failwith "scale_term : not implemented"
+  | Opp t   -> let s, t = scale_term t in s, Opp t
+  | Add(t1,t2) -> let s1,y1 = scale_term t1 and s2,y2 = scale_term t2 in
+    let g = gcd_big_int s1 s2 in
+    let s1' = div_big_int s1 g in
+    let s2' = div_big_int s2 g in
+    let e = mult_big_int g (mult_big_int s1' s2') in
+     if (compare_big_int e unit_big_int) = 0
+     then (unit_big_int, Add (y1,y2))
+     else 	e, Add (Mul(Const (Big_int s2'), y1),
+		       Mul (Const (Big_int s1'), y2))
+  | Sub _ -> failwith "scale term: not implemented"
+  | Mul(y,z) ->       let s1,y1 = scale_term y and s2,y2 = scale_term z in
+		       mult_big_int s1 s2 , Mul (y1, y2)
+  |  Pow(t,n) -> let s,t = scale_term t in
+		  power_big_int_positive_int s  n , Pow(t,n)
+  |   _ -> failwith "scale_term : not implemented"
+
+let scale_term t =
+ let (s,t') = scale_term t in
+  s,t'
+
+
+let get_index_of_ith_match f i l  =
+ let rec get j res l =
+  match l with
+   | [] -> failwith "bad index"
+   | e::l -> if f e
+     then 
+       (if j = i then res else get (j+1) (res+1) l )
+     else get j (res+1) l in
+  get 0 0 l
+
+
+let rec scale_certificate pos = match pos with
+ | Axiom_eq i ->  unit_big_int , Axiom_eq i
+ | Axiom_le i ->  unit_big_int , Axiom_le i
+ | Axiom_lt i ->   unit_big_int , Axiom_lt i
+ | Monoid l   -> unit_big_int , Monoid l
+ | Rational_eq n ->  (denominator n) , Rational_eq (Big_int (numerator n))
+ | Rational_le n ->  (denominator n) , Rational_le (Big_int (numerator n))
+ | Rational_lt n ->  (denominator n) , Rational_lt (Big_int (numerator n))
+ | Square t -> let s,t' =  scale_term t in 
+		mult_big_int s s , Square t'
+ | Eqmul (t, y) -> let s1,y1 = scale_term t and s2,y2 = scale_certificate y in
+		    mult_big_int s1 s2 , Eqmul (y1,y2)
+ | Sum (y, z) -> let s1,y1 = scale_certificate y 
+   and s2,y2 = scale_certificate z in
+   let g = gcd_big_int s1 s2 in
+   let s1' = div_big_int s1 g in
+   let s2' = div_big_int s2 g in
+    mult_big_int g (mult_big_int s1' s2'), 
+    Sum (Product(Rational_le (Big_int s2'), y1),
+	Product (Rational_le (Big_int s1'), y2))
+ | Product (y, z) -> 
+    let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in
+     mult_big_int s1 s2 , Product (y1,y2)
+
+
+open Micromega
+ let rec term_to_q_expr = function
+  | Const n ->  PEc (Ml2C.q n)
+  | Zero   ->  PEc ( Ml2C.q (Int 0))
+  | Var s   ->  PEX (Ml2C.index 
+		      (int_of_string (String.sub s 1 (String.length s - 1))))
+  | Mul(p1,p2) ->  PEmul(term_to_q_expr p1, term_to_q_expr p2)
+  | Add(p1,p2) ->   PEadd(term_to_q_expr p1, term_to_q_expr p2)
+  | Opp p ->   PEopp (term_to_q_expr p)
+  | Pow(t,n) ->  PEpow (term_to_q_expr t,Ml2C.n n)
+  | Sub(t1,t2) ->  PEsub (term_to_q_expr t1,  term_to_q_expr t2)
+  | _ -> failwith "term_to_q_expr: not implemented"
+
+let  q_cert_of_pos  pos = 
+ let rec _cert_of_pos = function
+   Axiom_eq i ->  Mc.S_In (Ml2C.nat i)
+  | Axiom_le i ->  Mc.S_In (Ml2C.nat i)
+  | Axiom_lt i ->  Mc.S_In (Ml2C.nat i)
+  | Monoid l  -> Mc.S_Monoid (Ml2C.list Ml2C.nat l)
+  | Rational_eq n | Rational_le n | Rational_lt n -> 
+     if compare_num n (Int 0) = 0 then Mc.S_Z else
+      Mc.S_Pos (Ml2C.q   n)
+  | Square t -> Mc.S_Square (term_to_q_expr  t)
+  | Eqmul (t, y) -> Mc.S_Ideal(term_to_q_expr t, _cert_of_pos y)
+  | Sum (y, z) -> Mc.S_Add  (_cert_of_pos y, _cert_of_pos z)
+  | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in
+  simplify_cone q_spec (_cert_of_pos pos)
+
+
+ let rec term_to_z_expr = function
+  | Const n ->  PEc (Ml2C.bigint (big_int_of_num n))
+  | Zero   ->  PEc ( Z0)
+  | Var s   ->  PEX (Ml2C.index 
+		      (int_of_string (String.sub s 1 (String.length s - 1))))
+  | Mul(p1,p2) ->  PEmul(term_to_z_expr p1, term_to_z_expr p2)
+  | Add(p1,p2) ->   PEadd(term_to_z_expr p1, term_to_z_expr p2)
+  | Opp p ->   PEopp (term_to_z_expr p)
+  | Pow(t,n) ->  PEpow (term_to_z_expr t,Ml2C.n n)
+  | Sub(t1,t2) ->  PEsub (term_to_z_expr t1,  term_to_z_expr t2)
+  | _ -> failwith "term_to_z_expr: not implemented"
+
+let  z_cert_of_pos  pos = 
+ let s,pos = (scale_certificate pos) in
+ let rec _cert_of_pos = function
+   Axiom_eq i ->  Mc.S_In (Ml2C.nat i)
+  | Axiom_le i ->  Mc.S_In (Ml2C.nat i)
+  | Axiom_lt i ->  Mc.S_In (Ml2C.nat i)
+  | Monoid l  -> Mc.S_Monoid (Ml2C.list Ml2C.nat l)
+  | Rational_eq n | Rational_le n | Rational_lt n -> 
+     if compare_num n (Int 0) = 0 then Mc.S_Z else
+      Mc.S_Pos (Ml2C.bigint (big_int_of_num  n))
+  | Square t -> Mc.S_Square (term_to_z_expr  t)
+  | Eqmul (t, y) -> Mc.S_Ideal(term_to_z_expr t, _cert_of_pos y)
+  | Sum (y, z) -> Mc.S_Add  (_cert_of_pos y, _cert_of_pos z)
+  | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in
+  simplify_cone z_spec (_cert_of_pos pos)
 
diff --git a/contrib/micromega/coq_micromega.ml b/contrib/micromega/coq_micromega.ml
index 29e2a183..02ff61a1 100644
--- a/contrib/micromega/coq_micromega.ml
+++ b/contrib/micromega/coq_micromega.ml
@@ -106,6 +106,7 @@ struct
      ["Coq" ; "micromega" ; "EnvRing"];
      ["Coq";"QArith"; "QArith_base"];
      ["Coq";"Reals" ; "Rdefinitions"];
+     ["Coq";"Reals" ; "Rpow_def"];
      ["LRing_normalise"]]
    
  let constant = gen_constant_in_modules "ZMicromega" coq_modules
@@ -163,6 +164,9 @@ struct
 
 
  let coq_Qmake = lazy (constant "Qmake")
+ let coq_R0    = lazy (constant "R0")
+ let coq_R1    = lazy (constant "R1")
+
 
  let coq_proofTerm = lazy (constant "ProofTerm")
  let coq_ratProof = lazy (constant "RatProof")
@@ -179,10 +183,36 @@ struct
  let coq_Zminus = lazy (constant "Zminus")
  let coq_Zopp = lazy (constant "Zopp")
  let coq_Zmult = lazy (constant "Zmult")
+ let coq_Zpower = lazy (constant "Zpower")
  let coq_N_of_Z = lazy 
   (gen_constant_in_modules "ZArithRing" 
     [["Coq";"setoid_ring";"ZArithRing"]] "N_of_Z")
 
+ let coq_Qgt = lazy (constant "Qgt")
+ let coq_Qge = lazy (constant "Qge")
+ let coq_Qle = lazy (constant "Qle")
+ let coq_Qlt = lazy (constant "Qlt")
+ let coq_Qeq = lazy (constant "Qeq")
+
+
+ let coq_Qplus = lazy (constant "Qplus")
+ let coq_Qminus = lazy (constant "Qminus")
+ let coq_Qopp = lazy (constant "Qopp")
+ let coq_Qmult = lazy (constant "Qmult")
+ let coq_Qpower = lazy (constant "Qpower")
+
+
+ let coq_Rgt = lazy (constant "Rgt")
+ let coq_Rge = lazy (constant "Rge")
+ let coq_Rle = lazy (constant "Rle")
+ let coq_Rlt = lazy (constant "Rlt")
+
+ let coq_Rplus = lazy (constant "Rplus")
+ let coq_Rminus = lazy (constant "Rminus")
+ let coq_Ropp = lazy (constant "Ropp")
+ let coq_Rmult = lazy (constant "Rmult")
+ let coq_Rpower = lazy (constant "pow")
+
 
  let coq_PEX = lazy (constant "PEX" )
  let coq_PEc = lazy (constant"PEc")
@@ -225,6 +255,7 @@ struct
   (gen_constant_in_modules "RingMicromega" 
     [["Coq" ; "micromega" ; "RingMicromega"] ; ["RingMicromega"] ] "Formula")
 
+
  type parse_error  = 
    | Ukn 
    | BadStr of string 
@@ -347,16 +378,11 @@ let dump_q q =
 
 let parse_q term =  
  match Term.kind_of_term term with
-  | Term.App(c, args) -> 
-     (
-      match Term.kind_of_term c with
-	Term.Construct((n,j),i) -> 
-      if Names.string_of_kn n  = "Coq.QArith.QArith_base#<>#Q"
-      then {Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
+  | Term.App(c, args) -> if c = Lazy.force coq_Qmake then
+	{Mc.qnum = parse_z args.(0) ; Mc.qden = parse_positive args.(1) }
       else raise ParseError
-       |  _ -> raise ParseError
-     )
-  |   _ -> raise ParseError
+  |  _ -> raise ParseError
+
   
  let rec parse_list parse_elt term = 
   let (i,c) = get_left_construct term in
@@ -466,19 +492,6 @@ let parse_q term =
    pp_cone o e
 
 
-
-
- let rec parse_op term = 
-  let (i,c) = get_left_construct term in
-   match i with
-    | 1 -> Mc.OpEq
-    | 2 -> Mc.OpLe
-    | 3 -> Mc.OpGe
-    | 4 -> Mc.OpGt
-    | 5 -> Mc.OpLt
-    | i -> raise ParseError
-
-
  let rec dump_op = function
   | Mc.OpEq-> Lazy.force coq_OpEq
   | Mc.OpNEq-> Lazy.force coq_OpNEq
@@ -510,68 +523,52 @@ let parse_q term =
 		dump_op o ; 
 		dump_expr typ dump_constant e2|])
 
+ let assoc_const x l = 
+  try 
+  snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+  with
+    Not_found -> raise ParseError
+
+ let zop_table = [ 
+  coq_Zgt, Mc.OpGt ; 
+  coq_Zge, Mc.OpGe ;
+  coq_Zlt, Mc.OpLt ;
+  coq_Zle, Mc.OpLe ]
+
+ let rop_table = [ 
+  coq_Rgt, Mc.OpGt ; 
+  coq_Rge, Mc.OpGe ;
+  coq_Rlt, Mc.OpLt ;
+  coq_Rle, Mc.OpLe ]
+
+ let qop_table = [ 
+  coq_Qlt, Mc.OpLt ;
+  coq_Qle, Mc.OpLe ;
+  coq_Qeq, Mc.OpEq
+ ]
 
 
  let parse_zop (op,args) =
   match kind_of_term op with
-   | Const x -> 
-      (match Names.string_of_con x with
-       | "Coq.ZArith.BinInt#<>#Zgt" -> (Mc.OpGt, args.(0), args.(1))
-       | "Coq.ZArith.BinInt#<>#Zge" -> (Mc.OpGe, args.(0), args.(1))
-       | "Coq.ZArith.BinInt#<>#Zlt" -> (Mc.OpLt, args.(0), args.(1))
-       | "Coq.ZArith.BinInt#<>#Zle" -> (Mc.OpLe, args.(0), args.(1))
-       (*| "Coq.Init.Logic#<>#not"    -> Mc.OpNEq  (* for backward compat *)*)
-       |   s -> raise ParseError
-      )
+   | Const x -> (assoc_const op zop_table, args.(0) , args.(1))
    |  Ind(n,0) -> 
-       (match Names.string_of_kn n with
-	| "Coq.Init.Logic#<>#eq" -> 
-	   if args.(0) <> Lazy.force coq_Z
-	   then raise ParseError
-	   else (Mc.OpEq, args.(1), args.(2))
-	|  _ -> raise ParseError)
+       if op = Lazy.force coq_Eq &&   args.(0) = Lazy.force coq_Z
+       then (Mc.OpEq, args.(1), args.(2))
+       else raise ParseError
    |   _ -> failwith "parse_zop"
 
 
  let parse_rop (op,args) =
-  try 
    match kind_of_term op with
-    | Const x -> 
-       (match Names.string_of_con x with
-	| "Coq.Reals.Rdefinitions#<>#Rgt" -> (Mc.OpGt, args.(0), args.(1))
-	| "Coq.Reals.Rdefinitions#<>#Rge" -> (Mc.OpGe, args.(0), args.(1))
-	| "Coq.Reals.Rdefinitions#<>#Rlt" -> (Mc.OpLt, args.(0), args.(1))
-	| "Coq.Reals.Rdefinitions#<>#Rle" -> (Mc.OpLe, args.(0), args.(1))
-	   (*| "Coq.Init.Logic#<>#not"-> Mc.OpNEq  (* for backward compat *)*)
-       |   s -> raise ParseError
-       )
+    | Const x -> (assoc_const op rop_table, args.(0) , args.(1))
     |  Ind(n,0) -> 
-	(match Names.string_of_kn n with
-	 | "Coq.Init.Logic#<>#eq" -> 
-	    (*   if args.(0) <> Lazy.force coq_R
-		 then raise ParseError
-		 else*) (Mc.OpEq, args.(1), args.(2))
-	 |  _ -> raise ParseError)
-    |   _ -> failwith "parse_rop"
-  with x -> 
-   (Pp.pp (Pp.str "parse_rop failure ") ; 
-    Pp.pp (Printer.prterm op) ; Pp.pp_flush ()) 
-   ; raise x
-
+       if op = Lazy.force coq_Eq &&   args.(0) = Lazy.force coq_R
+       then (Mc.OpEq, args.(1), args.(2))
+       else raise ParseError
+   |   _ -> failwith "parse_zop"
 
  let parse_qop (op,args) =
-  (
-   (match kind_of_term op with
-   | Const x -> 
-      (match Names.string_of_con x with
-       | "Coq.QArith.QArith_base#<>#Qgt" -> Mc.OpGt
-       | "Coq.QArith.QArith_base#<>#Qge" -> Mc.OpGe
-       | "Coq.QArith.QArith_base#<>#Qlt" -> Mc.OpLt
-       | "Coq.QArith.QArith_base#<>#Qle" -> Mc.OpLe
-       | "Coq.QArith.QArith_base#<>#Qeq" -> Mc.OpEq
-       |   s -> raise ParseError
-      )
-   |   _ -> failwith "parse_zop") , args.(0) , args.(1))
+   (assoc_const op qop_table, args.(0) , args.(1))
 
 
  module Env =
@@ -612,6 +609,14 @@ let parse_q term =
    | Ukn of string
 
 
+ let assoc_ops x l = 
+  try 
+    snd (List.find (fun (x',y) -> x = Lazy.force x') l)
+  with
+    Not_found -> Ukn "Oups"
+
+
+
  let parse_expr parse_constant parse_exp ops_spec env term = 
  if debug 
  then (Pp.pp (Pp.str "parse_expr: ");   
@@ -634,7 +639,7 @@ let parse_q term =
 	(
 	 match kind_of_term t with
 	  | Const c -> 
-	     ( match ops_spec (Names.string_of_con c) with
+	     ( match assoc_ops t ops_spec  with
 	      | Binop f -> combine env f (args.(0),args.(1))
 	      | Opp     -> let (expr,env) = parse_expr env args.(0) in
 			    (Mc.PEopp expr, env)
@@ -653,29 +658,29 @@ let parse_q term =
    parse_expr env term
     
 
-let zop_spec = function
- | "Coq.ZArith.BinInt#<>#Zplus"    -> Binop (fun x y -> Mc.PEadd(x,y))
- | "Coq.ZArith.BinInt#<>#Zminus"   -> Binop (fun x y -> Mc.PEsub(x,y)) 
- | "Coq.ZArith.BinInt#<>#Zmult"    -> Binop  (fun x y -> Mc.PEmul (x,y))
-  | "Coq.ZArith.BinInt#<>#Zopp"     ->  Opp
-  | "Coq.ZArith.Zpow_def#<>#Zpower" -> Power
-  |  s                                   -> Ukn s
+ let zop_spec = 
+   [ 
+     coq_Zplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+     coq_Zminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+     coq_Zmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
+     coq_Zopp   , Opp ; 
+     coq_Zpower , Power]
 
-let qop_spec = function
- | "Coq.QArith.QArith_base#<>#Qplus"    -> Binop (fun x y -> Mc.PEadd(x,y))
- | "Coq.QArith.QArith_base#<>#Qminus"   -> Binop (fun x y -> Mc.PEsub(x,y)) 
- | "Coq.QArith.QArith_base#<>#Qmult"    -> Binop  (fun x y -> Mc.PEmul (x,y)) 
-  | "Coq.QArith.QArith_base#<>#Qopp"     ->  Opp
-  | "Coq.QArith.QArith_base#<>#Qpower" -> Power
-  |  s                                   -> Ukn s
+let qop_spec = 
+  [
+     coq_Qplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+     coq_Qminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+     coq_Qmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
+     coq_Qopp   , Opp ; 
+     coq_Qpower , Power]
 
-let rop_spec = function
- | "Coq.Reals.Rdefinitions#<>#Rplus"    -> Binop (fun x y -> Mc.PEadd(x,y))
- | "Coq.Reals.Rdefinitions#<>#Rminus"   -> Binop (fun x y -> Mc.PEsub(x,y)) 
- | "Coq.Reals.Rdefinitions#<>#Rmult"    -> Binop  (fun x y -> Mc.PEmul (x,y))
- | "Coq.Reals.Rdefinitions#<>#Ropp"     -> Opp
- | "Coq.Reals.Rpow_def#<>#pow"          -> Power
- |  s                                        -> Ukn s
+let rop_spec = 
+  [
+     coq_Rplus , Binop (fun x y -> Mc.PEadd(x,y)) ;
+     coq_Rminus , Binop (fun x y -> Mc.PEsub(x,y)) ;
+     coq_Rmult  , Binop  (fun x y -> Mc.PEmul (x,y)) ; 
+     coq_Ropp   , Opp ; 
+     coq_Rpower , Power]
 
 
 
@@ -691,12 +696,12 @@ let rconstant term =
        Pp.pp (Pp.str "rconstant: ");
        Pp.pp (Printer.prterm  term); Pp.pp_flush ());
  match Term.kind_of_term term with
-  | Const x ->        
-     (match Names.string_of_con x with
-      | "Coq.Reals.Rdefinitions#<>#R0" -> Mc.Z0
-      | "Coq.Reals.Rdefinitions#<>#R1" -> Mc.Zpos Mc.XH
-      | _   -> raise ParseError
-     )
+  | Const x ->  
+      if term = Lazy.force coq_R0
+      then Mc.Z0
+      else if term = Lazy.force coq_R1
+      then Mc.Zpos Mc.XH
+      else raise ParseError
   |  _ -> raise ParseError
 
 
@@ -731,23 +736,6 @@ let parse_rexpr =
   
  (* generic parsing of arithmetic expressions *)
   
- let rec parse_conj parse_arith env term = 
-  match kind_of_term term with
-   | App(l,rst) -> 
-      (match kind_of_term l with
-       | Ind (n,_) -> 
-	  ( match Names.string_of_kn n with
-	   | "Coq.Init.Logic#<>#and" -> 
-	      let (e1,env) = parse_arith env rst.(0) in
-	      let (e2,env) = parse_conj parse_arith env rst.(1) in
-	       (Mc.Cons(e1,e2),env)
-	   |   _ -> (* This might be an equality *) 
-		let (e,env) = parse_arith env term in
-		 (Mc.Cons(e,Mc.Nil),env))
-       |  _ -> (* This is an arithmetic expression *)
-	   let (e,env) = parse_arith env term in
-	    (Mc.Cons(e,Mc.Nil),env))
-   |  _ -> failwith "parse_conj(2)"
 
 
 
@@ -850,46 +838,6 @@ let parse_rexpr =
    xdump f
     
 
- (* Backward compat *)
-
- let rec parse_concl parse_arith env term =
-  match kind_of_term term with
-   | Prod(_,expr,rst) -> (* a -> b *)
-      let (lhs,rhs,env) = parse_concl parse_arith env rst in
-      let (e,env) = parse_arith env expr in
-       (Mc.Cons(e,lhs),rhs,env)
-   | App(_,_) -> 
-      let (conj, env) = parse_conj parse_arith env term in
-       (Mc.Nil,conj,env)
-   |  Ind(n,_) -> 
-       (match (Names.string_of_kn n) with
-	| "Coq.Init.Logic#<>#False" -> (Mc.Nil,Mc.Nil,env)
-	|    s                           -> 
-	      print_string s ; flush stdout;
-	      failwith "parse_concl")
-   |  _ -> failwith "parse_concl"
-
-
- let rec parse_hyps parse_arith env goal_hyps hyps = 
-  match hyps with
-   | [] -> ([],goal_hyps,env)
-   | (i,t)::l -> 
-      let (li,lt,env) = parse_hyps parse_arith env goal_hyps l in
-       try 
-	let (c,env) = parse_arith env  t in
-	 (i::li, Mc.Cons(c,lt), env)
-       with  x -> 
-	(*(if debug then Printf.printf "parse_arith : %s\n" x);*)
-	(li,lt,env)
-
-
- let parse_goal parse_arith env hyps term = 
-  try
-   let (lhs,rhs,env) = parse_concl parse_arith env term in
-   let (li,lt,env) = parse_hyps parse_arith env lhs hyps in
-    (li,lt,rhs,env)
-  with Failure x -> raise ParseError
-   (* backward compat *)
 
 
  (* ! reverse the list of bindings *)
@@ -1235,8 +1183,8 @@ let lift_ratproof prover l =
   | Some c -> Some (Mc.RatProof c)
 
 
-type csdpcert = Certificate.Mc.z Certificate.Mc.coneMember option
-type micromega_polys = (Micromega.z Mc.pExpr, Mc.op1) Micromega.prod list
+type csdpcert = Sos.positivstellensatz option
+type micromega_polys = (Micromega.q Mc.pExpr, Mc.op1) Micromega.prod list
 type provername = string * int option
 
 let call_csdpcert provername poly =
@@ -1255,36 +1203,84 @@ let call_csdpcert provername poly =
   close_in ch_from; Sys.remove tmp_from;
   cert
 
-let omicron gl = 
+let rec z_to_q_expr e = 
+ match e with
+  | Mc.PEc z   -> Mc.PEc {Mc.qnum = z ; Mc.qden = Mc.XH}
+  | Mc.PEX x   -> Mc.PEX x
+  | Mc.PEadd(e1,e2) -> Mc.PEadd(z_to_q_expr e1, z_to_q_expr e2)
+  | Mc.PEsub(e1,e2) -> Mc.PEsub(z_to_q_expr e1, z_to_q_expr e2)
+  | Mc.PEmul(e1,e2) -> Mc.PEmul(z_to_q_expr e1, z_to_q_expr e2)
+  | Mc.PEopp(e) -> Mc.PEopp(z_to_q_expr e)
+  | Mc.PEpow(e,n) -> Mc.PEpow(z_to_q_expr e,n)
+
+
+let call_csdpcert_q provername poly = 
+ match call_csdpcert provername poly with
+  | None -> None
+  | Some cert -> 
+     let cert = Certificate.q_cert_of_pos cert in
+      match Mc.qWeakChecker (CamlToCoq.list (fun x -> x) poly)  cert with
+       | Mc.True -> Some cert
+       | Mc.False ->  (print_string "buggy certificate" ; flush stdout) ;None
+
+
+let call_csdpcert_z provername poly = 
+ let l = List.map (fun (Mc.Pair(e,o)) -> (Mc.Pair(z_to_q_expr e,o))) poly in
+  match call_csdpcert provername l with
+   | None -> None
+   | Some cert -> 
+      let cert = Certificate.z_cert_of_pos cert in
+       match Mc.zWeakChecker (CamlToCoq.list (fun x -> x) poly)  cert with
+	| Mc.True -> Some cert
+	| Mc.False ->  (print_string "buggy certificate" ; flush stdout) ;None
+
+
+
+
+let psatzl_Z gl = 
  micromega_gen parse_zarith  Mc.negate Mc.normalise zz_domain_spec
   [lift_ratproof 
     (Certificate.linear_prover Certificate.z_spec), "fourier refutation" ] gl
 
 
-let qomicron gl = 
+let psatzl_Q gl = 
  micromega_gen  parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec 
   [ Certificate.linear_prover Certificate.q_spec, "fourier refutation" ]   gl
 
-let romicron gl = 
+let psatz_Q i gl = 
+ micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise qq_domain_spec
+  [ call_csdpcert_q ("real_nonlinear_prover", Some i), "fourier refutation" ]  gl
+
+let psatzl_R gl = 
  micromega_gen  parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec 
   [ Certificate.linear_prover Certificate.z_spec, "fourier refutation" ]   gl
 
 
-let rmicromega i gl = 
- micromega_gen parse_rarith Mc.negate Mc.normalise rz_domain_spec
-  [ call_csdpcert ("real_nonlinear_prover", Some i), "fourier refutation" ]  gl
+let psatz_R i gl = 
+ micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise rz_domain_spec
+  [ call_csdpcert_z  ("real_nonlinear_prover", Some i), "fourier refutation" ]  gl
 
   
-let micromega i gl = 
+let psatz_Z i gl = 
  micromega_gen parse_zarith Mc.negate Mc.normalise zz_domain_spec 
- [lift_ratproof (call_csdpcert ("real_nonlinear_prover",Some i)), 
+ [lift_ratproof (call_csdpcert_z ("real_nonlinear_prover",Some i)), 
   "fourier refutation" ] gl
 
 
-let sos gl = 
+let sos_Z gl = 
  micromega_gen parse_zarith Mc.negate Mc.normalise  zz_domain_spec 
-  [lift_ratproof (call_csdpcert ("pure_sos", None)), "pure sos refutation"]  gl
+  [lift_ratproof (call_csdpcert_z ("pure_sos", None)), "pure sos refutation"]  gl
+
+let sos_Q gl = 
+ micromega_gen parse_qarith Mc.cnf_negate Mc.cnf_normalise  qq_domain_spec 
+  [call_csdpcert_q ("pure_sos", None), "pure sos refutation"]  gl
+
+let sos_R gl = 
+ micromega_gen parse_rarith Mc.cnf_negate Mc.cnf_normalise  rz_domain_spec 
+  [call_csdpcert_z ("pure_sos", None), "pure sos refutation"]  gl
+
+
 
-let zomicron gl = 
+let xlia gl = 
  micromega_gen parse_zarith Mc.negate Mc.normalise   zz_domain_spec 
   [Certificate.zlinear_prover, "zprover"] gl
diff --git a/contrib/micromega/csdpcert.ml b/contrib/micromega/csdpcert.ml
index cfaf6ae1..e451a38f 100644
--- a/contrib/micromega/csdpcert.ml
+++ b/contrib/micromega/csdpcert.ml
@@ -27,7 +27,7 @@ struct
  open Mc
 
  let rec expr_to_term = function
-  |  PEc z ->  Const  (Big_int (C2Ml.z_big_int z))
+  |  PEc z ->  Const  (C2Ml.q_to_num z)
   |  PEX v ->  Var ("x"^(string_of_int (C2Ml.index v)))
   |  PEmul(p1,p2) -> 
       let p1 = expr_to_term p1 in
@@ -40,25 +40,15 @@ struct
   |  PEopp p ->  Opp (expr_to_term p)
 
       
- let rec term_to_expr = function
-  | Const n ->  PEc (Ml2C.bigint (big_int_of_num n))
-  | Zero   ->  PEc ( Z0)
-  | Var s   ->  PEX (Ml2C.index 
-		      (int_of_string (String.sub s 1 (String.length s - 1))))
-  | Mul(p1,p2) ->  PEmul(term_to_expr p1, term_to_expr p2)
-  | Add(p1,p2) ->   PEadd(term_to_expr p1, term_to_expr p2)
-  | Opp p ->   PEopp (term_to_expr p)
-  | Pow(t,n) ->  PEpow (term_to_expr t,Ml2C.n n)
-  | Sub(t1,t2) ->  PEsub (term_to_expr t1,  term_to_expr t2)
-  | _ -> failwith "term_to_expr: not implemented"
-
- let term_to_expr e =
+
+
+(* let term_to_expr e =
   let e' = term_to_expr e in
    if debug 
    then Printf.printf "term_to_expr : %s - %s\n"  
     (string_of_poly (poly_of_term  e)) 
     (string_of_poly (poly_of_term (expr_to_term e')));
-   e'
+   e' *)
 
 end 
 open M      
@@ -66,110 +56,8 @@ open M
 open List
 open Mutils 
 
-let rec scale_term t = 
- match t with
-  | Zero    -> unit_big_int , Zero
-  | Const n ->  (denominator n) , Const (Big_int (numerator n))
-  | Var n   -> unit_big_int , Var n
-  | Inv _   -> failwith "scale_term : not implemented"
-  | Opp t   -> let s, t = scale_term t in s, Opp t
-  | Add(t1,t2) -> let s1,y1 = scale_term t1 and s2,y2 = scale_term t2 in
-    let g = gcd_big_int s1 s2 in
-    let s1' = div_big_int s1 g in
-    let s2' = div_big_int s2 g in
-    let e = mult_big_int g (mult_big_int s1' s2') in
-     if (compare_big_int e unit_big_int) = 0
-     then (unit_big_int, Add (y1,y2))
-     else 	e, Add (Mul(Const (Big_int s2'), y1),
-		       Mul (Const (Big_int s1'), y2))
-  | Sub _ -> failwith "scale term: not implemented"
-  | Mul(y,z) ->       let s1,y1 = scale_term y and s2,y2 = scale_term z in
-		       mult_big_int s1 s2 , Mul (y1, y2)
-  |  Pow(t,n) -> let s,t = scale_term t in
-		  power_big_int_positive_int s  n , Pow(t,n)
-  |   _ -> failwith "scale_term : not implemented"
-
-let scale_term t =
- let (s,t') = scale_term t in
-  s,t'
-   
-
 
 
-let rec scale_certificate pos = match pos with
- | Axiom_eq i ->  unit_big_int , Axiom_eq i
- | Axiom_le i ->  unit_big_int , Axiom_le i
- | Axiom_lt i ->   unit_big_int , Axiom_lt i
- | Monoid l   -> unit_big_int , Monoid l
- | Rational_eq n ->  (denominator n) , Rational_eq (Big_int (numerator n))
- | Rational_le n ->  (denominator n) , Rational_le (Big_int (numerator n))
- | Rational_lt n ->  (denominator n) , Rational_lt (Big_int (numerator n))
- | Square t -> let s,t' =  scale_term t in 
-		mult_big_int s s , Square t'
- | Eqmul (t, y) -> let s1,y1 = scale_term t and s2,y2 = scale_certificate y in
-		    mult_big_int s1 s2 , Eqmul (y1,y2)
- | Sum (y, z) -> let s1,y1 = scale_certificate y 
-   and s2,y2 = scale_certificate z in
-   let g = gcd_big_int s1 s2 in
-   let s1' = div_big_int s1 g in
-   let s2' = div_big_int s2 g in
-    mult_big_int g (mult_big_int s1' s2'), 
-    Sum (Product(Rational_le (Big_int s2'), y1),
-	Product (Rational_le (Big_int s1'), y2))
- | Product (y, z) -> 
-    let s1,y1 = scale_certificate y and s2,y2 = scale_certificate z in
-     mult_big_int s1 s2 , Product (y1,y2)
-
-
-let is_eq = function  Mc.Equal -> true | _ -> false
-let is_le = function  Mc.NonStrict -> true | _ -> false
-let is_lt = function  Mc.Strict -> true | _ -> false
-
-let get_index_of_ith_match f i l  =
- let rec get j res l =
-  match l with
-   | [] -> failwith "bad index"
-   | e::l -> if f e
-     then 
-       (if j = i then res else get (j+1) (res+1) l )
-     else get j (res+1) l in
-  get 0 0 l
-
-
-let  cert_of_pos eq le lt ll l pos = 
- let s,pos = (scale_certificate pos) in
- let rec _cert_of_pos = function
-   Axiom_eq i -> let idx = get_index_of_ith_match is_eq i l in
-		  Mc.S_In (Ml2C.nat idx)
-  | Axiom_le i -> let idx = get_index_of_ith_match is_le i l in
-		   Mc.S_In (Ml2C.nat idx)
-  | Axiom_lt i -> let idx = get_index_of_ith_match is_lt i l in
-		   Mc.S_In (Ml2C.nat idx)
-  | Monoid l  -> Mc.S_Monoid (Ml2C.list Ml2C.nat l)
-  | Rational_eq n | Rational_le n | Rational_lt n -> 
-     if compare_num n (Int 0) = 0 then Mc.S_Z else
-      Mc.S_Pos (Ml2C.bigint (big_int_of_num  n))
-  | Square t -> Mc.S_Square (term_to_expr  t)
-  | Eqmul (t, y) -> Mc.S_Ideal(term_to_expr t, _cert_of_pos y)
-  | Sum (y, z) -> Mc.S_Add  (_cert_of_pos y, _cert_of_pos z)
-  | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in
-  s, Certificate.simplify_cone Certificate.z_spec (_cert_of_pos pos)
-
-
-let  term_of_cert l pos = 
- let l = List.map fst' l in
- let rec _cert_of_pos = function
-  | Mc.S_In i -> expr_to_term (List.nth l (C2Ml.nat i))
-  | Mc.S_Pos p -> Const (C2Ml.num  p)
-  | Mc.S_Z     -> Const (Int 0)
-  | Mc.S_Square t -> Mul(expr_to_term t, expr_to_term t)
-  | Mc.S_Monoid m -> List.fold_right 
-     (fun x m -> Mul (expr_to_term (List.nth l (C2Ml.nat x)),m)) 
-     (C2Ml.list (fun x -> x) m)  (Const (Int 1))
-  | Mc.S_Ideal (t, y) -> Mul(expr_to_term t, _cert_of_pos y)
-  | Mc.S_Add (y, z) -> Add  (_cert_of_pos y, _cert_of_pos z)
-  | Mc.S_Mult (y, z) -> Mul (_cert_of_pos y, _cert_of_pos z) in
-  (_cert_of_pos pos)
 
 let rec canonical_sum_to_string = function s -> failwith "not implemented"
 
@@ -208,22 +96,6 @@ let rec sets_of_list l =
   | e::l -> let s = sets_of_list l in
 	     s@(List.map (fun s0 -> e::s0) s) 
 
-let  cert_of_pos  pos = 
- let s,pos = (scale_certificate pos) in
- let rec _cert_of_pos = function
-   Axiom_eq i ->  Mc.S_In (Ml2C.nat i)
-  | Axiom_le i ->  Mc.S_In (Ml2C.nat i)
-  | Axiom_lt i ->  Mc.S_In (Ml2C.nat i)
-  | Monoid l  -> Mc.S_Monoid (Ml2C.list Ml2C.nat l)
-  | Rational_eq n | Rational_le n | Rational_lt n -> 
-     if compare_num n (Int 0) = 0 then Mc.S_Z else
-      Mc.S_Pos (Ml2C.bigint (big_int_of_num  n))
-  | Square t -> Mc.S_Square (term_to_expr  t)
-  | Eqmul (t, y) -> Mc.S_Ideal(term_to_expr t, _cert_of_pos y)
-  | Sum (y, z) -> Mc.S_Add  (_cert_of_pos y, _cert_of_pos z)
-  | Product (y, z) -> Mc.S_Mult (_cert_of_pos y, _cert_of_pos z) in
-  s, Certificate.simplify_cone Certificate.z_spec (_cert_of_pos pos)
-
 (* The exploration is probably not complete - for simple cases, it works... *)
 let real_nonlinear_prover d l =
  try 
@@ -272,15 +144,7 @@ let real_nonlinear_prover d l =
 
   let proof = list_fold_right_elements 
    (fun s t -> Sum(s,t)) (proof_ne :: proofs_ideal @ proofs_cone) in
-   
-  let s,proof' = scale_certificate proof in
-  let cert  = snd (cert_of_pos proof') in
-   if debug 
-   then Printf.printf "cert poly : %s\n" 
-    (string_of_poly (poly_of_term (term_of_cert l cert)));
-   match Mc.zWeakChecker (Ml2C.list (fun x -> x) l)  cert with
-    | Mc.True -> Some cert
-    | Mc.False ->  (print_string "buggy certificate" ; flush stdout) ;None
+   Some proof
  with 
   | Sos.TooDeep -> None
 
@@ -300,16 +164,16 @@ let pure_sos  l =
 		     (term_of_poly p)), rst)) 
 		     polys (Rational_lt (Int 0))) in
   let proof = Sum(Axiom_lt i, pos) in
-  let s,proof' = scale_certificate proof in
-  let cert  = snd (cert_of_pos proof') in
-   Some cert
+(*  let s,proof' = scale_certificate proof in
+  let cert  = snd (cert_of_pos proof') in *)
+   Some proof
  with
   | Not_found -> (* This is no strict inequality *) None
   |  x        -> None
 
 
-type micromega_polys = (Micromega.z Mc.pExpr, Mc.op1) Micromega.prod list
-type csdp_certificate = Certificate.Mc.z Certificate.Mc.coneMember option
+type micromega_polys = (Micromega.q Mc.pExpr, Mc.op1) Micromega.prod list
+type csdp_certificate = Sos.positivstellensatz option
 type provername = string * int option
 
 let main () =
diff --git a/contrib/micromega/g_micromega.ml4 b/contrib/micromega/g_micromega.ml4
index 259b5d4b..50024e78 100644
--- a/contrib/micromega/g_micromega.ml4
+++ b/contrib/micromega/g_micromega.ml4
@@ -14,7 +14,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: g_micromega.ml4 10947 2008-05-19 19:10:40Z herbelin $ *)
+(* $Id: g_micromega.ml4 11306 2008-08-05 16:51:08Z notin $ *)
 
 open Quote
 open Ring
@@ -26,34 +26,49 @@ let out_arg = function
   | ArgVar _ -> anomaly "Unevaluated or_var variable"
   | ArgArg x -> x
 
-TACTIC EXTEND Micromega
-| [ "micromegap" int_or_var(i) ] -> [ Coq_micromega.micromega (out_arg i) ]
-| [ "micromegap" ] -> [ Coq_micromega.micromega (-1) ]
+TACTIC EXTEND PsatzZ
+| [ "psatz_Z" int_or_var(i) ] -> [ Coq_micromega.psatz_Z (out_arg i) ]
+| [ "psatz_Z" ] -> [ Coq_micromega.psatz_Z (-1) ]
 END
 
-TACTIC EXTEND Sos
-[ "sosp" ] -> [ Coq_micromega.sos]
+TACTIC EXTEND Sos_Z
+| [ "sos_Z" ] -> [ Coq_micromega.sos_Z]
+   END
+
+TACTIC EXTEND Sos_Q
+| [ "sos_Q" ] -> [ Coq_micromega.sos_Q]
+   END
+
+TACTIC EXTEND Sos_R
+| [ "sos_R" ] -> [ Coq_micromega.sos_R]
 END
 
 
 TACTIC EXTEND Omicron
-[ "omicronp"  ] -> [ Coq_micromega.omicron]
+[ "psatzl_Z"  ] -> [ Coq_micromega.psatzl_Z]
 END
 
 TACTIC EXTEND QOmicron
-[ "qomicronp"  ] -> [ Coq_micromega.qomicron]
+[ "psatzl_Q"  ] -> [ Coq_micromega.psatzl_Q]
 END
 
 
 TACTIC EXTEND ZOmicron
-[ "zomicronp"  ] -> [ Coq_micromega.zomicron]
+[ "xlia"  ] -> [ Coq_micromega.xlia]
 END
 
 TACTIC EXTEND ROmicron
-[ "romicronp"  ] -> [ Coq_micromega.romicron]
+[ "psatzl_R"  ] -> [ Coq_micromega.psatzl_R]
 END
 
 TACTIC EXTEND RMicromega
-| [ "rmicromegap" int_or_var(i) ] -> [ Coq_micromega.rmicromega (out_arg i) ]
-| [ "rmicromegap" ] -> [ Coq_micromega.rmicromega (-1) ]
+| [ "psatz_R" int_or_var(i) ] -> [ Coq_micromega.psatz_R (out_arg i) ]
+| [ "psatz_R" ] -> [ Coq_micromega.psatz_R (-1) ]
+END
+
+
+TACTIC EXTEND QMicromega
+| [ "psatz_Q" int_or_var(i) ] -> [ Coq_micromega.psatz_Q (out_arg i) ]
+| [ "psatz_Q" ] -> [ Coq_micromega.psatz_Q (-1) ]
 END
+
diff --git a/contrib/romega/ROmega.v b/contrib/romega/ROmega.v
index 68bc43bb..4281cc57 100644
--- a/contrib/romega/ROmega.v
+++ b/contrib/romega/ROmega.v
@@ -9,3 +9,4 @@
 Require Import ReflOmegaCore.
 Require Export Setoid.
 Require Export PreOmega.
+Require Export ZArith_base.
diff --git a/contrib/romega/ReflOmegaCore.v b/contrib/romega/ReflOmegaCore.v
index 9d379548..12176d66 100644
--- a/contrib/romega/ReflOmegaCore.v
+++ b/contrib/romega/ReflOmegaCore.v
@@ -7,7 +7,7 @@
 
  *************************************************************************)
 
-Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable.
+Require Import List Bool Sumbool EqNat Setoid Ring_theory Decidable ZArith_base.
 Delimit Scope Int_scope with I.
 
 (* Abstract Integers. *)
@@ -81,7 +81,6 @@ End Int.
 
 Module Z_as_Int <: Int.
 
-  Require Import ZArith_base.
   Open Scope Z_scope.
 
   Definition int := Z. 
diff --git a/contrib/setoid_ring/Field_theory.v b/contrib/setoid_ring/Field_theory.v
index 65a397ac..b2e5cc4b 100644
--- a/contrib/setoid_ring/Field_theory.v
+++ b/contrib/setoid_ring/Field_theory.v
@@ -1619,6 +1619,7 @@ split.
 generalize (PCond_cons_inv_l _ _ _ H1); simpl; auto.
 apply H0.
 generalize (PCond_cons_inv_r _ _ _ H1); simpl; auto.
+clear get_sign get_sign_spec. 
 generalize Hp; case l0; simpl; intuition.
 Qed.
 
diff --git a/contrib/setoid_ring/InitialRing.v b/contrib/setoid_ring/InitialRing.v
index c1fa963f..e664b3b7 100644
--- a/contrib/setoid_ring/InitialRing.v
+++ b/contrib/setoid_ring/InitialRing.v
@@ -38,14 +38,6 @@ Proof.
  exact Zmult_plus_distr_l. trivial. exact Zminus_diag.
 Qed.
 
- Lemma Zeqb_ok : forall x y, Zeq_bool x y = true -> x = y.
- Proof.
-  intros x y.
-  assert (H := Zcompare_Eq_eq x y);unfold Zeq_bool;
-  destruct (Zcompare x y);intros H1;auto;discriminate H1.
- Qed.
-
-
 (** Two generic morphisms from Z to (abrbitrary) rings, *)
 (**second one is more convenient for proofs but they are ext. equal*)
 Section ZMORPHISM.
@@ -174,7 +166,7 @@ Section ZMORPHISM.
    Zeq_bool x y = true -> [x] == [y].
  Proof.
   intros x y H.
-  assert (H1 := Zeqb_ok x y H);unfold IDphi in H1.
+  assert (H1 := Zeq_bool_eq x y H);unfold IDphi in H1.
   rewrite H1;rrefl.
  Qed.
   
diff --git a/contrib/setoid_ring/Ring_theory.v b/contrib/setoid_ring/Ring_theory.v
index 29feab5c..531ab3ca 100644
--- a/contrib/setoid_ring/Ring_theory.v
+++ b/contrib/setoid_ring/Ring_theory.v
@@ -494,7 +494,7 @@ Qed.
  Proof. intros;mrewrite. Qed.
 
  Lemma ARdistr_r : forall x y z, z * (x + y) == z*x + z*y.
- Proof. 
+ Proof.
   intros;mrewrite. 
   repeat rewrite (ARth.(ARmul_comm) z);sreflexivity.
  Qed.
diff --git a/contrib/setoid_ring/ZArithRing.v b/contrib/setoid_ring/ZArithRing.v
index 4a5b623b..942915ab 100644
--- a/contrib/setoid_ring/ZArithRing.v
+++ b/contrib/setoid_ring/ZArithRing.v
@@ -50,7 +50,7 @@ Ltac Zpower_neg :=
   end.   
 
 Add Ring Zr : Zth
-  (decidable Zeqb_ok, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
+  (decidable Zeq_bool_eq, constants [Zcst], preprocess [Zpower_neg;unfold Zsucc],
    power_tac Zpower_theory [Zpow_tac],
     (* The two following option are not needed, it is the default chose when the set of 
         coefficiant is usual ring Z *)
diff --git a/contrib/setoid_ring/newring.ml4 b/contrib/setoid_ring/newring.ml4
index dd79801d..3d022add 100644
--- a/contrib/setoid_ring/newring.ml4
+++ b/contrib/setoid_ring/newring.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(*i $Id: newring.ml4 11094 2008-06-10 19:35:23Z herbelin $ i*)
+(*i $Id: newring.ml4 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 open Pp
 open Util
@@ -452,11 +452,14 @@ let (theory_to_obj, obj_to_theory) =
 
 
 let setoid_of_relation env a r =
-  lapp coq_mk_Setoid
-    [|a ; r ; 
-      Class_tactics.reflexive_proof env a r ; 
-      Class_tactics.symmetric_proof env a r ; 
-      Class_tactics.transitive_proof env a r |]
+  try 
+    lapp coq_mk_Setoid
+      [|a ; r ; 
+	Class_tactics.reflexive_proof env a r ; 
+	Class_tactics.symmetric_proof env a r ; 
+	Class_tactics.transitive_proof env a r |]
+  with Not_found ->
+    error "cannot find setoid relation"
 
 let op_morph r add mul opp req m1 m2 m3 =
   lapp coq_mk_reqe [| r; add; mul; opp; req; m1; m2; m3 |]
diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4
index 88243b60..4cf5336d 100644
--- a/contrib/subtac/g_subtac.ml4
+++ b/contrib/subtac/g_subtac.ml4
@@ -14,7 +14,7 @@
   Syntax for the subtac terms and types.
   Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
 
-(* $Id: g_subtac.ml4 10919 2008-05-11 22:04:26Z msozeau $ *)
+(* $Id: g_subtac.ml4 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 
 open Flags
@@ -139,10 +139,10 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations
     END
 
 VERNAC COMMAND EXTEND Subtac_Set_Solver
-| [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ 
+| [ "Obligation" "Tactic" ":=" tactic(t) ] -> [ 
     Coqlib.check_required_library ["Coq";"Program";"Tactics"];
     Tacinterp.add_tacdef false 
-      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ]
+      [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligation_tactic"), true, t)] ]
 END
 
 VERNAC COMMAND EXTEND Subtac_Show_Obligations
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml
index a59ad6f5..7bfa107b 100644
--- a/contrib/subtac/subtac.ml
+++ b/contrib/subtac/subtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac.ml 11150 2008-06-19 11:38:27Z msozeau $ *)
+(* $Id: subtac.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Global
 open Pp
@@ -229,7 +229,8 @@ let subtac (loc, command) =
       debug 2 (Himsg.explain_pretype_error env exn);
       raise e
 	
-  | (Stdpp.Exc_located (loc, e')) as e ->
+  | (Stdpp.Exc_located (loc, Proof_type.LtacLocated (_,e')) |
+     Stdpp.Exc_located (loc, e') as e) ->
       debug 2 (str "Parsing exception: ");
       (match e' with
       | Type_errors.TypeError (env, exn) ->
diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml
index c7182bd2..04bf54d3 100644
--- a/contrib/subtac/subtac_cases.ml
+++ b/contrib/subtac/subtac_cases.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_cases.ml 11154 2008-06-19 18:42:19Z msozeau $ *)
+(* $Id: subtac_cases.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Cases
 open Util
@@ -2056,8 +2056,10 @@ let compile_cases loc style (typing_fun, isevars) (tycon : Evarutil.type_constra
 	    t, prepare_predicate_from_arsign_tycon loc env (Evd.evars_of !isevars)
 	      tomatchs sign (lift tomatchs_len t)
       in
-      let arity = 
-	it_mkProd_or_LetIn (lift neqs arity) (context_of_arsign eqs)
+      let neqs, arity = 
+	let ctx = context_of_arsign eqs in
+	let neqs = List.length ctx in
+	  neqs, it_mkProd_or_LetIn (lift neqs arity) ctx
       in
       let lets, matx = 
 	(* Type the rhs under the assumption of equations *)
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 15addb44..9a5539e2 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.ml 11047 2008-06-03 23:08:00Z msozeau $ i*)
+(*i $Id: subtac_classes.ml 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 open Pretyping
 open Evd
@@ -73,26 +73,18 @@ let interp_casted_constr_evars evdref env ?(impls=([],[])) c typ =
 let type_ctx_instance isevars env ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
-      let t' = replace_vars subst t in
+      let t' = substl subst t in
       let c = interp_casted_constr_evars isevars env ce t' in
+      isevars := resolve_typeclasses ~onlyargs:true ~fail:true env !isevars;
       let d = na, Some c, t' in
-	(na, c) :: subst, d :: instctx)
+	c :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
 
-(*let superclass_ce = CRef (Ident (dummy_loc, id_of_string ".superclass"))*)
-
 let type_class_instance_params isevars env id n ctx inst subst =
   List.fold_left2
     (fun (subst, instctx) (na, _, t) ce ->
       let t' = replace_vars subst t in
-      let c = 
-(* 	if ce = superclass_ce then *)
-	(* 	  (\* Control over the evars which are direct superclasses to avoid partial instanciations *)
-	(* 	     in instance search. *\) *)
-	(* 	  Evarutil.e_new_evar isevars env ~src:(dummy_loc, ImplicitArg (VarRef id, (n, Some na))) t' *)
-	(* 	else *)
-	interp_casted_constr_evars isevars env ce t' 
-      in
+      let c = interp_casted_constr_evars isevars env ce t' in
       let d = na, Some c, t' in
 	(na, c) :: subst, d :: instctx)
     (subst, []) (List.rev ctx) inst
@@ -140,9 +132,9 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
   let k, ctx', imps, subst = 
     let c = Command.generalize_constr_expr tclass ctx in
     let c', imps = interp_type_evars_impls ~evdref:isevars env c in
-    let ctx, c = Classes.decompose_named_assum c' in
+    let ctx, c = Sign.decompose_prod_assum c' in
     let cl, args = Typeclasses.dest_class_app c in
-      cl, ctx, imps, substitution_of_constrs (List.map snd cl.cl_context) (List.rev (Array.to_list args))
+      cl, ctx, imps, (List.rev (Array.to_list args))
   in
   let id = 
     match snd instid with
@@ -155,11 +147,11 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	  let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
 	    Termops.next_global_ident_away false i (Termops.ids_of_context env)
   in
-  let env' = Classes.push_named_context ctx' env in
+  let env' = push_rel_context ctx' env in
   isevars := Evarutil.nf_evar_defs !isevars;
   isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
   let sigma = Evd.evars_of !isevars in
-  let substctx = Typeclasses.nf_substitution sigma subst in
+  let substctx = List.map (Evarutil.nf_evar sigma) subst in
   let subst, _propsctx = 
     let props = 
       List.map (fun (x, l, d) -> 
@@ -172,8 +164,8 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	List.fold_left
 	  (fun (props, rest) (id,_,_) -> 
 	    try 
-	      let ((loc, mid), c) = List.find (fun ((_,id'), c) -> id' = id) rest in
-	      let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in
+	      let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+	      let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
 		Constrintern.add_glob loc (ConstRef (List.assoc mid k.cl_projs));
 		c :: props, rest'
 	    with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
@@ -184,20 +176,13 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(on_free_vars=Class
 	else
 	  type_ctx_instance isevars env' k.cl_props props substctx
   in
-  let inst_constr, ty_constr = instance_constructor k (List.rev_map snd subst) in
+  let inst_constr, ty_constr = instance_constructor k (List.rev subst) in
     isevars := Evarutil.nf_evar_defs !isevars;
-    let term = Evarutil.nf_isevar !isevars (it_mkNamedLambda_or_LetIn inst_constr ctx')
-    and termtype = Evarutil.nf_isevar !isevars (it_mkNamedProd_or_LetIn ty_constr ctx') 
+    let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
+    and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx') 
     in
       isevars := undefined_evars !isevars;
       Evarutil.check_evars env Evd.empty !isevars termtype;
-(*   let imps =  *)
-(*     Util.list_map_i  *)
-(*       (fun i binder -> *)
-(* 	match binder with *)
-(* 	ExplByPos (i, Some na), (true, true)) *)
-(*       1 ctx *)
-(*   in *)
       let hook gr = 
 	let cst = match gr with ConstRef kn -> kn | _ -> assert false in
 	let inst = Typeclasses.new_instance k pri global cst in
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 43f00107..afb0d38d 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: subtac_classes.mli 10797 2008-04-15 13:19:33Z msozeau $ i*)
+(*i $Id: subtac_classes.mli 11282 2008-07-28 11:51:53Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -26,11 +26,11 @@ open Classes
 
 val type_ctx_instance :     Evd.evar_defs ref ->
     Environ.env ->
-    (Names.identifier * 'a * Term.constr) list ->
+    ('a * Term.constr option * Term.constr) list ->
     Topconstr.constr_expr list ->
-    (Names.identifier * Term.constr) list ->
-    (Names.identifier * Term.constr) list *
-    (Names.identifier * Term.constr option * Term.constr) list
+    Term.constr list ->
+    Term.constr list *
+    ('a * Term.constr option * Term.constr) list
 
 val new_instance : 
   ?global:bool ->
diff --git a/contrib/subtac/subtac_coercion.ml b/contrib/subtac/subtac_coercion.ml
index b45e23d0..b046f0b3 100644
--- a/contrib/subtac/subtac_coercion.ml
+++ b/contrib/subtac/subtac_coercion.ml
@@ -6,7 +6,7 @@
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
-(* $Id: subtac_coercion.ml 11143 2008-06-18 15:52:42Z msozeau $ *)
+(* $Id: subtac_coercion.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Util
 open Names
@@ -111,41 +111,31 @@ module Coercion = struct
       : (Term.constr -> Term.constr) option 
       =
     let x = nf_evar (evars_of !isevars) x and y = nf_evar (evars_of !isevars) y in
-(*       (try debug 1 (str "Coerce called for " ++ (my_print_constr env x) ++  *)
-(* 		  str " and "++ my_print_constr env y ++  *)
-(* 		  str " with evars: " ++ spc () ++ *)
-(* 		  my_print_evardefs !isevars); *)
-(*        with _ -> ()); *)
     let rec coerce_unify env x y =
-(*       (try debug 1 (str "coerce_unify from " ++ (my_print_constr env x) ++  *)
-(* 		  str " to "++ my_print_constr env y) *)
-(*        with _ -> ()); *)
       let x = hnf env isevars x and y = hnf env isevars y in
 	try 
 	  isevars := the_conv_x_leq env x y !isevars;
-	  (* 	(try debug 1 (str "Unified " ++ (my_print_constr env x) ++  *)
-	  (* 			str " and "++ my_print_constr env y); *)
-	  (* 	 with _ -> ()); *)
 	  None
 	with Reduction.NotConvertible -> coerce' env x y
     and coerce' env x y : (Term.constr -> Term.constr) option =
       let subco () = subset_coerce env isevars x y in
+      let dest_prod c =
+	match Reductionops.decomp_n_prod env (evars_of !isevars) 1 c with
+	| [(na,b,t)], c -> (na,t), c
+	| _ -> raise NoSubtacCoercion
+      in
       let rec coerce_application typ typ' c c' l l' =
 	let len = Array.length l in
 	let rec aux tele typ typ' i co = 
-(* 	  (try trace (str "coerce_application.aux from " ++ (my_print_constr env x) ++ *)
-(* 			 str " to "++ my_print_constr env y *)
-(* 		       ++ str "in env:" ++ my_print_env env); *)
-(* 	    with _ -> ()); *)
 	  if i < len then
 	    let hdx = l.(i) and hdy = l'.(i) in
 	      try isevars := the_conv_x_leq env hdx hdy !isevars;
-		let (n, eqT, restT) = destProd typ in
-		let (n', eqT', restT') = destProd typ' in
+		let (n, eqT), restT = dest_prod typ in
+		let (n', eqT'), restT' = dest_prod typ' in
 		aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co
 	      with Reduction.NotConvertible ->
-		let (n, eqT, restT) = destProd typ in
-		let (n', eqT', restT') = destProd typ' in
+		let (n, eqT), restT = dest_prod typ in
+		let (n', eqT'), restT' = dest_prod typ' in
 		let _ = 
 		  try isevars := the_conv_x_leq env eqT eqT' !isevars
 		  with Reduction.NotConvertible -> raise NoSubtacCoercion
@@ -163,12 +153,12 @@ module Coercion = struct
 				      [| eqT; hdx; pred; x; hdy; evar|]) in
 		  aux (hdy :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i)  (fun x -> eq_app (co x))
 	  else Some co
-	in aux [] typ typ' 0 (fun x -> x)
+	in 
+	  if isEvar c || isEvar c' then
+	    (* Second-order unification needed. *)
+	    raise NoSubtacCoercion;
+	  aux [] typ typ' 0 (fun x -> x)
       in
-(* 	(try trace (str "coerce' from " ++ (my_print_constr env x) ++ *)
-(* 		       str " to "++ my_print_constr env y *)
-(* 		       ++ str "in env:" ++ my_print_env env); *)
-(* 	  with _ -> ()); *)
 	match (kind_of_term x, kind_of_term y) with
 	  | Sort s, Sort s' -> 
 	      (match s, s' with
@@ -179,13 +169,6 @@ module Coercion = struct
 	  | Prod (name, a, b), Prod (name', a', b') ->
 	      let name' = Name (Nameops.next_ident_away (id_of_string "x") (Termops.ids_of_context env)) in
 	      let env' = push_rel (name', None, a') env in
-		
-(* 	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in *)
-(* 	      let name'' = Name (Nameops.next_ident_away (id_of_string "x'") (Termops.ids_of_context env)) in *)
-(* 	      let env'' = push_rel (name'', Some (app_opt c1 (mkRel 1)), lift 1 a) env' in *)
-(* 	      let c2 = coerce_unify env'' (liftn 1 1 b) (lift 1 b') in *)
-(* 				     mkLetIn (name'', app_opt c1 (mkRel 1), (lift 1 a), *)
-
 	      let c1 = coerce_unify env' (lift 1 a') (lift 1 a) in
 		(* env, x : a' |- c1 : lift 1 a' > lift 1 a *)
 	      let coec1 = app_opt c1 (mkRel 1) in
@@ -295,7 +278,6 @@ module Coercion = struct
     and subset_coerce env isevars x y =
       match disc_subset x with
 	  Some (u, p) -> 
-	    (* trace (str "Inserting projection ");	     *)
 	    let c = coerce_unify env u y in
 	    let f x = 
 	      app_opt c (mkApp ((Lazy.force sig_).proj1, 
@@ -423,7 +405,11 @@ module Coercion = struct
       isevars, { uj_val = app_opt ct j.uj_val; 
 		 uj_type = typ' }
 
-
+  let inh_coerce_to_prod loc env isevars t =
+    let typ = whd_betadeltaiota env (evars_of isevars) (snd t) in
+    let _, typ' = mu env isevars typ in
+      isevars, (fst t, typ')
+	
   let inh_coerce_to_fail env evd rigidonly v t c1 =
     if rigidonly & not (Heads.is_rigid env c1 && Heads.is_rigid env t)
     then
@@ -504,14 +490,13 @@ module Coercion = struct
 	  None -> 0, 0
 	| Some (init, cur) -> init, cur
     in
-      (* a little more effort to get products is needed *)
-      try let rels, rng = decompose_prod_n nabs t in
+      try 
+	let rels, rng = Reductionops.decomp_n_prod env (evars_of isevars) nabs t in
 	(* The final range free variables must have been replaced by evars, we accept only that evars
 	   in rng are applied to free vars. *)
-	if noccur_with_meta 0 (succ nabsinit) rng then (
-(* 	  trace (str "No occur between 0 and " ++ int (succ nabsinit)); *)
+	if noccur_with_meta 1 (succ nabs) rng then (
 	  let env', t, t' =
-	    let env' = List.fold_right (fun (n, t) env -> push_rel (n, None, t) env) rels env in
+	    let env' = push_rel_context rels env in
 	      env', rng, lift nabs t'
 	  in
 	    try
@@ -523,6 +508,4 @@ module Coercion = struct
 		error_cannot_coerce env' sigma (t, t'))
 	else isevars
       with _ -> isevars
-(*  	trace (str "decompose_prod_n failed"); *)
-(*  	raise (Invalid_argument "Subtac_coercion.inh_conv_coerces_to") *)
 end
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 5bff6ad1..a2f54b02 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -350,9 +350,27 @@ let compute_possible_guardness_evidences (n,_) (_, fixctx) fixtype =
 
 let push_named_context = List.fold_right push_named
 
+let check_evars env initial_sigma evd c =
+  let sigma = evars_of evd in
+  let c = nf_evar sigma c in
+  let rec proc_rec c =
+    match kind_of_term c with
+      | Evar (evk,args) ->
+          assert (Evd.mem sigma evk);
+	  if not (Evd.mem initial_sigma evk) then
+            let (loc,k) = evar_source evk evd in
+	      (match k with
+	      | QuestionMark _ -> ()
+	      | _ ->
+		  let evi = nf_evar_info sigma (Evd.find sigma evk) in
+		    Pretype_errors.error_unsolvable_implicit loc env sigma evi k None)
+      | _ -> iter_constr proc_rec c
+  in proc_rec c
+
 let interp_recursive fixkind l boxed =
   let env = Global.env() in
   let fixl, ntnl = List.split l in
+  let kind = if fixkind <> Command.IsCoFixpoint then Fixpoint else CoFixpoint in
   let fixnames = List.map (fun fix -> fix.Command.fix_name) fixl in
 
   (* Interp arities allowing for unresolved types *)
@@ -384,20 +402,17 @@ let interp_recursive fixkind l boxed =
   let rec_sign = nf_named_context_evar (evars_of evd) rec_sign in
     
   let recdefs = List.length rec_sign in
-(*   List.iter (check_evars env_rec Evd.empty evd) fixdefs; *)
-(*   List.iter (check_evars env Evd.empty evd) fixtypes; *)
-(*   check_mutuality env kind (List.combine fixnames fixdefs); *)
+  List.iter (check_evars env_rec Evd.empty evd) fixdefs;
+  List.iter (check_evars env Evd.empty evd) fixtypes;
+  Command.check_mutuality env kind (List.combine fixnames fixdefs);
 
   (* Russell-specific code *)
 
   (* Get the interesting evars, those that were not instanciated *)
   let isevars = Evd.undefined_evars evd in
-  trace (str "got undefined evars" ++ Evd.pr_evar_defs isevars);
   let evm = Evd.evars_of isevars in
-  trace (str "got the evm, recdefs is " ++ int recdefs);
   (* Solve remaining evars *)
   let rec collect_evars id def typ imps = 
-    let _ = try trace (str "In collect evars, isevars is: " ++ Evd.pr_evar_defs isevars) with _ -> () in
       (* Generalize by the recursive prototypes  *)
     let def = 
       Termops.it_mkNamedLambda_or_LetIn def rec_sign
diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 27520867..3a6a351b 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -42,6 +42,7 @@ val interp_binder :     Evd.evar_defs ref ->
     Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
 
 
+
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
 
diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml
index 55cdc7c4..a393e2c9 100644
--- a/contrib/subtac/subtac_obligations.ml
+++ b/contrib/subtac/subtac_obligations.ml
@@ -119,7 +119,7 @@ let from_prg : program_info ProgMap.t ref = ref ProgMap.empty
 let freeze () = !from_prg, !default_tactic_expr
 let unfreeze (v, t) = from_prg := v; set_default_tactic t
 let init () =
-  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligations_tactic" [])
+  from_prg := ProgMap.empty; set_default_tactic (Subtac_utils.tactics_call "obligation_tactic" [])
 
 let _ = 
   Summary.declare_summary "program-tcc-table"
@@ -442,6 +442,7 @@ and solve_obligation_by_tac prg obls i tac =
 	       true		 
 	    else false
 	  with
+	    | Stdpp.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
 	    | Stdpp.Exc_located(_, Refiner.FailError (_, s))
 	    | Refiner.FailError (_, s) ->
 		user_err_loc (obl.obl_location, "solve_obligation", s)
diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml
index 0e987cf2..ad76bdeb 100644
--- a/contrib/subtac/subtac_pretyping.ml
+++ b/contrib/subtac/subtac_pretyping.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping.ml 11047 2008-06-03 23:08:00Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Global
 open Pp
@@ -117,7 +117,6 @@ let env_with_binders env isevars l =
   in aux (env, []) l
 
 let subtac_process env isevars id bl c tycon =
-(*   let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *)
   let c = Command.abstract_constr_expr c bl in
   let tycon = 
     match tycon with
@@ -132,12 +131,14 @@ let subtac_process env isevars id bl c tycon =
   let imps = Implicit_quantifiers.implicits_of_rawterm c in
   let coqc, ctyp = interp env isevars c tycon in
   let evm = non_instanciated_map env isevars (evars_of !isevars) in
-    evm, coqc, (match tycon with Some (None, c) -> c | _ -> ctyp), imps
+  let ty = nf_isevar !isevars (match tycon with Some (None, c) -> c | _ -> ctyp) in
+    evm, coqc, ty, imps
 
 open Subtac_obligations
 
 let subtac_proof kind env isevars id bl c tycon =
   let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in
-  let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in
-  let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in
+  let evm' = Subtac_utils.evars_of_term evm Evd.empty coqc in
+  let evm' = Subtac_utils.evars_of_term evm evm' coqt in
+  let evars, def, ty = Eterm.eterm_obligations env id !isevars evm' 0 coqc coqt in
     add_definition id def ty ~implicits:imps ~kind:kind evars
diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml
index afa5817f..559b6ac1 100644
--- a/contrib/subtac/subtac_pretyping_F.ml
+++ b/contrib/subtac/subtac_pretyping_F.ml
@@ -7,7 +7,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: subtac_pretyping_F.ml 11143 2008-06-18 15:52:42Z msozeau $ *)
+(* $Id: subtac_pretyping_F.ml 11282 2008-07-28 11:51:53Z msozeau $ *)
 
 open Pp
 open Util
@@ -246,6 +246,8 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		  uj_type = it_mkProd_or_LetIn j.uj_type ctxt })
             ctxtv vdef in
 	evar_type_fixpoint loc env isevars names ftys vdefj;
+	let ftys = Array.map (nf_evar (evars_of !isevars)) ftys in
+	let fdefs = Array.map (fun x -> nf_evar (evars_of !isevars) (j_val x)) vdefj in
 	let fixj = match fixkind with
 	  | RFix (vn,i) ->
 	      (* First, let's find the guard indexes. *)
@@ -260,11 +262,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 		   | None -> list_map_i (fun i _ -> i) 0 ctxtv.(i))
 		vn)
 	      in 
-	      let fixdecls = (names,ftys,Array.map j_val vdefj) in 
+	      let fixdecls = (names,ftys,fdefs) in 
 	      let indexes = search_guard loc env possible_indexes fixdecls in 
 	      make_judge (mkFix ((indexes,i),fixdecls)) ftys.(i)
 	  | RCoFix i -> 
-	      let cofix = (i,(names,ftys,Array.map j_val vdefj)) in
+	      let cofix = (i,(names,ftys,fdefs)) in
 	      (try check_cofix env cofix with e -> Stdpp.raise_with_loc loc e);
 	      make_judge (mkCoFix cofix) ftys.(i) in
 	inh_conv_coerce_to_tycon loc env isevars fixj tycon
@@ -273,13 +275,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	inh_conv_coerce_to_tycon loc env isevars (pretype_sort s) tycon
 
     | RApp (loc,f,args) -> 
-	let length = List.length args in	 
+	let length = List.length args in 
 	let ftycon = 
-	  match tycon with
-	      None -> None
+	  if length > 0 then
+	    match tycon with
+	    | None -> None
 	    | Some (None, ty) -> mk_abstr_tycon length ty
 	    | Some (Some (init, cur), ty) ->
 		Some (Some (length + init, length + cur), ty)
+	  else tycon
 	in
 	let fj = pretype ftycon env isevars lvar f in
  	let floc = loc_of_rawconstr f in
@@ -291,23 +295,13 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
               let resty = whd_betadeltaiota env (evars_of !isevars) resj.uj_type in
       		match kind_of_term resty with
 		  | Prod (na,c1,c2) ->
-		      let hj = pretype (mk_tycon c1) env isevars lvar c in
+		      Option.iter (fun ty -> isevars :=
+			Coercion.inh_conv_coerces_to loc env !isevars resty ty) tycon;
+		      let evd, (_, _, tycon) = split_tycon loc env !isevars tycon in
+		      isevars := evd;
+		      let hj = pretype (mk_tycon (nf_isevar !isevars c1)) env isevars lvar c in
 		      let value, typ = applist (j_val resj, [j_val hj]), subst1 hj.uj_val c2 in
 		      let typ' = nf_isevar !isevars typ in
-		      let tycon = 
-			Option.map 
-			  (fun (abs, ty) ->
-			     match abs with
-				 None ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ'
-				     (abs, ty);
-				   (abs, ty)
-			       | Some (init, cur) ->
-				   isevars := Coercion.inh_conv_coerces_to loc env !isevars typ' 
-				     (abs, ty);
-				   (Some (init, pred cur), ty))
-			  tycon
-		      in 
 			apply_rec env (n+1) 
 			  { uj_val = nf_isevar !isevars value;
 			    uj_type = nf_isevar !isevars typ' }
@@ -319,7 +313,6 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 			  (join_loc floc argloc) env (evars_of !isevars)
 	      		  resj [hj]
 	in
-	let ftycon = Option.map (lift_abstr_tycon_type (-1)) ftycon in
 	let resj = j_nf_evar (evars_of !isevars) (apply_rec env 1 fj ftycon args) in
 	let resj =
 	  match kind_of_term resj.uj_val with
@@ -332,12 +325,22 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct
 	  inh_conv_coerce_to_tycon loc env isevars resj tycon
 
     | RLambda(loc,name,k,c1,c2)      ->
-	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in
+	let tycon' = evd_comb1 
+	  (fun evd tycon -> 
+	    match tycon with 
+	    | None -> evd, tycon 
+	    | Some ty -> 
+		let evd, ty' = Coercion.inh_coerce_to_prod loc env evd ty in
+		  evd, Some ty') 
+	  isevars tycon 
+	in
+	let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon' in
 	let dom_valcon = valcon_of_tycon dom in
 	let j = pretype_type dom_valcon env isevars lvar c1 in
 	let var = (name,None,j.utj_val) in
 	let j' = pretype rng (push_rel var env) isevars lvar c2 in 
-	  judge_of_abstraction env name j j'
+	let resj = judge_of_abstraction env name j j' in
+	  inh_conv_coerce_to_tycon loc env isevars resj tycon
 
     | RProd(loc,name,k,c1,c2)        ->
 	let j = pretype_type empty_valcon env isevars lvar c1 in
diff --git a/contrib/subtac/test/ListsTest.v b/contrib/subtac/test/ListsTest.v
index 3ceea173..05fc0803 100644
--- a/contrib/subtac/test/ListsTest.v
+++ b/contrib/subtac/test/ListsTest.v
@@ -1,5 +1,5 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
-Require Import Coq.subtac.Utils.
+Require Import Coq.Program.Program.
 Require Import List.
 
 Set Implicit Arguments.
@@ -7,7 +7,7 @@ Set Implicit Arguments.
 Section Accessors.
   Variable A : Set.
 
-  Program Definition myhd : forall { l : list A | length l <> 0 }, A :=  
+  Program Definition myhd : forall (l : list A | length l <> 0), A :=  
     fun l =>
       match l with
         | nil => !
@@ -39,7 +39,7 @@ Section app.
 
   Next Obligation.
     intros.
-    destruct_call app ; subtac_simpl.
+    destruct_call app ; program_simpl.
   Defined.
   
   Program Lemma app_id_l : forall l : list A, l = nil ++ l.
@@ -49,7 +49,7 @@ Section app.
   
   Program Lemma app_id_r : forall l : list A, l = l ++ nil.
   Proof.
-    induction l ; simpl ; auto.
+    induction l ; simpl in * ; auto. 
     rewrite <- IHl ; auto.
   Qed.
 
@@ -70,16 +70,24 @@ Section Nth.
 
   Next Obligation.
   Proof.
-    intros.
-    inversion H.
+    simpl in *. auto with arith. 
   Defined.
 
+  Next Obligation.
+  Proof.
+    inversion H.
+  Qed.
+
   Program Fixpoint nth' (l : list A) (n : nat | n < length l) { struct l } : A := 
     match l, n with
       | hd :: _, 0 => hd
       | _ :: tl, S n' => nth' tl n'
       | nil, _ => !
     end.
+  Next Obligation.
+  Proof.
+    simpl in *. auto with arith. 
+  Defined.
 
   Next Obligation.
   Proof.
diff --git a/contrib/subtac/test/take.v b/contrib/subtac/test/take.v
index 87ab47d6..2e17959c 100644
--- a/contrib/subtac/test/take.v
+++ b/contrib/subtac/test/take.v
@@ -1,9 +1,12 @@
 (* -*- coq-prog-args: ("-emacs-U" "-debug") -*- *)
 Require Import JMeq.
 Require Import List.
-Require Import Coq.subtac.Utils.
+Require Import Program.
 
 Set Implicit Arguments.
+Obligations Tactic := idtac.
+
+Print cons.
 
 Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct l } : { l' : list A | length l' = n } :=
   match n with
@@ -16,21 +19,14 @@ Program Fixpoint take (A : Set) (l : list A) (n : nat | n <= length l) { struct
   end.
 
 Require Import Omega.
-
+Solve All Obligations.
 Next Obligation.
-  intros.
-  simpl in l0.
-  apply le_S_n ; exact l0.
-Defined.
-
-Next Obligation.
-  intros.
-  destruct_call take ; subtac_simpl.
+  destruct_call take ; program_simpl.
 Defined.
 
 Next Obligation.
   intros.
-  inversion l0.
+  inversion H.
 Defined.
 
 
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4
index 9afd07a6..05be01bc 100644
--- a/contrib/xml/proofTree2Xml.ml4
+++ b/contrib/xml/proofTree2Xml.ml4
@@ -82,8 +82,7 @@ let first_word s =
 
 let string_of_prim_rule x = match x with
   | Proof_type.Intro _-> "Intro"
-  | Proof_type.Intro_replacing _-> "Intro_replacing"
-  | Proof_type.Cut (_,_,_) -> "Cut"
+  | Proof_type.Cut _ -> "Cut"
   | Proof_type.FixRule (_,_,_) -> "FixRule"
   | Proof_type.Cofix (_,_)-> "Cofix"
   | Proof_type.Refine _ -> "Refine"