diff options
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 22 |
1 files changed, 12 insertions, 10 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 24894fc9f5..5ede9d6a99 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -16,6 +16,7 @@ open Names open Nameops open Namegen open Constr +open Context open Libnames open Globnames open Impargs @@ -1020,6 +1021,7 @@ let sort_info_of_level_info (info: level_info) : (Libnames.qualid * int) option let glob_sort_of_level (level: glob_level) : glob_sort = match level with + | GSProp -> GSProp | GProp -> GProp | GSet -> GSet | GType info -> GType [sort_info_of_level_info info] @@ -1188,7 +1190,6 @@ let check_constructor_length env loc cstr len_pl pl0 = (error_wrong_numarg_constructor ?loc env cstr (Inductiveops.constructor_nrealargs cstr))) -open Term open Declarations (* Similar to Cases.adjust_local_defs but on RCPat *) @@ -1197,16 +1198,15 @@ let insert_local_defs_in_pattern (ind,j) l = if mip.mind_consnrealdecls.(j-1) = mip.mind_consnrealargs.(j-1) then (* Optimisation *) l else - let typi = mip.mind_nf_lc.(j-1) in - let (_,typi) = decompose_prod_n_assum (Context.Rel.length mib.mind_params_ctxt) typi in - let (decls,_) = decompose_prod_assum typi in + let (ctx, _) = mip.mind_nf_lc.(j-1) in + let decls = List.skipn (Context.Rel.length mib.mind_params_ctxt) (List.rev ctx) in let rec aux decls args = match decls, args with | Context.Rel.Declaration.LocalDef _ :: decls, args -> (DAst.make @@ RCPatAtom None) :: aux decls args | _, [] -> [] (* In particular, if there were trailing local defs, they have been inserted *) | Context.Rel.Declaration.LocalAssum _ :: decls, a :: args -> a :: aux decls args | _ -> assert false in - aux (List.rev decls) l + aux decls l let add_local_defs_and_check_length loc env g pl args = match g with | ConstructRef cstr -> @@ -2184,7 +2184,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = (add_name match_acc CAst.(make ?loc x)) (CAst.make ?loc x::var_acc) | _ -> let fresh = - Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in + Namegen.next_name_away_with_default_using_types "iV" cano_name.binder_name forbidden_names (EConstr.of_constr ty) in canonize_args t tt (Id.Set.add fresh forbidden_names) ((fresh,c)::match_acc) ((CAst.make ?loc:(cases_pattern_loc c) @@ Name fresh)::var_acc) end @@ -2433,9 +2433,10 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = in let sigma, t = understand_tcc ~flags env sigma ~expected_type:IsType t' in match b with - None -> - let d = LocalAssum (na,t) in - let impls = + None -> + let r = Retyping.relevance_of_type env sigma t in + let d = LocalAssum (make_annot na r,t) in + let impls = if k == Implicit then let na = match na with Name n -> Some n | Anonymous -> None in (ExplByPos (n, na), (true, true, true)) :: impls @@ -2444,7 +2445,8 @@ let interp_glob_context_evars ?(program_mode=false) env sigma k bl = (push_rel d env, sigma, d::params, succ n, impls) | Some b -> let sigma, c = understand_tcc ~flags env sigma ~expected_type:(OfType t) b in - let d = LocalDef (na, c, t) in + let r = Retyping.relevance_of_type env sigma t in + let d = LocalDef (make_annot na r, c, t) in (push_rel d env, sigma, d::params, n, impls)) (env,sigma,[],k+1,[]) (List.rev bl) in sigma, ((env, par), impls) |