diff options
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 |