3 files changed, 20 insertions, 3 deletions
diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index eb3abfa5ae..b9503831c9 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -187,7 +187,7 @@ let sigT_info = lazy
     ci_pp_info   =  { ind_nargs = 0; style = LetStyle }
   }
 
-let telescope = function
+let rec telescope = function
   | [] -> assert false
   | [(n, None, t)] -> t, [n, Some (mkRel 1), t], mkRel 1
   | (n, None, t) :: tl ->
@@ -208,7 +208,8 @@ let telescope = function
 	(List.rev tys) tl (mkRel 1, [])
       in ty, ((n, Some last, t) :: subst), constr
 
-  | _ -> raise (Invalid_argument "telescope")
+  | (n, Some b, t) :: tl -> let ty, subst, term = telescope tl in
+      ty, ((n, Some b, t) :: subst), lift 1 term
 
 let nf_evar_context isevars ctx =
   List.map (fun (n, b, t) ->
diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
index 0f24915e30..55991c8e88 100644
--- a/plugins/subtac/subtac_command.mli
+++ b/plugins/subtac/subtac_command.mli
@@ -43,7 +43,7 @@ val interp_binder :     Evd.evar_map ref ->
 
 
 val telescope :
-  (Names.name * 'a option * Term.types) list ->
+  (Names.name * Term.types option * Term.types) list ->
   Term.types * (Names.name * Term.types option * Term.types) list *
     Term.constr
 
diff --git a/test-suite/bugs/closed/shouldsucceed/2393.v b/test-suite/bugs/closed/shouldsucceed/2393.v
new file mode 100644
index 0000000000..6a559e75c3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2393.v
@@ -0,0 +1,16 @@
+Require Import Program.
+
+Inductive T := MkT.
+
+Definition sizeOf (t : T) : nat
+    := match t with
+       | MkT => 1
+       end.
+Variable vect : nat -> Type.
+Program Fixpoint idType (t : T) (n := sizeOf t) (b : vect n) {measure n} : T
+    := match t with
+       | MkT => MkT
+       end.
+
+Require Import Wf_nat.
+Solve Obligations using auto with arith.