From 6b9a9124d3bd24fe9305df613547139f6f609c60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 10 Aug 2017 16:15:57 +0200 Subject: Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr. The motivations are: - To reflect the concrete syntax more closely. - To factorize the different places where "contexts" are internalized: before this patch, there is a different treatment of `Definition f '(x,y) := x+y` and `Definition f := fun '(x,y) => x+y`, and a hack to interpret `Definition f `pat := c : t`. With the patch, the fix to avoid seeing a variable named `pat` works for both `fun 'x => ...` and `Definition f 'x := ...`. The drawbacks are: - Counterpart to reflecting the concrete syntax more closerly, there are more redundancies in the syntax. For instance, the case `CLetIn (na,b,t,c)` can appears also in the form `CProdN (CLocalDef (na,b,t)::rest,d)` and `CLambdaN (CLocalDef (na,b,t)::rest,d)`. - Changes in the API, hence adaptation of plugins referring to `constr_expr` needed. --- plugins/ltac/pptactic.ml | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) (limited to 'plugins/ltac/pptactic.ml') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index e5ff473568..4f430b79e4 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -353,9 +353,10 @@ let string_of_genarg_arg (ArgumentType arg) = let rec strip_ty acc n ty = match ty.CAst.v with Constrexpr.CProdN(bll,a) -> - let nb = - List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in - let bll = List.map (fun (x, _, y) -> x, y) bll in + let bll = List.map (function + | CLocalAssum (nal,_,t) -> nal,t + | _ -> user_err Pp.(str "Cannot translate fix tactic: not only products")) bll in + let nb = List.fold_left (fun i (nal,t) -> i + List.length nal) 0 bll in if nb >= n then (List.rev (bll@acc)), a else strip_ty (bll@acc) (n-nb) a | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in -- cgit v1.2.3