diff options
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/genarg.ml | 2 | ||||
| -rw-r--r-- | interp/genarg.mli | 2 |
2 files changed, 2 insertions, 2 deletions
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 *) |