From 1f36cdefd841526f804bd2dd51c1d88309333376 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Mon, 7 Nov 2016 14:47:15 +0100
Subject: Fixes to compile with ocaml 4.01

---
 engine/termops.ml     | 2 +-
 ltac/extratactics.ml4 | 2 +-
 tactics/hints.ml      | 4 +++-
 toplevel/classes.ml   | 6 ++++--
 4 files changed, 9 insertions(+), 5 deletions(-)

diff --git a/engine/termops.ml b/engine/termops.ml
index 35cacc65b2..697b9a5f15 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -980,7 +980,7 @@ let smash_rel_context sign =
 let fold_named_context_both_sides f l ~init = List.fold_right_and_left f l init
 
 let mem_named_context_val id ctxt =
-  try Environ.lookup_named_val id ctxt; true with Not_found -> false
+  try ignore(Environ.lookup_named_val id ctxt); true with Not_found -> false
 
 let compact_named_context_reverse sign =
   let compact l decl =
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index d9780dcc8c..8ae95c315b 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -316,7 +316,7 @@ let project_hint pri l2r r =
   in
   let ctx = Evd.universe_context_set sigma in
   let c = Declare.declare_definition ~internal:Declare.InternalTacticRequest id (c,ctx) in
-  let info = Vernacexpr.({hint_priority = pri; hint_pattern = None}) in
+  let info = {Vernacexpr.hint_priority = pri; hint_pattern = None} in
     (info,false,true,Hints.PathAny, Hints.IsGlobRef (Globnames.ConstRef c))
 
 let add_hints_iff l2r lc n bl =
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 9cbfe20d96..53573bc7e4 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -84,7 +84,9 @@ let secvars_of_hyps hyps =
   if all then Id.Pred.full (* If the whole section context is available *)
   else pred
 
-let empty_hint_info = Vernacexpr.{ hint_priority = None; hint_pattern = None }
+let empty_hint_info =
+  let open Vernacexpr in
+  { hint_priority = None; hint_pattern = None }
 
 (************************************************************************)
 (*           The Type of Constructions Autotactic Hints                 *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 1f13ab6374..1528cbb2f6 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -51,9 +51,11 @@ let _ =
        | IsGlobal gr -> Hints.IsGlobRef gr
      in
      let info =
-       Vernacexpr.{ info with hint_pattern =
+       let open Vernacexpr in
+       { info with hint_pattern =
 		   Option.map
-		   (Constrintern.intern_constr_pattern (Global.env())) info.hint_pattern } in
+		     (Constrintern.intern_constr_pattern (Global.env()))
+		     info.hint_pattern } in
      Flags.silently (fun () ->
 	Hints.add_hints local [typeclasses_db]
 	  (Hints.HintsResolveEntry
-- 
cgit v1.2.3