diff options
Diffstat (limited to 'contrib')
25 files changed, 542 insertions, 216 deletions
diff --git a/contrib/first-order/instances.ml b/contrib/first-order/instances.ml index 8eeb8b642d..56cea8e075 100644 --- a/contrib/first-order/instances.ml +++ b/contrib/first-order/instances.ml @@ -125,9 +125,9 @@ let mk_open_instance id gl m t= let rec raux n t= if n=0 then t else match t with - RLambda(loc,name,_,t0)-> + RLambda(loc,name,k,_,t0)-> let t1=raux (n-1) t0 in - RLambda(loc,name,RHole (dummy_loc,Evd.BinderType name),t1) + RLambda(loc,name,k,RHole (dummy_loc,Evd.BinderType name),t1) | _-> anomaly "can't happen" in let ntt=try Pretyping.Default.understand evmap env (raux m rawt) diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 612be05e3b..97f7c1d97a 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -139,8 +139,8 @@ type newfixpoint_expr = let rec abstract_rawconstr c = function | [] -> c | Topconstr.LocalRawDef (x,b)::bl -> Topconstr.mkLetInC(x,b,abstract_rawconstr c bl) - | Topconstr.LocalRawAssum (idl,t)::bl -> - List.fold_right (fun x b -> Topconstr.mkLambdaC([x],t,b)) idl + | Topconstr.LocalRawAssum (idl,k,t)::bl -> + List.fold_right (fun x b -> Topconstr.mkLambdaC([x],k,t,b)) idl (abstract_rawconstr c bl) let interp_casted_constr_with_implicits sigma env impls c = @@ -213,7 +213,7 @@ let rec is_rec names = | RRec _ -> error "RRec not handled" | RIf(_,b,_,lhs,rhs) -> (lookup names b) || (lookup names lhs) || (lookup names rhs) - | RLetIn(_,na,t,b) | RLambda(_,na,t,b) | RProd(_,na,t,b) -> + | RLetIn(_,na,t,b) | RLambda(_,na,_,t,b) | RProd(_,na,_,t,b) -> lookup names t || lookup (Nameops.name_fold Idset.remove na names) b | RLetTuple(_,nal,_,t,b) -> lookup names t || lookup @@ -434,7 +434,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b | None -> begin match args with - | [Topconstr.LocalRawAssum ([(_,Name x)],t)] -> t,x + | [Topconstr.LocalRawAssum ([(_,Name x)],k,t)] -> t,x | _ -> error "Recursive argument must be specified" end | Some wf_args -> @@ -442,7 +442,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b match List.find (function - | Topconstr.LocalRawAssum(l,t) -> + | Topconstr.LocalRawAssum(l,k,t) -> List.exists (function (_,Name id) -> id = wf_args | _ -> false) l @@ -450,7 +450,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b ) args with - | Topconstr.LocalRawAssum(_,t) -> t,wf_args + | Topconstr.LocalRawAssum(_,k,t) -> t,wf_args | _ -> assert false with Not_found -> assert false in @@ -462,7 +462,7 @@ let register_mes fname rec_impls wf_mes_expr wf_arg using_lemmas args ret_type b let fun_from_mes = let applied_mes = Topconstr.mkAppC(wf_mes_expr,[Topconstr.mkIdentC wf_arg]) in - Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],wf_arg_type,applied_mes) + Topconstr.mkLambdaC ([(dummy_loc,Name wf_arg)],Topconstr.default_binder_kind,wf_arg_type,applied_mes) in let wf_rel_from_mes = Topconstr.mkAppC(Topconstr.mkRefC ltof,[wf_arg_type;fun_from_mes]) @@ -570,11 +570,11 @@ let rec add_args id new_args b = CArrow(loc,add_args id new_args b1, add_args id new_args b2) | CProdN(loc,nal,b1) -> CProdN(loc, - List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, + List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) | CLambdaN(loc,nal,b1) -> CLambdaN(loc, - List.map (fun (nal,b2) -> (nal,add_args id new_args b2)) nal, + List.map (fun (nal,k,b2) -> (nal,k,add_args id new_args b2)) nal, add_args id new_args b1) | CLetIn(loc,na,b1,b2) -> CLetIn(loc,na,add_args id new_args b1,add_args id new_args b2) @@ -644,13 +644,15 @@ let rec chop_n_arrow n t = let new_n = let rec aux (n:int) = function [] -> n - | (nal,t'')::nal_ta' -> + | (nal,k,t'')::nal_ta' -> let nal_l = List.length nal in if n >= nal_l then aux (n - nal_l) nal_ta' else - let new_t' = Topconstr.CProdN(dummy_loc,((snd (list_chop n nal)),t'')::nal_ta',t') + let new_t' = + Topconstr.CProdN(dummy_loc, + ((snd (list_chop n nal)),k,t'')::nal_ta',t') in raise (Stop new_t') in @@ -668,12 +670,12 @@ let rec get_args b t : Topconstr.local_binder list * | Topconstr.CLambdaN (loc, (nal_ta), b') -> begin let n = - (List.fold_left (fun n (nal,_) -> + (List.fold_left (fun n (nal,_,_) -> n+List.length nal) 0 nal_ta ) in let nal_tas,b'',t'' = get_args b' (chop_n_arrow n t) in - (List.map (fun (nal,ta) -> - (Topconstr.LocalRawAssum (nal,ta))) nal_ta)@nal_tas, b'',t'' + (List.map (fun (nal,k,ta) -> + (Topconstr.LocalRawAssum (nal,k,ta))) nal_ta)@nal_tas, b'',t'' end | _ -> [],b,t @@ -716,7 +718,7 @@ let make_graph (f_ref:global_reference) = (List.map (function | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_) -> nal + | Topconstr.LocalRawAssum (nal,_,_) -> nal ) bl ) @@ -730,7 +732,7 @@ let make_graph (f_ref:global_reference) = (List.map (function | Topconstr.LocalRawDef (na,_)-> [] - | Topconstr.LocalRawAssum (nal,_) -> + | Topconstr.LocalRawAssum (nal,_,_) -> List.map (fun (loc,n) -> CRef(Libnames.Ident(loc, Nameops.out_name n))) diff --git a/contrib/funind/indfun_common.ml b/contrib/funind/indfun_common.ml index 5ad4632e40..78e2c44087 100644 --- a/contrib/funind/indfun_common.ml +++ b/contrib/funind/indfun_common.ml @@ -76,7 +76,7 @@ let chop_rlambda_n = then List.rev acc,rt else match rt with - | Rawterm.RLambda(_,name,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b + | Rawterm.RLambda(_,name,k,t,b) -> chop_lambda_n ((name,t,false)::acc) (n-1) b | Rawterm.RLetIn(_,name,v,b) -> chop_lambda_n ((name,v,true)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rlambda_n", @@ -90,7 +90,7 @@ let chop_rprod_n = then List.rev acc,rt else match rt with - | Rawterm.RProd(_,name,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + | Rawterm.RProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (Util.UserError("chop_rprod_n",str "chop_rprod_n: Not enough products")) in chop_prod_n [] diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index b6398a3291..4b3492b125 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -148,7 +148,7 @@ END VERNAC ARGUMENT EXTEND binder2 [ "(" ne_ident_list(idl) ":" lconstr(c) ")"] -> [ - LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,c) ] + LocalRawAssum (List.map (fun id -> (Util.dummy_loc,Name id)) idl,Topconstr.default_binder_kind,c) ] END diff --git a/contrib/funind/merge.ml b/contrib/funind/merge.ml index 44df085988..adec67e36f 100644 --- a/contrib/funind/merge.ml +++ b/contrib/funind/merge.ml @@ -830,7 +830,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = let _ = prNamedRConstr (string_of_name nme) tp in let _ = prstr " ; " in let typ = rawterm_to_constr_expr tp in - LocalRawAssum ([(dummy_loc,nme)] , typ) :: acc) + LocalRawAssum ([(dummy_loc,nme)], Topconstr.default_binder_kind, typ) :: acc) [] params in let concl = Constrextern.extern_constr false (Global.env()) concl in let arity,_ = @@ -838,7 +838,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) = (fun (acc,env) (nm,_,c) -> let typ = Constrextern.extern_constr false env c in let newenv = Environ.push_rel (nm,None,c) env in - CProdN (dummy_loc, [[(dummy_loc,nm)],typ] , acc) , newenv) + CProdN (dummy_loc, [[(dummy_loc,nm)],Topconstr.default_binder_kind,typ] , acc) , newenv) (concl,Global.env()) (shift.funresprms2 @ shift.funresprms1 @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in @@ -867,7 +867,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] [] t in - RProd (dummy_loc,nme,traw,t2) + RProd (dummy_loc,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false @@ -877,7 +877,7 @@ let mkProd_reldecl (rdecl:rel_declaration) (t2:rawconstr) = match rdecl with | (nme,None,t) -> let traw = Detyping.detype false [] [] t in - RProd (dummy_loc,nme,traw,t2) + RProd (dummy_loc,nme,Explicit,traw,t2) | (_,Some _,_) -> assert false diff --git a/contrib/funind/rawterm_to_relation.ml b/contrib/funind/rawterm_to_relation.ml index 2f6f5914da..9bea4f1e02 100644 --- a/contrib/funind/rawterm_to_relation.ml +++ b/contrib/funind/rawterm_to_relation.ml @@ -586,7 +586,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = | RProd _ -> error "Cannot apply a type" end (* end of the application treatement *) - | RLambda(_,n,t,b) -> + | RLambda(_,n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -601,7 +601,7 @@ let rec build_entry_lc env funnames avoid rt : rawconstr build_entry_return = let new_env = raw_push_named (new_n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in combine_results (combine_lam new_n) t_res b_res - | RProd(_,n,t,b) -> + | RProd(_,n,_,t,b) -> (* we first compute the list of constructor corresponding to the body of the function, then the one corresponding to the type @@ -865,7 +865,7 @@ let is_res id = *) let rec rebuild_cons nb_args relname args crossed_types depth rt = match rt with - | RProd(_,n,t,b) -> + | RProd(_,n,k,t,b) -> let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t::crossed_types in begin @@ -928,7 +928,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = (Idset.filter not_free_in_t id_to_exclude) | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude end - | RLambda(_,n,t,b) -> + | RLambda(_,n,k,t,b) -> begin let not_free_in_t id = not (is_free_in id t) in let new_crossed_types = t :: crossed_types in @@ -944,7 +944,7 @@ let rec rebuild_cons nb_args relname args crossed_types depth rt = then new_b, Idset.remove id (Idset.filter not_free_in_t id_to_exclude) else - RProd(dummy_loc,n,t,new_b),Idset.filter not_free_in_t id_to_exclude + RProd(dummy_loc,n,k,t,new_b),Idset.filter not_free_in_t id_to_exclude | _ -> anomaly "Should not have an anonymous function here" (* We have renamed all the anonymous functions during alpha_renaming phase *) @@ -1016,7 +1016,7 @@ let rec compute_cst_params relnames params = function compute_cst_params_from_app [] (params,rtl) | RApp(_,f,args) -> List.fold_left (compute_cst_params relnames) params (f::args) - | RLambda(_,_,t,b) | RProd(_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> + | RLambda(_,_,_,t,b) | RProd(_,_,_,t,b) | RLetIn(_,_,t,b) | RLetTuple(_,_,_,t,b) -> let t_params = compute_cst_params relnames params t in compute_cst_params relnames t_params b | RCases _ -> params (* If there is still cases at this point they can only be @@ -1153,7 +1153,7 @@ let do_build_inductive else Topconstr.CProdN (dummy_loc, - [[(dummy_loc,n)],Constrextern.extern_rawconstr Idset.empty t], + [[(dummy_loc,n)],Topconstr.default_binder_kind,Constrextern.extern_rawconstr Idset.empty t], acc ) ) @@ -1173,7 +1173,7 @@ let do_build_inductive Topconstr.LocalRawDef((dummy_loc,n), Constrextern.extern_rawconstr Idset.empty t) else Topconstr.LocalRawAssum - ([(dummy_loc,n)], Constrextern.extern_rawconstr Idset.empty t) + ([(dummy_loc,n)], Topconstr.default_binder_kind, Constrextern.extern_rawconstr Idset.empty t) ) rels_params in diff --git a/contrib/funind/rawtermops.ml b/contrib/funind/rawtermops.ml index e8cce47adb..0c03c1e619 100644 --- a/contrib/funind/rawtermops.ml +++ b/contrib/funind/rawtermops.ml @@ -12,8 +12,8 @@ let idmap_is_empty m = m = Idmap.empty let mkRRef ref = RRef(dummy_loc,ref) let mkRVar id = RVar(dummy_loc,id) let mkRApp(rt,rtl) = RApp(dummy_loc,rt,rtl) -let mkRLambda(n,t,b) = RLambda(dummy_loc,n,t,b) -let mkRProd(n,t,b) = RProd(dummy_loc,n,t,b) +let mkRLambda(n,t,b) = RLambda(dummy_loc,n,Explicit,t,b) +let mkRProd(n,t,b) = RProd(dummy_loc,n,Explicit,t,b) let mkRLetIn(n,t,b) = RLetIn(dummy_loc,n,t,b) let mkRCases(rto,l,brl) = RCases(dummy_loc,rto,l,brl) let mkRSort s = RSort(dummy_loc,s) @@ -26,7 +26,7 @@ let mkRCast(b,t) = RCast(dummy_loc,b,CastConv (Term.DEFAULTcast,t)) *) let raw_decompose_prod = let rec raw_decompose_prod args = function - | RProd(_,n,t,b) -> + | RProd(_,n,k,t,b) -> raw_decompose_prod ((n,t)::args) b | rt -> args,rt in @@ -34,7 +34,7 @@ let raw_decompose_prod = let raw_decompose_prod_or_letin = let rec raw_decompose_prod args = function - | RProd(_,n,t,b) -> + | RProd(_,n,k,t,b) -> raw_decompose_prod ((n,None,Some t)::args) b | RLetIn(_,n,t,b) -> raw_decompose_prod ((n,Some t,None)::args) b @@ -58,7 +58,7 @@ let raw_decompose_prod_n n = if i<=0 then args,c else match c with - | RProd(_,n,t,b) -> + | RProd(_,n,_,t,b) -> raw_decompose_prod (i-1) ((n,t)::args) b | rt -> args,rt in @@ -70,7 +70,7 @@ let raw_decompose_prod_or_letin_n n = if i<=0 then args,c else match c with - | RProd(_,n,t,b) -> + | RProd(_,n,_,t,b) -> raw_decompose_prod (i-1) ((n,None,Some t)::args) b | RLetIn(_,n,t,b) -> raw_decompose_prod (i-1) ((n,Some t,None)::args) b @@ -135,15 +135,17 @@ let change_vars = change_vars mapping rt', List.map (change_vars mapping) rtl ) - | RLambda(loc,name,t,b) -> + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, + k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) - | RProd(loc,name,t,b) -> + | RProd(loc,name,k,t,b) -> RProd(loc, name, + k, change_vars mapping t, change_vars (remove_name_from_mapping mapping name) b ) @@ -261,21 +263,21 @@ let rec alpha_rt excluded rt = let new_rt = match rt with | RRef _ | RVar _ | REvar _ | RPatVar _ -> rt - | RLambda(loc,Anonymous,t,b) -> + | RLambda(loc,Anonymous,k,t,b) -> let new_id = Nameops.next_ident_away (id_of_string "_x") excluded in let new_excluded = new_id :: excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - RLambda(loc,Name new_id,new_t,new_b) - | RProd(loc,Anonymous,t,b) -> + RLambda(loc,Name new_id,k,new_t,new_b) + | RProd(loc,Anonymous,k,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in - RProd(loc,Anonymous,new_t,new_b) + RProd(loc,Anonymous,k,new_t,new_b) | RLetIn(loc,Anonymous,t,b) -> let new_t = alpha_rt excluded t in let new_b = alpha_rt excluded b in RLetIn(loc,Anonymous,new_t,new_b) - | RLambda(loc,Name id,t,b) -> + | RLambda(loc,Name id,k,t,b) -> let new_id = Nameops.next_ident_away id excluded in let t,b = if new_id = id @@ -287,8 +289,8 @@ let rec alpha_rt excluded rt = let new_excluded = new_id::excluded in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - RLambda(loc,Name new_id,new_t,new_b) - | RProd(loc,Name id,t,b) -> + RLambda(loc,Name new_id,k,new_t,new_b) + | RProd(loc,Name id,k,t,b) -> let new_id = Nameops.next_ident_away id excluded in let new_excluded = new_id::excluded in let t,b = @@ -300,7 +302,7 @@ let rec alpha_rt excluded rt = in let new_t = alpha_rt new_excluded t in let new_b = alpha_rt new_excluded b in - RProd(loc,Name new_id,new_t,new_b) + RProd(loc,Name new_id,k,new_t,new_b) | RLetIn(loc,Name id,t,b) -> let new_id = Nameops.next_ident_away id excluded in let t,b = @@ -389,7 +391,7 @@ let is_free_in id = | REvar _ -> false | RPatVar _ -> false | RApp(_,rt,rtl) -> List.exists is_free_in (rt::rtl) - | RLambda(_,n,t,b) | RProd(_,n,t,b) | RLetIn(_,n,t,b) -> + | RLambda(_,n,_,t,b) | RProd(_,n,_,t,b) | RLetIn(_,n,t,b) -> let check_in_b = match n with | Name id' -> id_ord id' id <> 0 @@ -460,17 +462,19 @@ let replace_var_by_term x_id term = replace_var_by_pattern rt', List.map replace_var_by_pattern rtl ) - | RLambda(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | RLambda(loc,name,t,b) -> + | RLambda(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, + k, replace_var_by_pattern t, replace_var_by_pattern b ) - | RProd(_,Name id,_,_) when id_ord id x_id == 0 -> rt - | RProd(loc,name,t,b) -> + | RProd(_,Name id,_,_,_) when id_ord id x_id == 0 -> rt + | RProd(loc,name,k,t,b) -> RProd(loc, name, + k, replace_var_by_pattern t, replace_var_by_pattern b ) @@ -590,8 +594,8 @@ let ids_of_rawterm c = | RVar (_,id) -> id::acc | RApp (loc,g,args) -> ids_of_rawterm [] g @ List.flatten (List.map (ids_of_rawterm []) args) @ acc - | RLambda (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc - | RProd (loc,na,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | RLambda (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc + | RProd (loc,na,k,ty,c) -> idof na :: ids_of_rawterm [] ty @ ids_of_rawterm [] c @ acc | RLetIn (loc,na,b,c) -> idof na :: ids_of_rawterm [] b @ ids_of_rawterm [] c @ acc | RCast (loc,c,CastConv(k,t)) -> ids_of_rawterm [] c @ ids_of_rawterm [] t @ acc | RCast (loc,c,CastCoerce) -> ids_of_rawterm [] c @ acc @@ -622,15 +626,17 @@ let zeta_normalize = zeta_normalize_term rt', List.map zeta_normalize_term rtl ) - | RLambda(loc,name,t,b) -> + | RLambda(loc,name,k,t,b) -> RLambda(loc, name, + k, zeta_normalize_term t, zeta_normalize_term b ) - | RProd(loc,name,t,b) -> + | RProd(loc,name,k,t,b) -> RProd(loc, - name, + name, + k, zeta_normalize_term t, zeta_normalize_term b ) @@ -691,8 +697,8 @@ let expand_as = with Not_found -> rt end | RApp(loc,f,args) -> RApp(loc,expand_as map f,List.map (expand_as map) args) - | RLambda(loc,na,t,b) -> RLambda(loc,na,expand_as map t, expand_as map b) - | RProd(loc,na,t,b) -> RProd(loc,na,expand_as map t, expand_as map b) + | RLambda(loc,na,k,t,b) -> RLambda(loc,na,k,expand_as map t, expand_as map b) + | RProd(loc,na,k,t,b) -> RProd(loc,na,k,expand_as map t, expand_as map b) | RLetIn(loc,na,v,b) -> RLetIn(loc,na, expand_as map v,expand_as map b) | RLetTuple(loc,nal,(na,po),v,b) -> RLetTuple(loc,nal,(na,Option.map (expand_as map) po), diff --git a/contrib/interface/name_to_ast.ml b/contrib/interface/name_to_ast.ml index b0a34cfd12..172c7479c2 100644 --- a/contrib/interface/name_to_ast.ml +++ b/contrib/interface/name_to_ast.ml @@ -28,7 +28,7 @@ let convert_env = let convert_binder env (na, b, c) = match b with | Some b -> LocalRawDef ((dummy_loc,na), extern_constr true env b) - | None -> LocalRawAssum ([dummy_loc,na], extern_constr true env c) in + | None -> LocalRawAssum ([dummy_loc,na], default_binder_kind, extern_constr true env c) in let rec cvrec env = function [] -> [] | b::rest -> (convert_binder env b)::(cvrec (push_rel b env) rest) in @@ -140,8 +140,8 @@ let make_variable_ast name typ implicits = let make_definition_ast name c typ implicits = - VernacDefinition ((Global,false,Definition), (dummy_loc,name), DefineBody ([], None, - (constr_to_ast c), Some (constr_to_ast typ)), + VernacDefinition ((Global,false,Definition), (dummy_loc,name), + DefineBody ([], None, constr_to_ast c, Some (constr_to_ast typ)), (fun _ _ -> ())) ::(implicits_to_ast_list implicits);; diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 0e4f660724..05c227de03 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -312,7 +312,7 @@ let make_fix_struct (n,bl) = let rec xlate_binder = function - (l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t) + (l,k,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t) and xlate_return_info = function | (Some Anonymous, None) | (None, None) -> CT_coerce_NONE_to_RETURN_INFO CT_none @@ -325,7 +325,7 @@ and xlate_formula_opt = | Some e -> CT_coerce_FORMULA_to_FORMULA_OPT (xlate_formula e) and xlate_binder_l = function - LocalRawAssum(l,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t) + LocalRawAssum(l,_,t) -> CT_binder(xlate_id_opt_ne_list l, xlate_formula t) | LocalRawDef(n,v) -> CT_coerce_DEF_to_BINDER(CT_def(xlate_id_opt n, xlate_formula v)) and @@ -459,7 +459,7 @@ and xlate_matched_formula = function CT_coerce_FORMULA_to_MATCHED_FORMULA(xlate_formula f) and xlate_formula_expl = function (a, None) -> xlate_formula a - | (a, Some (_,ExplByPos i)) -> + | (a, Some (_,ExplByPos (i, _))) -> xlate_error "explicitation of implicit by rank not supported" | (a, Some (_,ExplByName i)) -> CT_labelled_arg(CT_ident (string_of_id i), xlate_formula a) @@ -1609,7 +1609,7 @@ let rec xlate_vernac = | VernacDeclareTacticDefinition (true, tacs) -> (match List.map (function - ((_, id), body) -> + ((_, id), _, body) -> CT_tac_def(CT_ident (string_of_id id), xlate_tactic body)) tacs with [] -> assert false @@ -1834,6 +1834,10 @@ let rec xlate_vernac = xlate_error "TODO: Print Canonical Structures" | PrintAssumptions _ -> xlate_error "TODO: Print Needed Assumptions" + | PrintInstances _ -> + xlate_error "TODO: Print Instances" + | PrintTypeClasses -> + xlate_error "TODO: Print TypeClasses" | PrintInspect n -> CT_inspect (CT_int n) | PrintUniverses opt_s -> CT_print_universes(ctf_STRING_OPT opt_s) | PrintSetoids -> CT_print_setoids @@ -2075,6 +2079,12 @@ let rec xlate_vernac = | Local -> CT_local in CT_coercion (local_opt, id_opt, xlate_ident id1, xlate_class id2, xlate_class id3) + + (* TypeClasses *) + | VernacSetInstantiationTactic _|VernacDeclareInstance _|VernacContext _| + VernacInstance (_, _, _)|VernacClass (_, _, _, _, _) -> + xlate_error "TODO: Type Classes commands" + | VernacResetName id -> CT_reset (xlate_ident (snd id)) | VernacResetInitial -> CT_restore_state (CT_ident "Initial") | VernacExtend (s, l) -> @@ -2088,7 +2098,7 @@ let rec xlate_vernac = | VernacNop -> CT_proof_no_op | VernacComments l -> CT_scomments(CT_scomment_content_list (List.map xlate_comment l)) - | VernacDeclareImplicits(true, id, opt_positions) -> + | VernacDeclareImplicits(true, id, _, opt_positions) -> CT_implicits (reference_to_ct_ID id, match opt_positions with @@ -2097,11 +2107,11 @@ let rec xlate_vernac = CT_coerce_ID_LIST_to_ID_LIST_OPT (CT_id_list (List.map - (function ExplByPos x, _ + (function ExplByPos (x,_), _, _ -> xlate_error "explication argument by rank is obsolete" - | ExplByName id, _ -> CT_ident (string_of_id id)) l))) - | VernacDeclareImplicits(false, id, opt_positions) -> + | ExplByName id, _, _ -> CT_ident (string_of_id id)) l))) + | VernacDeclareImplicits(false, id, _, opt_positions) -> xlate_error "TODO: Implicit Arguments Global" | VernacReserve((_,a)::l, f) -> CT_reserve(CT_id_ne_list(xlate_ident a, diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 26b6b30944..87c4d9bc79 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -1061,7 +1061,7 @@ let (value_f:constr list -> global_reference -> constr) = List.fold_left2 (fun acc x_id a -> RLambda - (d0, Name x_id, RDynamic(d0, constr_in a), + (d0, Name x_id, Explicit, RDynamic(d0, constr_in a), acc ) ) diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml index d1b4b50ebd..9cb65f76e0 100644 --- a/contrib/subtac/eterm.ml +++ b/contrib/subtac/eterm.ml @@ -121,7 +121,7 @@ let rec chop_product n t = | Prod (_, _, b) -> if noccurn 1 b then chop_product (pred n) (Termops.pop b) else None | _ -> None -let eterm_obligations env name isevars evm fs t tycon = +let eterm_obligations env name isevars evm fs t ty = (* 'Serialize' the evars, we assume that the types of the existentials refer to previous existentials in the list only *) trace (str " In eterm: isevars: " ++ my_print_evardefs isevars); @@ -165,6 +165,7 @@ let eterm_obligations env name isevars evm fs t tycon = let t', _, transparent = (* Substitute evar refs in the term by variables *) subst_evar_constr evts 0 t in + let ty, _, _ = subst_evar_constr evts 0 ty in let evars = List.map (fun (_, ((_, name), _, opaque, typ, deps)) -> name, typ, not (opaque = None) && not (Idset.mem name transparent), deps) evts in @@ -177,7 +178,7 @@ let eterm_obligations env name isevars evm fs t tycon = Termops.print_constr_env (Global.env ()) typ)) evars); with _ -> ()); - Array.of_list (List.rev evars), t' + Array.of_list (List.rev evars), t', ty let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n diff --git a/contrib/subtac/eterm.mli b/contrib/subtac/eterm.mli index a2582c5ca0..e23fd535ca 100644 --- a/contrib/subtac/eterm.mli +++ b/contrib/subtac/eterm.mli @@ -19,9 +19,9 @@ val mkMetas : int -> constr list (* val eterm_term : evar_map -> constr -> types option -> constr * types option * (identifier * types) list *) (* env, id, evars, number of - function prototypes to try to clear from evars contexts, object and optional type *) -val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types option -> - (identifier * types * bool * Intset.t) array * constr + function prototypes to try to clear from evars contexts, object and type *) +val eterm_obligations : env -> identifier -> evar_defs -> evar_map -> int -> constr -> types -> + (identifier * types * bool * Intset.t) array * constr * types (* Obl. name, type as product, opacity (true = opaque) and dependencies as indexes into the array *) val etermtac : open_constr -> tactic diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index c2691c781c..49e312aeb6 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -44,17 +44,20 @@ struct let subtac_nameopt : identifier option Gram.Entry.e = gec "subtac_nameopt" end +open Rawterm open SubtacGram open Util open Pcoq - +open Prim +open Constr let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram - GLOBAL: subtac_gallina_loc Constr.binder_let Constr.binder subtac_nameopt; + GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder_let Constr.binder subtac_nameopt; subtac_gallina_loc: - [ [ g = Vernac.gallina -> loc, g ] ] + [ [ g = Vernac.gallina -> loc, g + | g = Vernac.gallina_ext -> loc, g ] ] ; subtac_nameopt: @@ -63,18 +66,18 @@ GEXTEND Gram ; Constr.binder_let: - [ [ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> - let typ = mkAppC (sigref, [mkLambdaC ([id], t, c)]) in - LocalRawAssum ([id], typ) + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + LocalRawAssum ([id], default_binder_kind, typ) ] ]; Constr.binder: [ [ "("; id=Prim.name; ":"; c=Constr.lconstr; "|"; p=Constr.lconstr; ")" -> - ([id],mkAppC (sigref, [mkLambdaC ([id], c, p)])) + ([id],default_binder_kind, mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, c, p)])) | "("; id=Prim.name; ":"; c=Constr.lconstr; ")" -> - ([id],c) + ([id],default_binder_kind, c) | "("; id=Prim.name; lid=LIST1 Prim.name; ":"; c=Constr.lconstr; ")" -> - (id::lid,c) + (id::lid,default_binder_kind, c) ] ]; END diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index 4f5e302c22..56ebc4f522 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -49,6 +49,22 @@ open Decl_kinds open Tacinterp open Tacexpr +let solve_tccs_in_type env id isevars evm c typ = + if not (evm = Evd.empty) then + let stmt_id = Nameops.add_suffix id "_stmt" in + let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 c typ in + (** Make all obligations transparent so that real dependencies can be sorted out by the user *) + let obls = Array.map (fun (id, t, op, d) -> (id, t, false, d)) obls in + match Subtac_obligations.add_definition stmt_id c' typ obls with + Subtac_obligations.Defined cst -> constant_value (Global.env()) cst + | _ -> + errorlabstrm "start_proof" + (str "The statement obligations could not be resolved automatically, " ++ spc () ++ + str "write a statement definition first.") + else + let _ = Typeops.infer_type env c in c + + let start_proof_com env isevars sopt kind (bl,t) hook = let id = match sopt with | Some id -> @@ -60,21 +76,11 @@ let start_proof_com env isevars sopt kind (bl,t) hook = next_global_ident_away false (id_of_string "Unnamed_thm") (Pfedit.get_all_proof_names ()) in - let evm, c, typ = + let evm, c, typ, _imps = Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr t bl) None in - if not (evm = Evd.empty) then - let stmt_id = Nameops.add_suffix id "_stmt" in - let obls, c' = eterm_obligations env stmt_id !isevars evm 0 c (Some typ) in - match Subtac_obligations.add_definition stmt_id c' typ obls with - Subtac_obligations.Defined cst -> Command.start_proof id kind (constant_value (Global.env()) cst) hook - | _ -> - errorlabstrm "start_proof" - (str "The statement obligations could not be resolved automatically, " ++ spc () ++ - str "write a statement definition first.") - else - let _ = Typeops.infer_type env c in - Command.start_proof id kind c hook + let c = solve_tccs_in_type env id isevars evm c typ in + Command.start_proof id kind c hook let print_subgoals () = Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () @@ -88,10 +94,12 @@ let assumption_message id = Flags.if_verbose message ((string_of_id id) ^ " is assumed") let declare_assumption env isevars idl is_coe k bl c nl = - if not (Pfedit.refining ()) then - let evm, c, typ = - Subtac_pretyping.subtac_process env isevars (snd (List.hd idl)) [] (Command.generalize_constr_expr c bl) None + if not (Pfedit.refining ()) then + let id = snd (List.hd idl) in + let evm, c, typ, imps = + Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None in + let c = solve_tccs_in_type env id isevars evm c typ in List.iter (Command.declare_one_assumption is_coe k c nl) idl else errorlabstrm "Command.Assumption" @@ -114,8 +122,13 @@ let subtac (loc, command) = match command with VernacDefinition (defkind, (locid, id), expr, hook) -> (match expr with - ProveBody (bl, c) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c None) - | DefineBody (bl, _, c, tycon) -> + | ProveBody (bl, t) -> + if Lib.is_modtype () then + errorlabstrm "Subtac_command.StartProof" + (str "Proof editing mode not supported in module types"); + start_proof_and_print env isevars (Some id) (Global, DefinitionBody Definition) (bl,t) + (fun _ _ -> ()) + | DefineBody (bl, _, c, tycon) -> ignore(Subtac_pretyping.subtac_proof env isevars id bl c tycon)) | VernacFixpoint (l, b) -> let _ = trace (str "Building fixpoint") in @@ -135,6 +148,9 @@ let subtac (loc, command) = | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl + | VernacInstance (sup, is, props) -> + Subtac_classes.new_instance sup is props + (* | VernacCoFixpoint (l, b) -> *) (* let _ = trace (str "Building cofixpoint") in *) (* ignore(Subtac_command.build_recursive l b) *) diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index 34c398289a..e46ca822ee 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1395,9 +1395,9 @@ let set_arity_signature dep n arsign tomatchl pred x = let rec decomp_lam_force n avoid l p = if n = 0 then (List.rev l,p,avoid) else match p with - | RLambda (_,(Name id as na),_,c) -> + | RLambda (_,(Name id as na),k,_,c) -> decomp_lam_force (n-1) (id::avoid) (na::l) c - | RLambda (_,(Anonymous as na),_,c) -> decomp_lam_force (n-1) avoid (na::l) c + | RLambda (_,(Anonymous as na),k,_,c) -> decomp_lam_force (n-1) avoid (na::l) c | _ -> let x = next_ident_away (id_of_string "x") avoid in decomp_lam_force (n-1) (x::avoid) (Name x :: l) @@ -2091,13 +2091,12 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e (* let env = nf_evars_env !isevars (env : env) in *) (* trace (str "Evars : " ++ my_print_evardefs !isevars); *) (* trace (str "Env : " ++ my_print_env env); *) - - let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in - let tomatchs_len = List.length tomatchs_lets in - let tycon = lift_tycon tomatchs_len tycon in - let env = push_rel_context tomatchs_lets env in let _isdep = List.exists (fun (x, y) -> is_dependent_ind y) tomatchs in if predopt = None then + let tomatchs, tomatchs_lets = abstract_tomatch env tomatchs in + let tomatchs_len = List.length tomatchs_lets in + let tycon = lift_tycon tomatchs_len tycon in + let env = push_rel_context tomatchs_lets env in let len = List.length eqns in let sign, allnames, signlen, eqs, neqs, args = (* The arity signature *) @@ -2185,7 +2184,6 @@ let compile_cases loc (typing_fun, isevars) (tycon : Evarutil.type_constraint) e let j = compile pb in (* We check for unused patterns *) List.iter (check_unused_pattern env) matx; - let j = { j with uj_val = it_mkLambda_or_LetIn j.uj_val tomatchs_lets } in inh_conv_coerce_to_tycon loc env isevars j tycon end diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml new file mode 100644 index 0000000000..da91b04062 --- /dev/null +++ b/contrib/subtac/subtac_classes.ml @@ -0,0 +1,187 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) + +open Pretyping +open Evd +open Environ +open Term +open Rawterm +open Topconstr +open Names +open Libnames +open Pp +open Vernacexpr +open Constrintern +open Subtac_command +open Typeclasses +open Typeclasses_errors +open Termops +open Decl_kinds +open Entries + +module SPretyping = Subtac_pretyping.Pretyping + +let interp_binder_evars evdref env na t = + let t = Constrintern.intern_gen true (Evd.evars_of !evdref) env t in + SPretyping.understand_tcc_evars evdref env IsType t + +let interp_binders_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) ((loc, i), t) -> + let n = Name i in + let t' = interp_binder_evars isevars env n t in + let d = (i,None,t') in + (push_named d env, i :: ids, d::params)) + (env, avoid, []) l + +let interp_typeclass_context_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) (iid, bk, cl) -> + let t' = interp_binder_evars isevars env (snd iid) cl in + let i = match snd iid with + | Anonymous -> Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids + | Name id -> id + in + let d = (i,None,t') in + (push_named d env, i :: ids, d::params)) + (env, avoid, []) l + +let interp_constrs_evars isevars env avoid l = + List.fold_left + (fun (env, ids, params) t -> + let t' = interp_binder_evars isevars env Anonymous t in + let id = Nameops.next_name_away (Termops.named_hd env t' Anonymous) ids in + let d = (id,None,t') in + (push_named d env, id :: ids, d::params)) + (env, avoid, []) l + +let type_ctx_instance isevars env ctx inst subst = + List.fold_left2 + (fun (subst, instctx) (na, _, t) ce -> + let t' = replace_vars subst t in + let c = interp_casted_constr_evars isevars env ce t' in + let d = na, Some c, t' in + (na, c) :: subst, d :: instctx) + (subst, []) (List.rev ctx) inst + +let substitution_of_constrs ctx cstrs = + List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] + +let new_instance sup (instid, bk, cl) props = + let id, par = Implicit_quantifiers.destClassApp cl in + let env = Global.env() in + let isevars = ref (Evd.create_evar_defs Evd.empty) in + let avoid = Termops.ids_of_context env in + let k = + try class_info (snd id) + with Not_found -> unbound_class env id + in + let gen_ctx, sup = Implicit_quantifiers.resolve_class_binders (vars_of_env env) sup in + let gen_ctx = + let is_free ((_, x), _) = + let f l = not (List.exists (fun ((_, y), _) -> y = x) l) in + let g l = not (List.exists (fun ((_, y), _, _) -> y = Name x) l) in + f gen_ctx && g sup + in + let parbinders = Implicit_quantifiers.compute_constrs_freevars_binders (vars_of_env env) par in + let parbinders' = List.filter is_free parbinders in + gen_ctx @ parbinders' + in + let env', avoid, genctx = interp_binders_evars isevars env avoid gen_ctx in + let env', avoid, supctx = interp_typeclass_context_evars isevars env' avoid sup in + + let subst = + match bk with + | Explicit -> + if List.length par <> List.length k.cl_context + List.length k.cl_params then + Classes.mismatched_params env par (k.cl_params @ k.cl_context); + let len = List.length k.cl_context in + let ctx, par = Util.list_chop len par in + let subst, _ = type_ctx_instance isevars env' k.cl_context ctx [] in + let subst = Typeclasses.substitution_of_named_context isevars env' k.cl_name len subst + k.cl_super + in + let subst, par = type_ctx_instance isevars env' k.cl_params par subst in subst + + | Implicit -> + let t' = interp_type_evars isevars env' (Topconstr.mkAppC (CRef (Ident id), par)) in + match kind_of_term t' with + App (c, args) -> + substitution_of_constrs (k.cl_params @ k.cl_super @ k.cl_context) + (List.rev (Array.to_list args)) + | _ -> assert false + in + isevars := Evarutil.nf_evar_defs !isevars; + let sigma = Evd.evars_of !isevars in + let substctx = Typeclasses.nf_substitution 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 + 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 (_, c) = List.find (fun ((_,id'), c) -> id' = id) rest in + let rest' = List.filter (fun ((_,id'), c) -> id' <> id) rest in + c :: props, rest' + with Not_found -> (CHole Util.dummy_loc :: props), rest) + ([], props) k.cl_props + in + if rest <> [] then + unbound_method env k.cl_name (fst (List.hd rest)) + else + type_ctx_instance isevars env' k.cl_props props substctx + in + let app = + applistc (mkConstruct (k.cl_impl, 1)) (List.rev_map snd subst) + in + let term = it_mkNamedLambda_or_LetIn (it_mkNamedLambda_or_LetIn app supctx) genctx in + isevars := Evarutil.nf_evar_defs !isevars; + let term = Evarutil.nf_isevar !isevars term in + let termtype = + let app = applistc (mkInd (k.cl_impl)) (List.rev_map snd substctx) in + let t = it_mkNamedProd_or_LetIn (it_mkNamedProd_or_LetIn app supctx) genctx in + Evarutil.nf_isevar !isevars t + in + isevars := undefined_evars !isevars; + let id = + match snd instid with + Name id -> id + | Anonymous -> + let i = Nameops.add_suffix (snd id) "_instance_" in + Termops.next_global_ident_away false i (Termops.ids_of_context env) + in + let imps = + Util.list_map_i + (fun i (na, b, t) -> ExplByPos (i, Some na), (true, true)) + 1 (genctx @ List.rev supctx) + in + let hook cst = + let inst = + { is_class = k; + is_name = id; +(* is_params = paramsctx; *) +(* is_super = superctx; *) + is_impl = cst; +(* is_add_hint = (fun () -> Classes.add_instance_hint id); *) + } + in + Classes.add_instance_hint id; + Impargs.declare_manual_implicits false (ConstRef cst) 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 + ignore (Subtac_obligations.add_definition id constr typ ~kind:Instance ~hook obls) diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli new file mode 100644 index 0000000000..ce4b32cad8 --- /dev/null +++ b/contrib/subtac/subtac_classes.mli @@ -0,0 +1,39 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(*i $Id: classes.mli 6748 2005-02-18 22:17:50Z herbelin $ i*) + +(*i*) +open Names +open Decl_kinds +open Term +open Sign +open Evd +open Environ +open Nametab +open Mod_subst +open Topconstr +open Util +open Typeclasses +open Implicit_quantifiers +open Classes +(*i*) + +val type_ctx_instance : Evd.evar_defs ref -> + Environ.env -> + (Names.identifier * 'a * Term.constr) list -> + Topconstr.constr_expr list -> + (Names.identifier * Term.constr) list -> + (Names.identifier * Term.constr) list * + (Names.identifier * Term.constr option * Term.constr) list + +val new_instance : + typeclass_context -> + typeclass_constraint -> + binder_def_list -> + unit diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index a9a30c57af..9afa6f0675 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -98,11 +98,11 @@ let interp_binder sigma env na t = let interp_context sigma env params = List.fold_left (fun (env,params) d -> match d with - | LocalRawAssum ([_,na],(CHole _ as t)) -> + | LocalRawAssum ([_,na],k,(CHole _ as t)) -> let t = interp_binder sigma env na t in let d = (na,None,t) in (push_rel d env, d::params) - | LocalRawAssum (nal,t) -> + | LocalRawAssum (nal,k,t) -> let t = interp_type sigma env t in let ctx = list_map_i (fun i (_,na) -> (na,None,lift i t)) 0 nal in let ctx = List.rev ctx in @@ -152,7 +152,7 @@ let collect_non_rec env = let list_of_local_binders l = let rec aux acc = function Topconstr.LocalRawDef (n, c) :: tl -> aux ((n, Some c, None) :: acc) tl - | Topconstr.LocalRawAssum (nl, c) :: tl -> + | Topconstr.LocalRawAssum (nl, k, c) :: tl -> aux (List.fold_left (fun acc n -> (n, None, Some c) :: acc) acc nl) tl | [] -> List.rev acc in aux [] l @@ -294,12 +294,11 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = lift lift_cst prop ; lift lift_cst intern_body_lam |]) | Some f -> - lift (succ after_length) - (mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), - [| argtyp ; - f ; - lift lift_cst prop ; - lift lift_cst intern_body_lam |])) + mkApp (constr_of_global (Lazy.force fix_measure_sub_ref), + [| lift lift_cst argtyp ; + lift lift_cst f ; + lift lift_cst prop ; + lift lift_cst intern_body_lam |]) in let def_appl = applist (fix_def, gen_rels (after_length + 1)) in let def = it_mkLambda_or_LetIn def_appl binders_rel in @@ -316,13 +315,13 @@ let build_wellfounded (recname, n, bl,arityc,body) r measure notation boxed = let evm = non_instanciated_map env isevars evm in (* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) - let evars, evars_def = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc (Some fullctyp) in + let evars, evars_def, evars_typ = Eterm.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp in (* (try trace (str "Generated obligations : "); *) (* Array.iter *) (* (fun (n, t, _) -> trace (str "Evar " ++ str (string_of_id n) ++ spc () ++ my_print_constr env t)) *) (* evars; *) (* with _ -> ()); *) - Subtac_obligations.add_definition recname evars_def fullctyp evars + Subtac_obligations.add_definition recname evars_def evars_typ evars let nf_evar_context isevars ctx = List.map (fun (n, b, t) -> @@ -412,11 +411,12 @@ let build_mutrec lnameargsardef boxed = (* Generalize by the recursive prototypes *) let def = Termops.it_mkNamedLambda_or_LetIn def rec_sign - and typ = + and typ = Termops.it_mkNamedProd_or_LetIn typ rec_sign in - let evm = Subtac_utils.evars_of_term evm Evd.empty def in - let evars, def = Eterm.eterm_obligations env id isevars evm recdefs def (Some typ) in + let evm' = Subtac_utils.evars_of_term evm Evd.empty def in + let evm' = Subtac_utils.evars_of_term evm evm' typ in + let evars, def, typ = Eterm.eterm_obligations env id isevars evm' recdefs def typ in collect_evars (succ i) ((id, def, typ, evars) :: acc) else acc in diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index e3cf7a57a5..c184169ac7 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -12,6 +12,8 @@ open Decl_kinds open Util open Evd +type definition_hook = constant -> unit + let pperror cmd = Util.errorlabstrm "Program" cmd let error s = pperror (str s) @@ -40,6 +42,9 @@ type program_info = { prg_obligations: obligations; prg_deps : identifier list; prg_nvrec : int array; + prg_implicits : (Topconstr.explicitation * (bool * bool)) list; + prg_kind : definition_object_kind; + prg_hook : definition_hook; } let assumption_message id = @@ -106,7 +111,7 @@ let progmap_union = ProgMap.fold ProgMap.add let cache (_, (infos, tac)) = from_prg := infos; - default_tactic_expr := tac + set_default_tactic tac let (input,output) = declare_object @@ -125,24 +130,30 @@ let rec intset_to = function let subst_body prg = let obls, _ = prg.prg_obligations in - subst_deps obls (intset_to (pred (Array.length obls))) prg.prg_body - + let ints = intset_to (pred (Array.length obls)) in + subst_deps obls ints prg.prg_body, + subst_deps obls ints (Termops.refresh_universes prg.prg_type) + let declare_definition prg = - let body = subst_body prg in + let body, typ = subst_body prg in (try trace (str "Declaring: " ++ Ppconstr.pr_id prg.prg_name ++ spc () ++ my_print_constr (Global.env()) body ++ str " : " ++ my_print_constr (Global.env()) prg.prg_type); with _ -> ()); let ce = { const_entry_body = body; - const_entry_type = Some (Termops.refresh_universes prg.prg_type); + const_entry_type = Some typ; const_entry_opaque = false; const_entry_boxed = false} in let c = Declare.declare_constant - prg.prg_name (DefinitionEntry ce,IsDefinition Definition) + prg.prg_name (DefinitionEntry ce,IsDefinition prg.prg_kind) in + let gr = ConstRef c in + if Impargs.is_implicit_args () || prg.prg_implicits <> [] then + Impargs.declare_manual_implicits false gr (Impargs.is_implicit_args ()) prg.prg_implicits; print_message (definition_message c); + prg.prg_hook c; c open Pp @@ -151,14 +162,18 @@ open Ppconstr let declare_mutual_definition l = let len = List.length l in let namerec = Array.of_list (List.map (fun x -> x.prg_name) l) in - let arrec = - Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) - in - let recvec = - Array.of_list - (List.map (fun x -> - let subs = (subst_body x) in - snd (decompose_lam_n len subs)) l) +(* let arrec = *) +(* Array.of_list (List.map (fun x -> snd (decompose_prod_n len x.prg_type)) l) *) +(* in *) + let recvec, arrec = + let l, l' = + List.split + (List.map (fun x -> + let subs, typ = (subst_body x) in + snd (decompose_lam_n len subs), + snd (decompose_prod_n len typ)) l) + in + Array.of_list l, Array.of_list l' in let nvrec = (List.hd l).prg_nvrec in let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in @@ -205,7 +220,7 @@ let try_tactics obls = let red = Reductionops.nf_betaiota -let init_prog_info n b t deps nvrec obls = +let init_prog_info n b t deps nvrec obls impls kind hook = let obls' = Array.mapi (fun i (n, t, o, d) -> @@ -216,7 +231,7 @@ let init_prog_info n b t deps nvrec obls = obls in { prg_name = n ; prg_body = b; prg_type = red t; prg_obligations = (obls', Array.length obls'); - prg_deps = deps; prg_nvrec = nvrec; } + prg_deps = deps; prg_nvrec = nvrec; prg_implicits = impls; prg_kind = kind; prg_hook = hook; } let get_prog name = let prg_infos = !from_prg in @@ -327,7 +342,8 @@ let rec solve_obligation prg num = | _ -> ()); trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ Subtac_utils.my_print_constr (Global.env ()) obl.obl_type); - Pfedit.by !default_tactic + Pfedit.by !default_tactic; + Flags.if_verbose (fun () -> msg (Printer.pr_open_subgoals ())) () | l -> pperror (str "Obligation " ++ int user_num ++ str " depends on obligation(s) " ++ str (string_of_list ", " (fun x -> string_of_int (succ x)) l)) @@ -393,9 +409,22 @@ and auto_solve_obligations n : progress = Flags.if_verbose msgnl (str "Solving obligations automatically..."); try solve_obligations n !default_tactic with NoObligations _ -> Dependent -let add_definition n b t obls = +open Pp +let show_obligations ?(msg=true) n = + let prg = get_prog_err n in + let n = prg.prg_name in + let obls, rem = prg.prg_obligations in + if msg then msgnl (int rem ++ str " obligation(s) remaining: "); + Array.iteri (fun i x -> + match x.obl_body with + None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ + my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()) + | Some _ -> ()) + obls + +let add_definition n b t ?(implicits=[]) ?(kind=Definition) ?(hook=fun x -> ()) obls = Flags.if_verbose pp (str (string_of_id n) ++ str " has type-checked"); - let prg = init_prog_info n b t [] (Array.make 0 0) obls in + let prg = init_prog_info n b t [] (Array.make 0 0) obls implicits kind hook in let obls,_ = prg.prg_obligations in if Array.length obls = 0 then ( Flags.if_verbose ppnl (str "."); @@ -406,19 +435,30 @@ let add_definition n b t obls = let len = Array.length obls in let _ = Flags.if_verbose ppnl (str ", generating " ++ int len ++ str " obligation(s)") in from_prg := ProgMap.add n prg !from_prg; - auto_solve_obligations (Some n)) + let res = auto_solve_obligations (Some n) in + match res with + | Remain rem when rem < 5 -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res + | _ -> res) -let add_mutual_definitions l nvrec = +let add_mutual_definitions l ?(implicits=[]) ?(kind=Definition) nvrec = let deps = List.map (fun (n, b, t, obls) -> n) l in let upd = List.fold_left (fun acc (n, b, t, obls) -> - let prg = init_prog_info n b t deps nvrec obls in + let prg = init_prog_info n b t deps nvrec obls implicits kind (fun x -> ()) in ProgMap.add n prg acc) !from_prg l in from_prg := upd; - List.iter (fun x -> ignore(auto_solve_obligations (Some x))) deps - + let _defined = + List.fold_left (fun finished x -> + if finished then finished + else + match auto_solve_obligations (Some x) with + Defined _ -> (* If one definition is turned into a constant, the whole block is defined. *) true + | _ -> false) + false deps + in () + let admit_obligations n = let prg = get_prog_err n in let obls, rem = prg.prg_obligations in @@ -447,18 +487,5 @@ let next_obligation n = array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls in solve_obligation prg i - -open Pp -let show_obligations n = - let prg = get_prog_err n in - let n = prg.prg_name in - let obls, rem = prg.prg_obligations in - msgnl (int rem ++ str " obligation(s) remaining: "); - Array.iteri (fun i x -> - match x.obl_body with - None -> msgnl (str "Obligation" ++ spc() ++ int (succ i) ++ spc () ++ str "of" ++ spc() ++ str (string_of_id n) ++ str ":" ++ spc () ++ - my_print_constr (Global.env ()) x.obl_type ++ str "." ++ fnl ()) - | Some _ -> ()) - obls - + let default_tactic () = !default_tactic diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index cd70d5233d..30fbd02843 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -12,11 +12,18 @@ type progress = (* Resolution status of a program *) val set_default_tactic : Tacexpr.glob_tactic_expr -> unit val default_tactic : unit -> Proof_type.tactic +type definition_hook = constant -> unit + val add_definition : Names.identifier -> Term.constr -> Term.types -> - obligation_info -> progress + ?implicits:(Topconstr.explicitation * (bool * bool)) list -> + ?kind:Decl_kinds.definition_object_kind -> + ?hook:definition_hook -> obligation_info -> progress val add_mutual_definitions : - (Names.identifier * Term.constr * Term.types * obligation_info) list -> int array -> unit + (Names.identifier * Term.constr * Term.types * obligation_info) list -> + ?implicits:(Topconstr.explicitation * (bool * bool)) list -> + ?kind:Decl_kinds.definition_object_kind -> + int array -> unit val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr option -> unit @@ -31,7 +38,7 @@ val try_solve_obligation : int -> Names.identifier option -> Proof_type.tactic - val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit -val show_obligations : Names.identifier option -> unit +val show_obligations : ?msg:bool -> Names.identifier option -> unit val admit_obligations : Names.identifier option -> unit diff --git a/contrib/subtac/subtac_pretyping.ml b/contrib/subtac/subtac_pretyping.ml index a0e7e6951c..0703bcb837 100644 --- a/contrib/subtac/subtac_pretyping.ml +++ b/contrib/subtac/subtac_pretyping.ml @@ -70,7 +70,12 @@ let merge_evms x y = let interp env isevars c tycon = let j = pretype tycon env isevars ([],[]) c in - let evm = evars_of !isevars in + let _ = isevars := Evarutil.nf_evar_defs !isevars in + let evd,_ = consider_remaining_unif_problems env !isevars in + let unevd = undefined_evars evd in + let unevd' = Typeclasses.resolve_typeclasses env (Evd.evars_of unevd) evd in + let evm = evars_of unevd' in + isevars := unevd'; nf_evar evm j.uj_val, nf_evar evm j.uj_type let find_with_index x l = @@ -98,7 +103,7 @@ let env_with_binders env isevars l = let coqdef, deftyp = interp env isevars rawdef empty_tycon in let reldecl = (name, Some coqdef, deftyp) in aux (push_rel reldecl env, reldecl :: rels) tl - | Topconstr.LocalRawAssum (bl, typ) :: tl -> + | Topconstr.LocalRawAssum (bl, k, typ) :: tl -> let rawtyp = coqintern_type !isevars env typ in let coqtyp, typtyp = interp env isevars rawtyp empty_tycon in let acc = @@ -111,45 +116,28 @@ let env_with_binders env isevars l = | [] -> acc in aux (env, []) l -let subtac_process env isevars id l c tycon = - let c = Command.abstract_constr_expr c l in -(* let env_binders, binders_rel = env_with_binders env isevars l in *) +let subtac_process env isevars id bl c tycon = +(* let bl = Implicit_quantifiers.ctx_of_class_binders (vars_of_env env) cbl @ l in *) + let imps = Implicit_quantifiers.implicits_of_binders bl in + let c = Command.abstract_constr_expr c bl in let tycon = match tycon with None -> empty_tycon | Some t -> - let t = Command.generalize_constr_expr t l in + let t = Command.generalize_constr_expr t bl in let t = coqintern_type !isevars env t in let coqt, ttyp = interp env isevars t empty_tycon in mk_tycon coqt in let c = coqintern_constr !isevars env c in let coqc, ctyp = interp env isevars c tycon in -(* let _ = try trace (str "Interpreted term: " ++ my_print_constr env coqc ++ spc () ++ *) -(* str "Coq type: " ++ my_print_constr env ctyp) *) -(* with _ -> () *) -(* in *) -(* let _ = try trace (str "Original evar map: " ++ Evd.pr_evar_map (evars_of !isevars)) with _ -> () in *) - -(* let fullcoqc = it_mkLambda_or_LetIn coqc binders_rel *) -(* and fullctyp = it_mkProd_or_LetIn ctyp binders_rel *) -(* in *) - let fullcoqc = Evarutil.nf_evar (evars_of !isevars) coqc in - let fullctyp = Evarutil.nf_evar (evars_of !isevars) ctyp in -(* let evm = evars_of_term (evars_of !isevars) Evd.empty fullctyp in *) -(* let evm = evars_of_term (evars_of !isevars) evm fullcoqc in *) -(* let _ = try trace (str "After evar normalization remain: " ++ spc () ++ *) -(* Evd.pr_evar_map evm) *) -(* with _ -> () *) -(* in *) let evm = non_instanciated_map env isevars (evars_of !isevars) in -(* let _ = try trace (str "Non instanciated evars map: " ++ Evd.pr_evar_map evm) with _ -> () in *) - evm, fullcoqc, fullctyp + evm, coqc, ctyp, imps open Subtac_obligations -let subtac_proof env isevars id l c tycon = - let evm, coqc, coqt = subtac_process env isevars id l c tycon in +let subtac_proof env isevars id bl c tycon = + let evm, coqc, coqt, imps = subtac_process env isevars id bl c tycon in let evm = Subtac_utils.evars_of_term evm Evd.empty coqc in - let evars, def = Eterm.eterm_obligations env id !isevars evm 0 coqc (Some coqt) in - add_definition id def coqt evars + let evars, def, ty = Eterm.eterm_obligations env id !isevars evm 0 coqc coqt in + add_definition id def ty ~implicits:imps evars diff --git a/contrib/subtac/subtac_pretyping.mli b/contrib/subtac/subtac_pretyping.mli index afe554c87e..4af37043fd 100644 --- a/contrib/subtac/subtac_pretyping.mli +++ b/contrib/subtac/subtac_pretyping.mli @@ -5,11 +5,19 @@ open Sign open Evd open Global open Topconstr +open Implicit_quantifiers +open Impargs module Pretyping : Pretyping.S +val interp : + Environ.env -> + Evd.evar_defs ref -> + Rawterm.rawconstr -> + Evarutil.type_constraint -> Term.constr * Term.constr + val subtac_process : env -> evar_defs ref -> identifier -> local_binder list -> - constr_expr -> constr_expr option -> evar_map * constr * types + constr_expr -> constr_expr option -> evar_map * constr * types * manual_explicitation list val subtac_proof : env -> evar_defs ref -> identifier -> local_binder list -> constr_expr -> constr_expr option -> Subtac_obligations.progress diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 0ed0632c65..a2d5be66c1 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -200,11 +200,11 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | RRec (loc,fixkind,names,bl,lar,vdef) -> let rec type_bl env ctxt = function [] -> ctxt - | (na,None,ty)::bl -> + | (na,k,None,ty)::bl -> let ty' = pretype_type empty_valcon env isevars lvar ty in let dcl = (na,None,ty'.utj_val) in type_bl (push_rel dcl env) (add_rel_decl dcl ctxt) bl - | (na,Some bd,ty)::bl -> + | (na,k,Some bd,ty)::bl -> let ty' = pretype_type empty_valcon env isevars lvar ty in let bd' = pretype (mk_tycon ty'.utj_val) env isevars lvar ty in let dcl = (na,Some bd'.uj_val,ty'.utj_val) in @@ -326,7 +326,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | _ -> resj in inh_conv_coerce_to_tycon loc env isevars resj tycon - | RLambda(loc,name,c1,c2) -> + | RLambda(loc,name,k,c1,c2) -> let (name',dom,rng) = evd_comb1 (split_tycon loc env) isevars tycon in let dom_valcon = valcon_of_tycon dom in let j = pretype_type dom_valcon env isevars lvar c1 in @@ -334,7 +334,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let j' = pretype rng (push_rel var env) isevars lvar c2 in judge_of_abstraction env name j j' - | RProd(loc,name,c1,c2) -> + | RProd(loc,name,k,c1,c2) -> let j = pretype_type empty_valcon env isevars lvar c1 in let var = (name,j.utj_val) in let env' = push_rel_assum var env in @@ -557,7 +557,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (pretype tycon env isevars lvar c).uj_val | IsType -> (pretype_type empty_valcon env isevars lvar c).utj_val in - nf_evar (evars_of !isevars) c' + let evd,_ = consider_remaining_unif_problems env !isevars in + let evd = nf_evar_defs evd in + let c' = nf_evar (evars_of evd) c' in +(* let evd = undefined_evars evd in *) + let evd = Typeclasses.resolve_typeclasses env (evars_of evd) evd in + let c' = nf_evar (evars_of evd) c' in + isevars := evd; + c' (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage @@ -585,11 +592,16 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let ise_pretype_gen fail_evar sigma env lvar kind c = let isevars = ref (Evd.create_evar_defs sigma) in let c = pretype_gen isevars env lvar kind c in - let isevars,_ = consider_remaining_unif_problems env !isevars in - let c = nf_evar (evars_of isevars) c in - if fail_evar then check_evars env sigma isevars c; - isevars, c - +(* let evd,_ = consider_remaining_unif_problems env !isevars in *) +(* let evd = nf_evar_defs evd in *) +(* let c = nf_evar (evars_of evd) c in *) +(* let evd = undefined_evars evd in *) +(* let evd = Typeclasses.resolve_typeclasses env sigma evd in *) +(* let c = nf_evar (evars_of evd) c in *) + let evd = !isevars in + if fail_evar then check_evars env (Evd.evars_of evd) evd c; + evd, c + (** Entry points of the high-level type synthesis algorithm *) let understand_gen kind sigma env c = @@ -604,8 +616,15 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let understand_ltac sigma env lvar kind c = ise_pretype_gen false sigma env lvar kind c - let understand_tcc_evars isevars env kind c = - pretype_gen isevars env ([],[]) kind c + let understand_tcc_evars evdref env kind c = + pretype_gen evdref env ([],[]) kind c + +(* evdref := nf_evar_defs !evdref; *) +(* let c = nf_evar (evars_of !evdref) c in *) +(* let evd = undefined_evars !evdref in *) +(* let evd = Typeclasses.resolve_typeclasses env (evars_of evd) !evdref in *) +(* evdref := evd; *) +(* nf_evar (evars_of evd) c *) let understand_tcc sigma env ?expected_type:exptyp c = let ev, t = ise_pretype_gen false sigma env ([],[]) (OfType exptyp) c in diff --git a/contrib/subtac/subtac_utils.ml b/contrib/subtac/subtac_utils.ml index d5df9adc92..46a8bd203c 100644 --- a/contrib/subtac/subtac_utils.ml +++ b/contrib/subtac/subtac_utils.ml @@ -357,19 +357,31 @@ let print_message m = (* Solve an obligation using tactics, return the corresponding proof term *) let solve_by_tac evi t = - debug 2 (str "Solving goal using tactics: " ++ Evd.pr_evar_info evi); let id = id_of_string "H" in - try + try Pfedit.start_proof id goal_kind evi.evar_hyps evi.evar_concl (fun _ _ -> ()); - debug 2 (str "Started proof"); Pfedit.by (tclCOMPLETE t); - let _,(const,_,_) = Pfedit.cook_proof () in + let _,(const,_,_) = Pfedit.cook_proof () in Pfedit.delete_current_proof (); const.Entries.const_entry_body - with e -> + with e -> Pfedit.delete_current_proof(); raise Exit +(* let apply_tac t goal = t goal *) + +(* let solve_by_tac evi t = *) +(* let ev = 1 in *) +(* let evm = Evd.add Evd.empty ev evi in *) +(* let goal = {it = evi; sigma = evm } in *) +(* let (res, valid) = apply_tac t goal in *) +(* if res.it = [] then *) +(* let prooftree = valid [] in *) +(* let proofterm, obls = Refiner.extract_open_proof res.sigma prooftree in *) +(* if obls = [] then proofterm *) +(* else raise Exit *) +(* else raise Exit *) + let rec string_of_list sep f = function [] -> "" | x :: [] -> f x diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index 82d7c19e51..3a0fdfb9b9 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -491,7 +491,10 @@ let kind_of_constant kn = | DK.IsDefinition DK.IdentityCoercion -> Pp.warning "IdentityCoercion not supported in dtd (used Definition instead)"; "DEFINITION","Definition" - | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> + | DK.IsDefinition DK.Instance -> + Pp.warning "Instance not supported in dtd (used Definition instead)"; + "DEFINITION","Definition" + | DK.IsProof (DK.Theorem|DK.Lemma|DK.Corollary|DK.Fact|DK.Remark as thm) -> "THEOREM",DK.string_of_theorem_kind thm | DK.IsProof _ -> Pp.warning "Unsupported theorem kind (used Theorem instead)"; |