← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to test-suite/bugs/closed/shouldsucceed/2608.v

  • Committer: Package Import Robot
  • Author(s): Stéphane Glondu
  • Date: 2012-01-03 23:42:48 UTC
  • mfrom: (1.2.4)
  • Revision ID: package-import@ubuntu.com-20120103234248-p9r8h1579n67v55a
Tags: 8.3pl3-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
test-suite/bugs/closed/shouldsucceed/2608.v
 
1
 
 
2
Module Type T.
 
3
  Parameter Inline t : Type.
 
4
End T.
 
5
 
 
6
Module M.
 
7
  Definition t := nat.
 
8
End M.
 
9
 
 
10
Module Make (X:T).
 
11
  Include X.
 
12
 
 
13
  (* here t is : (Top.Make.t,Top.X.t) *)
 
14
 
 
15
  (* in libobject HEAD : EvalConstRef (Top.X.t,Top.X.t)
 
16
     which is substituted by : {Top.X |-> Top.Make [, Top.Make.t=>Top.X.t]}
 
17
     which gives : EvalConstRef (Top.Make.t,Top.X.t) *)
 
18
 
 
19
End Make.
 
20
 
 
21
Module P := Make M.
 
22
 
 
23
  (* resolver returned by add_module : Top.P.t=>inline *)
 
24
  (* then constant_of_delta_kn P.t produces (Top.P.t,Top.P.t) *)
 
25
 
 
26
  (* in libobject HEAD : EvalConstRef (Top.Make.t,Top.X.t)
 
27
     given to subst = {<X#1> |-> Top.M [, Top.M.t=>inline]}
 
28
     which used to give : EvalConstRef (Top.Make.t,Top.M.t)
 
29
     given to subst = {Top.Make |-> Top.P [, Top.P.t=>inline]}
 
30
     which used to give : EvalConstRef (Top.P.t,Top.M.t) *)
 
31
 
 
32
Definition u := P.t.
 
33
 (* was raising Not_found since Heads.head_map knows of (Top.P.t,Top.M.t)
 
34
    and not of (Top.P.t,Top.P.t) *)