diff options
| -rw-r--r-- | .depend | 26 | ||||
| -rw-r--r-- | lib/util.ml | 15 | ||||
| -rw-r--r-- | lib/util.mli | 1 | ||||
| -rw-r--r-- | library/declare.ml | 8 |
4 files changed, 36 insertions, 14 deletions
@@ -60,6 +60,8 @@ parsing/extend.cmi: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \ parsing/g_minicoq.cmi: kernel/names.cmi lib/pp.cmi kernel/sign.cmi \ kernel/term.cmi parsing/pcoq.cmi: parsing/coqast.cmi +parsing/pretty.cmi: kernel/inductive.cmi library/lib.cmi kernel/names.cmi \ + lib/pp.cmi kernel/term.cmi parsing/printer.cmi: parsing/coqast.cmi kernel/names.cmi lib/pp.cmi \ kernel/sign.cmi kernel/term.cmi parsing/termast.cmi: parsing/coqast.cmi kernel/names.cmi kernel/sign.cmi \ @@ -357,6 +359,14 @@ parsing/esyntax.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/extend.cmi \ lib/gmap.cmx lib/gmapl.cmx lib/pp.cmx lib/util.cmx parsing/esyntax.cmi parsing/lexer.cmo: lib/util.cmi parsing/lexer.cmi parsing/lexer.cmx: lib/util.cmx parsing/lexer.cmi +parsing/pretty.cmo: kernel/evd.cmi kernel/generic.cmi library/lib.cmi \ + library/library.cmi kernel/names.cmi library/nametab.cmi lib/pp.cmi \ + parsing/printer.cmi kernel/reduction.cmi kernel/term.cmi \ + parsing/pretty.cmi +parsing/pretty.cmx: kernel/evd.cmx kernel/generic.cmx library/lib.cmx \ + library/library.cmx kernel/names.cmx library/nametab.cmx lib/pp.cmx \ + parsing/printer.cmx kernel/reduction.cmx kernel/term.cmx \ + parsing/pretty.cmi parsing/printer.cmo: parsing/ast.cmi parsing/coqast.cmi library/declare.cmi \ parsing/esyntax.cmi parsing/extend.cmi library/global.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi lib/pp.cmi \ @@ -672,19 +682,19 @@ toplevel/vernacentries.cmo: parsing/ast.cmi pretyping/class.cmi \ kernel/environ.cmi kernel/evd.cmi parsing/extend.cmi \ library/libobject.cmi library/library.cmi proofs/macros.cmi \ kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \ - proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi proofs/proof_trees.cmi \ - kernel/reduction.cmi proofs/refiner.cmi library/states.cmi lib/system.cmi \ - proofs/tacmach.cmi kernel/term.cmi kernel/typing.cmi \ - toplevel/vernacinterp.cmi toplevel/vernacentries.cmi + proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \ + proofs/proof_trees.cmi kernel/reduction.cmi proofs/refiner.cmi \ + library/states.cmi lib/system.cmi proofs/tacmach.cmi kernel/term.cmi \ + kernel/typing.cmi toplevel/vernacinterp.cmi toplevel/vernacentries.cmi toplevel/vernacentries.cmx: parsing/ast.cmx pretyping/class.cmi \ pretyping/classops.cmx parsing/coqast.cmx library/declare.cmx \ kernel/environ.cmx kernel/evd.cmx parsing/extend.cmi \ library/libobject.cmx library/library.cmx proofs/macros.cmx \ kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmi \ - proofs/pfedit.cmi lib/pp.cmx lib/pp_control.cmx proofs/proof_trees.cmx \ - kernel/reduction.cmx proofs/refiner.cmx library/states.cmx lib/system.cmx \ - proofs/tacmach.cmx kernel/term.cmx kernel/typing.cmx \ - toplevel/vernacinterp.cmx toplevel/vernacentries.cmi + proofs/pfedit.cmi lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \ + proofs/proof_trees.cmx kernel/reduction.cmx proofs/refiner.cmx \ + library/states.cmx lib/system.cmx proofs/tacmach.cmx kernel/term.cmx \ + kernel/typing.cmx toplevel/vernacinterp.cmx toplevel/vernacentries.cmi toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \ toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \ proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \ diff --git a/lib/util.ml b/lib/util.ml index 77d26ecf4..59f119a50 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -390,6 +390,16 @@ let rec prlist_with_sep sep elem l = match l with let e = elem h and s = sep() and r = prlist_with_sep sep elem t in [< e; s; r >] +let prvecti elem v = + let n = Array.length v in + let rec pr i = + if i = 0 then + elem 0 v.(0) + else + let r = pr (i-1) and e = elem i v.(i) in [< r; e >] + in + pr (n-1) + let prvect_with_sep sep elem v = let rec pr n = if n = 0 then @@ -397,5 +407,6 @@ let prvect_with_sep sep elem v = else let r = pr (n-1) and s = sep() and e = elem v.(n) in [< r; s; e >] - in - if Array.length v = 0 then [< >] else pr (Array.length v - 1) + in + let n = Array.length v in + if n = 0 then [< >] else pr (n - 1) diff --git a/lib/util.mli b/lib/util.mli index 30d7bdee7..b8b72da09 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -123,6 +123,7 @@ val pr_str : string -> std_ppcmds val pr_coma : unit -> std_ppcmds val prlist : ('a -> 'b Stream.t) -> 'a list -> 'b Stream.t +val prvecti : (int -> 'a -> 'b Stream.t) -> 'a array -> 'b Stream.t val prlist_with_sep : (unit -> 'a Stream.t) -> ('b -> 'a Stream.t) -> 'b list -> 'a Stream.t val prvect_with_sep : diff --git a/library/declare.ml b/library/declare.ml index aca22ebd2..52355a7e2 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -38,7 +38,7 @@ let (in_variable, out_variable) = load_function = load_variable; open_function = open_variable; specification_function = specification_variable } in - declare_object ("Variable", od) + declare_object ("VARIABLE", od) let declare_variable id c = let obj = (id,c) in @@ -63,7 +63,7 @@ let (in_parameter, out_parameter) = load_function = (fun _ -> ()); open_function = open_parameter; specification_function = specification_parameter } in - declare_object ("Parameter", od) + declare_object ("PARAMETER", od) let declare_parameter id c = let sp = add_leaf id CCI (in_parameter c) in @@ -89,7 +89,7 @@ let (in_constant, out_constant) = load_function = (fun _ -> ()); open_function = open_constant; specification_function = specification_constant } in - declare_object ("Constant", od) + declare_object ("CONSTANT", od) let declare_constant id ce = let sp = add_leaf id CCI (in_constant ce) in @@ -123,7 +123,7 @@ let (in_inductive, out_inductive) = load_function = (fun _ -> ()); open_function = open_inductive; specification_function = specification_inductive } in - declare_object ("Inductive", od) + declare_object ("INDUCTIVE", od) let declare_mind mie = let id = match mie.mind_entry_inds with |