aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/environ.ml5
-rw-r--r--kernel/names.ml96
-rw-r--r--kernel/names.mli49
-rw-r--r--library/declare.ml4
-rw-r--r--library/declare.mli2
-rw-r--r--library/lib.ml4
-rw-r--r--library/lib.mli4
-rw-r--r--parsing/pretty.ml168
-rw-r--r--parsing/pretty.mli1
-rw-r--r--pretyping/class.ml8
-rw-r--r--pretyping/class.mli6
-rw-r--r--pretyping/evarutil.ml3
-rw-r--r--proofs/pfedit.ml3
-rw-r--r--toplevel/discharge.ml2
14 files changed, 95 insertions, 260 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 2613199ff..7501471e5 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -232,10 +232,9 @@ let hdchar env c =
if i=0 then
lowercase_first_char (basename sp)
else
- let na = id_of_global env (IndRef x) in lowercase_first_char na
+ lowercase_first_char (id_of_global env (IndRef x))
| IsMutConstruct ((sp,i) as x,_) ->
- let na = id_of_global env (ConstructRef x) in
- String.lowercase(List.hd(explode_id na))
+ lowercase_first_char (id_of_global env (ConstructRef x))
| IsVar id -> lowercase_first_char id
| IsSort s -> sort_hdchar s
| IsRel n ->
diff --git a/kernel/names.ml b/kernel/names.ml
index 2686763aa..11a4ce28e 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -12,15 +12,18 @@ type identifier = {
type name = Name of identifier | Anonymous
-let make_ident sa n = { atom = sa; index = n }
+let code_of_0 = Char.code '0'
+let code_of_9 = Char.code '9'
+
let repr_ident { atom = sa; index = n } = (sa,n)
+let make_ident sa n =
+ let c = Char.code (String.get sa (String.length sa -1)) in
+ if c < code_of_0 or c > code_of_9 then { atom = sa; index = n }
+ else { atom = sa^"_"; index = n }
let string_of_id { atom = s; index = n } =
s ^ (if n = -1 then "" else string_of_int n)
-let code_of_0 = Char.code '0'
-let code_of_9 = Char.code '9'
-
let id_of_string s =
let slen = String.length s in
(* [n'] is the position of the first non nullary digit *)
@@ -46,17 +49,12 @@ let id_of_string s =
let atompart_of_id id = id.atom
let index_of_id id = id.index
-let explode_id { atom = s; index = n } =
- (explode s) @ (if n = -1 then [] else explode (string_of_int n))
-
let print_id { atom = a; index = n } =
match (a,n) with
| ("",-1) -> [< 'sTR"[]" >]
| ("",n) -> [< 'sTR"[" ; 'iNT n ; 'sTR"]" >]
| (s,n) -> [< 'sTR s ; (if n = (-1) then [< >] else [< 'iNT n >]) >]
-let print_idl idl = prlist_with_sep pr_spc print_id idl
-
let id_ord id1 id2 =
let (s1,n1) = repr_ident id1
and (s2,n2) = repr_ident id2 in
@@ -82,17 +80,26 @@ module Idmap = Map.Make(IdOrdered)
(* Fresh names *)
+let add_subscript_to_ident id n =
+ if n < 0 then error "Only natural numbers are allowed as subscripts";
+ if id.index = -1 then { atom = id.atom; index = n }
+ else { atom = (string_of_id id)^"_"; index = n }
let lift_ident { atom = str; index = i } = { atom = str; index = i+1 }
-let next_ident_away ({atom=str} as id) avoid =
- let rec name_rec i =
- let create = if i = (-1) then id else {atom=str;index=i} in
- if List.mem create avoid then name_rec (i+1) else create
- in
- name_rec (-1)
-
-let rec next_ident_away_from {atom=str;index=i} avoid =
+let next_ident_away id avoid =
+ if List.mem id avoid then
+ let str = if id.index = -1 then id.atom else
+ (* Ce serait sans doute mieux avec quelque chose inspiré de
+ *** string_of_id id ^ "_" *** mais ça brise la compatibilité... *)
+ id.atom in
+ let rec name_rec i =
+ let create = {atom=str;index=i} in
+ if List.mem create avoid then name_rec (i+1) else create in
+ name_rec 0
+ else id
+
+let next_ident_away_from {atom=str;index=i} avoid =
let rec name_rec i =
let create = {atom=str;index=i} in
if List.mem create avoid then name_rec (i+1) else create
@@ -109,17 +116,6 @@ let next_name_away name l =
| Name(str) -> next_ident_away str l
| Anonymous -> id_of_string "_"
-(* returns lids@[i1..in] where i1..in are new identifiers prefixed id *)
-let get_new_ids n id lids =
- let rec get_rec n acc =
- if n = 0 then
- acc
- else
- let nid = next_ident_away id (acc@lids) in
- get_rec (n-1) (nid::acc)
- in
- get_rec n []
-
let id_of_name default = function
| Name s -> s
| Anonymous -> default
@@ -140,10 +136,12 @@ let kind_of_string = function
| _ -> invalid_arg "kind_of_string"
-(* Section paths *)
+(*s Section paths *)
+
+type dir_path = string list
type section_path = {
- dirpath : string list ;
+ dirpath : dir_path ;
basename : identifier ;
kind : path_kind }
@@ -154,14 +152,15 @@ let kind_of_path sp = sp.kind
let basename sp = sp.basename
let dirpath sp = sp.dirpath
-let string_of_path_mind sp id =
- let (sl,_,k) = repr_path sp in
+(* parsing and printing of section paths *)
+let string_of_dirpath sl = String.concat "#" (""::sl)
+
+let string_of_path sp =
+ let (sl,id,k) = repr_path sp in
String.concat ""
((List.flatten (List.map (fun s -> ["#";s]) sl))
@ [ "#"; string_of_id id; "."; string_of_kind k ])
-let string_of_path sp = string_of_path_mind sp sp.basename
-
let path_of_string s =
try
let (sl,s,k) = parse_section_path s in
@@ -171,33 +170,6 @@ let path_of_string s =
let print_sp sp = [< 'sTR (string_of_path sp) >]
-
-let coerce_path k { dirpath = p; basename = id } =
- { dirpath = p; basename = id; kind = k }
-
-let ccisp_of_fwsp = function
- | { dirpath = p; basename = id; kind = FW } ->
- { dirpath = p; basename = id; kind = CCI }
- | _ -> invalid_arg "ccisp_of_fwsp"
-
-let ccisp_of { dirpath = p; basename = id } =
- { dirpath = p; basename = id; kind = CCI }
-
-let objsp_of { dirpath = p; basename = id } =
- { dirpath = p; basename = id; kind = OBJ }
-
-let fwsp_of_ccisp = function
- | { dirpath = p; basename = id; kind = CCI } ->
- { dirpath = p; basename = id; kind = FW }
- | _ -> invalid_arg "fwsp_of_ccisp"
-
-let fwsp_of { dirpath = p; basename = id } =
- { dirpath = p; basename = id; kind = FW }
-
-let append_to_path sp str =
- let (sp,id,k) = repr_path sp in
- make_path sp (id_of_string ((string_of_id id)^str)) k
-
let sp_of_wd = function
| [] -> invalid_arg "Names.sp_of_wd"
| l -> let (bn,dp) = list_sep_last l in make_path dp (id_of_string bn) OBJ
@@ -215,7 +187,7 @@ let sp_ord sp1 sp2 =
else
ck
-let sp_gt (sp1,sp2) = sp_ord sp1 sp2 > 0
+let dirpath_prefix_of = list_prefix_of
module SpOrdered =
struct
diff --git a/kernel/names.mli b/kernel/names.mli
index 84b25d9cd..1e1b4cb3f 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -10,19 +10,22 @@ open Pp
type identifier
type name = Name of identifier | Anonymous
+(* Constructor of an identifier;
+ [make_ident] builds an identifier from a string and an index; if
+ the string ends by a digit, a "_" is inserted *)
val make_ident : string -> int -> identifier
-val string_of_id : identifier -> string
-val id_of_string : string -> identifier
-val explode_id : identifier -> string list
-val print_id : identifier -> std_ppcmds
-val print_idl : identifier list -> std_ppcmds
+(* Some destructors of an identifier *)
val atompart_of_id : identifier -> string
-val index_of_id : identifier -> int
-val id_ord : identifier -> identifier -> int
-val id_without_number : identifier -> bool
val first_char : identifier -> string
+val index_of_id : identifier -> int
+
+(* Parsing and printing of identifiers *)
+val string_of_id : identifier -> string
+val id_of_string : string -> identifier
+val print_id : identifier -> std_ppcmds
+(* Identifiers sets and maps *)
module Idset : Set.S with type elt = identifier
module Idmap : Map.S with type key = identifier
@@ -32,32 +35,42 @@ val next_ident_away : identifier -> identifier list -> identifier
val next_name_away : name -> identifier list -> identifier
val next_name_away_with_default :
string -> name -> identifier list -> identifier
-val get_new_ids : int -> identifier -> identifier list -> identifier list
-
-val id_of_name : identifier -> name -> identifier
+(*s path_kind is currently degenerated, only [CCI] is used *)
type path_kind = CCI | FW | OBJ
+(* parsing and printing of path kinds *)
val string_of_kind : path_kind -> string
val kind_of_string : string -> path_kind
+(*s Directory paths = section names paths *)
+type dir_path = string list
+
+(* Printing of directory paths as "#module#submodule" *)
+val string_of_dirpath : dir_path -> string
+
(*s Section paths *)
type section_path
-val make_path : string list -> identifier -> path_kind -> section_path
-val repr_path : section_path -> string list * identifier * path_kind
-val dirpath : section_path -> string list
+(* Constructors of [section_path] *)
+val make_path : dir_path -> identifier -> path_kind -> section_path
+
+(* Destructors of [section_path] *)
+val repr_path : section_path -> dir_path * identifier * path_kind
+val dirpath : section_path -> dir_path
val basename : section_path -> identifier
val kind_of_path : section_path -> path_kind
val sp_of_wd : string list -> section_path
val wd_of_sp : section_path -> string list
+(* Parsing and printing of section path as "#module#id#kind" *)
val path_of_string : string -> section_path
val string_of_path : section_path -> string
-val string_of_path_mind : section_path -> identifier -> string
val print_sp : section_path -> std_ppcmds
+(*
+val string_of_path_mind : section_path -> identifier -> string
val coerce_path : path_kind -> section_path -> section_path
val fwsp_of : section_path -> section_path
val ccisp_of : section_path -> section_path
@@ -68,8 +81,13 @@ val append_to_path : section_path -> string -> section_path
val sp_ord : section_path -> section_path -> int
val sp_gt : section_path * section_path -> bool
+*)
+(* [is_dirpath_prefix p1 p2=true] if [p1] is a prefix of or is equal to [p2] *)
+val dirpath_prefix_of : dir_path -> dir_path -> bool
+(*
module Spset : Set.S with type elt = section_path
+*)
module Spmap : Map.S with type key = section_path
(*s Specific paths for declarations *)
@@ -80,3 +98,4 @@ type constructor_path = inductive_path * int
val hcons_names : unit ->
(section_path -> section_path) * (section_path -> section_path) *
(name -> name) * (identifier -> identifier) * (string -> string)
+
diff --git a/library/declare.ml b/library/declare.ml
index 84cc2e575..2383ca304 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -17,12 +17,12 @@ open Impargs
open Indrec
type strength =
- | DischargeAt of section_path
+ | DischargeAt of dir_path
| NeverDischarge
let make_strength = function
| [] -> NeverDischarge
- | l -> DischargeAt (sp_of_wd l)
+ | l -> DischargeAt l
let make_strength_0 () = make_strength (Lib.cwd())
diff --git a/library/declare.mli b/library/declare.mli
index b8e45bdea..6dfcb4065 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -17,7 +17,7 @@ open Inductive
[Nametab] and [Impargs]. *)
type strength =
- | DischargeAt of section_path
+ | DischargeAt of dir_path
| NeverDischarge
type section_variable_entry =
diff --git a/library/lib.ml b/library/lib.ml
index 171714c0e..74986d6fe 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -28,7 +28,7 @@ and library_segment = library_entry list
let lib_stk = ref ([] : (section_path * node) list)
let module_name = ref None
-let path_prefix = ref ([] : string list)
+let path_prefix = ref ([] : dir_path)
let recalc_path_prefix () =
let rec recalc = function
@@ -189,7 +189,7 @@ let reset_name id =
with Not_found ->
error (string_of_id id ^ ": no such entry")
-let is_section_p sp = list_prefix_of (wd_of_sp sp) !path_prefix
+let is_section_p sp = dirpath_prefix_of sp !path_prefix
(* State and initialization. *)
diff --git a/library/lib.mli b/library/lib.mli
index cf8b173b0..c6a0ba680 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -43,8 +43,8 @@ val open_section : string -> section_path
val close_section : string -> section_path * library_segment
val make_path : identifier -> path_kind -> section_path
-val cwd : unit -> string list
-val is_section_p : section_path -> bool
+val cwd : unit -> dir_path
+val is_section_p : dir_path -> bool
val start_module : string -> unit
val export_module : unit -> library_segment
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index 35d36bfca..288581c67 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -27,6 +27,7 @@ let print_basename sp =
warning "Undeclared constants in print_name";
string_of_path sp
+(*
let print_basename_mind sp mindid =
let (_,id,k) = repr_path sp in
try
@@ -37,7 +38,7 @@ let print_basename_mind sp mindid =
with Not_found ->
warning "Undeclared constants in print_name";
string_of_path_mind sp mindid
-
+*)
let print_closed_sections = ref false
let print_typed_value_in_env env (trm,typ) =
@@ -184,14 +185,6 @@ let print_mutual sp mib =
[<strcoind; strind>];
implicit_args_msg sp mipv >])
-let print_extracted_mutual sp =
- let mib = Global.lookup_mind (ccisp_of sp) in
- match mib.mind_singl with
- | None ->
- let fwsp = fwsp_of sp in
- print_mutual fwsp (Global.lookup_mind fwsp)
- | Some a -> fprterm a
-
let print_section_variable sp =
let ((id,_,_) as d,_,_) = out_variable sp in
let l = implicits_of_var id in
@@ -213,10 +206,10 @@ let print_constant with_values sep sp =
hOV 0 [< (match val_0 with
| None ->
[< 'sTR"*** [ ";
- 'sTR (print_basename (ccisp_of sp));
+ 'sTR (print_basename sp);
'sTR " : "; 'cUT ; prtype typ ; 'sTR" ]"; 'fNL >]
| _ ->
- [< 'sTR(print_basename (ccisp_of sp)) ;
+ [< 'sTR(print_basename sp) ;
'sTR sep; 'cUT ;
if with_values then
print_typed_body (val_0,typ)
@@ -225,7 +218,7 @@ let print_constant with_values sep sp =
print_impl_args (list_of_implicits l); 'fNL >]
else
hOV 0 [< 'sTR"Fw constant " ;
- 'sTR (print_basename (fwsp_of sp)) ; 'fNL>]
+ 'sTR (print_basename sp) ; 'fNL>]
let print_inductive sp =
let mib = Global.lookup_mind sp in
@@ -233,7 +226,7 @@ let print_inductive sp =
[< print_mutual sp mib; 'fNL >]
else
hOV 0 [< 'sTR"Fw inductive definition ";
- 'sTR (print_basename (fwsp_of sp)); 'fNL >]
+ 'sTR (print_basename sp); 'fNL >]
let print_leaf_entry with_values sep (sp,lobj) =
let tag = object_tag lobj in
@@ -355,7 +348,7 @@ let crible (fn : string -> env -> constr -> unit) name =
let env_ar = push_rels arities env in
(match kind_of_term const with
| IsMutInd ((sp',tyi),_) ->
- if sp = objsp_of sp' then
+ if sp=sp' then (*Suffit pas, cf les inds de Ensemble.v*)
print_constructors fn env_ar
(mind_nth_type_packet mib tyi)
| _ -> ());
@@ -501,151 +494,6 @@ let unfold_head_fconst =
in
unfrec
-(***
-let print_extracted_name name =
- let (sigma,(sign,fsign)) = initial_sigma_assumptions() in
- try
- let x = (Machops.global (gLOB sign) name) in
- match kind_of_term x with
- | IsConst _ ->
- let cont = snd(infexecute sigma (sign,fsign) x) in
- (match cont with
- | Inf {_VAL=trm; _TYPE=typ} ->
- (hOV 0
- [< 'sTR (string_of_id name);
- if defined_const sigma x then
- begin
- Constants.set_transparent_extraction name;
- [< 'sTR " ==>";'bRK(1,4);
- fprterm (unfold_head_fconst sigma trm); 'fNL>]
- end
- else
- [< >];
- 'sTR " : "; fprterm typ; 'fNL >])
- | _ -> error "Non informative term")
- | IsVar id ->
- (* Pourquoi on n'utilise pas fsign ? *)
- let a = snd(lookup_sign id sign) in
- let cont = snd(infexecute sigma (sign,fsign) a.body) in
- (match cont with (* Cradingue *)
- | Inf {_VAL=t;_TYPE=k} ->
- (match kind_of_term (whd_betadeltaiota sigma k) with
- | IsSort s ->
- fprint_var (string_of_id name) {body=t;typ=s})
- | _ -> error "Non informative term")
-
- | IsMutInd ((sp,_),_) ->
- let cont = snd(infexecute sigma (sign,fsign) x) in
- (match cont with
- | Inf _ ->
- (hOV 0 [< 'sTR (string_of_id name); 'sTR " ==>"; 'bRK(1,4);
- print_extracted_mutual sp >])
- | _ -> error "Non informative term")
- | IsMutConstruct _ ->
- let cont = snd(infexecute sigma (sign,fsign) x) in
- (match cont with
- | Inf d ->
- [< 'sTR ((string_of_id name) ^" ==> ");
- fprint_judge d ; 'fNL >]
- | _ -> error "Non informative term")
- | _ -> anomaly "should be a variable or constant"
- with Not_found ->
- error ((string_of_id name) ^ " not declared")
-
-let print_extraction () =
- let rec print_rec = function
- | (sp,Lib.LEAF lobj)::rest ->
- (match (sp,object_tag lobj) with
- | (sp,"CONSTANT") ->
- (try
- let (_,{cONSTBODY=d}) = const_of_path (fwsp_of sp) in
- [< print_rec rest;
- 'sTR(print_basename sp) ; 'sTR" ==> ";
- fprint_recipe d; 'fNL >]
- with Not_found ->
- print_rec rest)
- | (_,"VARIABLE") ->
- let (name,(_,cont),_,_,_,_) = outVariable lobj in
- [< print_rec rest;
- (match cont with
- | Some(t,_) -> fprint_var (string_of_id name) t
- | _ -> [< >]) >]
- | (sp,"INDUCTIVE") ->
- [< print_rec rest;
- (try
- [< print_extracted_mutual sp ; 'fNL >]
- with Not_found -> [<>]) >]
- | _ -> print_rec rest)
-
- | (sp,Lib.ClosedDir _)::rest -> print_rec rest
-
- | _::rest -> print_rec rest
-
- | [] -> [< 'fNL >]
- in
- [< print_rec (Lib.contents_after None); 'fNL >]
-
-let print_extracted_context () =
- let env = Lib.contents_after None in
- let rec print_var_rec = function
- | ((_,Lib.LEAF lobj))::rest ->
- if "VARIABLE" = object_tag lobj then
- let (name,(typ,cont),_,_,_,_) = outVariable lobj in
- [< print_var_rec rest ; 'fNL;
- match cont with
- | Some(t,_) -> fprint_var (string_of_id name) t
- | _ -> [< >] >]
- else
- print_var_rec rest
- | _::rest -> print_var_rec rest
- | [] -> [< 'fNL >]
-
- and print_last_constants = function
- | (sp,Lib.LEAF lobj)::rest ->
- (match object_tag lobj with
- | "CONSTANT" ->
- let (_,{cONSTBODY=c;cONSTTYPE=typ}) =
- const_of_path (fwsp_of sp) in
- [< print_last_constants rest;
- let s=print_basename sp in
- (try
- let (_,{cONSTBODY = d}) = const_of_path (fwsp_of sp) in
- [< 'sTR (s ^" ==> "); fprint_recipe d; 'fNL >]
- with Not_found ->
- [< >]) >]
- | "INDUCTIVE" ->
- [< print_last_constants rest;
- try print_extracted_mutual sp with Not_found -> [<>] >]
- | "VARIABLE" ->
- let (_,(_,cont),_,_,_,_) = outVariable lobj in
- (match cont with
- | Some _ -> [<>]
- | None -> print_last_constants rest)
- | _ -> print_last_constants rest)
-
- | (_,Lib.ClosedDir _)::rest -> print_last_constants rest
- | _ -> [< >]
- in
- [< print_var_rec env; print_last_constants env >]
-
-let print_extracted_vars () =
- let env = Lib.contents_after None in
- let rec print_var_rec = function
- | ((_,Lib.LEAF lobj))::rest ->
- if "VARIABLE" = object_tag lobj then
- let (name,(_,cont),_,_,_,_) = outVariable lobj in
- [< print_var_rec rest ; 'fNL;
- match cont with
- | Some (t,_) -> fprint_var (string_of_id name) t
- | _ -> [< >] >]
- else
- print_var_rec rest
- | _::rest -> print_var_rec rest
- | [] -> [< 'fNL >]
- in
- print_var_rec env
-***)
-
(* for debug *)
let inspect depth =
let rec inspectrec n res env =
@@ -665,7 +513,7 @@ open Classops
let string_of_strength = function
| NeverDischarge -> "(global)"
- | DischargeAt sp -> "(disch@"^(string_of_path sp)
+ | DischargeAt sp -> "(disch@"^(string_of_dirpath sp)
let print_coercion_value v = prterm v.cOE_VALUE.uj_val
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index dd7378d41..811e663de 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -16,7 +16,6 @@ open Environ
val assumptions_for_print : name list -> names_context
val print_basename : section_path -> string
-val print_basename_mind : section_path -> identifier -> string
val print_closed_sections : bool ref
val print_impl_args : int list -> std_ppcmds
val print_context : bool -> Lib.library_segment -> std_ppcmds
diff --git a/pretyping/class.ml b/pretyping/class.ml
index 6dfb3ca0b..75f4ee52d 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -22,7 +22,8 @@ let stre_gt = function
| (NeverDischarge,NeverDischarge) -> false
| (NeverDischarge,x) -> false
| (x,NeverDischarge) -> true
- | (DischargeAt sp1,DischargeAt sp2) -> sp_gt (sp1,sp2)
+ | (DischargeAt sp1,DischargeAt sp2) ->
+ dirpath_prefix_of sp1 sp2 (* was sp_gt but don't understand why - HH *)
let stre_max (stre1,stre2) =
if stre_gt (stre1,stre2) then stre1 else stre2
@@ -365,10 +366,7 @@ let try_add_new_coercion_record id stre source =
(* 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 defined_in_sec sp sec_sp = dirpath sp = sec_sp
let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) =
let env = Global.env () in
diff --git a/pretyping/class.mli b/pretyping/class.mli
index dc19ccce0..e88b3ccf0 100644
--- a/pretyping/class.mli
+++ b/pretyping/class.mli
@@ -18,9 +18,7 @@ val try_add_new_coercion_with_target : identifier -> strength ->
val try_add_new_class : identifier -> strength -> unit
val process_class :
- section_path -> (cl_typ * cl_info_typ) -> (cl_typ * cl_info_typ)
+ dir_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 ->
+ dir_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
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 080754172..f4cc94fd6 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -20,13 +20,14 @@ let rec filter_unique = function
if List.mem x l then filter_unique (List.filter (fun y -> x<>y) l)
else x::filter_unique l
+(*
let distinct_id_list =
let rec drec fresh = function
[] -> List.rev fresh
| id::rest ->
let id' = next_ident_away_from id fresh in drec (id'::fresh) rest
in drec []
-
+*)
(*
let filter_sign p sign x =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index d12a65db6..c883a5f27 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -36,7 +36,8 @@ let msg_proofs use_resume =
match Edit.dom proof_edits with
| [] -> [< 'sPC ; 'sTR"(No proof-editing in progress)." >]
| l -> [< 'sTR"." ; 'fNL ; 'sTR"Proofs currently edited:" ; 'sPC ;
- (print_idl (get_all_proof_names ())) ; 'sTR"." ;
+ (prlist_with_sep pr_spc print_id (get_all_proof_names ())) ;
+ 'sTR"." ;
(if use_resume then [< 'fNL ; 'sTR"Use \"Resume\" first." >]
else [< >])
>]
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b922aa13e..5b09315d9 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -239,7 +239,7 @@ let close_section _ s =
let oldenv = Global.env() in
let (sec_sp,decls) = close_section s in
let (ops,ids,_) =
- List.fold_left (process_item oldenv sec_sp) ([],[],[]) decls in
+ List.fold_left (process_item oldenv (wd_of_sp sec_sp)) ([],[],[]) decls in
Global.pop_named_decls ids;
List.iter process_operation (List.rev ops)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 01:25:48 +0000