diff options
author | 2017-05-02 16:04:50 +0200 | |
---|---|---|
committer | 2017-05-02 16:04:50 +0200 | |
commit | 28accc370aa2f6fafbf50b69be7ae5dc06104212 (patch) | |
tree | 7764de5a598390e9906f064170a480cfcfe0a38d /tactics | |
parent | 63503b99c46b27009e85e5c0fa9588b7424a589d (diff) | |
parent | 9a48211ea8439a8502145e508b70ede9b5929b2f (diff) |
Merge PR#582: Fix warnings
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/auto.ml | 4 | ||||
-rw-r--r-- | tactics/auto.mli | 1 | ||||
-rw-r--r-- | tactics/btermdn.mli | 1 | ||||
-rw-r--r-- | tactics/class_tactics.ml | 10 | ||||
-rw-r--r-- | tactics/class_tactics.mli | 2 | ||||
-rw-r--r-- | tactics/contradiction.mli | 1 | ||||
-rw-r--r-- | tactics/eauto.mli | 2 | ||||
-rw-r--r-- | tactics/elim.ml | 1 | ||||
-rw-r--r-- | tactics/elim.mli | 1 | ||||
-rw-r--r-- | tactics/eqdecide.ml | 1 | ||||
-rw-r--r-- | tactics/equality.ml | 1 | ||||
-rw-r--r-- | tactics/equality.mli | 1 | ||||
-rw-r--r-- | tactics/hints.ml | 2 | ||||
-rw-r--r-- | tactics/hints.mli | 1 | ||||
-rw-r--r-- | tactics/hipattern.ml | 1 | ||||
-rw-r--r-- | tactics/hipattern.mli | 1 | ||||
-rw-r--r-- | tactics/inv.ml | 1 | ||||
-rw-r--r-- | tactics/inv.mli | 1 | ||||
-rw-r--r-- | tactics/leminv.mli | 1 | ||||
-rw-r--r-- | tactics/tactics.ml | 4 | ||||
-rw-r--r-- | tactics/term_dnet.ml | 2 |
21 files changed, 5 insertions, 35 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 42230dff1..c2d12ebd0 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -10,16 +10,12 @@ module CVars = Vars open Pp open Util -open CErrors open Names -open Vars open Termops open EConstr open Environ -open Tacmach open Genredexpr open Tactics -open Tacticals open Clenv open Locus open Proofview.Notations diff --git a/tactics/auto.mli b/tactics/auto.mli index 32710e347..9ed9f0ae2 100644 --- a/tactics/auto.mli +++ b/tactics/auto.mli @@ -9,7 +9,6 @@ (** This files implements auto and related automation tactics *) open Names -open Term open EConstr open Clenv open Pattern diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli index 2a5e7c345..27f624f71 100644 --- a/tactics/btermdn.mli +++ b/tactics/btermdn.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open Pattern open Names diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 54e4405d1..2d6dffdd2 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -18,9 +18,7 @@ open Names open Term open Termops open EConstr -open Reduction open Proof_type -open Tacticals open Tacmach open Tactics open Clenv @@ -357,12 +355,12 @@ let shelve_dependencies gls = let hintmap_of sigma hdc secvars concl = match hdc with - | None -> fun db -> Hint_db.map_none secvars db + | None -> fun db -> Hint_db.map_none ~secvars db | Some hdc -> fun db -> if Hint_db.use_dn db then (* Using dnet *) - Hint_db.map_eauto sigma secvars hdc concl db - else Hint_db.map_existential sigma secvars hdc concl db + Hint_db.map_eauto sigma ~secvars hdc concl db + else Hint_db.map_existential sigma ~secvars hdc concl db (** Hack to properly solve dependent evars that are typeclasses *) let rec e_trivial_fail_db only_classes db_list local_db secvars = @@ -1219,7 +1217,6 @@ module Search = struct let intro_tac info kont gl = let open Proofview in - let open Proofview.Notations in let env = Goal.env gl in let sigma = Goal.sigma gl in let s = Sigma.to_evar_map sigma in @@ -1257,7 +1254,6 @@ module Search = struct let search_tac_gl ?st only_classes dep hints depth i sigma gls gl : unit Proofview.tactic = let open Proofview in - let open Proofview.Notations in if false (* In 8.6, still allow non-class goals only_classes && not (is_class_type sigma (Goal.concl gl)) *) then Tacticals.New.tclZEROMSG (str"Not a subgoal for a class") else diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index 738cc0feb..c5731e377 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -9,9 +9,7 @@ (** This files implements typeclasses eauto *) open Names -open Constr open EConstr -open Tacmach val catchable : exn -> bool diff --git a/tactics/contradiction.mli b/tactics/contradiction.mli index 510b135b0..2cf5a6829 100644 --- a/tactics/contradiction.mli +++ b/tactics/contradiction.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr open Misctypes diff --git a/tactics/eauto.mli b/tactics/eauto.mli index e2006ac1e..c952f4e72 100644 --- a/tactics/eauto.mli +++ b/tactics/eauto.mli @@ -6,9 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term open EConstr -open Proof_type open Hints open Tactypes diff --git a/tactics/elim.ml b/tactics/elim.ml index e37ec6bce..855cb206f 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -8,7 +8,6 @@ open Util open Names -open Term open Termops open EConstr open Inductiveops diff --git a/tactics/elim.mli b/tactics/elim.mli index dc1af79ba..fb7cc7b83 100644 --- a/tactics/elim.mli +++ b/tactics/elim.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Tacticals open Misctypes diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index bac3980d2..5012b0ef7 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -25,7 +25,6 @@ open Constr_matching open Misctypes open Tactypes open Hipattern -open Pretyping open Proofview.Notations open Tacmach.New open Coqlib diff --git a/tactics/equality.ml b/tactics/equality.ml index 25c28cf4a..cc7701ad5 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -14,7 +14,6 @@ open Names open Nameops open Term open Termops -open Environ open EConstr open Vars open Namegen diff --git a/tactics/equality.mli b/tactics/equality.mli index 5467b4af2..d979c580a 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -8,7 +8,6 @@ (*i*) open Names -open Term open Evd open EConstr open Environ diff --git a/tactics/hints.ml b/tactics/hints.ml index bcc068d3d..240178c9a 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1435,7 +1435,7 @@ let pr_hints_db (name,db,hintlist) = let pr_hint_list_for_head c = let dbs = current_db () in let validate (name, db) = - let hints = List.map (fun v -> 0, v) (Hint_db.map_all Id.Pred.full c db) in + let hints = List.map (fun v -> 0, v) (Hint_db.map_all ~secvars:Id.Pred.full c db) in (name, db, hints) in let valid_dbs = List.map validate dbs in diff --git a/tactics/hints.mli b/tactics/hints.mli index 467fd46d5..3a0339ff5 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -9,7 +9,6 @@ open Pp open Util open Names -open Term open EConstr open Environ open Globnames diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 851554b83..15b40b42d 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -40,7 +40,6 @@ let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 let meta2 = mkmeta 2 let meta3 = mkmeta 3 -let meta4 = mkmeta 4 let op2bool = function Some _ -> true | None -> false diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index dd09c3a4d..82a3d47b5 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open Evd open EConstr open Coqlib diff --git a/tactics/inv.ml b/tactics/inv.ml index 904a17417..266cac5c7 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -13,7 +13,6 @@ open Names open Nameops open Term open Termops -open Environ open EConstr open Vars open Namegen diff --git a/tactics/inv.mli b/tactics/inv.mli index 446a62f6d..5835e763d 100644 --- a/tactics/inv.mli +++ b/tactics/inv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Misctypes open Tactypes diff --git a/tactics/leminv.mli b/tactics/leminv.mli index 26d4ac994..a343fc81a 100644 --- a/tactics/leminv.mli +++ b/tactics/leminv.mli @@ -7,7 +7,6 @@ (************************************************************************) open Names -open Term open EConstr open Constrexpr open Misctypes diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4173f8734..211a7338b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -5040,10 +5040,6 @@ end (** Tacticals defined directly in term of Proofview *) module New = struct - open Proofview.Notations - - let exact_proof c = exact_proof c - open Genredexpr open Locus diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 2c863c42a..726fd23b6 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -49,7 +49,7 @@ struct | DNil (* debug *) - let pr_dconstr f : 'a t -> std_ppcmds = function + let _pr_dconstr f : 'a t -> std_ppcmds = function | DRel -> str "*" | DSort -> str "Sort" | DRef _ -> str "Ref" |