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 | |
| 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
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 5 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.mli | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2393.v | 16 |
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. |