diff options
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/classes.ml | 8 | ||||
| -rw-r--r-- | toplevel/command.ml | 8 | ||||
| -rw-r--r-- | toplevel/command.mli | 5 | ||||
| -rw-r--r-- | toplevel/record.ml | 2 |
4 files changed, 12 insertions, 11 deletions
diff --git a/toplevel/classes.ml b/toplevel/classes.ml index 8dcbf4b28..bf9ee1269 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -99,7 +99,7 @@ let interp_type_evars evdref env ?(impls=([],[])) typ = let mk_interning_data env na impls typ = let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (na, ([], impl, Notation.compute_arguments_scope typ)) + in (na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) let interp_fields_evars isevars env avoid l = List.fold_left @@ -160,8 +160,8 @@ let new_class id par ar sup props = let supnames = List.fold_left (fun acc b -> match b with - LocalRawAssum (nl, _, _) -> nl @ acc - | LocalRawDef _ -> assert(false)) + | LocalRawAssum (nl, _, _) -> nl @ acc + | LocalRawDef _ -> assert(false)) [] sup in @@ -241,7 +241,7 @@ let new_class id par ar sup props = params arity fieldimpls fields ~kind:Method ~name:idarg false (List.map (fun _ -> false) fields) in IndRef (kn,0), (List.map2 (fun (id, _, _) y -> Nameops.out_name id, Option.get y) - fields (Recordops.lookup_projections (kn,0))) + (List.rev fields) (Recordops.lookup_projections (kn,0))) in let ctx_context = List.map (fun ((na, b, t) as d) -> diff --git a/toplevel/command.ml b/toplevel/command.ml index f18cecb20..9ae3f8e82 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -442,7 +442,7 @@ let declare_eliminations sp = (* 3b| Mutual inductive definitions *) -let compute_interning_datas env l nal typl impll = +let compute_interning_datas env ty l nal typl impll = let mk_interning_data na typ impls = let idl, impl = let impl = @@ -452,7 +452,7 @@ let compute_interning_datas env l nal typl impll = let sub_impl' = List.filter is_status_implicit sub_impl in (List.map name_of_implicit sub_impl', impl) in - (na, (idl, impl, compute_arguments_scope typ)) in + (na, (ty, idl, impl, compute_arguments_scope typ)) in (l, list_map3 mk_interning_data nal typl impll) let declare_interning_data (_,impls) (df,c,scope) = @@ -526,7 +526,7 @@ let interp_mutual paramsl indl notations finite = (* Compute interpretation metadatas *) let indimpls = List.map (fun _ -> userimpls) fullarities in - let impls = compute_interning_datas env0 params indnames fullarities indimpls in + let impls = compute_interning_datas env0 Inductive params indnames fullarities indimpls in let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in let constructors = @@ -832,7 +832,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_types env fixnames fixtypes in (* Get interpretation metadatas *) - let impls = compute_interning_datas env [] fixnames fixtypes fiximps in + let impls = compute_interning_datas env Recursive [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) diff --git a/toplevel/command.mli b/toplevel/command.mli index 227152f14..a1e976c79 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -56,10 +56,11 @@ val declare_assumption : identifier located list -> val declare_interning_data : 'a * Constrintern.implicits_env -> string * Topconstr.constr_expr * Topconstr.scope_name option -> unit -val compute_interning_datas : Environ.env -> 'a list -> 'b list -> +val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type -> + 'a list -> 'b list -> Term.types list ->Impargs.manual_explicitation list list -> 'a list * - ('b * (Names.identifier list * Impargs.implicits_list * + ('b * (Constrintern.var_internalisation_type * Names.identifier list * Impargs.implicits_list * Topconstr.scope_name option list)) list diff --git a/toplevel/record.ml b/toplevel/record.ml index b1271f516..ae97a8db4 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -38,7 +38,7 @@ let interp_evars evdref env ?(impls=([],[])) k typ = let mk_interning_data env na impls typ = let impl = Impargs.compute_implicits_with_manual env typ (Impargs.is_implicit_args()) impls - in (out_name na, ([], impl, Notation.compute_arguments_scope typ)) + in (out_name na, (Constrintern.Method, [], impl, Notation.compute_arguments_scope typ)) let interp_fields_evars isevars env l = List.fold_left |