2 files changed, 11 insertions, 11 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index e9102e9c82..61d207b953 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -550,11 +550,11 @@ type tcc_lemma_value =
   | Value of constr
   | Not_needed
 
-(* We only "purify" on exceptions *)
+(* We only "purify" on exceptions. XXX: What is this doing here? *)
 let funind_purify f x =
-  let st = Vernacentries.freeze_interp_state `No in
+  let st = Vernacstate.freeze_interp_state `No in
   try f x
   with e ->
     let e = CErrors.push e in
-    Vernacentries.unfreeze_interp_state st;
+    Vernacstate.unfreeze_interp_state st;
     Exninfo.iraise e
diff --git a/plugins/micromega/micromega.ml b/plugins/micromega/micromega.ml
index 7da4a3b829..52c6ef983d 100644
--- a/plugins/micromega/micromega.ml
+++ b/plugins/micromega/micromega.ml
@@ -981,8 +981,8 @@ let rec or_cnf unsat deduce f f' =
 
 (** val and_cnf : 'a1 cnf -> 'a1 cnf -> 'a1 cnf **)
 
-let and_cnf f1 f2 =
-  app f1 f2
+let and_cnf =
+  app
 
 (** val xcnf :
     ('a2 -> bool) -> ('a2 -> 'a2 -> 'a2 option) -> ('a1 -> 'a2 cnf) -> ('a1
@@ -1204,22 +1204,22 @@ type 't formula = { flhs : 't pExpr; fop : op2; frhs : 't pExpr }
     'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1
     -> 'a1) -> ('a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pExpr -> 'a1 pol **)
 
-let norm cO cI cplus ctimes cminus copp ceqb =
-  norm_aux cO cI cplus ctimes cminus copp ceqb
+let norm =
+  norm_aux
 
 (** val psub0 :
     'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1) -> ('a1
     -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol -> 'a1 pol **)
 
-let psub0 cO cplus cminus copp ceqb =
-  psub cO cplus cminus copp ceqb
+let psub0 =
+  psub
 
 (** val padd0 :
     'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> bool) -> 'a1 pol -> 'a1 pol
     -> 'a1 pol **)
 
-let padd0 cO cplus ceqb =
-  padd cO cplus ceqb
+let padd0 =
+  padd
 
 (** val xnormalise :
     'a1 -> 'a1 -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1 -> 'a1) -> ('a1 -> 'a1