diff options
| author | Matthieu Sozeau | 2016-11-07 14:47:15 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-11-07 14:47:15 +0100 |
| commit | 1f36cdefd841526f804bd2dd51c1d88309333376 (patch) | |
| tree | 9d13ea499cfebf6285eccc6d8b434bcf5ea9e41b | |
| parent | a4cecc13cde3239d6a86f98ba6bba0e4554306bd (diff) | |
Fixes to compile with ocaml 4.01
| -rw-r--r-- | engine/termops.ml | 2 | ||||
| -rw-r--r-- | ltac/extratactics.ml4 | 2 | ||||
| -rw-r--r-- | tactics/hints.ml | 4 | ||||
| -rw-r--r-- | 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 |