From 726a8500e8f23ef19e5fe8b03bb745db111ade0c Mon Sep 17 00:00:00 2001
From: Claude Marche <Claude.Marche@inria.fr>
Date: Tue, 11 Sep 2012 12:56:04 +0200
Subject: [PATCH] compiles with both Coq 8.3 and 8.4

---
 src/coq-tactic/coqCompat.8.3.ml | 3 ++-
 src/coq-tactic/why3tac.ml       | 2 --
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/src/coq-tactic/coqCompat.8.3.ml b/src/coq-tactic/coqCompat.8.3.ml
index e4327c091..efe0076d3 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 6ef6bdc88..a0f5b84da 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 _ -> ()
-- 
GitLab