diff options
| author | herbelin | 2004-08-23 12:58:27 +0000 |
|---|---|---|
| committer | herbelin | 2004-08-23 12:58:27 +0000 |
| commit | e07c4d7d7545652ee0e5f2cd05c53b45f92e0df6 (patch) | |
| tree | 22b06756e26a7186b2f9079e32d1dd5870fc7372 /pretyping | |
| parent | 0b18e84d1fc34dd098dfff91e83d795ce41bb774 (diff) | |
Correction bug #830 : les noms des implicites temporaires étaient inconnus au moment de l'affichage
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6021 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 2 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 47edc73cea..1aeca07cb7 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -49,7 +49,7 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings type hole_kind = - | ImplicitArg of global_reference * int + | ImplicitArg of global_reference * (int * identifier option) | BinderType of name | QuestionMark | CasesType diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 29237a675b..54bb306bd0 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -47,7 +47,7 @@ type 'a bindings = type 'a with_bindings = 'a * 'a bindings type hole_kind = - | ImplicitArg of global_reference * int + | ImplicitArg of global_reference * (int * identifier option) | BinderType of name | QuestionMark | CasesType |