diff options
author | Stephane Glondu <steph@glondu.net> | 2012-01-07 17:59:15 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2012-01-07 18:20:56 +0100 |
commit | 2ee61d5995ef572f0124691f10630305a59b4f73 (patch) | |
tree | eaeffb7be70ce770a822108f8a527312f67fd8b2 /test-suite/bugs/closed/shouldsucceed/2608.v | |
parent | ba021624830c7ad5df0688d144e4305551ae1a5f (diff) | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) |
Prepare upload to squeeze-backportsdebian/8.3.pl3+dfsg-1_bpo60+1
Diffstat (limited to 'test-suite/bugs/closed/shouldsucceed/2608.v')
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2608.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/shouldsucceed/2608.v b/test-suite/bugs/closed/shouldsucceed/2608.v new file mode 100644 index 00000000..a4c95ff9 --- /dev/null +++ b/test-suite/bugs/closed/shouldsucceed/2608.v @@ -0,0 +1,34 @@ + +Module Type T. + Parameter Inline t : Type. +End T. + +Module M. + Definition t := nat. +End M. + +Module Make (X:T). + Include X. + + (* here t is : (Top.Make.t,Top.X.t) *) + + (* in libobject HEAD : EvalConstRef (Top.X.t,Top.X.t) + which is substituted by : {Top.X |-> Top.Make [, Top.Make.t=>Top.X.t]} + which gives : EvalConstRef (Top.Make.t,Top.X.t) *) + +End Make. + +Module P := Make M. + + (* resolver returned by add_module : Top.P.t=>inline *) + (* then constant_of_delta_kn P.t produces (Top.P.t,Top.P.t) *) + + (* in libobject HEAD : EvalConstRef (Top.Make.t,Top.X.t) + given to subst = {<X#1> |-> Top.M [, Top.M.t=>inline]} + which used to give : EvalConstRef (Top.Make.t,Top.M.t) + given to subst = {Top.Make |-> Top.P [, Top.P.t=>inline]} + which used to give : EvalConstRef (Top.P.t,Top.M.t) *) + +Definition u := P.t. + (* was raising Not_found since Heads.head_map knows of (Top.P.t,Top.M.t) + and not of (Top.P.t,Top.P.t) *) |