aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
Diffstat (limited to 'interp')
-rw-r--r--interp/constrintern.ml30
1 files changed, 17 insertions, 13 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 8e2e3bd23..5c9a12c29 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -442,6 +442,22 @@ let intern_letin_binder intern ntnvars env ((loc,na as locna),def,ty) =
(push_name_env ntnvars (impls_term_list term) env locna,
(na,Explicit,term,ty))
+let intern_cases_pattern_as_binder ?loc ntnvars env p =
+ let il,cp =
+ match !intern_cases_pattern_fwd ntnvars (None,env.scopes) p with
+ | (il, [(subst,cp)]) ->
+ if not (Id.Map.equal Id.equal subst Id.Map.empty) then
+ user_err ?loc (str "Unsupported nested \"as\" clause.");
+ il,cp
+ | _ -> assert false
+ in
+ let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
+ let na = alias_of_pat cp in
+ let ienv = Name.fold_right Id.Set.remove na env.ids in
+ let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in
+ let na = (loc, Name id) in
+ env,((cp,il),id),na
+
let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = function
| CLocalAssum(nal,bk,ty) ->
let env, bl' = intern_assumption intern ntnvars env nal bk ty in
@@ -456,19 +472,7 @@ let intern_local_binder_aux ?(global_level=false) intern ntnvars (env,bl) = func
| Some ty -> ty
| None -> CAst.make ?loc @@ CHole(None,Misctypes.IntroAnonymous,None)
in
- let il,cp =
- match !intern_cases_pattern_fwd ntnvars (None,env.scopes) p with
- | (il, [(subst,cp)]) ->
- if not (Id.Map.equal Id.equal subst Id.Map.empty) then
- user_err ?loc (str "Unsupported nested \"as\" clause.");
- il,cp
- | _ -> assert false
- in
- let env = {env with ids = List.fold_right Id.Set.add il env.ids} in
- let na = alias_of_pat cp in
- let ienv = Name.fold_right Id.Set.remove na env.ids in
- let id = Namegen.next_name_away_with_default "pat" (alias_of_pat cp) ienv in
- let na = (loc, Name id) in
+ let env, ((cp,il),id),na = intern_cases_pattern_as_binder ?loc ntnvars env p in
let bk = Default Explicit in
let _, bl' = intern_assumption intern ntnvars env [na] bk tyc in
let _,(_,bk,t) = List.hd bl' in