From 183c4bbe325390f729b1b35985b5f5524a46b907 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 12 Oct 2010 14:00:10 +0000
Subject: Fix bug #2393: allow let-ins inside telescopes (only fails when
 there's no undefined variables in the context now).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13532 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_command.ml  | 5 +++--
 plugins/subtac/subtac_command.mli | 2 +-
 2 files changed, 4 insertions(+), 3 deletions(-)

(limited to 'plugins')

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
 
-- 
cgit v1.2.3