diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-04-04 16:55:56 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-04-04 16:55:56 +0200 |
| commit | c112063ba5f562d511ed0cbd754a41539fc48fe1 (patch) | |
| tree | 1f7e244b3d3b0963d07463604d77bdf35001e67c /plugins/ssrmatching | |
| parent | b824d8ad00001f6c41d0fc8bbf528dccb937c887 (diff) | |
| parent | ea10a2da9ac11ea57e9eb80d0d6baf9321886da4 (diff) | |
Merge branch 'trunk' into pr379
Diffstat (limited to 'plugins/ssrmatching')
| -rw-r--r-- | plugins/ssrmatching/ssrmatching.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 01e20d0f1..3150d6a1b 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -156,7 +156,7 @@ let mkCHole loc = CHole (loc, None, IntroAnonymous, None) let mkCLambda loc name ty t = CLambdaN (loc, [[loc, name], Default Explicit, ty], t) let mkCLetIn loc name bo t = - CLetIn (loc, (loc, name), bo, t) + CLetIn (loc, (loc, name), bo, None, t) let mkCCast loc t ty = CCast (loc,t, dC ty) (** Constructors for rawconstr *) let mkRHole = GHole (dummy_loc, InternalHole, IntroAnonymous, None) @@ -1204,7 +1204,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = pp(lazy(str"typed as: " ++ pr_pattern_w_ids red)); let mkXLetIn loc x (a,(g,c)) = match c with | Some b -> a,(g,Some (mkCLetIn loc x (mkCHole loc) b)) - | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), g), None) in + | None -> a,(GLetIn (loc,x,(GHole (loc, BinderType x, IntroAnonymous, None)), None, g), None) in match red with | T t -> let sigma, t = interp_term ist gl t in sigma, T t | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t |