From e07c4d7d7545652ee0e5f2cd05c53b45f92e0df6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 23 Aug 2004 12:58:27 +0000
Subject: 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
---
 pretyping/rawterm.ml  | 2 +-
 pretyping/rawterm.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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
-- 
cgit v1.2.3