diff --git a/src/coq-tactic/coqCompat.8.3.ml b/src/coq-tactic/coqCompat.8.3.ml
index e4327c09125b483f5f6baa3609d4bcc6abaa6250..efe0076d386f43cd2ad225a41ab15ff0bee05f83 100644
--- a/src/coq-tactic/coqCompat.8.3.ml
+++ b/src/coq-tactic/coqCompat.8.3.ml
@@ -1,2 +1,3 @@
 
-let body_of_constant c = c.const_body
+
+let body_of_constant c = c.Declarations.const_body
diff --git a/src/coq-tactic/why3tac.ml b/src/coq-tactic/why3tac.ml
index 6ef6bdc88930d4d80740013957123025f92a5cde..a0f5b84da80350c85fdd73ab5ef7185667df69fc 100644
--- a/src/coq-tactic/why3tac.ml
+++ b/src/coq-tactic/why3tac.ml
@@ -1125,10 +1125,8 @@ let tr_top_decl = function
   | _, Lib.CompilingLibrary _
   | _, Lib.OpenedModule _
   | _, Lib.ClosedModule  _
-(*
   | _, Lib.OpenedModtype _
   | _, Lib.ClosedModtype _
-*)
   | _, Lib.OpenedSection _
   | _, Lib.ClosedSection _
   | _, Lib.FrozenState _ -> ()