From 74503ecc689d8da84491330307fd2ba82683c9c3 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 10 Apr 2003 21:50:10 +0000
Subject: Relachement globalisation Unfold en usage interactif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3907 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/genarg.ml  | 2 +-
 interp/genarg.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 0f2e031cc7..e1df0ab721 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -40,7 +40,7 @@ type argument_type =
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a or_metanum = AN of 'a | MetaNum of int located
-type 'a and_short_name = 'a * identifier option
+type 'a and_short_name = 'a * identifier located option
 type rawconstr_and_expr = rawconstr * constr_expr option
 
 (* Dynamics but tagged by a type expression *)
diff --git a/interp/genarg.mli b/interp/genarg.mli
index c938d4c516..88865f022a 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -17,7 +17,7 @@ open Topconstr
 
 type 'a or_var = ArgArg of 'a | ArgVar of identifier located
 type 'a or_metanum = AN of 'a | MetaNum of int located
-type 'a and_short_name = 'a * identifier option
+type 'a and_short_name = 'a * identifier located option
 
 (* In globalize tactics, we need to keep the initial constr_expr to recompute*)
 (* in the environment by the effective calls to Intro, Inversion, etc *)
-- 
cgit v1.2.3