From 250a3dfc1f46f9f705c471445a416476099ecc5d Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 28 Jan 2013 22:44:32 +0000
Subject: Fixed bug #2966 (de Bruijn error in computation of heads for
 coercions).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16168 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/heads.ml              |  2 +-
 test-suite/bugs/closed/2966.v | 79 +++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 80 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/2966.v

diff --git a/library/heads.ml b/library/heads.ml
index 0d3ed0fdb..62e27dd00 100644
--- a/library/heads.ml
+++ b/library/heads.ml
@@ -92,7 +92,7 @@ let kind_of_head env t =
     | [] ->
       let () = assert (not b) in
       aux (k + 1) [] c b
-    | h :: l -> aux (k + 1) l (subst1 h c) b
+    | h :: l -> aux k l (subst1 h c) b
     end
   | LetIn _ -> assert false
   | Meta _ | Evar _ -> NotImmediatelyComputableHead
diff --git a/test-suite/bugs/closed/2966.v b/test-suite/bugs/closed/2966.v
new file mode 100644
index 000000000..e1c8d0047
--- /dev/null
+++ b/test-suite/bugs/closed/2966.v
@@ -0,0 +1,79 @@
+(** Non-termination and state monad with extraction *)
+Require Import List.
+
+Set Implicit Arguments.
+Set Asymmetric Patterns.
+
+Module MemSig.
+  Definition t: Type := list Type.
+  
+  Definition Nth (sig: t) (n: nat): Type :=
+    nth n sig unit.
+End MemSig.
+
+(** A memory of type [Mem.t s] is the union of cells whose type is specified
+    by [s]. *)
+Module Mem.
+  Inductive t: MemSig.t -> Type :=
+  | Nil: t nil
+  | Cons: forall (T: Type), option T -> forall (sig: MemSig.t), t sig ->
+    t (T :: sig).
+End Mem.
+
+Module Ref.
+  Inductive t (sig: MemSig.t) (T: Type): Type :=
+  | Input: t sig T.
+  
+  Definition Read (sig: MemSig.t) (T: Type) (ref: t sig T) (s: Mem.t sig)
+    : option T :=
+    match ref with
+    | Input => None
+    end.
+End Ref.
+
+Module Monad.
+  Definition t (sig: MemSig.t) (A: Type) :=
+    Mem.t sig -> option A * Mem.t sig.
+  
+  Definition Return (sig: MemSig.t) (A: Type) (x: A): t sig A :=
+    fun s =>
+      (Some x, s).
+  
+  Definition Bind (sig: MemSig.t) (A B: Type) (x: t sig A) (f: A -> t sig B)
+    : t sig B :=
+    fun s =>
+    match x s with
+    | (Some x', s') => f x' s'
+    | (None, s') => (None, s')
+    end.
+
+  Definition Select (T: Type) (f g: unit -> T): T :=
+    f tt.
+  
+  (** Read in a reference. *)
+  Definition Read (sig: MemSig.t) (T: Type) (ref: Ref.t sig T)
+    : t sig T :=
+    fun s =>
+      match Ref.Read ref s with
+      | None => (None, s)
+      | Some x => (Some x, s)
+      end.
+End Monad.
+
+Import Monad.
+
+Definition pop (sig: MemSig.t) (T: Type) (trace: Ref.t sig (list T))
+  : Monad.t sig T :=
+  Bind (Read trace) (fun _ s => (None, s)).
+
+Definition sig: MemSig.t := (list nat: Type) :: nil.
+
+Definition trace: Ref.t sig (list nat).
+Admitted.
+
+Definition Gre (sig: MemSig.t) (trace: _)
+    (f: bool -> bool): Monad.t sig nat :=
+    Select (fun _ => pop trace) (fun _ => Return 0).
+
+Definition Arg :=
+  Gre trace (fun _ => false).
-- 
cgit v1.2.3