aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib
diff options
context:
space:
mode:
Diffstat (limited to 'contrib')
-rw-r--r--contrib/funind/merge.ml2
-rw-r--r--contrib/funind/rawterm_to_relation.ml2
-rw-r--r--contrib/interface/name_to_ast.ml2
-rw-r--r--contrib/interface/xlate.ml6
-rw-r--r--contrib/subtac/subtac_classes.ml91
-rw-r--r--contrib/subtac/subtac_classes.mli4
-rw-r--r--contrib/subtac/subtac_command.ml2
7 files changed, 56 insertions, 53 deletions
diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml
index b7cee7390..9bbd165df 100644
--- a/contrib/funind/merge.ml
+++ b/contrib/funind/merge.ml
@@ -863,7 +863,7 @@ let rawterm_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
List.map (* zeta_normalize t ? *)
(fun (id,t) -> false, ((dummy_loc,id),rawterm_to_constr_expr t))
rawlist in
- lident , bindlist , cstr_expr , lcstor_expr
+ lident , bindlist , Some cstr_expr , lcstor_expr
diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml
index c16e645c7..75f6207fc 100644
--- a/contrib/funind/rawterm_to_relation.ml
+++ b/contrib/funind/rawterm_to_relation.ml
@@ -1192,7 +1192,7 @@ let do_build_inductive
let rel_ind i ext_rel_constructors =
((dummy_loc,relnames.(i)),
rel_params,
- rel_arities.(i),
+ Some rel_arities.(i),
ext_rel_constructors),None
in
let ext_rel_constructors = (Array.mapi rel_ind ext_rels_constructors) in
diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml
index 7ee38fc23..f41d88bd6 100644
--- a/contrib/interface/name_to_ast.ml
+++ b/contrib/interface/name_to_ast.ml
@@ -109,7 +109,7 @@ let convert_one_inductive sp tyi =
let sp = sp_of_global (IndRef (sp, tyi)) in
(((dummy_loc,basename sp),
convert_env(List.rev params),
- (extern_constr true envpar arity),
+ Some (extern_constr true envpar arity),
Constructors (convert_constructors envpar cstrnames cstrtypes)), None);;
(* This function converts a Mutual inductive definition to a Coqast.t.
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 73acbf0f3..8ec6cfb2f 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1979,14 +1979,14 @@ let rec xlate_vernac =
((if add_coercion then CT_coercion_atm else
CT_coerce_NONE_to_COERCION_OPT(CT_none)),
xlate_ident s, xlate_binder_list binders,
- xlate_formula c1, record_constructor,
+ xlate_formula (Option.get c1), record_constructor,
build_record_field_list field_list)
| VernacInductive (isind, lmi) ->
let co_or_ind = if isind then "Inductive" else "CoInductive" in
let strip_mutind = function
(((_,s), parameters, c, Constructors constructors), notopt) ->
CT_ind_spec
- (xlate_ident s, xlate_binder_list parameters, xlate_formula c,
+ (xlate_ident s, xlate_binder_list parameters, xlate_formula (Option.get c),
build_constructors constructors,
translate_opt_notation_decl notopt)
| _ -> xlate_error "TODO: Record notation in (Co)Inductive" in
@@ -2148,7 +2148,7 @@ let rec xlate_vernac =
(* Type Classes *)
| VernacDeclareInstance _|VernacContext _|
- VernacInstance (_, _, _, _, _)|VernacClass (_, _, _, _, _) ->
+ VernacInstance (_, _, _, _, _) ->
xlate_error "TODO: Type Classes commands"
| VernacResetName id -> CT_reset (xlate_ident (snd id))
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index 7b8d982d1..150abd8d6 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -122,58 +122,61 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
in
let id =
match snd instid with
- Name id ->
- let sp = Lib.make_path id in
- if Nametab.exists_cci sp then
- errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
- id
- | Anonymous ->
- let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
- Termops.next_global_ident_away false i (Termops.ids_of_context env)
+ | Name id ->
+ let sp = Lib.make_path id in
+ if Nametab.exists_cci sp then
+ errorlabstrm "new_instance" (Nameops.pr_id id ++ Pp.str " already exists");
+ id
+ | Anonymous ->
+ let i = Nameops.add_suffix (Classes.id_of_class k) "_instance_0" in
+ Termops.next_global_ident_away false i (Termops.ids_of_context env)
in
let env' = push_rel_context ctx' env in
isevars := Evarutil.nf_evar_defs !isevars;
isevars := resolve_typeclasses ~onlyargs:false ~fail:true env' !isevars;
let sigma = Evd.evars_of !isevars in
let substctx = List.map (Evarutil.nf_evar sigma) subst in
- let subst, _propsctx =
- let props =
- List.map (fun (x, l, d) ->
- x, Topconstr.abstract_constr_expr d (Classes.binders_of_lidents l))
- props
- in
+ let subst =
+ let props = match props with CRecord (loc, _, fs) -> fs | _ -> assert false in
if List.length props > List.length k.cl_props then
Classes.mismatched_props env' (List.map snd props) k.cl_props;
- let props, rest =
- List.fold_left
- (fun (props, rest) (id,_,_) ->
- try
- let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
- let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
- Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
- c :: props, rest'
- with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
- ([], props) k.cl_props
- in
- if rest <> [] then
- unbound_method env' k.cl_impl (fst (List.hd rest))
- else
- type_ctx_instance isevars env' k.cl_props props substctx
+ match k.cl_props with
+ | [(na,b,ty)] ->
+ let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in
+ let ty' = substl subst ty in
+ let c = interp_casted_constr_evars isevars env' term ty' in
+ c :: subst
+ | _ ->
+ let props, rest =
+ List.fold_left
+ (fun (props, rest) (id,_,_) ->
+ try
+ let ((loc, mid), c) = List.find (fun ((_,id'), c) -> Name id' = id) rest in
+ let rest' = List.filter (fun ((_,id'), c) -> Name id' <> id) rest in
+ Option.iter (fun x -> Dumpglob.add_glob loc (ConstRef x)) (List.assoc mid k.cl_projs);
+ c :: props, rest'
+ with Not_found -> (CHole (Util.dummy_loc, None) :: props), rest)
+ ([], props) k.cl_props
+ in
+ if rest <> [] then
+ unbound_method env' k.cl_impl (fst (List.hd rest))
+ else
+ fst (type_ctx_instance isevars env' k.cl_props props substctx)
in
let inst_constr, ty_constr = instance_constructor k (List.rev subst) in
- isevars := Evarutil.nf_evar_defs !isevars;
- let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
- and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx')
+ isevars := Evarutil.nf_evar_defs !isevars;
+ let term = Evarutil.nf_isevar !isevars (it_mkLambda_or_LetIn inst_constr ctx')
+ and termtype = Evarutil.nf_isevar !isevars (it_mkProd_or_LetIn ty_constr ctx')
+ in
+ isevars := undefined_evars !isevars;
+ Evarutil.check_evars env Evd.empty !isevars termtype;
+ let hook gr =
+ let cst = match gr with ConstRef kn -> kn | _ -> assert false in
+ let inst = Typeclasses.new_instance k pri global cst in
+ Impargs.declare_manual_implicits false gr ~enriching:false imps;
+ Typeclasses.add_instance inst
in
- isevars := undefined_evars !isevars;
- Evarutil.check_evars env Evd.empty !isevars termtype;
- let hook gr =
- let cst = match gr with ConstRef kn -> kn | _ -> assert false in
- let inst = Typeclasses.new_instance k pri global cst in
- Impargs.declare_manual_implicits false gr ~enriching:false imps;
- Typeclasses.add_instance inst
- in
- let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
- let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
- id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
-
+ let evm = Subtac_utils.evars_of_term (Evd.evars_of !isevars) Evd.empty term in
+ let obls, constr, typ = Eterm.eterm_obligations env id !isevars evm 0 term termtype in
+ id, Subtac_obligations.add_definition id constr typ ~kind:(Global,false,Instance) ~hook obls
+
diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli
index 583c1a165..917ed8059 100644
--- a/contrib/subtac/subtac_classes.mli
+++ b/contrib/subtac/subtac_classes.mli
@@ -34,9 +34,9 @@ val type_ctx_instance : Evd.evar_defs ref ->
val new_instance :
?global:bool ->
- Topconstr.local_binder list ->
+ local_binder list ->
typeclass_constraint ->
- binder_def_list ->
+ constr_expr ->
?generalize:bool ->
int option ->
identifier * Subtac_obligations.progress
diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml
index 191400212..4876b0655 100644
--- a/contrib/subtac/subtac_command.ml
+++ b/contrib/subtac/subtac_command.ml
@@ -99,7 +99,7 @@ let interp_binder sigma env na t =
SPretyping.pretype_gen sigma env ([], []) IsType (locate_if_isevar (loc_of_rawconstr t) na t)
let interp_context_evars evdref env params =
- let bl = Constrintern.intern_context (Evd.evars_of !evdref) env params in
+ let bl = Constrintern.intern_context false (Evd.evars_of !evdref) env params in
let (env, par, _, impls) =
List.fold_left
(fun (env,params,n,impls) (na, k, b, t) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 00:38:49 +0000