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 | |
| parent | 120ed3238345fb088afbfa5dac153dc28e4bc6ee (diff) | |
Correction Show Implicits
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3891 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | library/impargs.ml | 2 | ||||
| -rw-r--r-- | library/impargs.mli | 1 | ||||
| -rw-r--r-- | toplevel/vernacentries.ml | 6 |
3 files changed, 4 insertions, 5 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 diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index a32f6b8a1e..d536be9bd0 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1022,8 +1022,10 @@ let vernac_show = function else (match nopt with | None -> show_open_subgoals () | (Some n) -> show_nth_open_subgoal n) - | ShowGoalImplicitly None -> Impargs.implicitly show_open_subgoals () - | ShowGoalImplicitly (Some n) -> Impargs.implicitly show_nth_open_subgoal n + | ShowGoalImplicitly None -> + Constrextern.with_implicits show_open_subgoals () + | ShowGoalImplicitly (Some n) -> + Constrextern.with_implicits show_nth_open_subgoal n | ShowProof -> show_proof () | ShowNode -> show_node () | ShowScript -> show_script () |