7 files changed, 19 insertions, 15 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 2ed436c6bf..58744b5754 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -19,7 +19,7 @@ open Context.Rel.Declaration
 
 let qflag=ref true
 
-let red_flags=ref Closure.betaiotazeta
+let red_flags=ref CClosure.betaiotazeta
 
 let (=?) f g i1 i2 j1 j2=
   let c=f i1 i2 in
@@ -59,12 +59,12 @@ let ind_hyps nevar ind largs gls=
     Array.map myhyps types
 
 let special_nf gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.norm_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> CClosure.norm_val infos (CClosure.inject t))
 
 let special_whd gl=
-  let infos=Closure.create_clos_infos !red_flags (pf_env gl) in
-    (fun t -> Closure.whd_val infos (Closure.inject t))
+  let infos=CClosure.create_clos_infos !red_flags (pf_env gl) in
+    (fun t -> CClosure.whd_val infos (CClosure.inject t))
 
 type kind_of_formula=
     Arrow of constr*constr
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 0f70d3ea05..5db8ff59ad 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -11,7 +11,7 @@ open Globnames
 
 val qflag : bool ref
 
-val red_flags: Closure.RedFlags.reds ref
+val red_flags: CClosure.RedFlags.reds ref
 
 val (=?) : ('a -> 'a -> int) -> ('b -> 'b -> int) ->
   'a -> 'a -> 'b -> 'b -> int
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index cec3505a97..95095b09cb 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -120,6 +120,11 @@ let pr_firstorder_using_raw _ _ _ l = str "using " ++ prlist_with_sep pr_comma p
 let pr_firstorder_using_glob _ _ _ l = str "using " ++ prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) l
 let pr_firstorder_using_typed _ _ _ l = str "using " ++ prlist_with_sep pr_comma pr_global l
 
+let warn_deprecated_syntax =
+  CWarnings.create ~name:"firstorder-deprecated-syntax" ~category:"deprecated"
+    (fun () -> Pp.strbrk "Deprecated syntax; use \",\" as separator")
+
+
 ARGUMENT EXTEND firstorder_using
   TYPED AS reference_list
   PRINTED BY pr_firstorder_using_typed
@@ -130,8 +135,7 @@ ARGUMENT EXTEND firstorder_using
 | [ "using" reference(a) ] -> [ [a] ]
 | [ "using" reference(a) "," ne_reference_list_sep(l,",") ] -> [ a::l ]
 | [ "using" reference(a) reference(b) reference_list(l) ] -> [
-    Flags.if_verbose
-      Feedback.msg_warning (Pp.str "Deprecated syntax; use \",\" as separator");
+    warn_deprecated_syntax ();
     a::b::l
   ]
 | [ ] -> [ [] ]
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index d7da85b4f4..628af4e719 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -24,8 +24,8 @@ let update_flags ()=
   in
     List.iter f (Classops.coercions ());
     red_flags:=
-    Closure.RedFlags.red_add_transparent
-      Closure.betaiotazeta
+    CClosure.RedFlags.red_add_transparent
+      CClosure.betaiotazeta
       (Names.Id.Pred.full,Names.Cpred.complement !predref)
 
 let ground_tac solver startseq gl=
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 5eff2f2774..eebd974ea8 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -8,7 +8,7 @@
 
 open Unify
 open Rules
-open Errors
+open CErrors
 open Util
 open Term
 open Vars
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
       let typ=pf_unsafe_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_betadeltaiota env evmap typ) in
+      let (nam,_,_)=destProd (whd_all env evmap typ) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
@@ -156,7 +156,7 @@ let left_instance_tac (inst,id) continue seq=
 		      (mkApp(idc,[|ot|])) rc in
 		  let evmap, _ =
 		    try Typing.type_of (pf_env gl) evmap gt
-		    with e when Errors.noncritical e ->
+		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
 	    else
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 92b6e828e8..ffb63af072 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Errors
+open CErrors
 open Util
 open Names
 open Term
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 3e8033da07..1248b60a76 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 open Term
-open Errors
+open CErrors
 open Util
 open Formula
 open Unify