diff options
| author | herbelin | 2003-04-09 16:29:30 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-09 16:29:30 +0000 |
| commit | d43c0c89c0b28bdf0983c5c3e5848b55d3602818 (patch) | |
| tree | ca94a784674ade72893a7d5a5331fe7eb2597dd8 /library | |
| parent | 120ed3238345fb088afbfa5dac153dc28e4bc6ee (diff) | |
Correction Show Implicits
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3891 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | library/impargs.mli | 1 |
2 files changed, 0 insertions, 3 deletions
diff --git a/library/impargs.ml b/library/impargs.ml index fb9d41b2ad..eae576fdbe 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -81,8 +81,6 @@ let with_implicits ((a,b,c),(d,e,g)) f x = raise e end -let implicitly f = with_implicits ((false,false,false),(false,false,false)) f - (*s Computation of implicit arguments *) (* We remember various information about why an argument is (automatically) diff --git a/library/impargs.mli b/library/impargs.mli index a9f57e2887..4109bea063 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -28,7 +28,6 @@ val is_strict_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool type implicits_flags -val implicitly : ('a -> 'b) -> 'a -> 'b val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b (*s An [implicits_list] is a list of positions telling which arguments |