diff options
| -rw-r--r-- | toplevel/class.ml | 471 | ||||
| -rw-r--r-- | toplevel/class.mli | 25 | ||||
| -rw-r--r-- | toplevel/record.ml | 170 | ||||
| -rw-r--r-- | toplevel/record.mli | 12 |
4 files changed, 678 insertions, 0 deletions
diff --git a/toplevel/class.ml b/toplevel/class.ml new file mode 100644 index 000000000..5c762636f --- /dev/null +++ b/toplevel/class.ml @@ -0,0 +1,471 @@ + +open Util +open Pp +open Names +open Generic +open Term +open Inductive +open Constant +open Environ +open Lib +open Classops +open Declare + +(* manipulations concernant les strength *) + +(* gt dans le sens de "longueur du sp" (donc le moins persistant) *) + +(* strength * strength -> bool *) + +let stre_gt = function + (NeverDischarge,NeverDischarge) -> false + | (NeverDischarge,x) -> false + | (x,NeverDischarge) -> true + | (DischargeAt sp1,DischargeAt sp2) -> sp_gt (sp1,sp2) + +let stre_max (stre1,stre2) = + if stre_gt (stre1,stre2) then stre1 else stre2 + +let stre_max4 stre1 stre2 stre3 stre4 = + stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4))) + +let id_of_varid = function + | (VAR id) -> id + | _ -> anomaly "class__id_of_varid" + +let stre_of_VAR c = variable_strength (destVar c) + +(* lf liste des variable dont depend la coercion f + lc liste des variable dont depend la classe source *) + +let rec stre_unif_cond = function + ([],[]) -> NeverDischarge + | (v::l,[]) -> stre_of_VAR v + | ([],v::l) -> stre_of_VAR v + | (v1::l1,v2::l2) -> + if v1=v2 then stre_unif_cond (l1,l2) + else + let stre1 = (stre_of_VAR v1) + and stre2 = (stre_of_VAR v2) + in stre_max (stre1,stre2) + +let stre_of_coe = function + NAM_SP sp -> + (match global_operator sp (basename sp) with + Const sp, _ -> constant_strength sp + | _ -> NeverDischarge) + | NAM_Var id -> variable_strength id + | _ -> NeverDischarge + +(* try_add_class : Names.identifier -> + Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *) + +let try_add_class id v clpopt streopt check_exist = + let env = Global.env () in + let t = Retyping.get_type_of env Evd.empty v in + let p1 = + try arity_sort t + with Not_found -> errorlabstrm "try_add_class" + [< 'sTR "Type of "; 'sTR (string_of_id id); + 'sTR " does not end with a sort" >] in + let cl,p = + match clpopt with + None -> let (cl,_)=constructor_at_head v in (cl,p1) + | Some (cl,p2) -> (fully_applied id p2 p1;cl,p1) in + if check_exist & class_exists cl then + errorlabstrm "try_add_new_class" + [< 'sTR (string_of_id id) ; 'sTR " is already a class" >]; + let stre' = stre_of_cl cl in + let stre = (match streopt with + (Some stre) -> stre_max (stre,stre') + | None -> stre') in + add_new_class (cl,(string_of_id id),stre,p); + stre + + +(* try_add_new_class : Names.identifier -> unit *) + +let try_add_new_class id stre = + let v = global_reference CCI id in + let _ = try_add_class id v None (Some stre) true in () + + +(* check_class : Names.identifier -> + Term.constr -> cl_typ -> int -> int * Libobject.strength *) + +let check_class id v cl p = + try + let _,clinfo = class_info cl in + if p = clinfo.cL_PARAM + then clinfo.cL_STRE + else errorlabstrm "fully_applied" + [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >] + with Not_found -> try_add_class id v (Some (cl,p)) None false + + +(* decomposition de constr vers coe_typ *) + +let coe_constructor_at_head t = + let rec aux t' = + match kind_of_term t' with + IsConst (sp,l) -> (Array.to_list l),NAM_SP sp + | IsMutInd (sp,_,l) -> (Array.to_list l),NAM_SP sp + | IsVar id -> [],NAM_Var id + | IsCast (c,_) -> aux c + | IsMutConstruct (sp,i,j,l) -> (Array.to_list l),NAM_Construct ((sp,i),j) + | IsAppL(f,args) -> aux f + | _ -> raise Not_found + in aux (collapse_appl t) + +let constructor_at_head1 t = + let rec aux t' = + match kind_of_term t' with + IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0 + | IsMutInd (sp,i,l) -> t',[],(Array.to_list l),CL_IND (sp,i),0 + | IsVar id -> t',[],[],CL_Var id,0 + | IsCast (c,_) -> aux c + | IsAppL(f,args) -> let t',_,l,c,_ = aux f in t',args,l,c,List.length args + | IsProd (_,_,_) -> t',[],[],CL_FUN,0 + | IsSort _ -> t',[],[],CL_SORT,0 + | _ -> raise Not_found + in aux (collapse_appl t) + + +(* condition d'heritage uniforme *) + +let uniform_cond nargs lt = + let rec aux = function + (0,[]) -> true + | (n,t::l) -> (strip_outer_cast t = Rel n) & (aux ((n-1),l)) + | _ -> false + in aux (nargs,lt) + +let id_of_cl = function + CL_FUN -> (id_of_string "FUNCLASS") + | CL_SORT -> (id_of_string "SORTCLASS") + | CL_SP sp -> (basename sp) + | CL_IND (sp,i) -> + (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename + | CL_Var id -> id + +let string_of_cl = function + CL_FUN -> "FUNCLASS" + | CL_SORT -> "SORTCLASS" + | CL_SP sp -> string_of_id (basename sp) + | CL_IND (sp,i) -> + string_of_id + (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename + | CL_Var id -> string_of_id id + +(* +lp est la liste (inverse'e) des arguments de la coercion +ids est le nom de la classe source +sps_opt est le sp de la classe source dans le cas des structures +retourne: +la classe souce +nbre d'arguments de la classe +le constr de la class +l'indice de la classe source dans la liste lp +la liste des variables dont depend la classe source +*) + +type choice = Ident of identifier | Section_path of section_path + +let get_source lp source = + let aux test = + let rec aux1 n = function + [] -> raise Not_found + | t1::lt -> + try (let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in + if test cl1 + then cl1,p1,v1,lv1,n,l + else aux1 (n+1) lt) + with _ -> aux1 (n + 1) lt + in aux1 1 lp + in match source with + None -> + let (v1,lv1,l,cl1,p1) as x = + (match lp with + [] -> raise Not_found + | t1::_ -> + try constructor_at_head1 t1 + with _ -> raise Not_found) + in (id_of_cl cl1),(cl1,p1,v1,lv1,1,l) + | Some (Ident id) -> id, aux (function cl -> id_of_cl cl = id) + | Some (Section_path sp) -> + basename sp, + aux (function + CL_SP sp1 -> sp=sp1 + | CL_IND (sp1,i) -> sp=sp1 + | _ -> false) + +let get_target t ind = + if (ind > 1) + then CL_FUN,0,t + else let v2,_,_,cl2,p2 = constructor_at_head1 t in + cl2,p2,v2 + + +let prods_of t = + let rec aux acc = function + DOP2(Prod,c1,DLAM(_,c2)) -> aux (c1::acc) c2 + | (DOP2(Cast,c,_)) -> aux acc c + | t -> t::acc + in aux [] t + +(* coercion identite' *) + +let lams_of t = + let rec aux acc = function + DOP2(Lambda,c1,DLAM(x,c2)) -> aux ((x,c1)::acc) c2 + | (DOP2(Cast,c,_)) -> aux acc c + | t -> acc,t + in aux [] t + +let build_id_coercion idf_opt ids = + let env = Global.env () in + let vs = global env ids in + let c = match (strip_outer_cast vs) with + (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' -> + (try Instantiate.constant_value env c' + with _ -> errorlabstrm "build_id_coercion" + [< 'sTR(string_of_id ids); + 'sTR" must be a transparent constant" >]) + | _ -> errorlabstrm "build_id_coercion" + [< 'sTR(string_of_id ids); 'sTR" must be a transparent constant" >] in + let lams,t = lams_of c in + let lams = List.rev lams in + let llams = List.length lams in + let val_f = + List.fold_right + (fun (x,t) u -> + DOP2(Lambda,t,DLAM(x,u))) + lams + (DOP2(Lambda,(applistc vs (rel_list 0 llams)), + DLAM(Name (id_of_string "x"),Rel 1))) in + let typ_f = + List.fold_right + (fun (x,t) c -> DOP2(Prod,t,DLAM(x,c))) + lams + (DOP2(Prod,(applistc vs (rel_list 0 llams)), + DLAM(Anonymous,lift 1 t))) in + let constr_f = DOP2(Cast,val_f,typ_f) in + (* juste pour verification *) + let _ = try Typing.type_of env Evd.empty constr_f + with _ -> + error "cannot be defined as coercion - may be a bad number of arguments" in + let idf = + (match idf_opt with + Some(idf) -> idf + | None -> + id_of_string ("Id_"^(string_of_id ids)^"_"^ + (string_of_cl (fst (constructor_at_head t))))) in + let constr_entry = {const_entry_body = constr_f; const_entry_type = None } in + let _ = declare_constant idf (constr_entry,NeverDischarge,false) + in idf + +let coercion_syntax_entry id n = + let args = (String.concat " " (list_tabulate (fun _ -> "$_") n)) ^ " $c" in + let str = "level 10: " ^ (string_of_id id) ^ + " [ <<(" ^ (string_of_id id) ^ " " ^ args ^ ")>> ]" ^ + " -> [ (APPLIST $c):E ]" + in + try + let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in + Metasyntax.add_syntax_obj "constr" [se] + with Stdpp.Exc_located _ -> anomaly ("ill-formed syntax entry: "^str) + +let fun_coercion_syntax_entry id n = + let args = + if n<0 then anomaly "fun_coercion_syntax_entry" + else + String.concat " " (list_tabulate (fun _ -> "$_") n) ^ " $c ($LIST $l)" in + let str = "level 10: " ^ ((string_of_id id)^"1") ^ + " [ (APPLIST " ^ (string_of_id id) ^ " " ^ args ^ ") ] " ^ + "-> [ (APPLIST $c ($LIST $l)):E ]" + in + try + let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in + Metasyntax.add_syntax_obj "constr" [se] + with Stdpp.Exc_located _ -> anomaly ("ill-formed syntax entry: "^str) + + + +let coercion_syntax idf ps clt = + match clt with + CL_FUN -> + (fun_coercion_syntax_entry idf ps; + coercion_syntax_entry idf ps) + | _ -> coercion_syntax_entry idf ps + + +let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps = + let _ = add_anonymous_leaf + (inCoercion + ((coef, + {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}), + cls,clt)) in + coercion_syntax idf ps clt + +(* +nom de la fonction coercion +strength de f +nom de la classe source (optionnel) +sp de la classe source (dans le cas des structures) +nom de la classe target (optionnel) +booleen "coercion identite'?" + +lorque source est None alors target est None aussi. +*) + +let try_add_new_coercion_core idf stre source target isid = + let env = Global.env () in + let v = global env idf in + let t = Retyping.get_type_of env Evd.empty v in + let k = Retyping.get_type_of env Evd.empty t in + let vj = {uj_val=v; uj_type=t; uj_kind = k} in + let f_vardep,coef = coe_constructor_at_head v in + if coercion_exists coef then + errorlabstrm "try_add_coercion" + [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >]; + let lp = prods_of t in + let llp = List.length lp in + if llp <= 1 then + errorlabstrm "try_add_coercion" + [< 'sTR"Does not correspond to a coercion" >]; + + let ids,(cls,ps,vs,lvs,ind,s_vardep) = + try get_source (List.tl lp) source + with Not_found -> errorlabstrm "try_add_coercion" + [<'sTR"We do not find the source class " >] in + + if (cls = CL_FUN) then + errorlabstrm "try_add_coercion" + [< 'sTR"FUNCLASS cannot be a source class" >]; + if (cls = CL_SORT) then + errorlabstrm "try_add_coercion" + [< 'sTR"SORTCLASS cannot be a source class" >]; + if not (uniform_cond (llp-1-ind) lvs) then + errorlabstrm "try_add_coercion" + [<'sTR(string_of_id idf); + 'sTR" does not respect the inheritance uniform condition" >]; + + let clt,pt,vt = + try get_target (List.hd lp) ind + with Not_found -> errorlabstrm "try_add_coercion" + [<'sTR"We cannot find the target class" >] in + let idt = + (match target with + Some idt -> + if idt = id_of_cl clt then idt + else errorlabstrm "try_add_coercion" + [<'sTR"The target class does not correspond to "; + 'sTR(string_of_id idt) >] + | None -> (id_of_cl clt)) in + let stres = check_class ids vs cls ps in + let stret = check_class idt vt clt pt in + let stref = stre_of_coe coef in + let streunif = stre_unif_cond (s_vardep,f_vardep) in + let stre' = stre_max4 stres stret stref streunif in + (* if (stre=NeverDischarge) & (stre'<>NeverDischarge) + then errorlabstrm "try_add_coercion" + [<'sTR(string_of_id idf); + 'sTR" must be declared as a local coercion (its strength is "; + 'sTR(string_of_strength stre');'sTR")" >] *) + let stre = stre_max (stre,stre') in + add_new_coercion_in_graph1 (coef,vj,stre,isid,cls,clt) idf ps + + +let try_add_new_coercion id stre = + try_add_new_coercion_core id stre None None false + +let try_add_new_coercion_subclass id stre = + let idf = build_id_coercion None id in + try_add_new_coercion_core idf stre (Some (Ident id)) None true + +let try_add_new_coercion_with_target id stre source target isid = + if isid then + let idf = build_id_coercion (Some id) source in + try_add_new_coercion_core idf stre (Some (Ident source)) (Some target) true + else + try_add_new_coercion_core id stre (Some (Ident source)) (Some target) false + +let try_add_new_coercion_record id stre source_sp = + try_add_new_coercion_core id stre (Some (Section_path source_sp)) None false + +(* fonctions pour le discharge: plutot sale *) + +let defined_in_sec sp sec_sp = + let ((p1,id1,k1)) = repr_path sp in + let ((p2,id2,k2)) = repr_path sec_sp in + p1 = (string_of_id id2)::p2 + +let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) = + let env = Global.env () in + match cl with + CL_Var id -> x + | CL_SP sp -> + if defined_in_sec sp sec_sp + then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + let v = global_reference CCI spid in + let t = Retyping.get_type_of env Evd.empty v in + let p = arity_sort t in + (CL_SP newsp,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) + else x + | CL_IND (sp,i) -> + if defined_in_sec sp sec_sp + then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + let v = global_reference CCI spid in + let t = Retyping.get_type_of env Evd.empty v in + let p = arity_sort t in + (CL_IND (newsp,i),{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) + else x + | _ -> anomaly "process_class" + +let process_cl sec_sp cl = + match cl with + CL_Var id -> CL_Var id + | CL_SP sp -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + CL_SP newsp + else cl + | CL_IND (sp,i) -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + CL_IND (newsp,i) + else cl + | _ -> cl + +let process_coercion sec_sp (((coe,coeinfo),s,t) as x) = + let s1= process_cl sec_sp s in + let t1 = process_cl sec_sp t in + let p = (snd (class_info s1)).cL_PARAM in + match coe with + NAM_Var id -> ((coe,coeinfo),s1,t1),id,p + | NAM_SP sp -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + let v = global_reference CCI spid in + ((NAM_SP newsp,coeinfo),s1,t1),spid,p + else ((coe,coeinfo),s1,t1),basename sp,p + | NAM_Construct ((sp,i),j) -> + if defined_in_sec sp sec_sp then + let ((_,spid,spk)) = repr_path sp in + let newsp = Lib.make_path spid CCI in + let id = Global.id_of_global (MutConstruct((newsp,i),j)) in + let v = global_reference CCI id in + (((NAM_Construct ((newsp,i),j)),coeinfo),s1,t1),id,p + else + ((coe,coeinfo),s1,t1), + Global.id_of_global (MutConstruct((sp,i),j)), + p + +(* Id: class.ml4,v 1.2 1997/06/17 17:44:10 dderaugl Exp $ *) diff --git a/toplevel/class.mli b/toplevel/class.mli new file mode 100644 index 000000000..094b2ecc2 --- /dev/null +++ b/toplevel/class.mli @@ -0,0 +1,25 @@ + +(* $Id$ *) + +open Names +open Term +open Classops +open Declare + +val try_add_new_coercion : identifier -> strength -> unit +val try_add_new_coercion_subclass : identifier -> strength -> unit +val try_add_new_coercion_record: identifier -> strength -> section_path -> unit +val try_add_new_coercion_with_target : identifier -> strength -> + identifier -> identifier -> bool -> unit + +val try_add_new_class : identifier -> strength -> unit +val process_class : + section_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ) +val process_coercion : + section_path -> (coe_typ * coe_info_typ) * cl_typ * cl_typ -> + ((coe_typ * coe_info_typ) * cl_typ * cl_typ) * identifier * int + +val defined_in_sec : section_path -> section_path -> bool +val coercion_syntax : identifier -> int -> cl_typ -> unit +val fun_coercion_syntax_entry : identifier -> int -> unit +val coercion_syntax_entry : identifier -> int -> unit diff --git a/toplevel/record.ml b/toplevel/record.ml new file mode 100644 index 000000000..cc44bc22b --- /dev/null +++ b/toplevel/record.ml @@ -0,0 +1,170 @@ + +(* $:Id$ *) + +open Util;; +open Names;; +open Term;; +(* +open Generic;; +open Mach;; +open Command;; +open More_util;; +open Pp;; + +open Constrtypes;; +open Termenv;; +open Trad;; +open Ast;; +open CoqAst;; + +open Machops;; +open Classops;; +open Recordops;; +*) + +(********** definition d'un record (structure) **************) + +let make_constructor fields appc = + let rec aux fields = + match fields with + [] -> appc + | (id,ty)::l -> ope("PROD",[ty; slam(Some (string_of_id id), aux l)]) + in aux fields;; + +(* free_vars existe de'ja` dans ast.ml *) + +let rec drop = function + [] -> [] + | (None::t) -> drop t + | ((Some id)::t) -> id::(drop t) +;; + +let fold curriedf l base = + List.fold_right (fun a -> fun b -> curriedf(a,b)) l base +;; + +let free_vars t = + let rec aux = function + (Nvar(_,s),accum) -> add_set (id_of_string s) accum +| (Node(_,_,tl),accum) -> fold aux tl accum +| (Slam(_,None,body),accum) -> + (aux(body,[]))@accum +| (Slam(_,Some id,body),accum) -> + (subtract (aux(body,[])) [(id_of_string id)])@accum +| (_,accum) -> accum + in aux(t,[]) +;; + +let free_in_asts id l = + let rec aux = + function [] -> true + | a::l -> (not (List.mem id (free_vars a))) & (aux l) in + aux l;; + +let all_vars t = + let rec aux = function + (Nvar(_,id),accum) -> add_set (id_of_string id) accum +| (Node(_,_,tl),accum) -> fold aux tl accum +| (Slam(_,None,body),accum) -> aux (body,accum) +| (Slam(_,Some id,body),accum) -> + aux (body,(union accum [(id_of_string id)])) +| (_,accum) -> accum + in aux(t,[]) +;; + +let print_id_list l = + [< 'sTR "[" ; prlist (fun id -> [< 'sTR (string_of_id id) >]) l; 'sTR "]" >] +;; + +let typecheck_params_and_field ps fs = + let sign0 = initial_sign() in + let sign1,newps = + List.fold_left + (fun (sign,newps) (id,t) -> + let tj = type_of_com sign t in + (add_sign (id,tj) sign,(id,tj.body)::newps)) + (sign0,[]) ps in + let sign2,newfs = + List.fold_left + (fun (sign,newfs) (id,t) -> + let tj = type_of_com sign t in + (add_sign (id,tj) sign,(id,tj.body)::newfs)) (sign1,[]) fs + in List.rev(newps),List.rev(newfs) +;; + + +let mk_LambdaCit = List.fold_right (fun (x,a) b -> mkNamedLambda x a b);; + + +let definition_structure (coe_constr,struc,ps,cfs,const,s) = + + let (sign,fsign) = initial_assumptions() in + let fs = List.map snd cfs in + let coers = List.map fst cfs in + let idps = List.map fst ps in + let typs = List.map snd ps in + let idfs = List.map fst fs in + let tyfs = List.map snd fs in + let _ = if not (free_in_asts struc tyfs) + then message "Error: A record cannot be recursive" in + let newps,newfs = typecheck_params_and_field ps fs in + let app_constructor = ope("APPLIST", + (ope("XTRA",[str "!";(nvar (string_of_id struc))])):: + List.map (fun id -> nvar(string_of_id id)) idps) in + let type_constructor = make_constructor fs app_constructor in + let _ = build_mutual ps [(struc,s,[(const,type_constructor)])] true in + + let x = next_ident_away (id_of_string "x") + (List.fold_left (fun l ty -> union (all_vars ty) l) + (union idps (fst sign)) tyfs) in + let r = Machops.global (gLOB sign) struc in + let (rsp,_,_) = destMutInd r in + let rid = basename rsp in + let lp = length idps in + let rp1 = applist (r,(rel_list 0 lp)) in + let rp2 = applist (r,(rel_list 1 lp)) in + let warning_or_error coe st = if coe then (errorlabstrm "structure" st) + else pPNL [< 'sTR"Warning: "; st >] in + + let (sp_projs,_,_,_,_) = + List.fold_left + (fun (sp_projs,ids_ok,ids_not_ok,sigma,coes) (fi,ti) -> + let fv_ti = global_vars ti in + let bad_projs = (intersect ids_not_ok fv_ti) in + if bad_projs <> [] + then begin (warning_or_error (hd coes) + [< 'sTR(string_of_id fi); + 'sTR" cannot be defined. The projections "; + print_id_list bad_projs; 'sTR " were not defined" >]); + (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes)) + end + else + + let p = mkNamedLambda x rp2 (replace_vars sigma ti) in + let branch = mk_LambdaCit newfs (VAR fi) in + let proj = mk_LambdaCit newps + (mkNamedLambda x rp1 (mkMutCaseA (ci_of_mind r) p (Rel 1) [|branch|])) in + let ok = try (Declare.machine_constant (sign,fsign) + ((fi,false,NeverDischarge),proj); true) + with UserError(s,pps) -> + ((warning_or_error (hd coes) + [<'sTR (string_of_id fi); + 'sTR" cannot be defined. "; pps >]);false) in + if not ok + then (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes)) + else begin + if List.hd coes then + Class.try_add_new_coercion_record fi NeverDischarge rsp; + let constr_fi = Machops.global (gLOB sign) fi in + let constr_fip = + applist (constr_fi,(List.map (fun id -> VAR id) idps)@[VAR x]) + in (Some(path_of_const constr_fi)::sp_projs,fi::ids_ok,ids_not_ok, + (fi,{sinfo=Closed;sit=constr_fip})::sigma,(tl coes)) + end) + ([],[],[],[],coers) newfs + in (if coe_constr="COERCION" + then Class.try_add_new_coercion const NeverDischarge); + add_new_struc (rsp,const,lp,rev sp_projs) +;; + +(* $Id$ *) diff --git a/toplevel/record.mli b/toplevel/record.mli new file mode 100644 index 000000000..4e0ba6036d --- /dev/null +++ b/toplevel/record.mli @@ -0,0 +1,12 @@ + +(* $Id$ *) + +open Names +open Term + +val definition_structure : + string * identifier * (identifier * CoqAst.t) list * + (bool * (identifier * CoqAst.t)) list * identifier * + CoqAst.t -> unit;; + +(* $Id$ *) |