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.

1 files changed, 3 insertions, 3 deletions

diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 9822da1c7..499154d50 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -835,9 +835,9 @@ let rec mkCHoles ?loc n =
   if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1)
 let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
 let mkCLambda ?loc name ty t =  CAst.make ?loc @@
-   CLambdaN ([[loc, name], Default Explicit, ty], t)
+   CLambdaN ([CLocalAssum([loc, name], Default Explicit, ty)], t)
 let mkCArrow ?loc ty t = CAst.make ?loc @@
-   CProdN ([[Loc.tag Anonymous], Default Explicit, ty], t)
+   CProdN ([CLocalAssum([Loc.tag Anonymous], Default Explicit, ty)], t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, CastConv ty)
 
 let rec isCHoles = function { CAst.v = CHole _ } :: cl -> isCHoles cl | cl -> cl = []
@@ -855,7 +855,7 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
    | _, (_, Some ty) ->
     let rec force_type ty = CAst.(map (function
      | CProdN (abs, t) ->
-       n_binders := !n_binders +  List.length (List.flatten (List.map pi1 abs));
+       n_binders := !n_binders + List.length (List.flatten (List.map (function CLocalAssum (nal,_,_) -> nal | CLocalDef (na,_,_) -> [na] | CLocalPattern (_,_) -> (* We count a 'pat for 1; TO BE CHECKED *) [Loc.tag Name.Anonymous]) abs));
        CProdN (abs, force_type t)
      | CLetIn (n, v, oty, t) -> incr n_binders; CLetIn (n, v, oty, force_type t)
      | _ -> (mkCCast ty (mkCType None)).v)) ty in