From 82dc377451e2dc7810eea136b9a6ab8fc5ae48b5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 19 Aug 2016 20:34:40 +0200
Subject: Removing dead code in Impargs.

---
 library/impargs.ml  |  3 +--
 library/impargs.mli | 12 +-----------
 2 files changed, 2 insertions(+), 13 deletions(-)

diff --git a/library/impargs.ml b/library/impargs.ml
index 6da7e21100..db98bb9fd4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -68,10 +68,9 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern
 let is_contextual_implicit_args () = !implicit_args.contextual
 let is_maximal_implicit_args () = !implicit_args.maximal
 
-let with_implicits flags f x =
+let with_implicits f x =
   let oflags = !implicit_args in
   try
-    implicit_args := flags;
     let rslt = f x in
     implicit_args := oflags;
     rslt
diff --git a/library/impargs.mli b/library/impargs.mli
index 34e529ca2c..327f84d9fa 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool
 val is_contextual_implicit_args : unit -> bool
 val is_maximal_implicit_args : unit -> bool
 
-type implicits_flags
-val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b
+val with_implicits : ('a -> 'b) -> 'a -> 'b
 
 (** {6 ... } *)
 (** An [implicits_list] is a list of positions telling which arguments
@@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list
 
 val select_stronger_impargs : implicits_list list -> implicit_status list
 
-type implicit_interactive_request
-
-type implicit_discharge_request =
-  | ImplLocal
-  | ImplConstant of constant * implicits_flags
-  | ImplMutualInductive of mutual_inductive * implicits_flags
-  | ImplInteractive of global_reference * implicits_flags *
-      implicit_interactive_request
-
 val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
 (** Equality on [explicitation]. *)
-- 
cgit v1.2.3