diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /library/impargs.mli | |
| parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) | |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/library/impargs.mli b/library/impargs.mli index 79d506568..66d72abbb 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -68,7 +68,7 @@ type implicit_explanation = type maximal_insertion = bool (** true = maximal contextual insertion *) type force_inference = bool (** true = always infer, never turn into evar/subgoal *) -type implicit_status = (identifier * implicit_explanation * +type implicit_status = (Id.t * implicit_explanation * (maximal_insertion * force_inference)) option (** [None] = Not implicit *) @@ -78,7 +78,7 @@ type implicits_list = implicit_side_condition * implicit_status list val is_status_implicit : implicit_status -> bool val is_inferable_implicit : bool -> int -> implicit_status -> bool -val name_of_implicit : implicit_status -> identifier +val name_of_implicit : implicit_status -> Id.t val maximal_insertion_of : implicit_status -> bool val force_inference_of : implicit_status -> bool |