diff options
| author | msozeau | 2010-10-12 14:00:10 +0000 |
|---|---|---|
| committer | msozeau | 2010-10-12 14:00:10 +0000 |
| commit | 183c4bbe325390f729b1b35985b5f5524a46b907 (patch) | |
| tree | ebdafe15722b78fe423477f89a81f6f92325cb96 /plugins | |
| parent | f815aa9b59892a6c7cd2823c3c2a2424e616d4f2 (diff) | |
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
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 5 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.mli | 2 |
2 files changed, 4 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 |