diff options
| author | herbelin | 2003-04-10 21:50:10 +0000 |
|---|---|---|
| committer | herbelin | 2003-04-10 21:50:10 +0000 |
| commit | 74503ecc689d8da84491330307fd2ba82683c9c3 (patch) | |
| tree | 3ff370e6df65badf729c585891c1469d137041ef /interp | |
| parent | b7805a58736574e5eea74571fa0451a5fcc955c7 (diff) | |
Relachement globalisation Unfold en usage interactif
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3907 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |