diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-21 19:02:56 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-21 19:02:56 +0100 |
| commit | 4b0fe4e09d547f0e6ee98da3fd6f7a134e51f3fd (patch) | |
| tree | 9550d5b99c9023c9c0ad84d2d7b89e05f344348b /plugins/ssr/ssrcommon.ml | |
| parent | 2f13806f10b2781f84417014c8018097c8e8b2ad (diff) | |
| parent | 2aff5c40ba9b40b4e0188b799dde6f31585e356b (diff) | |
Merge PR #982: Miscellaneous extensions of notations (including granting BZ5585)
Diffstat (limited to 'plugins/ssr/ssrcommon.ml')
| -rw-r--r-- | plugins/ssr/ssrcommon.ml | 6 |
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 |