diff options
172 files changed, 1209 insertions, 1016 deletions
diff --git a/.travis.yml b/.travis.yml index e40568995..9c7ad553f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -37,33 +37,33 @@ env: - TEST_TARGET="test-suite" COMPILER="4.02.3+32bit" - TEST_TARGET="validate" TW="travis_wait" - TEST_TARGET="validate" COMPILER="4.02.3+32bit" TW="travis_wait" - - TEST_TARGET="ci-bignums" - - TEST_TARGET="ci-color" - - TEST_TARGET="ci-compcert" + - TEST_TARGET="ci-bignums TIMED=1" + - TEST_TARGET="ci-color TIMED=1" + - TEST_TARGET="ci-compcert TIMED=1" - TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - - TEST_TARGET="ci-coquelicot" - - TEST_TARGET="ci-geocoq" - - TEST_TARGET="ci-fiat-crypto" - - TEST_TARGET="ci-fiat-parsers" - - TEST_TARGET="ci-flocq" - - TEST_TARGET="ci-formal-topology" - - TEST_TARGET="ci-hott" - - TEST_TARGET="ci-iris-coq" - - TEST_TARGET="ci-math-classes" - - TEST_TARGET="ci-math-comp" - - TEST_TARGET="ci-sf" - - TEST_TARGET="ci-unimath" - - TEST_TARGET="ci-vst" + - TEST_TARGET="ci-coquelicot TIMED=1" + - TEST_TARGET="ci-geocoq TIMED=1" + - TEST_TARGET="ci-fiat-crypto TIMED=1" + - TEST_TARGET="ci-fiat-parsers TIMED=1" + - TEST_TARGET="ci-flocq TIMED=1" + - TEST_TARGET="ci-formal-topology TIMED=1" + - TEST_TARGET="ci-hott TIMED=1" + - TEST_TARGET="ci-iris-coq TIMED=1" + - TEST_TARGET="ci-math-classes TIMED=1" + - TEST_TARGET="ci-math-comp TIMED=1" + - TEST_TARGET="ci-sf TIMED=1" + - TEST_TARGET="ci-unimath TIMED=1" + - TEST_TARGET="ci-vst TIMED=1" # Not ready yet for 8.7 - # - TEST_TARGET="ci-cpdt" - # - TEST_TARGET="ci-metacoq" - # - TEST_TARGET="ci-tlc" + # - TEST_TARGET="ci-cpdt TIMED=1" + # - TEST_TARGET="ci-metacoq TIMED=1" + # - TEST_TARGET="ci-tlc TIMED=1" matrix: allow_failures: - env: TEST_TARGET="ci-coq-dpdgraph" EXTRA_OPAM="ocamlgraph" - - env: TEST_TARGET="ci-geocoq" + - env: TEST_TARGET="ci-geocoq TIMED=1" include: # Full Coq test-suite with two compilers diff --git a/API/API.mli b/API/API.mli index d39d3cb25..a99cd2a9a 100644 --- a/API/API.mli +++ b/API/API.mli @@ -47,7 +47,7 @@ sig val of_string : string -> t val of_string_soft : string -> t val to_string : t -> string - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t module Set : Set.S with type elt = t module Map : Map.ExtS with type key = t and module Set := Set @@ -67,7 +67,7 @@ sig val equal : t -> t -> bool val hash : t -> int val hcons : t -> t - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t end type name = Name.t = @@ -128,7 +128,7 @@ sig val compare : t -> t -> int val label : t -> Label.t val repr : t -> ModPath.t * DirPath.t * Label.t - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t val to_string : t -> string end @@ -159,7 +159,7 @@ sig val modpath : t -> ModPath.t val label : t -> Label.t val user : t -> KerName.t - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t end module Projection : @@ -169,6 +169,8 @@ sig val map : (Constant.t -> Constant.t) -> t -> t val constant : t -> Constant.t val equal : t -> t -> bool + val unfolded : t -> bool + val unfold : t -> t end type evaluable_global_reference = @@ -212,7 +214,7 @@ sig val var_full_transparent_state : transparent_state val cst_full_transparent_state : transparent_state - val pr_kn : KerName.t -> Pp.std_ppcmds + val pr_kn : KerName.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.KerName.print"] val eq_constant : Constant.t -> Constant.t -> bool @@ -297,11 +299,11 @@ sig val make_con : ModPath.t -> DirPath.t -> Label.t -> Constant.t [@@ocaml.deprecated "alias of API.Names.Constant.make3"] - val debug_pr_con : Constant.t -> Pp.std_ppcmds + val debug_pr_con : Constant.t -> Pp.t - val debug_pr_mind : MutInd.t -> Pp.std_ppcmds + val debug_pr_mind : MutInd.t -> Pp.t - val pr_con : Constant.t -> Pp.std_ppcmds + val pr_con : Constant.t -> Pp.t val string_of_con : Constant.t -> string @@ -323,7 +325,7 @@ sig sig type t val set : t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end type universe_level = Level.t @@ -331,13 +333,13 @@ sig module LSet : sig include CSig.SetS with type elt = universe_level - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t end module Universe : sig type t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end type universe = Universe.t @@ -348,7 +350,7 @@ sig val empty : t val of_array : Level.t array -> t val to_array : t -> Level.t array - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t end type 'a puniverses = 'a * Instance.t @@ -418,7 +420,7 @@ sig val union : 'a t -> 'a t -> 'a t val diff : 'a t -> 'a t -> 'a t val subst_union : 'a option t -> 'a option t -> 'a option t - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t end type 'a universe_map = 'a LMap.t @@ -426,18 +428,18 @@ sig type universe_level_subst = universe_level universe_map val enforce_leq : Universe.t constraint_function - val pr_uni : Universe.t -> Pp.std_ppcmds - val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> UContext.t -> Pp.std_ppcmds - val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> ContextSet.t -> Pp.std_ppcmds - val pr_universe_subst : universe_subst -> Pp.std_ppcmds - val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds - val pr_constraints : (Level.t -> Pp.std_ppcmds) -> Constraint.t -> Pp.std_ppcmds + val pr_uni : Universe.t -> Pp.t + val pr_universe_context : (Level.t -> Pp.t) -> UContext.t -> Pp.t + val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t + val pr_universe_subst : universe_subst -> Pp.t + val pr_universe_level_subst : universe_level_subst -> Pp.t + val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t end module UGraph : sig type t - val pr_universes : (Univ.Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr_universes : (Univ.Level.t -> Pp.t) -> t -> Pp.t end module Esubst : @@ -1033,8 +1035,8 @@ sig val subst_mps : substitution -> Constr.t -> Constr.t val subst_constant : substitution -> Names.Constant.t -> Names.Constant.t val subst_ind : substitution -> Names.inductive -> Names.inductive - val debug_pr_subst : substitution -> Pp.std_ppcmds - val debug_pr_delta : delta_resolver -> Pp.std_ppcmds + val debug_pr_subst : substitution -> Pp.t + val debug_pr_delta : delta_resolver -> Pp.t end module Opaqueproof : @@ -1749,10 +1751,10 @@ module Nameops : sig val atompart_of_id : Names.Id.t -> string - val pr_id : Names.Id.t -> Pp.std_ppcmds + val pr_id : Names.Id.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Id.print"] - val pr_name : Names.Name.t -> Pp.std_ppcmds + val pr_name : Names.Name.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Name.print"] val name_fold : (Names.Id.t -> 'a -> 'a) -> Names.Name.t -> 'a -> 'a @@ -1761,7 +1763,7 @@ sig val increment_subscript : Names.Id.t -> Names.Id.t val make_ident : string -> int option -> Names.Id.t val out_name : Names.Name.t -> Names.Id.t - val pr_lab : Names.Label.t -> Pp.std_ppcmds + val pr_lab : Names.Label.t -> Pp.t module Name : sig include module type of struct include Names.Name end @@ -1777,7 +1779,7 @@ sig open Names type full_path - val pr_path : full_path -> Pp.std_ppcmds + val pr_path : full_path -> Pp.t val make_path : Names.DirPath.t -> Names.Id.t -> full_path val eq_full_path : full_path -> full_path -> bool val dirpath : full_path -> Names.DirPath.t @@ -1787,7 +1789,7 @@ sig val make_qualid : Names.DirPath.t -> Names.Id.t -> qualid val qualid_eq : qualid -> qualid -> bool val repr_qualid : qualid -> Names.DirPath.t * Names.Id.t - val pr_qualid : qualid -> Pp.std_ppcmds + val pr_qualid : qualid -> Pp.t val string_of_qualid : qualid -> string val qualid_of_string : string -> qualid val qualid_of_path : full_path -> qualid @@ -1799,12 +1801,12 @@ sig | Ident of Names.Id.t Loc.located val loc_of_reference : reference -> Loc.t option val qualid_of_reference : reference -> qualid Loc.located - val pr_reference : reference -> Pp.std_ppcmds + val pr_reference : reference -> Pp.t val is_dirpath_prefix_of : Names.DirPath.t -> Names.DirPath.t -> bool val split_dirpath : Names.DirPath.t -> Names.DirPath.t * Names.Id.t val dirpath_of_string : string -> Names.DirPath.t - val pr_dirpath : Names.DirPath.t -> Pp.std_ppcmds + val pr_dirpath : Names.DirPath.t -> Pp.t val string_of_path : full_path -> string val basename : full_path -> Names.Id.t @@ -1929,7 +1931,7 @@ sig val locate_extended : Libnames.qualid -> Globnames.extended_global_reference val full_name_module : Libnames.qualid -> Names.DirPath.t val locate_tactic : Libnames.qualid -> Names.KerName.t - val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.std_ppcmds + val pr_global_env : Names.Id.Set.t -> Globnames.global_reference -> Pp.t val shortest_qualid_of_tactic : Names.KerName.t -> Libnames.qualid val basename_of_global : Globnames.global_reference -> Names.Id.t @@ -2052,7 +2054,7 @@ sig type key val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option val declare_equiv_keys : key -> key -> unit - val pr_keys : (Globnames.global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds + val pr_keys : (Globnames.global_reference -> Pp.t) -> Pp.t end module Coqlib : @@ -2127,14 +2129,14 @@ sig val constr_of_global : Globnames.global_reference -> Constr.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val new_sort_in_family : Sorts.family -> Sorts.t - val pr_with_global_universes : Univ.Level.t -> Pp.std_ppcmds - val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds + val pr_with_global_universes : Univ.Level.t -> Pp.t + val pr_universe_opt_subst : universe_opt_subst -> Pp.t type universe_constraint module Constraints : sig type t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end type universe_constraints = Constraints.t @@ -2752,9 +2754,9 @@ sig val it_mkLambda_or_LetIn : Constr.t -> Context.Rel.t -> Constr.t val local_occur_var : Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool val occur_var : Environ.env -> Evd.evar_map -> Names.Id.t -> EConstr.constr -> bool - val pr_evar_info : Evd.evar_info -> Pp.std_ppcmds + val pr_evar_info : Evd.evar_info -> Pp.t - val print_constr : EConstr.constr -> Pp.std_ppcmds + val print_constr : EConstr.constr -> Pp.t (** [dependent m t] tests whether [m] is a subterm of [t] *) val dependent : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool @@ -2798,8 +2800,8 @@ sig val ids_of_named_context : ('c, 't) Context.Named.pt -> Names.Id.t list val ids_of_context : Environ.env -> Names.Id.t list val global_of_constr : Evd.evar_map -> EConstr.constr -> Globnames.global_reference * EConstr.EInstance.t - val print_named_context : Environ.env -> Pp.std_ppcmds - val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds + val print_named_context : Environ.env -> Pp.t + val print_constr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t val clear_named_body : Names.Id.t -> Environ.env -> Environ.env val is_Prop : Evd.evar_map -> EConstr.constr -> bool val is_global : Evd.evar_map -> Globnames.global_reference -> EConstr.constr -> bool @@ -2820,14 +2822,14 @@ sig val replace_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> EConstr.constr -> EConstr.constr val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt - val pr_metaset : Evd.Metaset.t -> Pp.std_ppcmds - val pr_evar_map : ?with_univs:bool -> int option -> Evd.evar_map -> Pp.std_ppcmds - val pr_evar_universe_context : UState.t -> Pp.std_ppcmds + val pr_metaset : Evd.Metaset.t -> Pp.t + val pr_evar_map : ?with_univs:bool -> int option -> Evd.evar_map -> Pp.t + val pr_evar_universe_context : UState.t -> Pp.t end module Proofview_monad : sig - type lazy_msg = unit -> Pp.std_ppcmds + type lazy_msg = unit -> Pp.t module Info : sig type tree @@ -2903,10 +2905,10 @@ sig val ( >> ) : unit t -> 'a t -> 'a t val ( >>= ) : 'a t -> ('a -> 'b t) -> 'b t val print_char : char -> unit t - val print_debug : Pp.std_ppcmds -> unit t - val print_warning : Pp.std_ppcmds -> unit t - val print_notice : Pp.std_ppcmds -> unit t - val print_info : Pp.std_ppcmds -> unit t + val print_debug : Pp.t -> unit t + val print_warning : Pp.t -> unit t + val print_notice : Pp.t -> unit t + val print_info : Pp.t -> unit t val run : 'a t -> 'a type 'a ref val ref : 'a -> 'a ref t @@ -3036,7 +3038,7 @@ sig | Opt : 'a tag -> 'a option tag | Pair : 'a tag * 'b tag -> ('a * 'b) tag val create : string -> 'a typ - val pr : 'a typ -> Pp.std_ppcmds + val pr : 'a typ -> Pp.t val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option val typ_list : t list typ val typ_opt : t option typ @@ -3289,16 +3291,16 @@ sig val nf_evar : Evd.evar_map -> EConstr.constr -> EConstr.constr val nf_meta : Evd.evar_map -> EConstr.constr -> EConstr.constr val hnf_prod_appvect : Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr array -> EConstr.constr - val pr_state : state -> Pp.std_ppcmds + val pr_state : state -> Pp.t module Stack : sig type 'a t - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t end module Cst_stack : sig type t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end end @@ -3969,7 +3971,7 @@ sig EConstr.types * inheritance_path val get_coercion_value : coe_index -> Constr.t val coercions : unit -> coe_index list - val pr_cl_index : cl_index -> Pp.std_ppcmds + val pr_cl_index : cl_index -> Pp.t end module Detyping : @@ -4202,11 +4204,11 @@ sig Bigint.bigint prim_token_interpreter -> Bigint.bigint prim_token_uninterpreter -> unit val interp_notation_as_global_reference : ?loc:Loc.t -> (Globnames.global_reference -> bool) -> Constrexpr.notation -> delimiters option -> Globnames.global_reference - val locate_notation : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Constrexpr.notation -> - Notation_term.scope_name option -> Pp.std_ppcmds + val locate_notation : (Glob_term.glob_constr -> Pp.t) -> Constrexpr.notation -> + Notation_term.scope_name option -> Pp.t val find_delimiters_scope : ?loc:Loc.t -> delimiters -> Notation_term.scope_name - val pr_scope : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Notation_term.scope_name -> Pp.std_ppcmds - val pr_scopes : (Glob_term.glob_constr -> Pp.std_ppcmds) -> Pp.std_ppcmds + val pr_scope : (Glob_term.glob_constr -> Pp.t) -> Notation_term.scope_name -> Pp.t + val pr_scopes : (Glob_term.glob_constr -> Pp.t) -> Pp.t val interp_notation : ?loc:Loc.t -> Constrexpr.notation -> local_scopes -> Notation_term.interpretation * (notation_location * Notation_term.scope_name option) val uninterp_prim_token : Glob_term.glob_constr -> Notation_term.scope_name * Constrexpr.prim_token @@ -4339,19 +4341,19 @@ end module Miscprint : sig val pr_or_and_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_and_intro_pattern_expr -> Pp.std_ppcmds - val pr_intro_pattern_naming : Misctypes.intro_pattern_naming_expr -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a Misctypes.or_and_intro_pattern_expr -> Pp.t + val pr_intro_pattern_naming : Misctypes.intro_pattern_naming_expr -> Pp.t val pr_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a Misctypes.intro_pattern_expr Loc.located -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a Misctypes.intro_pattern_expr Loc.located -> Pp.t val pr_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a Misctypes.bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a Misctypes.bindings -> Pp.t val pr_bindings_no_with : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a Misctypes.bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a Misctypes.bindings -> Pp.t val pr_with_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a * 'a Misctypes.bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a * 'a Misctypes.bindings -> Pp.t end (* All items in the Goal modules are deprecated. *) @@ -4359,7 +4361,7 @@ module Goal : sig type goal = Evar.t - val pr_goal : goal -> Pp.std_ppcmds + val pr_goal : goal -> Pp.t module V82 : sig @@ -4436,7 +4438,7 @@ sig unit Proofview.tactic -> proof -> proof * (bool * Proofview_monad.Info.tree) val unshelve : proof -> proof val maximal_unfocus : 'a focus_kind -> proof -> proof - val pr_proof : proof -> Pp.std_ppcmds + val pr_proof : proof -> Pp.t module V82 : sig val grab_evars : proof -> proof @@ -4515,13 +4517,13 @@ sig val repackage : Evd.evar_map ref -> 'a -> 'a Evd.sigma val tclSHOWHYPS : Proof_type.tactic -> Proof_type.tactic - exception FailError of int * Pp.std_ppcmds Lazy.t + exception FailError of int * Pp.t Lazy.t val tclEVARS : Evd.evar_map -> Proof_type.tactic val tclMAP : ('a -> Proof_type.tactic) -> 'a list -> Proof_type.tactic val tclREPEAT : Proof_type.tactic -> Proof_type.tactic val tclORELSE : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic - val tclFAIL : int -> Pp.std_ppcmds -> Proof_type.tactic + val tclFAIL : int -> Pp.t -> Proof_type.tactic val tclIDTAC : Proof_type.tactic val tclTHEN : Proof_type.tactic -> Proof_type.tactic -> Proof_type.tactic val tclTHENLIST : Proof_type.tactic list -> Proof_type.tactic @@ -4580,7 +4582,7 @@ sig val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list - val pr_gls : Goal.goal Evd.sigma -> Pp.std_ppcmds + val pr_gls : Goal.goal Evd.sigma -> Pp.t val pf_nf_betaiota : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr @@ -4654,7 +4656,7 @@ sig val solve_evar_clause : Environ.env -> Evd.evar_map -> bool -> clause -> EConstr.constr Misctypes.bindings -> Evd.evar_map type clausenv - val pr_clenv : clausenv -> Pp.std_ppcmds + val pr_clenv : clausenv -> Pp.t end (************************************************************************) @@ -4849,7 +4851,7 @@ end module Genprint : sig - type 'a printer = 'a -> Pp.std_ppcmds + type 'a printer = 'a -> Pp.t val generic_top_print : Genarg.tlevel Genarg.generic_argument printer val register_print0 : ('raw, 'glb, 'top) Genarg.genarg_type -> 'raw printer -> 'glb printer -> 'top printer -> unit @@ -4857,74 +4859,74 @@ end module Pputils : sig - val pr_with_occurrences : ('a -> Pp.std_ppcmds) -> (string -> Pp.std_ppcmds) -> 'a Locus.with_occurrences -> Pp.std_ppcmds + val pr_with_occurrences : ('a -> Pp.t) -> (string -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t val pr_red_expr : - ('a -> Pp.std_ppcmds) * ('a -> Pp.std_ppcmds) * ('b -> Pp.std_ppcmds) * ('c -> Pp.std_ppcmds) -> - (string -> Pp.std_ppcmds) -> - ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.std_ppcmds - val pr_raw_generic : Environ.env -> Genarg.rlevel Genarg.generic_argument -> Pp.std_ppcmds - val pr_glb_generic : Environ.env -> Genarg.glevel Genarg.generic_argument -> Pp.std_ppcmds - val pr_or_var : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_var -> Pp.std_ppcmds - val pr_or_by_notation : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_by_notation -> Pp.std_ppcmds + ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + (string -> Pp.t) -> + ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t + val pr_raw_generic : Environ.env -> Genarg.rlevel Genarg.generic_argument -> Pp.t + val pr_glb_generic : Environ.env -> Genarg.glevel Genarg.generic_argument -> Pp.t + val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t + val pr_or_by_notation : ('a -> Pp.t) -> 'a Misctypes.or_by_notation -> Pp.t end module Ppconstr : sig - val pr_name : Names.Name.t -> Pp.std_ppcmds + val pr_name : Names.Name.t -> Pp.t [@@ocaml.deprecated "alias of API.Names.Name.print"] - val pr_id : Names.Id.t -> Pp.std_ppcmds - val pr_or_var : ('a -> Pp.std_ppcmds) -> 'a Misctypes.or_var -> Pp.std_ppcmds - val pr_with_comments : ?loc:Loc.t -> Pp.std_ppcmds -> Pp.std_ppcmds - val pr_lident : Names.Id.t Loc.located -> Pp.std_ppcmds - val pr_lname : Names.Name.t Loc.located -> Pp.std_ppcmds + val pr_id : Names.Id.t -> Pp.t + val pr_or_var : ('a -> Pp.t) -> 'a Misctypes.or_var -> Pp.t + val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t + val pr_lident : Names.Id.t Loc.located -> Pp.t + val pr_lname : Names.Name.t Loc.located -> Pp.t val prec_less : int -> int * Ppextend.parenRelation -> bool - val pr_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds - val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds - val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.std_ppcmds - val pr_lconstr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.std_ppcmds - val pr_binders : Constrexpr.local_binder_expr list -> Pp.std_ppcmds - val pr_glob_sort : Misctypes.glob_sort -> Pp.std_ppcmds + val pr_constr_expr : Constrexpr.constr_expr -> Pp.t + val pr_lconstr_expr : Constrexpr.constr_expr -> Pp.t + val pr_constr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t + val pr_lconstr_pattern_expr : Constrexpr.constr_pattern_expr -> Pp.t + val pr_binders : Constrexpr.local_binder_expr list -> Pp.t + val pr_glob_sort : Misctypes.glob_sort -> Pp.t end module Printer : sig - val pr_named_context : Environ.env -> Evd.evar_map -> Context.Named.t -> Pp.std_ppcmds - val pr_rel_context : Environ.env -> Evd.evar_map -> Context.Rel.t -> Pp.std_ppcmds - val pr_goal : Goal.goal Evd.sigma -> Pp.std_ppcmds - - val pr_constr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.std_ppcmds - val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.std_ppcmds - - val pr_constr : Constr.t -> Pp.std_ppcmds - - val pr_lconstr : Constr.t -> Pp.std_ppcmds - - val pr_econstr : EConstr.constr -> Pp.std_ppcmds - val pr_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds - val pr_constr_pattern : Pattern.constr_pattern -> Pp.std_ppcmds - val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.std_ppcmds - val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.std_ppcmds - val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds - val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.std_ppcmds - val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.std_ppcmds - val pr_closed_glob : Glob_term.closed_glob_constr -> Pp.std_ppcmds - val pr_lglob_constr : Glob_term.glob_constr -> Pp.std_ppcmds - val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.std_ppcmds - val pr_leconstr : EConstr.constr -> Pp.std_ppcmds - val pr_global : Globnames.global_reference -> Pp.std_ppcmds - val pr_lconstr_under_binders : Pattern.constr_under_binders -> Pp.std_ppcmds - val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.std_ppcmds - - val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.std_ppcmds - val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Pp.std_ppcmds - val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds - val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.std_ppcmds - val pr_ltype : Term.types -> Pp.std_ppcmds - val pr_ljudge : EConstr.unsafe_judgment -> Pp.std_ppcmds * Pp.std_ppcmds - val pr_idpred : Names.Id.Pred.t -> Pp.std_ppcmds - val pr_cpred : Names.Cpred.t -> Pp.std_ppcmds - val pr_transparent_state : Names.transparent_state -> Pp.std_ppcmds + val pr_named_context : Environ.env -> Evd.evar_map -> Context.Named.t -> Pp.t + val pr_rel_context : Environ.env -> Evd.evar_map -> Context.Rel.t -> Pp.t + val pr_goal : Goal.goal Evd.sigma -> Pp.t + + val pr_constr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t + val pr_lconstr_env : Environ.env -> Evd.evar_map -> Constr.t -> Pp.t + + val pr_constr : Constr.t -> Pp.t + + val pr_lconstr : Constr.t -> Pp.t + + val pr_econstr : EConstr.constr -> Pp.t + val pr_glob_constr : Glob_term.glob_constr -> Pp.t + val pr_constr_pattern : Pattern.constr_pattern -> Pp.t + val pr_glob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t + val pr_lglob_constr_env : Environ.env -> Glob_term.glob_constr -> Pp.t + val pr_econstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t + val pr_constr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t + val pr_lconstr_pattern_env : Environ.env -> Evd.evar_map -> Pattern.constr_pattern -> Pp.t + val pr_closed_glob : Glob_term.closed_glob_constr -> Pp.t + val pr_lglob_constr : Glob_term.glob_constr -> Pp.t + val pr_leconstr_env : Environ.env -> Evd.evar_map -> EConstr.constr -> Pp.t + val pr_leconstr : EConstr.constr -> Pp.t + val pr_global : Globnames.global_reference -> Pp.t + val pr_lconstr_under_binders : Pattern.constr_under_binders -> Pp.t + val pr_lconstr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t + + val pr_constr_under_binders_env : Environ.env -> Evd.evar_map -> Pattern.constr_under_binders -> Pp.t + val pr_closed_glob_env : Environ.env -> Evd.evar_map -> Glob_term.closed_glob_constr -> Pp.t + val pr_rel_context_of : Environ.env -> Evd.evar_map -> Pp.t + val pr_named_context_of : Environ.env -> Evd.evar_map -> Pp.t + val pr_ltype : Term.types -> Pp.t + val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t + val pr_idpred : Names.Id.Pred.t -> Pp.t + val pr_cpred : Names.Cpred.t -> Pp.t + val pr_transparent_state : Names.transparent_state -> Pp.t end (************************************************************************) @@ -4942,7 +4944,7 @@ sig val tclORELSE : tactic -> tactic -> tactic val tclDO : int -> tactic -> tactic val tclIDTAC : tactic - val tclFAIL : int -> Pp.std_ppcmds -> tactic + val tclFAIL : int -> Pp.t -> tactic val tclTHEN : tactic -> tactic -> tactic val tclTHENLIST : tactic list -> tactic val pf_constr_of_global : @@ -4979,12 +4981,12 @@ sig sig open Proofview val tclORELSE0 : unit tactic -> unit tactic -> unit tactic - val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic + val tclFAIL : int -> Pp.t -> 'a tactic val pf_constr_of_global : Globnames.global_reference -> EConstr.constr tactic val tclTHEN : unit tactic -> unit tactic -> unit tactic val tclTHENS : unit tactic -> unit tactic list -> unit tactic val tclFIRST : unit tactic list -> unit tactic - val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic + val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic val tclORELSE : unit tactic -> unit tactic -> unit tactic val tclREPEAT : unit tactic -> unit tactic val tclTRY : unit tactic -> unit tactic @@ -5041,7 +5043,7 @@ sig val check_scheme : 'a scheme_kind -> Names.inductive -> bool val find_scheme : ?mode:Declare.internal_flag -> 'a scheme_kind -> Names.inductive -> Names.Constant.t * Safe_typing.private_constants - val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds + val pr_scheme_kind : 'a scheme_kind -> Pp.t end module Elimschemes : @@ -5400,11 +5402,11 @@ sig val add_hints : bool -> hint_db_name list -> hints_entry -> unit val searchtable_map : hint_db_name -> hint_db - val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds - val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds + val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t + val pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t val glob_hints_path_atom : Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen - val pp_hints_path : hints_path -> Pp.std_ppcmds + val pp_hints_path : hints_path -> Pp.t val glob_hints_path : Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen val run_hint : hint -> @@ -5414,7 +5416,7 @@ sig val create_hint_db : bool -> hint_db_name -> Names.transparent_state -> bool -> unit val empty_hint_info : 'a Vernacexpr.hint_info_gen val repr_hint : hint -> (raw_hint * Clenv.clausenv) hint_ast - val pr_hint_db : Hint_db.t -> Pp.std_ppcmds + val pr_hint_db : Hint_db.t -> Pp.t end module Auto : @@ -5491,7 +5493,7 @@ sig val add_rew_rules : string -> raw_rew_rule list -> unit val find_rewrites : string -> rew_rule list val find_matches : string -> Constr.t -> rew_rule list - val print_rewrite_hintdb : string -> Pp.std_ppcmds + val print_rewrite_hintdb : string -> Pp.t end (************************************************************************) @@ -5504,8 +5506,8 @@ end module Ppvernac : sig - val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds - val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds + val pr_vernac : Vernacexpr.vernac_expr -> Pp.t + val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t end module Lemmas : @@ -5528,14 +5530,14 @@ end module Himsg : sig - val explain_refiner_error : Logic.refiner_error -> Pp.std_ppcmds - val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.std_ppcmds + val explain_refiner_error : Logic.refiner_error -> Pp.t + val explain_pretype_error : Environ.env -> Evd.evar_map -> Pretype_errors.pretype_error -> Pp.t end module ExplainErr : sig val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn - val register_additional_error_info : (Util.iexn -> Pp.std_ppcmds option Loc.located option) -> unit + val register_additional_error_info : (Util.iexn -> Pp.t option Loc.located option) -> unit end module Locality : @@ -5580,7 +5582,7 @@ sig val solve_all_obligations : unit Proofview.tactic option -> unit val admit_obligations : Names.Id.t option -> unit val show_obligations : ?msg:bool -> Names.Id.t option -> unit - val show_term : Names.Id.t option -> Pp.std_ppcmds + val show_term : Names.Id.t option -> Pp.t end module Command : @@ -1,3 +1,10 @@ +To be inserted at the proper place: + +Notations + +- Recursive notations with the recursive pattern repeating on the + right (e.g. "( x ; .. ; y ; z )") now supported. + Changes beyond V8.6 =================== @@ -75,6 +82,8 @@ Standard Library Plugins - The mathematical proof language (also known as declarative mode) was removed. +- A new command Extraction TestCompile has been introduced, not meant + for the general user but instead for Coq's test-suite. Dependencies @@ -137,6 +137,7 @@ endif # This should help preventing weird compilation failures caused by leftover # compiled files after deleting or moving some source files. +ifeq (,$(findstring clean,$(MAKECMDGOALS))) # Skip this for 'make clean' and alii ifndef ACCEPT_ALIEN_VO EXISTINGVO:=$(call find, '*.vo') KNOWNVO:=$(patsubst %.v,%.vo,$(call find, '*.v')) @@ -162,6 +163,7 @@ remove them first, for instance via 'make clean' \ (or skip this check via 'make ACCEPT_ALIEN_OBJ=1')) endif endif +endif # Apart from clean and tags, everything will be done in a sub-call to make # on Makefile.build. This way, we avoid doing here the -include of .d : diff --git a/Makefile.build b/Makefile.build index 7961092fa..b45c6427a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -237,7 +237,7 @@ endef # Camlp5 settings -CAMLP4DEPS:=grammar/compat5.cmo grammar/grammar.cma +CAMLP4DEPS:=grammar/grammar.cma CAMLP4USE=pa_extend.cmo q_MLast.cmo pa_macro.cmo -D$(CAMLVERSION) PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) diff --git a/Makefile.ci b/Makefile.ci index c8bc09fdc..1b09905cc 100644 --- a/Makefile.ci +++ b/Makefile.ci @@ -24,4 +24,9 @@ CI_TARGETS=ci-all \ # Generic rule, we use make to easy travis integraton with mixed rules $(CI_TARGETS): ci-%: - +./dev/ci/ci-$*.sh + rm -f ci-$*.ok + +(./dev/ci/ci-$*.sh 2>&1 && touch ci-$*.ok) | tee time-of-build.log + echo 'Aggregating timing log...' && echo -en 'travis_fold:start:coq.test.timing\\r' + python ./tools/make-one-time-file.py time-of-build.log + echo -en 'travis_fold:end:coq.test.timing\\r' + rm ci-$*.ok # must not be -f; we're checking to see that it exists diff --git a/Makefile.common b/Makefile.common index 85ecb1a08..afd6164fc 100644 --- a/Makefile.common +++ b/Makefile.common @@ -109,7 +109,7 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/librar TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma -GRAMMARCMA:=grammar/compat5.cmo grammar/grammar.cma +GRAMMARCMA:=grammar/grammar.cma # modules known by the toplevel of Coq diff --git a/checker/indtypes.mli b/checker/indtypes.mli index 7eaaf65f2..b0554989e 100644 --- a/checker/indtypes.mli +++ b/checker/indtypes.mli @@ -12,8 +12,8 @@ open Cic open Environ (*i*) -val prkn : kernel_name -> Pp.std_ppcmds -val prcon : constant -> Pp.std_ppcmds +val prkn : kernel_name -> Pp.t +val prcon : constant -> Pp.t (*s The different kinds of errors that may result of a malformed inductive definition. *) diff --git a/checker/univ.ml b/checker/univ.ml index e3abc436f..558315c2c 100644 --- a/checker/univ.ml +++ b/checker/univ.ml @@ -1071,7 +1071,7 @@ module Instance : sig val equal : t -> t -> bool val subst_fn : universe_level_subst_fn -> t -> t val subst : universe_level_subst -> t -> t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t val check_eq : t check_function val length : t -> int val append : t -> t -> t diff --git a/checker/univ.mli b/checker/univ.mli index 7f5aa7626..0a21019b1 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -20,7 +20,7 @@ sig val var : int -> t - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t (** Pretty-printing *) val equal : t -> t -> bool @@ -53,7 +53,7 @@ type universe = Universe.t (** Alias name. *) -val pr_uni : universe -> Pp.std_ppcmds +val pr_uni : universe -> Pp.t (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *) @@ -172,7 +172,7 @@ sig val subst : universe_level_subst -> t -> t (** Substitution by a level-to-level function. *) - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t (** Pretty-printing, no comments *) val check_eq : t check_function @@ -274,8 +274,8 @@ val check_subtype : universes -> AUContext.t -> AUContext.t -> bool (** {6 Pretty-printing of universes. } *) -val pr_constraint_type : constraint_type -> Pp.std_ppcmds -val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds -val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds +val pr_constraint_type : constraint_type -> Pp.t +val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t +val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t -val pr_universes : universes -> Pp.std_ppcmds +val pr_universes : universes -> Pp.t diff --git a/dev/ci/ci-hott.sh b/dev/ci/ci-hott.sh index 693135a4c..1bf6e9a87 100755 --- a/dev/ci/ci-hott.sh +++ b/dev/ci/ci-hott.sh @@ -7,4 +7,4 @@ HoTT_CI_DIR=${CI_BUILD_DIR}/HoTT git_checkout ${HoTT_CI_BRANCH} ${HoTT_CI_GITURL} ${HoTT_CI_DIR} -( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make ) +( cd ${HoTT_CI_DIR} && ./autogen.sh && ./configure && make -j ${NJOBS} ) diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 57c7a97d5..a48c491d3 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -18,6 +18,10 @@ We changed the type of the following functions: The returned term contains De Bruijn universe variables. - Global.body_of_constant: same as above. +We renamed the following datatypes: + + Pp.std_ppcmds -> Pp.t + ========================================= = CHANGES BETWEEN COQ V8.6 AND COQ V8.7 = ========================================= diff --git a/dev/doc/debugging.txt b/dev/doc/debugging.txt index 79cde4884..3e2b435b3 100644 --- a/dev/doc/debugging.txt +++ b/dev/doc/debugging.txt @@ -1,7 +1,7 @@ Debugging from Coq toplevel using Caml trace mechanism ====================================================== - 1. Launch bytecode version of Coq (coqtop.byte or coqtop -byte) + 1. Launch bytecode version of Coq (coqtop.byte) 2. Access Ocaml toplevel using vernacular command 'Drop.' 3. Install load paths and pretty printers for terms, idents, ... using Ocaml command '#use "base_include";;' (use '#use "include";;' for diff --git a/doc/refman/AsyncProofs.tex b/doc/refman/AsyncProofs.tex index b93ca2957..1609e4a04 100644 --- a/doc/refman/AsyncProofs.tex +++ b/doc/refman/AsyncProofs.tex @@ -51,6 +51,12 @@ proof does not begin with \texttt{Proof using}, the system records in an auxiliary file, produced along with the \texttt{.vo} file, the list of section variables used. +\subsubsection{Automatic suggestion of proof annotations} + +The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a +\texttt{Qed} command is processed, a correct proof annotation. It is up +to the user to modify the proof script accordingly. + \section{Proof blocks and error resilience} Coq 8.6 introduces a mechanism for error resiliency: in interactive mode Coq @@ -86,13 +92,7 @@ CoqIDE one of the following options: \texttt{-async-proofs-tactic-error-resilience off}, \texttt{-async-proofs-tactic-error-resilience all}, \texttt{-async-proofs-tactic-error-resilience $blocktype_1$,..., $blocktype_n$}. -Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. - -\subsubsection{Automatic suggestion of proof annotations} - -The command \texttt{Set Suggest Proof Using} makes Coq suggest, when a -\texttt{Qed} command is processed, a correct proof annotation. It is up -to the user to modify the proof script accordingly. +Valid proof block types are: ``curly'', ``par'', ``indent'', ``bullet''. \section{Interactive mode} diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex index fa3d61b1c..8cb049d50 100644 --- a/doc/refman/Extraction.tex +++ b/doc/refman/Extraction.tex @@ -21,9 +21,14 @@ be used (abusively) to refer to any of the three. Before using any of the commands or options described in this chapter, the extraction framework should first be loaded explicitly -via {\tt Require Extraction}. Note that in earlier versions of Coq, these -commands and options were directly available without any preliminary -{\tt Require}. +via {\tt Require Extraction}, or via the more robust +{\tt From Coq Require Extraction}. +Note that in earlier versions of Coq, these commands and options were +directly available without any preliminary {\tt Require}. + +\begin{coq_example} +Require Extraction. +\end{coq_example} \asection{Generating ML code} \comindex{Extraction} @@ -82,9 +87,20 @@ one monolithic file or one file per \Coq\ library. using prefixes \verb!coq_! or \verb!Coq_!. \end{description} -\noindent The list of globals \qualid$_i$ does not need to be -exhaustive: it is automatically completed into a complete and minimal -environment. +\noindent The following command is meant to help automatic testing of + the extraction, see for instance the {\tt test-suite} directory + in the \Coq\ sources. + +\begin{description} +\item {\tt Extraction TestCompile} \qualid$_1$ \dots\ \qualid$_n$. ~\par + All the globals (or modules) \qualid$_1$ \dots\ \qualid$_n$ and all + their dependencies are extracted to a temporary Ocaml file, just as in + {\tt Extraction "{\em file}"}. Then this temporary file and its + signature are compiled with the same Ocaml compiler used to built + \Coq. This command succeeds only if the extraction and the Ocaml + compilation succeed (and it fails if the current target language + of the extraction is not Ocaml). +\end{description} \asection{Extraction options} diff --git a/doc/refman/RefMan-int.tex b/doc/refman/RefMan-int.tex index fbeccb664..eca3efcdd 100644 --- a/doc/refman/RefMan-int.tex +++ b/doc/refman/RefMan-int.tex @@ -100,6 +100,11 @@ corresponds to the Chapter~\ref{Addoc-syntax}. presented. Finally, Chapter~\ref{Addoc-coqide} describes the \Coq{} integrated development environment. + +\item The fifth part documents a number of advanced features, including + coercions, canonical structures, typeclasses, program extraction, and + specialized solvers and tactics. See the table of contents for a complete + list. \end{itemize} At the end of the document, after the global index, the user can find @@ -120,15 +125,6 @@ documents: user can read also the tutorial on recursive types (document {\tt RecTutorial.ps}). -\item[Addendum] The fifth part (the Addendum) of the Reference Manual - is distributed as a separate document. It contains more - detailed documentation and examples about some specific aspects of the - system that may interest only certain users. It shares the indexes, - the page numbers and - the bibliography with the Reference Manual. If you see in one of the - indexes a page number that is outside the Reference Manual, it refers - to the Addendum. - \item[Installation] A text file INSTALL that comes with the sources explains how to install \Coq{}. diff --git a/doc/refman/RefMan-oth.tex b/doc/refman/RefMan-oth.tex index 3daaac88b..bf48057cd 100644 --- a/doc/refman/RefMan-oth.tex +++ b/doc/refman/RefMan-oth.tex @@ -656,7 +656,7 @@ dynamically. searched into the current {\ocaml} loadpath (see the command {\tt Add ML Path} in the Section~\ref{loadpath}). Loading of {\ocaml} files is only possible under the bytecode version of {\tt coqtop} -(i.e. {\tt coqtop} called with options {\tt -byte}, see chapter +(i.e. {\tt coqtop.byte}, see chapter \ref{Addoc-coqc}), or when {\Coq} has been compiled with a version of {\ocaml} that supports native {\tt Dynlink} ($\ge$ 3.11). @@ -739,7 +739,7 @@ the command {\tt Declare ML Module} in the Section~\ref{compiled}). \subsection[\tt Print ML Path {\str}.]{\tt Print ML Path {\str}.\comindex{Print ML Path}} This command displays the current {\ocaml} loadpath. This command makes sense only under the bytecode version of {\tt -coqtop}, i.e. using option {\tt -byte} (see the +coqtop}, i.e. {\tt coqtop.byte} (see the command {\tt Declare ML Module} in the section \ref{compiled}). diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index a23c43232..b13ae9b7b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4113,7 +4113,7 @@ is to set the cut expression to $c | e$, the initial cut expression being \texttt{emp}. -\item \texttt{Mode} {\tt (+ | ! | -)}$^*$ {\qualid} +\item \texttt{Mode} {\qualid} {\tt (+ | ! | -)}$^*$ \label{HintMode} \comindex{Hint Mode} diff --git a/engine/geninterp.ml b/engine/geninterp.ml index 9964433a8..e79e258fb 100644 --- a/engine/geninterp.ml +++ b/engine/geninterp.ml @@ -32,7 +32,7 @@ struct let repr = ValT.repr let create = ValT.create - let pr : type a. a typ -> Pp.std_ppcmds = fun t -> Pp.str (repr t) + let pr : type a. a typ -> Pp.t = fun t -> Pp.str (repr t) let typ_list = ValT.create "list" let typ_opt = ValT.create "option" diff --git a/engine/geninterp.mli b/engine/geninterp.mli index 9a925dcd8..492e372ad 100644 --- a/engine/geninterp.mli +++ b/engine/geninterp.mli @@ -30,7 +30,7 @@ sig val eq : 'a typ -> 'b typ -> ('a, 'b) CSig.eq option val repr : 'a typ -> string - val pr : 'a typ -> Pp.std_ppcmds + val pr : 'a typ -> Pp.t val typ_list : t list typ val typ_opt : t option typ diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli index aaebe4c1b..8c8f9fe93 100644 --- a/engine/logic_monad.mli +++ b/engine/logic_monad.mli @@ -57,11 +57,11 @@ module NonLogical : sig val print_char : char -> unit t (** Loggers. The buffer is also flushed. *) - val print_debug : Pp.std_ppcmds -> unit t - val print_warning : Pp.std_ppcmds -> unit t - val print_notice : Pp.std_ppcmds -> unit t - val print_info : Pp.std_ppcmds -> unit t - val print_error : Pp.std_ppcmds -> unit t + val print_debug : Pp.t -> unit t + val print_warning : Pp.t -> unit t + val print_notice : Pp.t -> unit t + val print_info : Pp.t -> unit t + val print_error : Pp.t -> unit t (** [Pervasives.raise]. Except that exceptions are wrapped with {!Exception}. *) diff --git a/engine/proofview.ml b/engine/proofview.ml index b4e2160f4..eef2b83f4 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -332,7 +332,7 @@ exception NoSuchGoals of int (* This hook returns a string to be appended to the usual message. Primarily used to add a suggestion about the right bullet to use to focus the next goal, if applicable. *) -let nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ()) +let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ()) let set_nosuchgoals_hook f = nosuchgoals_hook := f diff --git a/engine/proofview.mli b/engine/proofview.mli index 957c9213c..d92d0a7d5 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -235,7 +235,7 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic This hook is used to add a suggestion about bullets when applicable. *) exception NoSuchGoals of int -val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit +val set_nosuchgoals_hook: (int -> Pp.t) -> unit val tclFOCUS : int -> int -> 'a tactic -> 'a tactic @@ -526,7 +526,7 @@ module Trace : sig val log : Proofview_monad.lazy_msg -> unit tactic val name_tactic : Proofview_monad.lazy_msg -> 'a tactic -> 'a tactic - val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.std_ppcmds + val pr_info : ?lvl:int -> Proofview_monad.Info.tree -> Pp.t end diff --git a/engine/proofview_monad.ml b/engine/proofview_monad.ml index 1b737b6f4..d0f471225 100644 --- a/engine/proofview_monad.ml +++ b/engine/proofview_monad.ml @@ -62,7 +62,7 @@ end (** We typically label nodes of [Trace.tree] with messages to print. But we don't want to compute the result. *) -type lazy_msg = unit -> Pp.std_ppcmds +type lazy_msg = unit -> Pp.t let pr_lazy_msg msg = msg () (** Info trace. *) diff --git a/engine/proofview_monad.mli b/engine/proofview_monad.mli index 554583421..e7123218b 100644 --- a/engine/proofview_monad.mli +++ b/engine/proofview_monad.mli @@ -43,7 +43,7 @@ end (** We typically label nodes of [Trace.tree] with messages to print. But we don't want to compute the result. *) -type lazy_msg = unit -> Pp.std_ppcmds +type lazy_msg = unit -> Pp.t (** Info trace. *) module Info : sig @@ -58,7 +58,7 @@ module Info : sig type state = tag Trace.incr type tree = tag Trace.forest - val print : tree -> Pp.std_ppcmds + val print : tree -> Pp.t (** [collapse n t] flattens the first [n] levels of [Tactic] in an info trace, effectively forgetting about the [n] top level of diff --git a/engine/termops.ml b/engine/termops.ml index cf7c0cc20..2bd0c06d6 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -994,12 +994,14 @@ let rec strip_outer_cast sigma c = match EConstr.kind sigma c with (* flattens application lists throwing casts in-between *) let collapse_appl sigma c = match EConstr.kind sigma c with | App (f,cl) -> + if EConstr.isCast sigma f then let rec collapse_rec f cl2 = match EConstr.kind sigma (strip_outer_cast sigma f) with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | _ -> EConstr.mkApp (f,cl2) in collapse_rec f cl + else c | _ -> c (* First utilities for avoiding telescope computation for subst_term *) diff --git a/engine/termops.mli b/engine/termops.mli index c19a2d15a..2624afd30 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -9,16 +9,15 @@ (** This file defines various utilities for term manipulation that are not needed in the kernel. *) -open Pp open Names open Term open Environ open EConstr (** printers *) -val print_sort : sorts -> std_ppcmds -val pr_sort_family : sorts_family -> std_ppcmds -val pr_fix : ('a -> std_ppcmds) -> ('a, 'a) pfixpoint -> std_ppcmds +val print_sort : sorts -> Pp.t +val pr_sort_family : sorts_family -> Pp.t +val pr_fix : ('a -> Pp.t) -> ('a, 'a) pfixpoint -> Pp.t (** about contexts *) val push_rel_assum : Name.t * types -> env -> env @@ -279,25 +278,25 @@ val on_judgment_type : ('t -> 't) -> ('c, 't) punsafe_judgment -> ('c, 't) puns open Evd -val pr_existential_key : evar_map -> evar -> Pp.std_ppcmds +val pr_existential_key : evar_map -> evar -> Pp.t val pr_evar_suggested_name : existential_key -> evar_map -> Id.t -val pr_evar_info : evar_info -> Pp.std_ppcmds -val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.std_ppcmds -val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.std_ppcmds +val pr_evar_info : evar_info -> Pp.t +val pr_evar_constraints : evar_map -> evar_constraint list -> Pp.t +val pr_evar_map : ?with_univs:bool -> int option -> evar_map -> Pp.t val pr_evar_map_filter : ?with_univs:bool -> (Evar.t -> evar_info -> bool) -> - evar_map -> Pp.std_ppcmds -val pr_metaset : Metaset.t -> Pp.std_ppcmds -val pr_evar_universe_context : evar_universe_context -> Pp.std_ppcmds -val pr_evd_level : evar_map -> Univ.Level.t -> Pp.std_ppcmds + evar_map -> Pp.t +val pr_metaset : Metaset.t -> Pp.t +val pr_evar_universe_context : evar_universe_context -> Pp.t +val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t (** debug printer: do not use to display terms to the casual user... *) -val set_print_constr : (env -> Evd.evar_map -> constr -> std_ppcmds) -> unit -val print_constr : constr -> std_ppcmds -val print_constr_env : env -> Evd.evar_map -> constr -> std_ppcmds -val print_named_context : env -> std_ppcmds -val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds -val print_rel_context : env -> std_ppcmds -val print_env : env -> std_ppcmds +val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit +val print_constr : constr -> Pp.t +val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t +val print_named_context : env -> Pp.t +val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t +val print_rel_context : env -> Pp.t +val print_env : env -> Pp.t diff --git a/engine/uState.mli b/engine/uState.mli index 3776e4c9f..d198fbfbe 100644 --- a/engine/uState.mli +++ b/engine/uState.mli @@ -123,4 +123,4 @@ val update_sigma_env : t -> Environ.env -> t (** {5 Pretty-printing} *) -val pr_uctx_level : t -> Univ.Level.t -> Pp.std_ppcmds +val pr_uctx_level : t -> Univ.Level.t -> Pp.t diff --git a/engine/universes.mli b/engine/universes.mli index 0f6e419d0..fe40f8238 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -17,7 +17,7 @@ val is_set_minimization : unit -> bool (** Universes *) -val pr_with_global_universes : Level.t -> Pp.std_ppcmds +val pr_with_global_universes : Level.t -> Pp.t (** Local universe name <-> level mapping *) @@ -52,7 +52,7 @@ type universe_constraint = universe * universe_constraint_type * universe module Constraints : sig include Set.S with type elt = universe_constraint - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end type universe_constraints = Constraints.t @@ -203,7 +203,7 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s (** Pretty-printing *) -val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds +val pr_universe_opt_subst : universe_opt_subst -> Pp.t (** {6 Support for template polymorphism } *) diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp index 643b6277a..12b7b171b 100644 --- a/grammar/argextend.mlp +++ b/grammar/argextend.mlp @@ -137,7 +137,8 @@ let declare_tactic_argument loc s (typ, f, g, h) cl = let typ = match globtyp with None -> ExtraArgType s | Some typ -> typ in <:expr< let f = $lid:f$ in - fun ist v -> Ftactic.nf_enter (fun gl -> + fun ist v -> Ftactic.enter (fun gl -> + let gl = Proofview.Goal.assume gl in let (sigma, v) = Tacmach.New.of_old (fun gl -> f ist gl v) gl in let v = Geninterp.Val.inject (Geninterp.val_tag $make_topwit loc typ$) v in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Ftactic.return v) diff --git a/grammar/compat5.ml b/grammar/compat5.ml deleted file mode 100644 index 370d9e3a0..000000000 --- a/grammar/compat5.ml +++ /dev/null @@ -1,13 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -(* This file is meant for camlp5, for which there is nothing to - add to gain camlp5 compatibility :-). - - See [compat5.mlp] for the [camlp4] counterpart -*) diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 3eb5b0753..364fc883b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -58,7 +58,7 @@ module SentenceId : sig val connect : sentence -> signals val dbg_to_string : - GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.std_ppcmds + GText.buffer -> bool -> Stateid.t option -> sentence -> Pp.t end = struct @@ -163,7 +163,7 @@ let flags_to_color f = else `NAME Preferences.processed_color#get (* Move to utils? *) -let rec validate (s : Pp.std_ppcmds) = match Pp.repr s with +let rec validate (s : Pp.t) = match Pp.repr s with | Pp.Ppcmd_empty | Pp.Ppcmd_print_break _ | Pp.Ppcmd_force_newline -> true diff --git a/ide/document.mli b/ide/document.mli index fb96cb6d7..ab8e71808 100644 --- a/ide/document.mli +++ b/ide/document.mli @@ -102,7 +102,7 @@ val context : 'a document -> (id * 'a) list * (id * 'a) list (** debug print *) val print : - 'a document -> (bool -> id option -> 'a -> Pp.std_ppcmds) -> Pp.std_ppcmds + 'a document -> (bool -> id option -> 'a -> Pp.t) -> Pp.t (** Callbacks on documents *) diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml index cb2b365a4..67391f556 100644 --- a/ide/ide_slave.ml +++ b/ide/ide_slave.ml @@ -177,11 +177,9 @@ let process_goal sigma g = let min_env = Environ.reset_context env in let id = Goal.uid g in let ccl = - let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in - pr_goal_concl_style_env env sigma norm_constr + pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in let process_hyp d (env,l) = - let d = CompactedDecl.map_constr (fun c -> EConstr.Unsafe.to_constr (Reductionops.nf_evar sigma (EConstr.of_constr c))) d in let d' = CompactedDecl.to_named_context d in (List.fold_right Environ.push_named d' env, (pr_compacted_decl env sigma d) :: l) in @@ -210,7 +208,7 @@ let evars () = Stm.finish (); let pfts = Proof_global.give_me_the_proof () in let { Evd.it = all_goals ; sigma = sigma } = Proof.V82.subgoals pfts in - let exl = Evar.Map.bindings (Evarutil.non_instantiated sigma) in + let exl = Evar.Map.bindings (Evd.undefined_map sigma) in let map_evar ev = { Interface.evar_info = string_of_ppcmds (pr_evar sigma ev); } in let el = List.map map_evar exl in Some el diff --git a/ide/ideutils.ml b/ide/ideutils.ml index 2573b6d6f..83e5da950 100644 --- a/ide/ideutils.ml +++ b/ide/ideutils.ml @@ -316,7 +316,7 @@ let textview_width (view : #GText.view_skel) = let char_width = GPango.to_pixels metrics#approx_char_width in pixel_width / char_width -type logger = Feedback.level -> Pp.std_ppcmds -> unit +type logger = Feedback.level -> Pp.t -> unit let default_logger level message = let level = match level with diff --git a/ide/ideutils.mli b/ide/ideutils.mli index 458b8e0a5..f06a48aeb 100644 --- a/ide/ideutils.mli +++ b/ide/ideutils.mli @@ -67,7 +67,7 @@ val requote : string -> string val textview_width : #GText.view_skel -> int (** Returns an approximate value of the character width of a textview *) -type logger = Feedback.level -> Pp.std_ppcmds -> unit +type logger = Feedback.level -> Pp.t -> unit val default_logger : logger (** Default logger. It logs messages that the casual user should not see. *) diff --git a/ide/interface.mli b/ide/interface.mli index aab1d8272..1939a8427 100644 --- a/ide/interface.mli +++ b/ide/interface.mli @@ -17,9 +17,9 @@ type verbose = bool type goal = { goal_id : string; (** Unique goal identifier *) - goal_hyp : Pp.std_ppcmds list; + goal_hyp : Pp.t list; (** List of hypotheses *) - goal_ccl : Pp.std_ppcmds; + goal_ccl : Pp.t; (** Goal conclusion *) } @@ -121,7 +121,7 @@ type edit_id = int should probably retract to that point *) type 'a value = | Good of 'a - | Fail of (state_id * location * Pp.std_ppcmds) + | Fail of (state_id * location * Pp.t) type ('a, 'b) union = ('a, 'b) Util.union @@ -213,7 +213,7 @@ type about_sty = unit type about_rty = coq_info type handle_exn_sty = Exninfo.iexn -type handle_exn_rty = state_id * location * Pp.std_ppcmds +type handle_exn_rty = state_id * location * Pp.t (* Retrocompatibility stuff *) type interp_sty = (raw * verbose) * string diff --git a/ide/minilib.mli b/ide/minilib.mli index 4517a2374..c96e59b22 100644 --- a/ide/minilib.mli +++ b/ide/minilib.mli @@ -22,7 +22,7 @@ type level = [ (** debug printing *) val debug : bool ref -val log_pp : ?level:level -> Pp.std_ppcmds -> unit +val log_pp : ?level:level -> Pp.t -> unit val log : ?level:level -> string -> unit val coqide_config_home : unit -> string diff --git a/ide/richpp.mli b/ide/richpp.mli index f2ba15d22..84adc61ca 100644 --- a/ide/richpp.mli +++ b/ide/richpp.mli @@ -24,7 +24,7 @@ type 'annotation located = { that represents (located) annotations of this string. The [get_annotations] function is used to convert tags into the desired annotation. [width] sets the printing witdh of the formatter. *) -val rich_pp : int -> Pp.std_ppcmds -> Pp.pp_tag located Xml_datatype.gxml +val rich_pp : int -> Pp.t -> Pp.pp_tag located Xml_datatype.gxml (** [annotations_positions ssdoc] returns a list associating each annotations with its position in the string from which [ssdoc] is @@ -47,5 +47,5 @@ type richpp = Xml_datatype.xml (** Type of text with style annotations *) -val richpp_of_pp : int -> Pp.std_ppcmds -> richpp +val richpp_of_pp : int -> Pp.t -> richpp (** Extract style information from formatted text *) diff --git a/ide/wg_MessageView.ml b/ide/wg_MessageView.ml index d2a09dd94..65df2b849 100644 --- a/ide/wg_MessageView.ml +++ b/ide/wg_MessageView.ml @@ -28,9 +28,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Pp.std_ppcmds -> unit + method add : Pp.t -> unit method add_string : string -> unit - method set : Pp.std_ppcmds -> unit + method set : Pp.t -> unit method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) diff --git a/ide/wg_MessageView.mli b/ide/wg_MessageView.mli index 0ce257c3d..6bd0625f0 100644 --- a/ide/wg_MessageView.mli +++ b/ide/wg_MessageView.mli @@ -18,9 +18,9 @@ class type message_view = inherit GObj.widget method connect : message_view_signals method clear : unit - method add : Pp.std_ppcmds -> unit + method add : Pp.t -> unit method add_string : string -> unit - method set : Pp.std_ppcmds -> unit + method set : Pp.t -> unit method refresh : bool -> unit method push : Ideutils.logger (** same as [add], but with an explicit level instead of [Notice] *) diff --git a/ide/xmlprotocol.ml b/ide/xmlprotocol.ml index 06c695c77..4b521a968 100644 --- a/ide/xmlprotocol.ml +++ b/ide/xmlprotocol.ml @@ -117,7 +117,7 @@ let to_box = let open Pp in | x -> raise (Marshal_error("*ppbox",PCData x)) ) -let rec of_pp (pp : Pp.std_ppcmds) = let open Pp in match Pp.repr pp with +let rec of_pp (pp : Pp.t) = let open Pp in match Pp.repr pp with | Ppcmd_empty -> constructor "ppdoc" "empty" [] | Ppcmd_string s -> constructor "ppdoc" "string" [of_string s] | Ppcmd_glue sl -> constructor "ppdoc" "glue" [of_list of_pp sl] @@ -149,7 +149,7 @@ let rec to_pp xpp = let open Pp in let of_richpp x = Element ("richpp", [], [x]) (* Run-time Selectable *) -let of_pp (pp : Pp.std_ppcmds) = +let of_pp (pp : Pp.t) = match !msg_format with | Richpp margin -> of_richpp (Richpp.richpp_of_pp margin pp) | Ppcmds -> of_pp pp diff --git a/interp/notation.mli b/interp/notation.mli index dd0144e8d..e63ad10cd 100644 --- a/interp/notation.mli +++ b/interp/notation.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Bigint open Names open Libnames @@ -189,13 +188,13 @@ val make_notation_key : symbol list -> notation val decompose_notation_key : notation -> symbol list (** Prints scopes (expects a pure aconstr printer) *) -val pr_scope_class : scope_class -> std_ppcmds -val pr_scope : (glob_constr -> std_ppcmds) -> scope_name -> std_ppcmds -val pr_scopes : (glob_constr -> std_ppcmds) -> std_ppcmds -val locate_notation : (glob_constr -> std_ppcmds) -> notation -> - scope_name option -> std_ppcmds +val pr_scope_class : scope_class -> Pp.t +val pr_scope : (glob_constr -> Pp.t) -> scope_name -> Pp.t +val pr_scopes : (glob_constr -> Pp.t) -> Pp.t +val locate_notation : (glob_constr -> Pp.t) -> notation -> + scope_name option -> Pp.t -val pr_visibility: (glob_constr -> std_ppcmds) -> scope_name option -> std_ppcmds +val pr_visibility: (glob_constr -> Pp.t) -> scope_name option -> Pp.t (** {6 Printing rules for notations} *) diff --git a/interp/ppextend.mli b/interp/ppextend.mli index 4874989cd..a347a5c7b 100644 --- a/interp/ppextend.mli +++ b/interp/ppextend.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp - (** {6 Pretty-print. } *) (** Dealing with precedences *) @@ -28,9 +26,9 @@ type ppcut = | PpBrk of int * int | PpFnl -val ppcmd_of_box : ppbox -> std_ppcmds -> std_ppcmds +val ppcmd_of_box : ppbox -> Pp.t -> Pp.t -val ppcmd_of_cut : ppcut -> std_ppcmds +val ppcmd_of_cut : ppcut -> Pp.t type unparsing = | UnpMetaVar of int * parenRelation diff --git a/intf/notation_term.ml b/intf/notation_term.ml index 0fa0afdad..cee96040b 100644 --- a/intf/notation_term.ml +++ b/intf/notation_term.ml @@ -83,9 +83,10 @@ type notation_interp_env = { type grammar_constr_prod_item = | GramConstrTerminal of Tok.t | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option - | GramConstrListMark of int * bool + | GramConstrListMark of int * bool * int (* tells action rule to make a list of the n previous parsed items; - concat with last parsed list if true *) + concat with last parsed list when true; additionally release + the p last items as if they were parsed autonomously *) type notation_grammar = { notgram_level : int; diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 8f38e9d34..718917ab3 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -34,7 +34,7 @@ type structured_constant = | Const_univ_level of Univ.universe_level | Const_type of Univ.universe -val pp_struct_const : structured_constant -> Pp.std_ppcmds +val pp_struct_const : structured_constant -> Pp.t type reloc_table = (tag * int) array @@ -163,8 +163,8 @@ type comp_env = { in_env : vm_env ref (** the variables that are accessed *) } -val pp_bytecodes : bytecodes -> Pp.std_ppcmds -val pp_fv_elem : fv_elem -> Pp.std_ppcmds +val pp_bytecodes : bytecodes -> Pp.t +val pp_fv_elem : fv_elem -> Pp.t (*spiwack: moved this here because I needed it for retroknowledge *) type block = diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 3cd02fb9f..f1d0e4279 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -107,9 +107,9 @@ val subst_substituted : substitution -> 'a substituted -> 'a substituted (**/**) (* debugging *) val debug_string_of_subst : substitution -> string -val debug_pr_subst : substitution -> Pp.std_ppcmds +val debug_pr_subst : substitution -> Pp.t val debug_string_of_delta : delta_resolver -> string -val debug_pr_delta : delta_resolver -> Pp.std_ppcmds +val debug_pr_delta : delta_resolver -> Pp.t (**/**) (** [subst_mp sub mp] guarantees that whenever the result of the diff --git a/kernel/names.mli b/kernel/names.mli index 74d63c0ce..d111dd3c0 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -57,7 +57,7 @@ sig val to_string : t -> string (** Converts a identifier into an string. *) - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t (** Pretty-printer. *) module Set : Set.S with type elt = t @@ -105,7 +105,7 @@ sig val hcons : t -> t (** Hashconsing over names. *) - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t (** Pretty-printer (print "_" for [Anonymous]. *) end @@ -187,7 +187,7 @@ sig val to_id : t -> Id.t (** Conversion to an identifier. *) - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t (** Pretty-printer. *) module Set : Set.S with type elt = t @@ -286,7 +286,7 @@ sig val debug_to_string : t -> string (** Same as [to_string], but outputs information related to debug. *) - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t (** Comparisons *) val compare : t -> t -> int @@ -365,9 +365,9 @@ sig (** Displaying *) val to_string : t -> string - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t val debug_to_string : t -> string - val debug_print : t -> Pp.std_ppcmds + val debug_print : t -> Pp.t end @@ -447,9 +447,9 @@ sig (** Displaying *) val to_string : t -> string - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t val debug_to_string : t -> string - val debug_print : t -> Pp.std_ppcmds + val debug_print : t -> Pp.t end @@ -609,7 +609,7 @@ val mk_label : string -> label val string_of_label : label -> string (** @deprecated Same as [Label.to_string]. *) -val pr_label : label -> Pp.std_ppcmds +val pr_label : label -> Pp.t (** @deprecated Same as [Label.print]. *) val label_of_id : Id.t -> label @@ -695,7 +695,7 @@ val label : kernel_name -> Label.t val string_of_kn : kernel_name -> string (** @deprecated Same as [KerName.to_string]. *) -val pr_kn : kernel_name -> Pp.std_ppcmds +val pr_kn : kernel_name -> Pp.t (** @deprecated Same as [KerName.print]. *) val kn_ord : kernel_name -> kernel_name -> int @@ -731,7 +731,7 @@ module Projection : sig val map : (constant -> constant) -> t -> t val to_string : t -> string - val print : t -> Pp.std_ppcmds + val print : t -> Pp.t end @@ -776,10 +776,10 @@ val con_with_label : constant -> Label.t -> constant val string_of_con : constant -> string (** @deprecated Same as [Constant.to_string] *) -val pr_con : constant -> Pp.std_ppcmds +val pr_con : constant -> Pp.t (** @deprecated Same as [Constant.print] *) -val debug_pr_con : constant -> Pp.std_ppcmds +val debug_pr_con : constant -> Pp.t (** @deprecated Same as [Constant.debug_print] *) val debug_string_of_con : constant -> string @@ -826,10 +826,10 @@ val mind_modpath : mutual_inductive -> ModPath.t val string_of_mind : mutual_inductive -> string (** @deprecated Same as [MutInd.to_string] *) -val pr_mind : mutual_inductive -> Pp.std_ppcmds +val pr_mind : mutual_inductive -> Pp.t (** @deprecated Same as [MutInd.print] *) -val debug_pr_mind : mutual_inductive -> Pp.std_ppcmds +val debug_pr_mind : mutual_inductive -> Pp.t (** @deprecated Same as [MutInd.debug_print] *) val debug_string_of_mind : mutual_inductive -> string diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 4de373eb4..2fe555018 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -59,7 +59,7 @@ val check_subtype : AUContext.t check_function (** {6 Pretty-printing of universes. } *) -val pr_universes : (Level.t -> Pp.std_ppcmds) -> universes -> Pp.std_ppcmds +val pr_universes : (Level.t -> Pp.t) -> universes -> Pp.t (** {6 Dumping to a file } *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 02b02db89..d915fb8c9 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -892,7 +892,7 @@ module Instance : sig val subst_fn : universe_level_subst_fn -> t -> t - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t val levels : t -> LSet.t end = struct diff --git a/kernel/univ.mli b/kernel/univ.mli index 99092a543..a4f2e26b6 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -37,7 +37,7 @@ sig (** Create a new universe level from a unique identifier and an associated module path. *) - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t (** Pretty-printing *) val to_string : t -> string @@ -56,7 +56,7 @@ module LSet : sig include CSig.SetS with type elt = universe_level - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t (** Pretty-printing *) end @@ -86,10 +86,10 @@ sig val make : Level.t -> t (** Create a universe representing the given level. *) - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t (** Pretty-printing *) - val pr_with : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr_with : (Level.t -> Pp.t) -> t -> Pp.t val is_level : t -> bool (** Test if the universe is a level or an algebraic universe. *) @@ -127,7 +127,7 @@ type universe = Universe.t (** Alias name. *) -val pr_uni : universe -> Pp.std_ppcmds +val pr_uni : universe -> Pp.t (** The universes hierarchy: Type 0- = Prop <= Type 0 = Set <= Type 1 <= ... Typing of universes: Type 0-, Type 0 : Type 1; Type i : Type (i+1) if i>0 *) @@ -218,7 +218,7 @@ sig (** [subst_union x y] favors the bindings of the first map that are [Some], otherwise takes y's bindings. *) - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t (** Pretty-printing *) end @@ -270,7 +270,7 @@ sig val subst_fn : universe_level_subst_fn -> t -> t (** Substitution by a level-to-level function. *) - val pr : (Level.t -> Pp.std_ppcmds) -> t -> Pp.std_ppcmds + val pr : (Level.t -> Pp.t) -> t -> Pp.t (** Pretty-printing, no comments *) val levels : t -> LSet.t @@ -463,18 +463,18 @@ val make_abstract_instance : abstract_universe_context -> universe_instance (** {6 Pretty-printing of universes. } *) -val pr_constraint_type : constraint_type -> Pp.std_ppcmds -val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds -val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds -val pr_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> cumulativity_info -> Pp.std_ppcmds -val pr_abstract_universe_context : (Level.t -> Pp.std_ppcmds) -> abstract_universe_context -> Pp.std_ppcmds -val pr_abstract_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> abstract_cumulativity_info -> Pp.std_ppcmds -val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds -val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) -> - univ_inconsistency -> Pp.std_ppcmds - -val pr_universe_level_subst : universe_level_subst -> Pp.std_ppcmds -val pr_universe_subst : universe_subst -> Pp.std_ppcmds +val pr_constraint_type : constraint_type -> Pp.t +val pr_constraints : (Level.t -> Pp.t) -> constraints -> Pp.t +val pr_universe_context : (Level.t -> Pp.t) -> universe_context -> Pp.t +val pr_cumulativity_info : (Level.t -> Pp.t) -> cumulativity_info -> Pp.t +val pr_abstract_universe_context : (Level.t -> Pp.t) -> abstract_universe_context -> Pp.t +val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> abstract_cumulativity_info -> Pp.t +val pr_universe_context_set : (Level.t -> Pp.t) -> universe_context_set -> Pp.t +val explain_universe_inconsistency : (Level.t -> Pp.t) -> + univ_inconsistency -> Pp.t + +val pr_universe_level_subst : universe_level_subst -> Pp.t +val pr_universe_subst : universe_subst -> Pp.t (** {6 Hash-consing } *) diff --git a/kernel/vm.mli b/kernel/vm.mli index 6e9579aa4..df638acc1 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -50,9 +50,9 @@ type whd = (** For debugging purposes only *) -val pr_atom : atom -> Pp.std_ppcmds -val pr_whd : whd -> Pp.std_ppcmds -val pr_stack : stack -> Pp.std_ppcmds +val pr_atom : atom -> Pp.t +val pr_whd : whd -> Pp.t +val pr_stack : stack -> Pp.t (** Constructors *) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 8ef11a2cd..3f4e8aa12 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -14,7 +14,7 @@ let push = Backtrace.add_backtrace (* Errors *) -exception Anomaly of string option * std_ppcmds (* System errors *) +exception Anomaly of string option * Pp.t (* System errors *) let _ = let pr = function @@ -33,7 +33,7 @@ let is_anomaly = function | Anomaly _ -> true | _ -> false -exception UserError of string option * std_ppcmds (* User errors *) +exception UserError of string option * Pp.t (* User errors *) let todo s = prerr_string ("TODO: "^s^"\n") @@ -41,7 +41,7 @@ let user_err ?loc ?hdr strm = Loc.raise ?loc (UserError (hdr, strm)) let invalid_arg ?loc s = Loc.raise ?loc (Invalid_argument s) -exception AlreadyDeclared of std_ppcmds (* for already declared Schemes *) +exception AlreadyDeclared of Pp.t (* for already declared Schemes *) let alreadydeclared pps = raise (AlreadyDeclared(pps)) exception Timeout diff --git a/lib/cErrors.mli b/lib/cErrors.mli index ca0838575..f3253979f 100644 --- a/lib/cErrors.mli +++ b/lib/cErrors.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (***********************************************************************) -open Pp - (** This modules implements basic manipulations of errors for use throughout Coq's code. *) @@ -21,10 +19,10 @@ val push : exn -> Exninfo.iexn [Anomaly] is used for system errors and [UserError] for the user's ones. *) -val make_anomaly : ?label:string -> std_ppcmds -> exn +val make_anomaly : ?label:string -> Pp.t -> exn (** Create an anomaly. *) -val anomaly : ?loc:Loc.t -> ?label:string -> std_ppcmds -> 'a +val anomaly : ?loc:Loc.t -> ?label:string -> Pp.t -> 'a (** Raise an anomaly, with an optional location and an optional label identifying the anomaly. *) @@ -33,16 +31,16 @@ val is_anomaly : exn -> bool This is mostly provided for compatibility. Please avoid doing specific tricks with anomalies thanks to it. See rather [noncritical] below. *) -exception UserError of string option * std_ppcmds +exception UserError of string option * Pp.t (** Main error signaling exception. It carries a header plus a pretty printing doc *) -val user_err : ?loc:Loc.t -> ?hdr:string -> std_ppcmds -> 'a +val user_err : ?loc:Loc.t -> ?hdr:string -> Pp.t -> 'a (** Main error raising primitive. [user_err ?loc ?hdr pp] signals an error [pp] with optional header and location [hdr] [loc] *) -exception AlreadyDeclared of std_ppcmds -val alreadydeclared : std_ppcmds -> 'a +exception AlreadyDeclared of Pp.t +val alreadydeclared : Pp.t -> 'a val invalid_arg : ?loc:Loc.t -> string -> 'a @@ -74,16 +72,16 @@ exception Quit exception Unhandled -val register_handler : (exn -> Pp.std_ppcmds) -> unit +val register_handler : (exn -> Pp.t) -> unit (** The standard exception printer *) -val print : ?info:Exninfo.info -> exn -> Pp.std_ppcmds -val iprint : Exninfo.iexn -> Pp.std_ppcmds +val print : ?info:Exninfo.info -> exn -> Pp.t +val iprint : Exninfo.iexn -> Pp.t (** Same as [print], except that the "Please report" part of an anomaly isn't printed (used in Ltac debugging). *) -val print_no_report : exn -> Pp.std_ppcmds -val iprint_no_report : Exninfo.iexn -> Pp.std_ppcmds +val print_no_report : exn -> Pp.t +val iprint_no_report : Exninfo.iexn -> Pp.t (** Critical exceptions should not be caught and ignored by mistake by inner functions during a [vernacinterp]. They should be handled @@ -100,9 +98,9 @@ val handled : exn -> bool val error : string -> 'a [@@ocaml.deprecated "use [user_err] instead"] -val errorlabstrm : string -> std_ppcmds -> 'a +val errorlabstrm : string -> Pp.t -> 'a [@@ocaml.deprecated "use [user_err ~hdr] instead"] -val user_err_loc : Loc.t * string * std_ppcmds -> 'a +val user_err_loc : Loc.t * string * Pp.t -> 'a [@@ocaml.deprecated "use [user_err ~loc] instead"] diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index 0622d7593..ba152a19b 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -11,7 +11,7 @@ type status = Disabled | Enabled | AsError val set_current_loc : Loc.t option -> unit val create : name:string -> category:string -> ?default:status -> - ('a -> Pp.std_ppcmds) -> ?loc:Loc.t -> 'a -> unit + ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit val get_flags : unit -> string val set_flags : string -> unit diff --git a/lib/explore.ml b/lib/explore.ml index 1919af51e..7da077e96 100644 --- a/lib/explore.ml +++ b/lib/explore.ml @@ -14,7 +14,7 @@ module type SearchProblem = sig type state val branching : state -> state list val success : state -> bool - val pp : state -> std_ppcmds + val pp : state -> Pp.t end module Make = functor(S : SearchProblem) -> struct diff --git a/lib/explore.mli b/lib/explore.mli index 3c31d0766..5875246ff 100644 --- a/lib/explore.mli +++ b/lib/explore.mli @@ -27,7 +27,7 @@ module type SearchProblem = sig val success : state -> bool - val pp : state -> Pp.std_ppcmds + val pp : state -> Pp.t end diff --git a/lib/feedback.ml b/lib/feedback.ml index ed1d495d7..54d16a9be 100644 --- a/lib/feedback.ml +++ b/lib/feedback.ml @@ -32,7 +32,7 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t option * string * xml (* Generic messages *) - | Message of level * Loc.t option * Pp.std_ppcmds + | Message of level * Loc.t option * Pp.t type feedback = { id : Stateid.t; diff --git a/lib/feedback.mli b/lib/feedback.mli index bd3316abb..45a02d384 100644 --- a/lib/feedback.mli +++ b/lib/feedback.mli @@ -40,7 +40,7 @@ type feedback_content = (* Extra metadata *) | Custom of Loc.t option * string * xml (* Generic messages *) - | Message of level * Loc.t option * Pp.std_ppcmds + | Message of level * Loc.t option * Pp.t type feedback = { id : Stateid.t; (* The document part concerned *) @@ -78,20 +78,20 @@ relaxed. *) (* Should we advertise these functions more? Should they be the ONLY allowed way to output something? *) -val msg_info : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_info : ?loc:Loc.t -> Pp.t -> unit (** Message that displays information, usually in verbose mode, such as [Foobar is defined] *) -val msg_notice : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_notice : ?loc:Loc.t -> Pp.t -> unit (** Message that should be displayed, such as [Print Foo] or [Show Bar]. *) -val msg_warning : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_warning : ?loc:Loc.t -> Pp.t -> unit (** Message indicating that something went wrong, but without serious consequences. *) -val msg_error : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_error : ?loc:Loc.t -> Pp.t -> unit (** Message indicating that something went really wrong, though still recoverable; otherwise an exception would have been raised. *) -val msg_debug : ?loc:Loc.t -> Pp.std_ppcmds -> unit +val msg_debug : ?loc:Loc.t -> Pp.t -> unit (** For debugging purposes *) diff --git a/lib/future.mli b/lib/future.mli index ce9155657..acfce51a0 100644 --- a/lib/future.mli +++ b/lib/future.mli @@ -154,7 +154,7 @@ val purify : ('a -> 'b) -> 'a -> 'b val transactify : ('a -> 'b) -> 'a -> 'b (** Debug: print a computation given an inner printing function. *) -val print : ('a -> Pp.std_ppcmds) -> 'a computation -> Pp.std_ppcmds +val print : ('a -> Pp.t) -> 'a computation -> Pp.t type freeze (* These functions are needed to get rid of side effects. @@ -162,5 +162,5 @@ type freeze deal with the whole system state. *) val set_freeze : (unit -> freeze) -> (freeze -> unit) -> unit -val customize_not_ready_msg : (string -> Pp.std_ppcmds) -> unit -val customize_not_here_msg : (string -> Pp.std_ppcmds) -> unit +val customize_not_ready_msg : (string -> Pp.t) -> unit +val customize_not_here_msg : (string -> Pp.t) -> unit diff --git a/lib/genarg.ml b/lib/genarg.ml index 1174cfe10..b78fe4037 100644 --- a/lib/genarg.ml +++ b/lib/genarg.ml @@ -58,7 +58,7 @@ fun t1 t2 -> match t1, t2 with end | _ -> None -let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> std_ppcmds = function +let rec pr_genarg_type : type a b c. (a, b, c) genarg_type -> Pp.t = function | ListArg t -> pr_genarg_type t ++ spc () ++ str "list" | OptArg t -> pr_genarg_type t ++ spc () ++ str "opt" | PairArg (t1, t2) -> diff --git a/lib/genarg.mli b/lib/genarg.mli index d7f24eac1..7fa71299e 100644 --- a/lib/genarg.mli +++ b/lib/genarg.mli @@ -146,7 +146,7 @@ val abstract_argument_type_eq : ('a, 'l) abstract_argument_type -> ('b, 'l) abstract_argument_type -> ('a, 'b) CSig.eq option -val pr_argument_type : argument_type -> Pp.std_ppcmds +val pr_argument_type : argument_type -> Pp.t (** Print a human-readable representation for a given type. *) val genarg_tag : 'a generic_argument -> argument_type @@ -39,7 +39,9 @@ type doc_view = (* Following discussion on #390, we play on the safe side and make the internal representation opaque here. *) type t = doc_view + type std_ppcmds = t +[@@ocaml.deprecated "alias of Pp.t"] let repr x = x let unrepr x = x diff --git a/lib/pp.mli b/lib/pp.mli index 96656c8b6..2d11cad86 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -10,7 +10,7 @@ (** Pretty printing guidelines ******************************************) (* *) -(* `Pp.t` or `Pp.std_ppcmds` is the main pretty printing document type *) +(* `Pp.t` is the main pretty printing document type *) (* in the Coq system. Documents are composed laying out boxes, and *) (* users can add arbitrary tag metadata that backends are free *) (* to interpret. *) @@ -39,7 +39,9 @@ type pp_tag = string (* Following discussion on #390, we play on the safe side and make the internal representation opaque here. *) type t + type std_ppcmds = t +[@@ocaml.deprecated "alias of Pp.t"] type block_type = | Pp_hbox of int @@ -58,127 +60,127 @@ type doc_view = | Ppcmd_force_newline | Ppcmd_comment of string list -val repr : std_ppcmds -> doc_view -val unrepr : doc_view -> std_ppcmds +val repr : t -> doc_view +val unrepr : doc_view -> t (** {6 Formatting commands} *) -val str : string -> std_ppcmds -val brk : int * int -> std_ppcmds -val fnl : unit -> std_ppcmds -val ws : int -> std_ppcmds -val mt : unit -> std_ppcmds -val ismt : std_ppcmds -> bool +val str : string -> t +val brk : int * int -> t +val fnl : unit -> t +val ws : int -> t +val mt : unit -> t +val ismt : t -> bool -val comment : string list -> std_ppcmds +val comment : string list -> t (** {6 Manipulation commands} *) -val app : std_ppcmds -> std_ppcmds -> std_ppcmds +val app : t -> t -> t (** Concatenation. *) -val seq : std_ppcmds list -> std_ppcmds +val seq : t list -> t (** Multi-Concatenation. *) -val (++) : std_ppcmds -> std_ppcmds -> std_ppcmds +val (++) : t -> t -> t (** Infix alias for [app]. *) (** {6 Derived commands} *) -val spc : unit -> std_ppcmds -val cut : unit -> std_ppcmds -val align : unit -> std_ppcmds -val int : int -> std_ppcmds -val real : float -> std_ppcmds -val bool : bool -> std_ppcmds -val qstring : string -> std_ppcmds -val qs : string -> std_ppcmds -val quote : std_ppcmds -> std_ppcmds -val strbrk : string -> std_ppcmds +val spc : unit -> t +val cut : unit -> t +val align : unit -> t +val int : int -> t +val real : float -> t +val bool : bool -> t +val qstring : string -> t +val qs : string -> t +val quote : t -> t +val strbrk : string -> t (** {6 Boxing commands} *) -val h : int -> std_ppcmds -> std_ppcmds -val v : int -> std_ppcmds -> std_ppcmds -val hv : int -> std_ppcmds -> std_ppcmds -val hov : int -> std_ppcmds -> std_ppcmds +val h : int -> t -> t +val v : int -> t -> t +val hv : int -> t -> t +val hov : int -> t -> t (** {6 Tagging} *) -val tag : pp_tag -> std_ppcmds -> std_ppcmds +val tag : pp_tag -> t -> t (** {6 Printing combinators} *) -val pr_comma : unit -> std_ppcmds +val pr_comma : unit -> t (** Well-spaced comma. *) -val pr_semicolon : unit -> std_ppcmds +val pr_semicolon : unit -> t (** Well-spaced semicolon. *) -val pr_bar : unit -> std_ppcmds +val pr_bar : unit -> t (** Well-spaced pipe bar. *) -val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds +val pr_arg : ('a -> t) -> 'a -> t (** Adds a space in front of its argument. *) -val pr_non_empty_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds +val pr_non_empty_arg : ('a -> t) -> 'a -> t (** Adds a space in front of its argument if non empty. *) -val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_opt : ('a -> t) -> 'a option -> t (** Inner object preceded with a space if [Some], nothing otherwise. *) -val pr_opt_no_spc : ('a -> std_ppcmds) -> 'a option -> std_ppcmds +val pr_opt_no_spc : ('a -> t) -> 'a option -> t (** Same as [pr_opt] but without the leading space. *) -val pr_nth : int -> std_ppcmds +val pr_nth : int -> t (** Ordinal number with the correct suffix (i.e. "st", "nd", "th", etc.). *) -val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val prlist : ('a -> t) -> 'a list -> t (** Concatenation of the list contents, without any separator. Unlike all other functions below, [prlist] works lazily. If a strict behavior is needed, use [prlist_strict] instead. *) -val prlist_strict : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val prlist_strict : ('a -> t) -> 'a list -> t (** Same as [prlist], but strict. *) val prlist_with_sep : - (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a list -> std_ppcmds + (unit -> t) -> ('a -> t) -> 'a list -> t (** [prlist_with_sep sep pr [a ; ... ; c]] outputs [pr a ++ sep () ++ ... ++ sep () ++ pr c]. where the thunk sep is memoized, rather than being called each place its result is used. *) -val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvect : ('a -> t) -> 'a array -> t (** As [prlist], but on arrays. *) -val prvecti : (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds +val prvecti : (int -> 'a -> t) -> 'a array -> t (** Indexed version of [prvect]. *) val prvect_with_sep : - (unit -> std_ppcmds) -> ('a -> std_ppcmds) -> 'a array -> std_ppcmds + (unit -> t) -> ('a -> t) -> 'a array -> t (** As [prlist_with_sep], but on arrays. *) val prvecti_with_sep : - (unit -> std_ppcmds) -> (int -> 'a -> std_ppcmds) -> 'a array -> std_ppcmds + (unit -> t) -> (int -> 'a -> t) -> 'a array -> t (** Indexed version of [prvect_with_sep]. *) -val pr_enum : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pr_enum : ('a -> t) -> 'a list -> t (** [pr_enum pr [a ; b ; ... ; c]] outputs [pr a ++ str "," ++ pr b ++ str "," ++ ... ++ str "and" ++ pr c]. *) -val pr_sequence : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pr_sequence : ('a -> t) -> 'a list -> t (** Sequence of objects separated by space (unless an element is empty). *) -val surround : std_ppcmds -> std_ppcmds +val surround : t -> t (** Surround with parenthesis. *) -val pr_vertical_list : ('b -> std_ppcmds) -> 'b list -> std_ppcmds +val pr_vertical_list : ('b -> t) -> 'b list -> t (** {6 Main renderers, to formatter and to string } *) (** [pp_with fmt pp] Print [pp] to [fmt] and don't flush [fmt] *) -val pp_with : Format.formatter -> std_ppcmds -> unit +val pp_with : Format.formatter -> t -> unit -val string_of_ppcmds : std_ppcmds -> string +val string_of_ppcmds : t -> string diff --git a/lib/rtree.mli b/lib/rtree.mli index a1b06f38e..1a916bbaf 100644 --- a/lib/rtree.mli +++ b/lib/rtree.mli @@ -78,7 +78,7 @@ val map : ('a -> 'b) -> 'a t -> 'b t val smartmap : ('a -> 'a) -> 'a t -> 'a t (** A rather simple minded pretty-printer *) -val pp_tree : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds +val pp_tree : ('a -> Pp.t) -> 'a t -> Pp.t val eq_rtree : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool (** @deprecated Same as [Rtree.equal] *) diff --git a/lib/system.mli b/lib/system.mli index 5f800f191..7281de97c 100644 --- a/lib/system.mli +++ b/lib/system.mli @@ -96,7 +96,7 @@ type time val get_time : unit -> time val time_difference : time -> time -> float (** in seconds *) -val fmt_time_difference : time -> time -> Pp.std_ppcmds +val fmt_time_difference : time -> time -> Pp.t val with_time : bool -> ('a -> 'b) -> 'a -> 'b diff --git a/library/declaremods.mli b/library/declaremods.mli index 1f2aaf7b5..005594b8d 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -121,7 +121,7 @@ val iter_all_segments : (Libnames.object_name -> Libobject.obj -> unit) -> unit -val debug_print_modtab : unit -> Pp.std_ppcmds +val debug_print_modtab : unit -> Pp.t (** For printing modules, [process_module_binding] adds names of bound module (and its components) to Nametab. It also loads diff --git a/library/goptions.ml b/library/goptions.ml index fe014ef68..184c6fa11 100644 --- a/library/goptions.ml +++ b/library/goptions.ml @@ -57,10 +57,10 @@ module MakeTable = val table : (string * key table_of_A) list ref val encode : key -> t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds + val member_message : t -> bool -> Pp.t end) -> struct type option_mark = @@ -131,7 +131,7 @@ module type StringConvertArg = sig val key : option_name val title : string - val member_message : string -> bool -> std_ppcmds + val member_message : string -> bool -> Pp.t end module StringConvert = functor (A : StringConvertArg) -> @@ -161,10 +161,10 @@ sig val compare : t -> t -> int val encode : reference -> t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds + val member_message : t -> bool -> Pp.t end module RefConvert = functor (A : RefConvertArg) -> diff --git a/library/goptions.mli b/library/goptions.mli index 3100c1ce7..cec7250f1 100644 --- a/library/goptions.mli +++ b/library/goptions.mli @@ -43,7 +43,6 @@ All options are synchronized with the document. *) -open Pp open Libnames open Mod_subst @@ -64,7 +63,7 @@ module MakeStringTable : (A : sig val key : option_name val title : string - val member_message : string -> bool -> std_ppcmds + val member_message : string -> bool -> Pp.t end) -> sig val active : string -> bool @@ -88,10 +87,10 @@ module MakeRefTable : val compare : t -> t -> int val encode : reference -> t val subst : substitution -> t -> t - val printer : t -> std_ppcmds + val printer : t -> Pp.t val key : option_name val title : string - val member_message : t -> bool -> std_ppcmds + val member_message : t -> bool -> Pp.t end) -> sig val active : A.t -> bool @@ -177,6 +176,6 @@ type option_state = { } val get_tables : unit -> option_state OptionMap.t -val print_tables : unit -> std_ppcmds +val print_tables : unit -> Pp.t val error_undeclared_key : option_name -> 'a diff --git a/library/keys.mli b/library/keys.mli index 6fe9efc6e..d5dc0e2a1 100644 --- a/library/keys.mli +++ b/library/keys.mli @@ -19,5 +19,5 @@ val equiv_keys : key -> key -> bool val constr_key : ('a -> ('a, 't, 'u, 'i) Constr.kind_of_term) -> 'a -> key option (** Compute the head key of a term. *) -val pr_keys : (global_reference -> Pp.std_ppcmds) -> Pp.std_ppcmds +val pr_keys : (global_reference -> Pp.t) -> Pp.t (** Pretty-print the mapping *) diff --git a/library/libnames.mli b/library/libnames.mli index b6d6f7f3b..1b351290a 100644 --- a/library/libnames.mli +++ b/library/libnames.mli @@ -7,14 +7,13 @@ (************************************************************************) open Util -open Pp open Loc open Names (** {6 Dirpaths } *) (** FIXME: ought to be in Names.dir_path *) -val pr_dirpath : DirPath.t -> Pp.std_ppcmds +val pr_dirpath : DirPath.t -> Pp.t val dirpath_of_string : string -> DirPath.t val string_of_dirpath : DirPath.t -> string @@ -58,7 +57,7 @@ val basename : full_path -> Id.t (** Parsing and printing of section path as ["coq_root.module.id"] *) val path_of_string : string -> full_path val string_of_path : full_path -> string -val pr_path : full_path -> std_ppcmds +val pr_path : full_path -> Pp.t module Spmap : CSig.MapS with type key = full_path @@ -77,7 +76,7 @@ val repr_qualid : qualid -> DirPath.t * Id.t val qualid_eq : qualid -> qualid -> bool -val pr_qualid : qualid -> std_ppcmds +val pr_qualid : qualid -> Pp.t val string_of_qualid : qualid -> string val qualid_of_string : string -> qualid @@ -124,7 +123,7 @@ type reference = val eq_reference : reference -> reference -> bool val qualid_of_reference : reference -> qualid located val string_of_reference : reference -> string -val pr_reference : reference -> std_ppcmds +val pr_reference : reference -> Pp.t val loc_of_reference : reference -> Loc.t option val join_reference : reference -> reference -> reference diff --git a/library/nameops.mli b/library/nameops.mli index 88290f485..89aba2447 100644 --- a/library/nameops.mli +++ b/library/nameops.mli @@ -106,13 +106,13 @@ val name_max : Name.t -> Name.t -> Name.t val name_cons : Name.t -> Id.t list -> Id.t list (** @deprecated Same as [Name.cons] *) -val pr_name : Name.t -> Pp.std_ppcmds +val pr_name : Name.t -> Pp.t (** @deprecated Same as [Name.print] *) -val pr_id : Id.t -> Pp.std_ppcmds +val pr_id : Id.t -> Pp.t (** @deprecated Same as [Names.Id.print] *) -val pr_lab : Label.t -> Pp.std_ppcmds +val pr_lab : Label.t -> Pp.t (** some preset paths *) @@ -127,5 +127,5 @@ val coq_string : string (** "Coq" *) val default_root_prefix : DirPath.t (** Metavariables *) -val pr_meta : Term.metavariable -> Pp.std_ppcmds +val pr_meta : Term.metavariable -> Pp.t val string_of_meta : Term.metavariable -> string diff --git a/library/nametab.mli b/library/nametab.mli index be57f5dcc..025a63b1c 100644 --- a/library/nametab.mli +++ b/library/nametab.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Libnames open Globnames @@ -155,7 +154,7 @@ val basename_of_global : global_reference -> Id.t (** Printing of global references using names as short as possible. @raise Not_found when the reference is not in the global tables. *) -val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds +val pr_global_env : Id.Set.t -> global_reference -> Pp.t (** The [shortest_qualid] functions given an object with [user_name] diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index d4043f31e..ec422c58d 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -354,7 +354,7 @@ type (_, _) ty_symbol = type ('self, _, 'r) ty_rule = | TyStop : ('self, 'r, 'r) ty_rule | TyNext : ('self, 'a, 'r) ty_rule * ('self, 'b) ty_symbol -> ('self, 'b -> 'a, 'r) ty_rule -| TyMark : int * bool * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule +| TyMark : int * bool * int * ('self, 'a, 'r) ty_rule -> ('self, 'a, 'r) ty_rule type 'r gen_eval = Loc.t -> 'r env -> 'r @@ -368,18 +368,27 @@ let rec ty_eval : type s a. (s, a, Loc.t -> s) ty_rule -> s gen_eval -> s env -> | TyNext (rem, TyNonTerm (forpat, e, _, true)) -> fun f env v -> ty_eval rem f (push_item forpat e env v) -| TyMark (n, b, rem) -> +| TyMark (n, b, p, rem) -> fun f env -> let heads, constrs = List.chop n env.constrs in - let constrlists = - if b then (heads @ List.hd env.constrlists) :: List.tl env.constrlists - else heads :: env.constrlists + let constrlists, constrs = + if b then + (* We rearrange constrs = c1..cn rem and constrlists = [d1..dr e1..ep] rem' into + constrs = e1..ep rem and constrlists [c1..cn d1..dr] rem' *) + let constrlist = List.hd env.constrlists in + let constrlist, tail = List.chop (List.length constrlist - p) constrlist in + (heads @ constrlist) :: List.tl env.constrlists, tail @ constrs + else + (* We rearrange constrs = c1..cn e1..ep rem into + constrs = e1..ep rem and add a constr list [c1..cn] *) + let constrlist, tail = List.chop (n - p) heads in + constrlist :: env.constrlists, tail @ constrs in ty_eval rem f { env with constrs; constrlists; } let rec ty_erase : type s a r. (s, a, r) ty_rule -> (s, a, r) Extend.rule = function | TyStop -> Stop -| TyMark (_, _, r) -> ty_erase r +| TyMark (_, _, _, r) -> ty_erase r | TyNext (rem, TyTerm tok) -> Next (ty_erase rem, Atoken tok) | TyNext (rem, TyNonTerm (_, _, s, _)) -> Next (ty_erase rem, s) @@ -398,9 +407,9 @@ let make_ty_rule assoc from forpat prods = let s = symbol_of_entry assoc from e in let bind = match var with None -> false | Some _ -> true in AnyTyRule (TyNext (r, TyNonTerm (forpat, e, s, bind))) - | GramConstrListMark (n, b) :: rem -> + | GramConstrListMark (n, b, p) :: rem -> let AnyTyRule r = make_ty_rule rem in - AnyTyRule (TyMark (n, b, r)) + AnyTyRule (TyMark (n, b, p, r)) in make_ty_rule (List.rev prods) diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index e6abf1ccf..f904aa3e6 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -120,7 +120,7 @@ val term_equal : term -> term -> bool val constr_of_term : term -> constr -val debug : (unit -> Pp.std_ppcmds) -> unit +val debug : (unit -> Pp.t) -> unit val forest : state -> forest @@ -169,7 +169,7 @@ val find_instances : state -> (quant_eq * int array) list val execute : bool -> state -> explanation option -val pr_idx_term : forest -> int -> Pp.std_ppcmds +val pr_idx_term : forest -> int -> Pp.t val empty_forest: unit -> forest diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index d6342b59c..356bad98b 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -9,30 +9,29 @@ open Names open Globnames open Miniml -open Pp (** By default, in module Format, you can do horizontal placing of blocks even if they include newlines, as long as the number of chars in the blocks are less that a line length. To avoid this awkward situation, we attach a big virtual size to [fnl] newlines. *) -val fnl : unit -> std_ppcmds -val fnl2 : unit -> std_ppcmds -val space_if : bool -> std_ppcmds +val fnl : unit -> Pp.t +val fnl2 : unit -> Pp.t +val space_if : bool -> Pp.t -val pp_par : bool -> std_ppcmds -> std_ppcmds +val pp_par : bool -> Pp.t -> Pp.t (** [pp_apply] : a head part applied to arguments, possibly with parenthesis *) -val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds +val pp_apply : Pp.t -> bool -> Pp.t list -> Pp.t (** Same as [pp_apply], but with also protection of the head by parenthesis *) -val pp_apply2 : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds +val pp_apply2 : Pp.t -> bool -> Pp.t list -> Pp.t -val pp_tuple_light : (bool -> 'a -> std_ppcmds) -> 'a list -> std_ppcmds -val pp_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds -val pp_boxed_tuple : ('a -> std_ppcmds) -> 'a list -> std_ppcmds +val pp_tuple_light : (bool -> 'a -> Pp.t) -> 'a list -> Pp.t +val pp_tuple : ('a -> Pp.t) -> 'a list -> Pp.t +val pp_boxed_tuple : ('a -> Pp.t) -> 'a list -> Pp.t -val pr_binding : Id.t list -> std_ppcmds +val pr_binding : Id.t list -> Pp.t val rename_id : Id.t -> Id.Set.t -> Id.t @@ -80,4 +79,4 @@ val mk_ind : string -> string -> MutInd.t val is_native_char : ml_ast -> bool val get_native_char : ml_ast -> char -val pp_native_char : ml_ast -> std_ppcmds +val pp_native_char : ml_ast -> Pp.t diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index e10dcd48b..5769ff117 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -29,7 +29,7 @@ val mono_environment : (* Used by the Relation Extraction plugin *) val print_one_decl : - Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.std_ppcmds + Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.t (* Used by Extraction Compute *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 661842790..7644b49ce 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -295,7 +295,11 @@ let rec extract_type env db j c args = | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in extract_type_app env db (IndRef (kn,i),s) args - | Case _ | Fix _ | CoFix _ | Proj _ -> Tunknown + | Proj (p,t) -> + (* Let's try to reduce, if it hasn't already been done. *) + if Projection.unfolded p then Tunknown + else extract_type env db j (Term.mkProj (Projection.unfold p, t)) args + | Case _ | Fix _ | CoFix _ -> Tunknown | _ -> assert false (*s Auxiliary function dealing with type application. diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index be8282da0..edebba49d 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -8,7 +8,6 @@ (*s Target language for extraction: a core ML called MiniML. *) -open Pp open Names open Globnames @@ -205,19 +204,19 @@ type language_descr = { file_naming : ModPath.t -> string; (* the second argument is a comment to add to the preamble *) preamble : - Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs -> - std_ppcmds; - pp_struct : ml_structure -> std_ppcmds; + Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs -> + Pp.t; + pp_struct : ml_structure -> Pp.t; (* Concerning a possible interface file *) sig_suffix : string option; (* the second argument is a comment to add to the preamble *) sig_preamble : - Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs -> - std_ppcmds; - pp_sig : ml_signature -> std_ppcmds; + Id.t -> Pp.t option -> ModPath.t list -> unsafe_needs -> + Pp.t; + pp_sig : ml_signature -> Pp.t; (* for an isolated declaration print *) - pp_decl : ml_decl -> std_ppcmds; + pp_decl : ml_decl -> Pp.t; } diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 2b3007f02..7e47d0bc8 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -191,7 +191,7 @@ val find_custom_match : ml_branch array -> string val extraction_language : lang -> unit val extraction_inline : bool -> reference list -> unit -val print_extraction_inline : unit -> Pp.std_ppcmds +val print_extraction_inline : unit -> Pp.t val reset_extraction_inline : unit -> unit val extract_constant_inline : bool -> reference -> string list -> string -> unit @@ -206,7 +206,7 @@ val extraction_implicit : reference -> int_or_id list -> unit val extraction_blacklist : Id.t list -> unit val reset_extraction_blacklist : unit -> unit -val print_extraction_blacklist : unit -> Pp.std_ppcmds +val print_extraction_blacklist : unit -> Pp.t diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index 0a2e84bb8..ca6079c8b 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -57,4 +57,4 @@ val extend_with_ref_list : Environ.env -> Evd.evar_map -> global_reference list val extend_with_auto_hints : Environ.env -> Evd.evar_map -> Hints.hint_db_name list -> t -> t * Evd.evar_map -val print_cmap: global_reference list CM.t -> Pp.std_ppcmds +val print_cmap: global_reference list CM.t -> Pp.t diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 15ab396e3..5f6d78359 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -821,8 +821,9 @@ let build_proof | Fix _ | CoFix _ -> user_err Pp.(str ( "Anonymous local (co)fixpoints are not handled yet")) + | Proj _ -> user_err Pp.(str "Prod") - | Prod _ -> user_err Pp.(str "Prod") + | Prod _ -> do_finalize dyn_infos g | LetIn _ -> let new_infos = { dyn_infos with diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml index e3010e3b5..8cf5e8442 100644 --- a/plugins/funind/glob_term_to_relation.ml +++ b/plugins/funind/glob_term_to_relation.ml @@ -32,6 +32,14 @@ type binder_type = type glob_context = (binder_type*glob_constr) list + +let rec solve_trivial_holes pat_as_term e = + match pat_as_term.CAst.v,e.CAst.v with + | GHole _,_ -> e + | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe -> + CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse)) + | _,_ -> pat_as_term + (* compose_glob_context [(bt_1,n_1,t_1);......] rt returns b_1(n_1,t_1,.....,bn(n_k,t_k,rt)) where the b_i's are the @@ -226,7 +234,12 @@ let combine_lam n t b = compose_glob_context b.context b.value ) } - +let combine_prod2 n t b = + { + context = []; + value = mkGProd(n, compose_glob_context t.context t.value, + compose_glob_context b.context b.value ) + } let combine_prod n t b = { context = t.context@((Prod n,t.value)::b.context); value = b.value} @@ -604,7 +617,9 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return = let t_res = build_entry_lc env funnames avoid t in let new_env = raw_push_named (n,None,t) env in let b_res = build_entry_lc new_env funnames avoid b in - combine_results (combine_prod n) t_res b_res + if List.length t_res.result = 1 && List.length b_res.result = 1 + then combine_results (combine_prod2 n) t_res b_res + else combine_results (combine_prod n) t_res b_res | GLetIn(n,v,typ,b) -> (* we first compute the list of constructor corresponding to the body of the function, @@ -806,6 +821,12 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve let typ_as_constr = EConstr.of_constr typ_as_constr in let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in let pat_as_term = pattern_to_term pat in + (* removing trivial holes *) + let pat_as_term = solve_trivial_holes pat_as_term e in + (* observe (str "those_pattern_preconds" ++ spc () ++ *) + (* str "pat" ++ spc () ++ pr_glob_constr pat_as_term ++ spc ()++ *) + (* str "e" ++ spc () ++ pr_glob_constr e ++spc ()++ *) + (* str "typ_as_constr" ++ spc () ++ pr_lconstr typ_as_constr); *) List.fold_right (fun id acc -> if Id.Set.mem id this_pat_ids diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index 7cb35838c..003bb4e30 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -708,9 +708,6 @@ let expand_as = in expand_as Id.Map.empty - - - (* [resolve_and_replace_implicits ?expected_type env sigma rt] solves implicits of [rt] w.r.t. [env] and [sigma] and then replace them by their solution *) @@ -749,6 +746,30 @@ If someone knows how to prevent solved existantial removal in understand, pleas Detyping.detype false [] env ctx (EConstr.of_constr (f c)) | Evar_empty -> rt (* the hole was not solved : we do nothing *) ) + | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *) + ( + let res = + try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *) + Evd.fold (* to simulate an iter *) + (fun _ evi _ -> + match evi.evar_source with + | (loc_evi,BinderType na') -> + if Name.equal na na' && rt.CAst.loc = loc_evi then raise (Found evi) + | _ -> () + ) + ctx + (); + (* the hole was not solved : we do nothing *) + rt + with Found evi -> (* we found the evar corresponding to this hole *) + match evi.evar_body with + | Evar_defined c -> + (* we just have to lift the solution in glob_term *) + Detyping.detype false [] env ctx (EConstr.of_constr (f c)) + | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *) + in + res + ) | _ -> Glob_ops.map_glob_constr change rt in change rt diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index 7a60da44f..93e03852e 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -1,8 +1,8 @@ open Misctypes -val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit +val warn_cannot_define_graph : ?loc:Loc.t -> Pp.t * Pp.t -> unit -val warn_cannot_define_principle : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit +val warn_cannot_define_principle : ?loc:Loc.t -> Pp.t * Pp.t -> unit val do_generate_principle : bool -> diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index 5e425cd18..2e2ced790 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -1,5 +1,4 @@ open Names -open Pp (* The mk_?_id function build different name w.r.t. a function @@ -11,7 +10,7 @@ val mk_complete_id : Id.t -> Id.t val mk_equation_id : Id.t -> Id.t -val msgnl : std_ppcmds -> unit +val msgnl : Pp.t -> unit val fresh_id : Id.t list -> string -> Id.t val fresh_name : Id.t list -> string -> Name.t @@ -24,7 +23,7 @@ val id_of_name : Name.t -> Id.t val locate_ind : Libnames.reference -> inductive val locate_constant : Libnames.reference -> Constant.t val locate_with_msg : - Pp.std_ppcmds -> (Libnames.reference -> 'a) -> + Pp.t -> (Libnames.reference -> 'a) -> Libnames.reference -> 'a val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list @@ -89,8 +88,8 @@ val update_Function : function_info -> unit (** debugging *) -val pr_info : function_info -> Pp.std_ppcmds -val pr_table : unit -> Pp.std_ppcmds +val pr_info : function_info -> Pp.t +val pr_table : unit -> Pp.t (* val function_debug : bool ref *) diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli index acdf67779..b06f35ddc 100644 --- a/plugins/ltac/extraargs.mli +++ b/plugins/ltac/extraargs.mli @@ -14,13 +14,13 @@ open Misctypes val wit_orient : bool Genarg.uniform_genarg_type val orient : bool Pcoq.Gram.entry -val pr_orient : bool -> Pp.std_ppcmds +val pr_orient : bool -> Pp.t val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type val occurrences : (int list or_var) Pcoq.Gram.entry val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type -val pr_occurrences : int list or_var -> Pp.std_ppcmds +val pr_occurrences : int list or_var -> Pp.t val occurrences_of : int list -> Locus.occurrences val wit_natural : int Genarg.uniform_genarg_type @@ -55,7 +55,7 @@ type place = Id.t gen_place val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type val hloc : loc_place Pcoq.Gram.entry -val pr_hloc : loc_place -> Pp.std_ppcmds +val pr_hloc : loc_place -> Pp.t val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry val wit_by_arg_tac : @@ -64,8 +64,8 @@ val wit_by_arg_tac : Geninterp.Val.t option) Genarg.genarg_type val pr_by_arg_tac : - (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.std_ppcmds) -> - raw_tactic_expr option -> Pp.std_ppcmds + (int * Ppextend.parenRelation -> raw_tactic_expr -> Pp.t) -> + raw_tactic_expr option -> Pp.t val test_lpar_id_colon : unit Pcoq.Gram.entry diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 327b347ec..140cc3344 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -67,22 +67,22 @@ let declare_notation_tactic_pprule kn pt = prnotation_tab := KNmap.add kn pt !prnotation_tab type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> - 'a -> std_ppcmds + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a glob_extra_genarg_printer = - (glob_constr_and_expr -> std_ppcmds) -> - (glob_constr_and_expr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - 'a -> std_ppcmds + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a extra_genarg_printer = - (EConstr.constr -> std_ppcmds) -> - (EConstr.constr -> std_ppcmds) -> - (tolerability -> Val.t -> std_ppcmds) -> - 'a -> std_ppcmds + (EConstr.constr -> Pp.t) -> + (EConstr.constr -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + 'a -> Pp.t let keyword x = tag_keyword (str x) let primitive x = tag_primitive (str x) @@ -96,7 +96,7 @@ type 'a extra_genarg_printer = | None -> assert false | Some Refl -> x - let rec pr_value lev v : std_ppcmds = + let rec pr_value lev v : Pp.t = if has_type v Val.typ_list then pr_sequence (fun x -> pr_value lev x) (unbox v Val.typ_list) else if has_type v Val.typ_opt then @@ -272,7 +272,7 @@ type 'a extra_genarg_printer = | Glbwit (OptArg wit) -> Some (Option.map (in_gen (glbwit wit)) arg) | _ -> None - let rec pr_any_arg : type l. (_ -> l generic_argument -> std_ppcmds) -> _ -> l generic_argument -> std_ppcmds = + let rec pr_any_arg : type l. (_ -> l generic_argument -> Pp.t) -> _ -> l generic_argument -> Pp.t = fun prtac symb arg -> match symb with | Extend.Uentry tag when is_genarg tag (genarg_tag arg) -> prtac (1, Any) arg | Extend.Ulist1 s | Extend.Ulist0 s -> @@ -599,18 +599,18 @@ type 'a extra_genarg_printer = "raw", "glob" and "typed" levels *) type 'a printer = { - pr_tactic : tolerability -> 'tacexpr -> std_ppcmds; - pr_constr : 'trm -> std_ppcmds; - pr_lconstr : 'trm -> std_ppcmds; - pr_dconstr : 'dtrm -> std_ppcmds; - pr_pattern : 'pat -> std_ppcmds; - pr_lpattern : 'pat -> std_ppcmds; - pr_constant : 'cst -> std_ppcmds; - pr_reference : 'ref -> std_ppcmds; - pr_name : 'nam -> std_ppcmds; - pr_generic : 'lev generic_argument -> std_ppcmds; - pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> std_ppcmds; - pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> std_ppcmds; + pr_tactic : tolerability -> 'tacexpr -> Pp.t; + pr_constr : 'trm -> Pp.t; + pr_lconstr : 'trm -> Pp.t; + pr_dconstr : 'dtrm -> Pp.t; + pr_pattern : 'pat -> Pp.t; + pr_lpattern : 'pat -> Pp.t; + pr_constant : 'cst -> Pp.t; + pr_reference : 'ref -> Pp.t; + pr_name : 'nam -> Pp.t; + pr_generic : 'lev generic_argument -> Pp.t; + pr_extend : int -> ml_tactic_entry -> 'a gen_tactic_arg list -> Pp.t; + pr_alias : int -> KerName.t -> 'a gen_tactic_arg list -> Pp.t; } constraint 'a = < diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli index 1127c9831..0bf9bc7f6 100644 --- a/plugins/ltac/pptactic.mli +++ b/plugins/ltac/pptactic.mli @@ -9,7 +9,6 @@ (** This module implements pretty-printers for tactic_expr syntactic objects and their subcomponents. *) -open Pp open Genarg open Geninterp open Names @@ -24,22 +23,22 @@ type 'a grammar_tactic_prod_item_expr = | TacNonTerm of ('a * Names.Id.t option) Loc.located type 'a raw_extra_genarg_printer = - (constr_expr -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - (tolerability -> raw_tactic_expr -> std_ppcmds) -> - 'a -> std_ppcmds + (constr_expr -> Pp.t) -> + (constr_expr -> Pp.t) -> + (tolerability -> raw_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a glob_extra_genarg_printer = - (glob_constr_and_expr -> std_ppcmds) -> - (glob_constr_and_expr -> std_ppcmds) -> - (tolerability -> glob_tactic_expr -> std_ppcmds) -> - 'a -> std_ppcmds + (glob_constr_and_expr -> Pp.t) -> + (glob_constr_and_expr -> Pp.t) -> + (tolerability -> glob_tactic_expr -> Pp.t) -> + 'a -> Pp.t type 'a extra_genarg_printer = - (EConstr.t -> std_ppcmds) -> - (EConstr.t -> std_ppcmds) -> - (tolerability -> Val.t -> std_ppcmds) -> - 'a -> std_ppcmds + (EConstr.t -> Pp.t) -> + (EConstr.t -> Pp.t) -> + (tolerability -> Val.t -> Pp.t) -> + 'a -> Pp.t val declare_extra_genarg_pprule : ('a, 'b, 'c) genarg_type -> @@ -57,61 +56,61 @@ type pp_tactic = { val declare_notation_tactic_pprule : KerName.t -> pp_tactic -> unit val pr_with_occurrences : - ('a -> std_ppcmds) -> 'a Locus.with_occurrences -> std_ppcmds + ('a -> Pp.t) -> 'a Locus.with_occurrences -> Pp.t val pr_red_expr : - ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> - ('a,'b,'c) Genredexpr.red_expr_gen -> std_ppcmds + ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + ('a,'b,'c) Genredexpr.red_expr_gen -> Pp.t val pr_may_eval : - ('a -> std_ppcmds) -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> - ('c -> std_ppcmds) -> ('a,'b,'c) Genredexpr.may_eval -> std_ppcmds + ('a -> Pp.t) -> ('a -> Pp.t) -> ('b -> Pp.t) -> + ('c -> Pp.t) -> ('a,'b,'c) Genredexpr.may_eval -> Pp.t -val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds -val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds +val pr_and_short_name : ('a -> Pp.t) -> 'a and_short_name -> Pp.t +val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t val pr_in_clause : - ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t val pr_clauses : bool option -> - ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a Locus.clause_expr -> Pp.t -val pr_raw_generic : env -> rlevel generic_argument -> std_ppcmds +val pr_raw_generic : env -> rlevel generic_argument -> Pp.t -val pr_glb_generic : env -> glevel generic_argument -> std_ppcmds +val pr_glb_generic : env -> glevel generic_argument -> Pp.t val pr_raw_extend: env -> int -> - ml_tactic_entry -> raw_tactic_arg list -> std_ppcmds + ml_tactic_entry -> raw_tactic_arg list -> Pp.t val pr_glob_extend: env -> int -> - ml_tactic_entry -> glob_tactic_arg list -> std_ppcmds + ml_tactic_entry -> glob_tactic_arg list -> Pp.t val pr_extend : - (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds + (Val.t -> Pp.t) -> int -> ml_tactic_entry -> Val.t list -> Pp.t -val pr_alias_key : Names.KerName.t -> std_ppcmds +val pr_alias_key : Names.KerName.t -> Pp.t -val pr_alias : (Val.t -> std_ppcmds) -> - int -> Names.KerName.t -> Val.t list -> std_ppcmds +val pr_alias : (Val.t -> Pp.t) -> + int -> Names.KerName.t -> Val.t list -> Pp.t -val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds +val pr_ltac_constant : Nametab.ltac_constant -> Pp.t -val pr_raw_tactic : raw_tactic_expr -> std_ppcmds +val pr_raw_tactic : raw_tactic_expr -> Pp.t -val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> std_ppcmds +val pr_raw_tactic_level : tolerability -> raw_tactic_expr -> Pp.t -val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds +val pr_glob_tactic : env -> glob_tactic_expr -> Pp.t -val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> std_ppcmds +val pr_atomic_tactic : env -> Evd.evar_map -> atomic_tactic_expr -> Pp.t -val pr_hintbases : string list option -> std_ppcmds +val pr_hintbases : string list option -> Pp.t -val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds +val pr_auto_using : ('constr -> Pp.t) -> 'constr list -> Pp.t -val pr_match_pattern : ('a -> std_ppcmds) -> 'a match_pattern -> std_ppcmds +val pr_match_pattern : ('a -> Pp.t) -> 'a match_pattern -> Pp.t -val pr_match_rule : bool -> ('a -> std_ppcmds) -> ('b -> std_ppcmds) -> - ('b, 'a) match_rule -> std_ppcmds +val pr_match_rule : bool -> ('a -> Pp.t) -> ('b -> Pp.t) -> + ('b, 'a) match_rule -> Pp.t -val pr_value : tolerability -> Val.t -> std_ppcmds +val pr_value : tolerability -> Val.t -> Pp.t val ltop : tolerability diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index bbd7834d5..75b665aad 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -1461,7 +1461,7 @@ let solve_constraints env (evars,cstrs) = let nf_zeta = Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA]) -exception RewriteFailure of Pp.std_ppcmds +exception RewriteFailure of Pp.t type result = (evar_map * constr option * types) option option diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 35205ac58..23767c12f 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -61,8 +61,8 @@ val strategy_of_ast : (glob_constr_and_expr, raw_red_expr) strategy_ast -> strat val map_strategy : ('a -> 'b) -> ('c -> 'd) -> ('a, 'c) strategy_ast -> ('b, 'd) strategy_ast -val pr_strategy : ('a -> Pp.std_ppcmds) -> ('b -> Pp.std_ppcmds) -> - ('a, 'b) strategy_ast -> Pp.std_ppcmds +val pr_strategy : ('a -> Pp.t) -> ('b -> Pp.t) -> + ('a, 'b) strategy_ast -> Pp.t (** Entry point for user-level "rewrite_strat" *) val cl_rewrite_clause_strat : strategy -> Id.t option -> unit Proofview.tactic diff --git a/plugins/ltac/tacintern.mli b/plugins/ltac/tacintern.mli index b262473a9..e3a4d5c79 100644 --- a/plugins/ltac/tacintern.mli +++ b/plugins/ltac/tacintern.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Tacexpr open Genarg @@ -55,7 +54,7 @@ val intern_hyp : glob_sign -> Id.t Loc.located -> Id.t Loc.located val intern_genarg : glob_sign -> raw_generic_argument -> glob_generic_argument (** printing *) -val print_ltac : Libnames.qualid -> std_ppcmds +val print_ltac : Libnames.qualid -> Pp.t (** Reduction expressions *) diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 60a8f75ec..d3e625e73 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2000,7 +2000,7 @@ let lift f = (); fun ist x -> Ftactic.enter begin fun gl -> Ftactic.return (f ist env sigma x) end -let lifts f = (); fun ist x -> Ftactic.nf_enter begin fun gl -> +let lifts f = (); fun ist x -> Ftactic.enter begin fun gl -> let env = Proofview.Goal.env gl in let sigma = Proofview.Goal.sigma gl in let (sigma, v) = f ist env sigma x in diff --git a/plugins/ltac/tactic_debug.mli b/plugins/ltac/tactic_debug.mli index ef6362270..2475e41f9 100644 --- a/plugins/ltac/tactic_debug.mli +++ b/plugins/ltac/tactic_debug.mli @@ -58,16 +58,16 @@ val db_hyp_pattern_failure : val db_matching_failure : debug_info -> unit Proofview.NonLogical.t (** Prints an evaluation failure message for a rule *) -val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t +val db_eval_failure : debug_info -> Pp.t -> unit Proofview.NonLogical.t (** An exception handler *) -val explain_logic_error: exn -> Pp.std_ppcmds +val explain_logic_error: exn -> Pp.t (** For use in the Ltac debugger: some exception that are usually consider anomalies are acceptable because they are caught later in the process that is being debugged. One should not require from users that they report these anomalies. *) -val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds +val explain_logic_error_no_anomaly : exn -> Pp.t (** Prints a logic failure message for a rule *) val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t @@ -77,4 +77,4 @@ val db_breakpoint : debug_info -> Id.t Loc.located message_token list -> unit Proofview.NonLogical.t val extract_ltac_trace : - ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.std_ppcmds option Loc.located + ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located diff --git a/plugins/ltac/tactic_option.mli b/plugins/ltac/tactic_option.mli index dd91944d4..95cd243ec 100644 --- a/plugins/ltac/tactic_option.mli +++ b/plugins/ltac/tactic_option.mli @@ -12,4 +12,4 @@ open Vernacexpr val declare_tactic_option : ?default:Tacexpr.glob_tactic_expr -> string -> (* put *) (locality_flag -> glob_tactic_expr -> unit) * (* get *) (unit -> locality_flag * unit Proofview.tactic) * - (* print *) (unit -> Pp.std_ppcmds) + (* print *) (unit -> Pp.t) diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli index e0c09f394..86231cf19 100644 --- a/plugins/rtauto/proof_search.mli +++ b/plugins/rtauto/proof_search.mli @@ -38,9 +38,9 @@ val branching: state -> state list val success: state -> bool -val pp: state -> Pp.std_ppcmds +val pp: state -> Pp.t -val pr_form : form -> Pp.std_ppcmds +val pr_form : form -> Pp.t val reset_info : unit -> unit diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 4b045e989..2eadd5f26 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -41,7 +41,7 @@ val nohint : 'a ssrhint (******************************** misc ************************************) -val errorstrm : Pp.std_ppcmds -> 'a +val errorstrm : Pp.t -> 'a val anomaly : string -> 'a val array_app_tl : 'a array -> 'a list -> 'a list diff --git a/plugins/ssr/ssrparser.mli b/plugins/ssr/ssrparser.mli index bf6f44f11..88beeaa71 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -16,5 +16,5 @@ val ssrtclarg : Tacexpr.raw_tactic_expr Pcoq.Gram.entry val wit_ssrtclarg : (Tacexpr.raw_tactic_expr, Tacexpr.glob_tactic_expr, Geninterp.Val.t) Genarg.genarg_type val pr_ssrtclarg : 'a -> 'b -> (int * Ppextend.parenRelation -> 'c -> 'd) -> 'c -> 'd -val add_genarg : string -> ('a -> Pp.std_ppcmds) -> 'a Genarg.uniform_genarg_type +val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type diff --git a/plugins/ssr/ssrprinters.mli b/plugins/ssr/ssrprinters.mli index 5c68872b7..f23106826 100644 --- a/plugins/ssr/ssrprinters.mli +++ b/plugins/ssr/ssrprinters.mli @@ -11,16 +11,16 @@ open Ssrast val pp_term : - Goal.goal Evd.sigma -> EConstr.constr -> Pp.std_ppcmds + Goal.goal Evd.sigma -> EConstr.constr -> Pp.t -val pr_spc : unit -> Pp.std_ppcmds -val pr_bar : unit -> Pp.std_ppcmds +val pr_spc : unit -> Pp.t +val pr_bar : unit -> Pp.t val pr_list : - (unit -> Pp.std_ppcmds) -> ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds + (unit -> Pp.t) -> ('a -> Pp.t) -> 'a list -> Pp.t val pp_concat : - Pp.std_ppcmds -> - ?sep:Pp.std_ppcmds -> Pp.std_ppcmds list -> Pp.std_ppcmds + Pp.t -> + ?sep:Pp.t -> Pp.t list -> Pp.t val xInParens : ssrtermkind val xWithAt : ssrtermkind @@ -29,17 +29,17 @@ val xCpattern : ssrtermkind val pr_term : ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) -> - Pp.std_ppcmds + Pp.t -val pr_hyp : ssrhyp -> Pp.std_ppcmds +val pr_hyp : ssrhyp -> Pp.t -val prl_constr_expr : Constrexpr.constr_expr -> Pp.std_ppcmds -val prl_glob_constr : Glob_term.glob_constr -> Pp.std_ppcmds +val prl_constr_expr : Constrexpr.constr_expr -> Pp.t +val prl_glob_constr : Glob_term.glob_constr -> Pp.t val pr_guarded : - (string -> int -> bool) -> ('a -> Pp.std_ppcmds) -> 'a -> Pp.std_ppcmds + (string -> int -> bool) -> ('a -> Pp.t) -> 'a -> Pp.t -val pr_occ : ssrocc -> Pp.std_ppcmds +val pr_occ : ssrocc -> Pp.t -val ppdebug : Pp.std_ppcmds Lazy.t -> unit +val ppdebug : Pp.t Lazy.t -> unit diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 65ea76d16..8e2a1a717 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -15,7 +15,7 @@ open Term (** The type of context patterns, the patterns of the [set] tactic and [:] tactical. These are patterns that identify a precise subterm. *) type cpattern -val pr_cpattern : cpattern -> Pp.std_ppcmds +val pr_cpattern : cpattern -> Pp.t (** CS cpattern: (f _), (X in t), (t in X in t), (t as X in t) *) val cpattern : cpattern Pcoq.Gram.entry @@ -29,7 +29,7 @@ val wit_lcpattern : cpattern uniform_genarg_type These patterns also include patterns that identify all the subterms of a context (i.e. "in" prefix) *) type rpattern -val pr_rpattern : rpattern -> Pp.std_ppcmds +val pr_rpattern : rpattern -> Pp.t (** OS rpattern: f _, in t, X in t, in X in t, t in X in t, t as X in t *) val rpattern : rpattern Pcoq.Gram.entry @@ -50,7 +50,7 @@ type ('ident, 'term) ssrpattern = | E_As_X_In_T of 'term * 'ident * 'term type pattern = evar_map * (constr, constr) ssrpattern -val pp_pattern : pattern -> Pp.std_ppcmds +val pp_pattern : pattern -> Pp.t (** Extracts the redex and applies to it the substitution part of the pattern. @raise Anomaly if called on [In_T] or [In_X_In_T] *) @@ -115,7 +115,7 @@ val fill_occ_pattern : the T pattern above, and calls a continuation on its occurrences. *) type ssrdir = L2R | R2L -val pr_dir_side : ssrdir -> Pp.std_ppcmds +val pr_dir_side : ssrdir -> Pp.t (** a pattern for a term with wildcards *) type tpattern @@ -225,7 +225,7 @@ val loc_of_cpattern : cpattern -> Loc.t option val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool val cpattern_of_id : Names.Id.t -> cpattern -val pr_constr_pat : constr -> Pp.std_ppcmds +val pr_constr_pat : constr -> Pp.t val pf_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma val pf_unsafe_merge_uc : UState.t -> goal Evd.sigma -> goal Evd.sigma diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 078990a8c..1cc072a2a 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -89,7 +89,7 @@ sig type t val compare : t -> t -> int val equal : t -> t -> bool - val print : t -> std_ppcmds + val print : t -> Pp.t end type 'a t val empty : 'a t @@ -324,7 +324,7 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; (* rajouter une coercion dans le graphe *) let path_printer = ref (fun _ -> str "<a class path>" - : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> std_ppcmds) + : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) let install_path_printer f = path_printer := f diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 2e5ce30f3..8707078b5 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -95,15 +95,14 @@ val lookup_pattern_path_between : (**/**) (* Crade *) -open Pp val install_path_printer : - ((cl_index * cl_index) * inheritance_path -> std_ppcmds) -> unit + ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit (**/**) (** {6 This is for printing purpose } *) val string_of_class : cl_typ -> string -val pr_class : cl_typ -> std_ppcmds -val pr_cl_index : cl_index -> std_ppcmds +val pr_class : cl_typ -> Pp.t +val pr_cl_index : cl_index -> Pp.t val get_coercion_value : coe_index -> Constr.t val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list val classes : unit -> cl_typ list diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index f830d4be3..a27debe73 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -81,7 +81,7 @@ let encode_tuple r = module PrintingInductiveMake = functor (Test : sig val encode : reference -> inductive - val member_message : std_ppcmds -> bool -> std_ppcmds + val member_message : Pp.t -> bool -> Pp.t val field : string val title : string end) -> @@ -475,8 +475,8 @@ let rec detype flags avoid env sigma t = CAst.make @@ GApp (f',args''@args') | _ -> GApp (f',args') in - mkapp (detype flags avoid env sigma f) - (Array.map_to_list (detype flags avoid env sigma) args) + mkapp (detype flags avoid env sigma f) + (detype_array flags avoid env sigma args) | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u) | Proj (p,c) -> let noparams () = @@ -694,6 +694,15 @@ and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c = let t = if s != InProp && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in GLetIn (na', c, t, r) +(** We use a dedicated function here to prevent overallocation from + Array.map_to_list. *) +and detype_array flags avoid env sigma args = + let ans = ref [] in + for i = Array.length args - 1 downto 0 do + ans := detype flags avoid env sigma args.(i) :: !ans; + done; + !ans + let detype_rel_context ?(lax=false) where avoid env sigma sign = let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in let rec aux avoid env = function diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index ffd67299d..59f3f967d 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -66,7 +66,7 @@ val subst_genarg_hook : module PrintingInductiveMake : functor (Test : sig val encode : Libnames.reference -> Names.inductive - val member_message : Pp.std_ppcmds -> bool -> Pp.std_ppcmds + val member_message : Pp.t -> bool -> Pp.t val field : string val title : string end) -> @@ -75,9 +75,9 @@ module PrintingInductiveMake : val compare : t -> t -> int val encode : Libnames.reference -> Names.inductive val subst : substitution -> t -> t - val printer : t -> Pp.std_ppcmds + val printer : t -> Pp.t val key : Goptions.option_name val title : string - val member_message : t -> bool -> Pp.std_ppcmds + val member_message : t -> bool -> Pp.t val synchronous : bool end diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli index c727332c7..5477c5c99 100644 --- a/pretyping/evardefine.mli +++ b/pretyping/evardefine.mli @@ -43,5 +43,5 @@ val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts (** {6 debug pretty-printer:} *) -val pr_tycon : env -> evar_map -> type_constraint -> Pp.std_ppcmds +val pr_tycon : env -> evar_map -> type_constraint -> Pp.t diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index bfc6bf5cf..b4d87dfdb 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1136,8 +1136,13 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function evd_comb1 (define_evar_as_sort env.ExtraEnv.env) evdref ev | _ -> anomaly (Pp.str "Found a type constraint which is not a type.") in - { utj_val = v; - utj_type = s } + (* Correction of bug #5315 : we need to define an evar for *all* holes *) + let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in + let ev,_ = destEvar !evdref evkt in + evdref := Evd.define ev (to_constr !evdref v) !evdref; + (* End of correction of bug #5315 *) + { utj_val = v; + utj_type = s } | None -> let env = ltac_interp_name_env k0 lvar env !evdref in let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index de09edcdc..5480b14af 100644 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -67,7 +67,7 @@ type obj_typ = { (** Return the form of the component of a canonical structure *) val cs_pattern_of_constr : constr -> cs_pattern * int option * constr list -val pr_cs_pattern : cs_pattern -> Pp.std_ppcmds +val pr_cs_pattern : cs_pattern -> Pp.t val lookup_canonical_conversion : (global_reference * cs_pattern) -> constr * obj_typ val declare_canonical_structure : global_reference -> unit diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 1d75fecb1..356323543 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -272,7 +272,7 @@ module Stack : sig open EConstr type 'a app_node - val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds + val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t type cst_member = | Cst_const of pconstant @@ -290,7 +290,7 @@ sig exception IncompatibleFold2 - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t val empty : 'a t val is_empty : 'a t -> bool val append_app : 'a array -> 'a t -> 'a t diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index db407b6c9..1828196fe 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -26,7 +26,7 @@ module ReductionBehaviour : sig bool -> Globnames.global_reference -> (int list * int * flag list) -> unit val get : Globnames.global_reference -> (int list * int * flag list) option - val print : Globnames.global_reference -> Pp.std_ppcmds + val print : Globnames.global_reference -> Pp.t end (** Option telling if reduction should use the refolding machinery of cbn @@ -63,13 +63,13 @@ module Cst_stack : sig val best_cst : t -> (constr * constr list) option val best_replace : Evd.evar_map -> constr -> t -> constr -> constr val reference : Evd.evar_map -> t -> Constant.t option - val pr : t -> Pp.std_ppcmds + val pr : t -> Pp.t end module Stack : sig type 'a app_node - val pr_app_node : ('a -> Pp.std_ppcmds) -> 'a app_node -> Pp.std_ppcmds + val pr_app_node : ('a -> Pp.t) -> 'a app_node -> Pp.t type cst_member = | Cst_const of pconstant @@ -86,7 +86,7 @@ module Stack : sig | Update of 'a and 'a t = 'a member list - val pr : ('a -> Pp.std_ppcmds) -> 'a t -> Pp.std_ppcmds + val pr : ('a -> Pp.t) -> 'a t -> Pp.t val empty : 'a t val is_empty : 'a t -> bool @@ -145,7 +145,7 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -val pr_state : state -> Pp.std_ppcmds +val pr_state : state -> Pp.t (** {6 Reduction Function Operators } *) diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 163d3975a..ed3a9d0f9 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -48,4 +48,4 @@ val sorts_of_context : env -> evar_map -> rel_context -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr -val print_retype_error : retype_error -> Pp.std_ppcmds +val print_retype_error : retype_error -> Pp.t diff --git a/printing/genprint.ml b/printing/genprint.ml index bb9736d73..543b05024 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -9,7 +9,7 @@ open Pp open Genarg -type 'a printer = 'a -> std_ppcmds +type 'a printer = 'a -> Pp.t type ('raw, 'glb, 'top) genprinter = { raw : 'raw printer; diff --git a/printing/genprint.mli b/printing/genprint.mli index 24779a359..130a89c92 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -8,18 +8,17 @@ (** Entry point for generic printers *) -open Pp open Genarg -type 'a printer = 'a -> std_ppcmds +type 'a printer = 'a -> Pp.t -val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> std_ppcmds +val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> Pp.t (** Printer for raw level generic arguments. *) -val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> Pp.t (** Printer for glob level generic arguments. *) -val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> Pp.t (** Printer for top level generic arguments. *) val generic_raw_print : rlevel generic_argument printer diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index cf513321f..ee03bc900 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -731,10 +731,10 @@ let tag_var = tag Tag.variable (sep() ++ if prec_less prec inherited then strm else surround strm) type term_pr = { - pr_constr_expr : constr_expr -> std_ppcmds; - pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; - pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds + pr_constr_expr : constr_expr -> Pp.t; + pr_lconstr_expr : constr_expr -> Pp.t; + pr_constr_pattern_expr : constr_pattern_expr -> Pp.t; + pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } type precedence = Ppextend.precedence * Ppextend.parenRelation diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index fd232759e..833503485 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -9,10 +9,8 @@ (** This module implements pretty-printers for constr_expr syntactic objects and their subcomponents. *) -(** The default pretty-printers produce {!Pp.std_ppcmds} that are - interpreted as raw strings. *) +(** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *) open Loc -open Pp open Libnames open Constrexpr open Names @@ -28,45 +26,45 @@ val split_fix : val prec_less : int -> int * Ppextend.parenRelation -> bool -val pr_tight_coma : unit -> std_ppcmds +val pr_tight_coma : unit -> Pp.t -val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds +val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t -val pr_lident : Id.t located -> std_ppcmds -val pr_lname : Name.t located -> std_ppcmds +val pr_lident : Id.t located -> Pp.t +val pr_lname : Name.t located -> Pp.t -val pr_with_comments : ?loc:Loc.t -> std_ppcmds -> std_ppcmds -val pr_com_at : int -> std_ppcmds +val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t +val pr_com_at : int -> Pp.t val pr_sep_com : - (unit -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - constr_expr -> std_ppcmds + (unit -> Pp.t) -> + (constr_expr -> Pp.t) -> + constr_expr -> Pp.t -val pr_id : Id.t -> std_ppcmds -val pr_name : Name.t -> std_ppcmds -val pr_qualid : qualid -> std_ppcmds -val pr_patvar : patvar -> std_ppcmds +val pr_id : Id.t -> Pp.t +val pr_name : Name.t -> Pp.t +val pr_qualid : qualid -> Pp.t +val pr_patvar : patvar -> Pp.t -val pr_glob_level : glob_level -> std_ppcmds -val pr_glob_sort : glob_sort -> std_ppcmds -val pr_guard_annot : (constr_expr -> std_ppcmds) -> +val pr_glob_level : glob_level -> Pp.t +val pr_glob_sort : glob_sort -> Pp.t +val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> ('a * Names.Id.t) option * recursion_order_expr -> - std_ppcmds + Pp.t -val pr_record_body : (reference * constr_expr) list -> std_ppcmds -val pr_binders : local_binder_expr list -> std_ppcmds -val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds -val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds -val pr_constr_expr : constr_expr -> std_ppcmds -val pr_lconstr_expr : constr_expr -> std_ppcmds -val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds +val pr_record_body : (reference * constr_expr) list -> Pp.t +val pr_binders : local_binder_expr list -> Pp.t +val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t +val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t +val pr_constr_expr : constr_expr -> Pp.t +val pr_lconstr_expr : constr_expr -> Pp.t +val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t type term_pr = { - pr_constr_expr : constr_expr -> std_ppcmds; - pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; - pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds + pr_constr_expr : constr_expr -> Pp.t; + pr_lconstr_expr : constr_expr -> Pp.t; + pr_constr_pattern_expr : constr_pattern_expr -> Pp.t; + pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } val set_term_pr : term_pr -> unit @@ -91,5 +89,5 @@ type precedence val lsimpleconstr : precedence val ltop : precedence val modular_constr_pr : - ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) -> - (unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds + ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) -> + (unit->Pp.t) -> precedence -> constr_expr -> Pp.t diff --git a/printing/pputils.mli b/printing/pputils.mli index 0dee11e0b..1f4fa1390 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -6,26 +6,25 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Genarg open Misctypes open Locus open Genredexpr -val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds +val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t (** Prints an object surrounded by its commented location *) -val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds -val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds +val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t +val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t val pr_with_occurrences : - ('a -> std_ppcmds) -> (string -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds + ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t -val pr_short_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds -val pr_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds +val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t +val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t val pr_red_expr : - ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> - (string -> std_ppcmds) -> - ('a,'b,'c) red_expr_gen -> std_ppcmds + ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + (string -> Pp.t) -> + ('a,'b,'c) red_expr_gen -> Pp.t -val pr_raw_generic : Environ.env -> rlevel generic_argument -> std_ppcmds -val pr_glb_generic : Environ.env -> glevel generic_argument -> std_ppcmds +val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t +val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index ed5585b30..b88eed484 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -10,10 +10,10 @@ objects and their subcomponents. *) (** Prints a fixpoint body *) -val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds +val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t (** Prints a vernac expression *) -val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds +val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t (** Prints a vernac expression and closes it with a dot. *) -val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds +val pr_vernac : Vernacexpr.vernac_expr -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 17249262e..09859157c 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -33,17 +33,17 @@ open Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { - print_inductive : mutual_inductive -> std_ppcmds; - print_constant_with_infos : constant -> std_ppcmds; - print_section_variable : variable -> std_ppcmds; - print_syntactic_def : kernel_name -> std_ppcmds; - print_module : bool -> Names.module_path -> std_ppcmds; - print_modtype : module_path -> std_ppcmds; - print_named_decl : Context.Named.Declaration.t -> std_ppcmds; - print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; - print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds; + print_inductive : mutual_inductive -> Pp.t; + print_constant_with_infos : constant -> Pp.t; + print_section_variable : variable -> Pp.t; + print_syntactic_def : kernel_name -> Pp.t; + print_module : bool -> Names.module_path -> Pp.t; + print_modtype : module_path -> Pp.t; + print_named_decl : Context.Named.Declaration.t -> Pp.t; + print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; + print_context : bool -> int option -> Lib.library_segment -> Pp.t; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } let gallina_print_module = print_module diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 4add21fa7..f4277b6c5 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Environ open Reductionops @@ -19,57 +18,57 @@ open Misctypes val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref -val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds -val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option -val print_full_context : unit -> std_ppcmds -val print_full_context_typ : unit -> std_ppcmds -val print_full_pure_context : unit -> std_ppcmds -val print_sec_context : reference -> std_ppcmds -val print_sec_context_typ : reference -> std_ppcmds -val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> std_ppcmds -val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds +val print_context : bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option +val print_full_context : unit -> Pp.t +val print_full_context_typ : unit -> Pp.t +val print_full_pure_context : unit -> Pp.t +val print_sec_context : reference -> Pp.t +val print_sec_context_typ : reference -> Pp.t +val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t +val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> - Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds + Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : reference or_by_notation -> std_ppcmds -val print_opaque_name : reference -> std_ppcmds -val print_about : reference or_by_notation -> std_ppcmds -val print_impargs : reference or_by_notation -> std_ppcmds +val print_name : reference or_by_notation -> Pp.t +val print_opaque_name : reference -> Pp.t +val print_about : reference or_by_notation -> Pp.t +val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : unit -> std_ppcmds -val print_classes : unit -> std_ppcmds -val print_coercions : unit -> std_ppcmds -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds -val print_canonical_projections : unit -> std_ppcmds +val print_graph : unit -> Pp.t +val print_classes : unit -> Pp.t +val print_coercions : unit -> Pp.t +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_canonical_projections : unit -> Pp.t (** Pretty-printing functions for type classes and instances *) -val print_typeclasses : unit -> std_ppcmds -val print_instances : global_reference -> std_ppcmds -val print_all_instances : unit -> std_ppcmds +val print_typeclasses : unit -> Pp.t +val print_instances : global_reference -> Pp.t +val print_all_instances : unit -> Pp.t -val inspect : int -> std_ppcmds +val inspect : int -> Pp.t (** Locate *) -val print_located_qualid : reference -> std_ppcmds -val print_located_term : reference -> std_ppcmds -val print_located_tactic : reference -> std_ppcmds -val print_located_module : reference -> std_ppcmds +val print_located_qualid : reference -> Pp.t +val print_located_term : reference -> Pp.t +val print_located_tactic : reference -> Pp.t +val print_located_module : reference -> Pp.t type object_pr = { - print_inductive : mutual_inductive -> std_ppcmds; - print_constant_with_infos : constant -> std_ppcmds; - print_section_variable : variable -> std_ppcmds; - print_syntactic_def : kernel_name -> std_ppcmds; - print_module : bool -> Names.module_path -> std_ppcmds; - print_modtype : module_path -> std_ppcmds; - print_named_decl : Context.Named.Declaration.t -> std_ppcmds; - print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; - print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; - print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds + print_inductive : mutual_inductive -> Pp.t; + print_constant_with_infos : constant -> Pp.t; + print_section_variable : variable -> Pp.t; + print_syntactic_def : kernel_name -> Pp.t; + print_module : bool -> Names.module_path -> Pp.t; + print_modtype : module_path -> Pp.t; + print_named_decl : Context.Named.Declaration.t -> Pp.t; + print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; + print_context : bool -> int option -> Lib.library_segment -> Pp.t; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; + print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t } val set_object_pr : object_pr -> unit diff --git a/printing/printer.ml b/printing/printer.ml index 351678802..c6cf2254f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -727,7 +727,7 @@ let default_pr_subgoals ?(pr_first=true) match goals with | [] -> begin - let exl = Evarutil.non_instantiated sigma in + let exl = Evd.undefined_map sigma in if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else @@ -758,9 +758,9 @@ let default_pr_subgoals ?(pr_first=true) type printer_pr = { - pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds; - pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; - pr_goal : goal sigma -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoal : int -> evar_map -> goal list -> Pp.t; + pr_goal : goal sigma -> Pp.t; } let default_printer_pr = { diff --git a/printing/printer.mli b/printing/printer.mli index f8685b089..2c9a4d70e 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Globnames open Term @@ -25,96 +24,96 @@ val enable_goal_names_printing : bool ref (** Terms *) -val pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds -val pr_lconstr : constr -> std_ppcmds -val pr_lconstr_goal_style_env : env -> evar_map -> constr -> std_ppcmds +val pr_lconstr_env : env -> evar_map -> constr -> Pp.t +val pr_lconstr : constr -> Pp.t +val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t -val pr_constr_env : env -> evar_map -> constr -> std_ppcmds -val pr_constr : constr -> std_ppcmds -val pr_constr_goal_style_env : env -> evar_map -> constr -> std_ppcmds +val pr_constr_env : env -> evar_map -> constr -> Pp.t +val pr_constr : constr -> Pp.t +val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" in case of remaining issues (such as reference not in env). *) -val safe_pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds -val safe_pr_lconstr : constr -> std_ppcmds +val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t +val safe_pr_lconstr : constr -> Pp.t -val safe_pr_constr_env : env -> evar_map -> constr -> std_ppcmds -val safe_pr_constr : constr -> std_ppcmds +val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t +val safe_pr_constr : constr -> Pp.t -val pr_econstr_env : env -> evar_map -> EConstr.t -> std_ppcmds -val pr_econstr : EConstr.t -> std_ppcmds -val pr_leconstr_env : env -> evar_map -> EConstr.t -> std_ppcmds -val pr_leconstr : EConstr.t -> std_ppcmds +val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t +val pr_econstr : EConstr.t -> Pp.t +val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t +val pr_leconstr : EConstr.t -> Pp.t -val pr_etype_env : env -> evar_map -> EConstr.types -> std_ppcmds -val pr_letype_env : env -> evar_map -> EConstr.types -> std_ppcmds +val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t +val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t -val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds -val pr_open_constr : open_constr -> std_ppcmds +val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t +val pr_open_constr : open_constr -> Pp.t -val pr_open_lconstr_env : env -> evar_map -> open_constr -> std_ppcmds -val pr_open_lconstr : open_constr -> std_ppcmds +val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t +val pr_open_lconstr : open_constr -> Pp.t -val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds -val pr_constr_under_binders : constr_under_binders -> std_ppcmds +val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t +val pr_constr_under_binders : constr_under_binders -> Pp.t -val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds -val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds +val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t +val pr_lconstr_under_binders : constr_under_binders -> Pp.t -val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> std_ppcmds -val pr_ltype_env : env -> evar_map -> types -> std_ppcmds -val pr_ltype : types -> std_ppcmds +val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t +val pr_ltype_env : env -> evar_map -> types -> Pp.t +val pr_ltype : types -> Pp.t -val pr_type_env : env -> evar_map -> types -> std_ppcmds -val pr_type : types -> std_ppcmds +val pr_type_env : env -> evar_map -> types -> Pp.t +val pr_type : types -> Pp.t -val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> std_ppcmds -val pr_closed_glob : closed_glob_constr -> std_ppcmds +val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t +val pr_closed_glob : closed_glob_constr -> Pp.t -val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds -val pr_ljudge : EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t +val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_lglob_constr_env : env -> glob_constr -> std_ppcmds -val pr_lglob_constr : glob_constr -> std_ppcmds +val pr_lglob_constr_env : env -> glob_constr -> Pp.t +val pr_lglob_constr : glob_constr -> Pp.t -val pr_glob_constr_env : env -> glob_constr -> std_ppcmds -val pr_glob_constr : glob_constr -> std_ppcmds +val pr_glob_constr_env : env -> glob_constr -> Pp.t +val pr_glob_constr : glob_constr -> Pp.t -val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds -val pr_lconstr_pattern : constr_pattern -> std_ppcmds +val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t +val pr_lconstr_pattern : constr_pattern -> Pp.t -val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds -val pr_constr_pattern : constr_pattern -> std_ppcmds +val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t +val pr_constr_pattern : constr_pattern -> Pp.t -val pr_cases_pattern : cases_pattern -> std_ppcmds +val pr_cases_pattern : cases_pattern -> Pp.t -val pr_sort : evar_map -> sorts -> std_ppcmds +val pr_sort : evar_map -> sorts -> Pp.t (** Universe constraints *) -val pr_polymorphic : bool -> std_ppcmds -val pr_cumulative : bool -> bool -> std_ppcmds -val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds -val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds -val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> std_ppcmds +val pr_polymorphic : bool -> Pp.t +val pr_cumulative : bool -> bool -> Pp.t +val pr_universe_instance : evar_map -> Univ.universe_context -> Pp.t +val pr_universe_ctx : evar_map -> Univ.universe_context -> Pp.t +val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> Pp.t (** Printing global references using names as short as possible *) -val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds -val pr_global : global_reference -> std_ppcmds +val pr_global_env : Id.Set.t -> global_reference -> Pp.t +val pr_global : global_reference -> Pp.t -val pr_constant : env -> constant -> std_ppcmds -val pr_existential_key : evar_map -> existential_key -> std_ppcmds -val pr_existential : env -> evar_map -> existential -> std_ppcmds -val pr_constructor : env -> constructor -> std_ppcmds -val pr_inductive : env -> inductive -> std_ppcmds -val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds +val pr_constant : env -> constant -> Pp.t +val pr_existential_key : evar_map -> existential_key -> Pp.t +val pr_existential : env -> evar_map -> existential -> Pp.t +val pr_constructor : env -> constructor -> Pp.t +val pr_inductive : env -> inductive -> Pp.t +val pr_evaluable_reference : evaluable_global_reference -> Pp.t -val pr_pconstant : env -> pconstant -> std_ppcmds -val pr_pinductive : env -> pinductive -> std_ppcmds -val pr_pconstructor : env -> pconstructor -> std_ppcmds +val pr_pconstant : env -> pconstant -> Pp.t +val pr_pinductive : env -> pinductive -> Pp.t +val pr_pconstructor : env -> pconstructor -> Pp.t (** Contexts *) @@ -122,29 +121,29 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds val set_compact_context : bool -> unit val get_compact_context : unit -> bool -val pr_context_unlimited : env -> evar_map -> std_ppcmds -val pr_ne_context_of : std_ppcmds -> env -> evar_map -> std_ppcmds +val pr_context_unlimited : env -> evar_map -> Pp.t +val pr_ne_context_of : Pp.t -> env -> evar_map -> Pp.t -val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds -val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> std_ppcmds -val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds +val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> Pp.t +val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t +val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t -val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds -val pr_named_context_of : env -> evar_map -> std_ppcmds -val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds -val pr_rel_context_of : env -> evar_map -> std_ppcmds -val pr_context_of : env -> evar_map -> std_ppcmds +val pr_named_context : env -> evar_map -> Context.Named.t -> Pp.t +val pr_named_context_of : env -> evar_map -> Pp.t +val pr_rel_context : env -> evar_map -> Context.Rel.t -> Pp.t +val pr_rel_context_of : env -> evar_map -> Pp.t +val pr_context_of : env -> evar_map -> Pp.t (** Predicates *) -val pr_predicate : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds -val pr_cpred : Cpred.t -> std_ppcmds -val pr_idpred : Id.Pred.t -> std_ppcmds -val pr_transparent_state : transparent_state -> std_ppcmds +val pr_predicate : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t +val pr_cpred : Cpred.t -> Pp.t +val pr_idpred : Id.Pred.t -> Pp.t +val pr_transparent_state : transparent_state -> Pp.t (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) -val pr_goal : goal sigma -> std_ppcmds +val pr_goal : goal sigma -> Pp.t (** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals] prints the goals of the list [goals] followed by the goals in @@ -155,25 +154,25 @@ val pr_goal : goal sigma -> std_ppcmds focused goals unless the conrresponding option [enable_unfocused_goal_printing] is set. [seeds] is for printing dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list - -> goal list -> goal list -> std_ppcmds +val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list + -> goal list -> goal list -> Pp.t -val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds -val pr_concl : int -> evar_map -> goal -> std_ppcmds +val pr_subgoal : int -> evar_map -> goal list -> Pp.t +val pr_concl : int -> evar_map -> goal -> Pp.t -val pr_open_subgoals : ?proof:Proof.proof -> unit -> std_ppcmds -val pr_nth_open_subgoal : int -> std_ppcmds -val pr_evar : evar_map -> (evar * evar_info) -> std_ppcmds -val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds -val pr_evars : evar_map -> evar_info Evar.Map.t -> std_ppcmds -val pr_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map -> - Evar.Set.t -> std_ppcmds +val pr_open_subgoals : ?proof:Proof.proof -> unit -> Pp.t +val pr_nth_open_subgoal : int -> Pp.t +val pr_evar : evar_map -> (evar * evar_info) -> Pp.t +val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t +val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> + Evar.Set.t -> Pp.t -val pr_prim_rule : prim_rule -> std_ppcmds +val pr_prim_rule : prim_rule -> Pp.t (** Backwards compatibility *) -val prterm : constr -> std_ppcmds (** = pr_lconstr *) +val prterm : constr -> Pp.t (** = pr_lconstr *) (** Declarations for the "Print Assumption" command *) @@ -193,15 +192,15 @@ module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet val pr_assumptionset : - env -> Term.types ContextObjectMap.t -> std_ppcmds + env -> Term.types ContextObjectMap.t -> Pp.t -val pr_goal_by_id : Id.t -> std_ppcmds -val pr_goal_by_uid : string -> std_ppcmds +val pr_goal_by_id : Id.t -> Pp.t +val pr_goal_by_uid : string -> Pp.t type printer_pr = { - pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds; - pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; - pr_goal : goal sigma -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoal : int -> evar_map -> goal list -> Pp.t; + pr_goal : goal sigma -> Pp.t; };; val set_printer_pr : printer_pr -> unit diff --git a/printing/printmod.mli b/printing/printmod.mli index 81b577453..8c3f0149e 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -6,12 +6,11 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names (** false iff the module is an element of an open module type *) val printable_body : DirPath.t -> bool -val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds -val print_module : bool -> module_path -> std_ppcmds -val print_modtype : module_path -> std_ppcmds +val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> Pp.t +val print_module : bool -> module_path -> Pp.t +val print_modtype : module_path -> Pp.t diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 26c6e6014..9c69995f4 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -112,7 +112,7 @@ exception NotExtensibleClause val clenv_push_prod : clausenv -> clausenv (** {6 Pretty-print (debug only) } *) -val pr_clenv : clausenv -> Pp.std_ppcmds +val pr_clenv : clausenv -> Pp.t (** {6 Evar-based clauses} *) diff --git a/proofs/goal.mli b/proofs/goal.mli index cd71d11f8..6d3ec8bd4 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -20,7 +20,7 @@ val uid : goal -> string val get_by_uid : string -> goal (* Debugging help *) -val pr_goal : goal -> Pp.std_ppcmds +val pr_goal : goal -> Pp.t (* Layer to implement v8.2 tactic engine ontop of the new architecture. Types are different from what they used to be due to a change of the diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli index 21d410c7b..b75718cd0 100644 --- a/proofs/miscprint.mli +++ b/proofs/miscprint.mli @@ -11,27 +11,27 @@ open Misctypes (** Printing of [intro_pattern] *) val pr_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a intro_pattern_expr Loc.located -> Pp.t val pr_or_and_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t -val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds +val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.t (** Printing of [move_location] *) val pr_move_location : - ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds + ('a -> Pp.t) -> 'a move_location -> Pp.t val pr_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a bindings -> Pp.t val pr_bindings_no_with : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a bindings -> Pp.t val pr_with_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds + ('a -> Pp.t) -> + ('a -> Pp.t) -> 'a * 'a bindings -> Pp.t diff --git a/proofs/proof.mli b/proofs/proof.mli index 1865382e4..698aa48b0 100644 --- a/proofs/proof.mli +++ b/proofs/proof.mli @@ -182,7 +182,7 @@ val in_proof : proof -> (Evd.evar_map -> 'a) -> 'a focused goals. *) val unshelve : proof -> proof -val pr_proof : proof -> Pp.std_ppcmds +val pr_proof : proof -> Pp.t (*** Compatibility layer with <=v8.2 ***) module V82 : sig diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli index 9ae521d3f..9e924fec9 100644 --- a/proofs/proof_bullet.mli +++ b/proofs/proof_bullet.mli @@ -48,6 +48,6 @@ val suggest : proof -> Pp.t (* *) (**********************************************************) -val pr_goal_selector : Vernacexpr.goal_selector -> Pp.std_ppcmds +val pr_goal_selector : Vernacexpr.goal_selector -> Pp.t val get_default_goal_selector : unit -> Vernacexpr.goal_selector diff --git a/proofs/refine.mli b/proofs/refine.mli index 20f5a0791..3b0a9e5b6 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -17,7 +17,7 @@ open Proofview (** Printer used to print the constr which refine refines. *) val pr_constr : - (Environ.env -> Evd.evar_map -> Term.constr -> Pp.std_ppcmds) Hook.t + (Environ.env -> Evd.evar_map -> Term.constr -> Pp.t) Hook.t (** {7 Refinement primitives} *) diff --git a/proofs/refiner.ml b/proofs/refiner.ml index f1b1cd359..3e3313eb5 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -63,7 +63,7 @@ let tclIDTAC_MESSAGE s gls = let tclFAIL_s s gls = user_err ~hdr:"Refiner.tclFAIL_s" (str s) (* A special exception for levels for the Fail tactic *) -exception FailError of int * std_ppcmds Lazy.t +exception FailError of int * Pp.t Lazy.t (* The Fail tactic *) let tclFAIL lvl s g = raise (FailError (lvl,lazy s)) diff --git a/proofs/refiner.mli b/proofs/refiner.mli index aac10e81b..3ff010fe3 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -31,7 +31,7 @@ val refiner : rule -> tactic (** [tclIDTAC] is the identity tactic without message printing*) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : Pp.std_ppcmds -> tactic +val tclIDTAC_MESSAGE : Pp.t -> tactic (** [tclEVARS sigma] changes the current evar map *) val tclEVARS : evar_map -> tactic @@ -100,7 +100,7 @@ val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENFIRSTn : tactic -> tactic array -> tactic (** A special exception for levels for the Fail tactic *) -exception FailError of int * Pp.std_ppcmds Lazy.t +exception FailError of int * Pp.t Lazy.t (** Takes an exception and either raise it at the next level or do nothing. *) @@ -116,8 +116,8 @@ val tclTRY : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> Pp.std_ppcmds -> tactic -val tclFAIL_lazy : int -> Pp.std_ppcmds Lazy.t -> tactic +val tclFAIL : int -> Pp.t -> tactic +val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 2b7c36594..40b6573a1 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -94,8 +94,8 @@ val internal_cut_rev : bool -> Id.t -> types -> tactic val refine : constr -> tactic (** {6 Pretty-printing functions (debug only). } *) -val pr_gls : goal sigma -> Pp.std_ppcmds -val pr_glls : goal list sigma -> Pp.std_ppcmds +val pr_gls : goal sigma -> Pp.t +val pr_glls : goal list sigma -> Pp.t (* Variants of [Tacmach] functions built with the new proof engine *) module New : sig diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml index 25f9d7c18..9c58df5b2 100644 --- a/stm/asyncTaskQueue.ml +++ b/stm/asyncTaskQueue.ml @@ -123,7 +123,7 @@ module Make(T : Task) = struct "-worker-id"; name; "-async-proofs-worker-priority"; Flags.string_of_priority !Flags.async_proofs_worker_priority] - | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl + | ("-ideslave"|"-emacs"|"-batch")::tl -> set_slave_opt tl | ("-async-proofs" |"-toploop" |"-vio2vo" |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv" |"-compile" |"-compile-verbose" diff --git a/stm/stm.ml b/stm/stm.ml index 7c9620854..3386044f2 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1133,7 +1133,7 @@ let record_pb_time ?loc proof_name time = hints := Aux_file.set !hints proof_name proof_build_time end -exception RemoteException of Pp.std_ppcmds +exception RemoteException of Pp.t let _ = CErrors.register_handler (function | RemoteException ppcmd -> ppcmd | _ -> raise Unhandled) @@ -1274,7 +1274,7 @@ end = struct (* {{{ *) type error = { e_error_at : Stateid.t; e_safe_id : Stateid.t; - e_msg : Pp.std_ppcmds; + e_msg : Pp.t; e_safe_states : Stateid.t list } type response = @@ -1711,7 +1711,7 @@ end = struct (* {{{ *) type response = | RespBuiltSubProof of (Constr.constr * Evd.evar_universe_context) - | RespError of Pp.std_ppcmds + | RespError of Pp.t | RespNoProgress let name = ref "tacworker" diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli index 306ff1868..edbb7c6b7 100644 --- a/tactics/autorewrite.mli +++ b/tactics/autorewrite.mli @@ -40,7 +40,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic -val print_rewrite_hintdb : string -> Pp.std_ppcmds +val print_rewrite_hintdb : string -> Pp.t open Clenv diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3fc2fc31b..371debede 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -621,7 +621,7 @@ module V85 = struct type autoinfo = { hints : hint_db; is_evar: existential_key option; only_classes: bool; unique : bool; - auto_depth: int list; auto_last_tac: std_ppcmds Lazy.t; + auto_depth: int list; auto_last_tac: Pp.t Lazy.t; auto_path : global_reference option list; auto_cut : hints_path } type autogoal = goal * autoinfo @@ -972,7 +972,7 @@ end module Search = struct type autoinfo = { search_depth : int list; - last_tac : Pp.std_ppcmds Lazy.t; + last_tac : Pp.t Lazy.t; search_dep : bool; search_only_classes : bool; search_cut : hints_path; @@ -1460,7 +1460,6 @@ let is_mandatory p comp evd = (** In case of unsatisfiable constraints, build a nice error message *) let error_unresolvable env comp evd = - let evd = Evarutil.nf_evar_map_undefined evd in let is_part ev = match comp with | None -> true | Some s -> Evar.Set.mem ev s @@ -1474,8 +1473,7 @@ let error_unresolvable env comp evd = else (found, accu) in let (_, ev) = Evd.fold_undefined fold evd (true, None) in - Pretype_errors.unsatisfiable_constraints - (Evarutil.nf_env_evar evd env) evd ev comp + Pretype_errors.unsatisfiable_constraints env evd ev comp (** Check if an evar is concerned by the current resolution attempt, (and in particular is in the current component), and also update diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 64d4d3135..65864bd47 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -203,7 +203,7 @@ type search_state = { priority : int; depth : int; (*r depth of search before failing *) tacres : goal list sigma; - last_tactic : std_ppcmds Lazy.t; + last_tactic : Pp.t Lazy.t; dblist : hint_db list; localdb : hint_db list; prev : prev_search_state; diff --git a/tactics/hints.mli b/tactics/hints.mli index 6325a4470..44e5370e9 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Util open Names open EConstr @@ -85,10 +84,10 @@ type hints_path = global_reference hints_path_gen val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool val path_derivate : hints_path -> hints_path_atom -> hints_path -val pp_hints_path_gen : ('a -> Pp.std_ppcmds) -> 'a hints_path_gen -> Pp.std_ppcmds -val pp_hints_path_atom : ('a -> Pp.std_ppcmds) -> 'a hints_path_atom_gen -> Pp.std_ppcmds -val pp_hints_path : hints_path -> Pp.std_ppcmds -val pp_hint_mode : hint_mode -> Pp.std_ppcmds +val pp_hints_path_gen : ('a -> Pp.t) -> 'a hints_path_gen -> Pp.t +val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t +val pp_hints_path : hints_path -> Pp.t +val pp_hint_mode : hint_mode -> Pp.t val glob_hints_path_atom : Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen val glob_hints_path : @@ -261,12 +260,12 @@ val rewrite_db : hint_db_name (** Printing hints *) -val pr_searchtable : unit -> std_ppcmds -val pr_applicable_hint : unit -> std_ppcmds -val pr_hint_ref : global_reference -> std_ppcmds -val pr_hint_db_by_name : hint_db_name -> std_ppcmds -val pr_hint_db : Hint_db.t -> std_ppcmds -val pr_hint : hint -> Pp.std_ppcmds +val pr_searchtable : unit -> Pp.t +val pr_applicable_hint : unit -> Pp.t +val pr_hint_ref : global_reference -> Pp.t +val pr_hint_db_by_name : hint_db_name -> Pp.t +val pr_hint_db : Hint_db.t -> Pp.t +val pr_hint : hint -> Pp.t (** Hook for changing the initialization of auto *) diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 005555caa..f825c4f4a 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -48,4 +48,4 @@ val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant val check_scheme : 'a scheme_kind -> inductive -> bool -val pr_scheme_kind : 'a scheme_kind -> Pp.std_ppcmds +val pr_scheme_kind : 'a scheme_kind -> Pp.t diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 4ad9c6541..2a04c413b 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Term open EConstr @@ -19,7 +18,7 @@ open Tactypes (** Tacticals i.e. functions from tactics to tactics. *) val tclIDTAC : tactic -val tclIDTAC_MESSAGE : std_ppcmds -> tactic +val tclIDTAC_MESSAGE : Pp.t -> tactic val tclORELSE0 : tactic -> tactic -> tactic val tclORELSE : tactic -> tactic -> tactic val tclTHEN : tactic -> tactic -> tactic @@ -41,8 +40,8 @@ val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic -val tclFAIL : int -> std_ppcmds -> tactic -val tclFAIL_lazy : int -> std_ppcmds Lazy.t -> tactic +val tclFAIL : int -> Pp.t -> tactic +val tclFAIL_lazy : int -> Pp.t Lazy.t -> tactic val tclDO : int -> tactic -> tactic val tclPROGRESS : tactic -> tactic val tclSHOWHYPS : tactic -> tactic @@ -160,9 +159,9 @@ module New : sig (* [tclFAIL n msg] fails with [msg] as an error message at level [n] (meaning that it will jump over [n] error catching tacticals FROM THIS MODULE. *) - val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic + val tclFAIL : int -> Pp.t -> 'a tactic - val tclZEROMSG : ?loc:Loc.t -> Pp.std_ppcmds -> 'a tactic + val tclZEROMSG : ?loc:Loc.t -> Pp.t -> 'a tactic (** Fail with a [User_Error] containing the given message. *) val tclOR : unit tactic -> unit tactic -> unit tactic diff --git a/tactics/tactics.ml b/tactics/tactics.ml index cb905e749..82d58074b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2979,7 +2979,7 @@ let specialize (c,lbind) ipat = sigma,hd' | _ ,_ -> assert false in let sigma,hd = rebuild_lambdas sigma (List.rev lprod) [] c_hd tstack in - sigma, hd + Evd.clear_metas sigma, hd in let typ = Retyping.get_type_of env sigma term in let tac = diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index e90e1959e..64ba38a51 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -49,7 +49,7 @@ struct | DNil (* debug *) - let _pr_dconstr f : 'a t -> std_ppcmds = function + let _pr_dconstr f : 'a t -> Pp.t = function | DRel -> str "*" | DSort -> str "Sort" | DRef _ -> str "Ref" diff --git a/test-suite/bugs/closed/2141.v b/test-suite/bugs/closed/2141.v index 098a7e9e7..c556ff0b2 100644 --- a/test-suite/bugs/closed/2141.v +++ b/test-suite/bugs/closed/2141.v @@ -11,5 +11,6 @@ End FSetHide. Module NatSet' := FSetHide NatSet. Recursive Extraction NatSet'.fold. +Extraction TestCompile NatSet'.fold. (* Extraction "test2141.ml" NatSet'.fold. *)
\ No newline at end of file diff --git a/test-suite/bugs/closed/3287.v b/test-suite/bugs/closed/3287.v index 1b758acd7..4b3e7ff05 100644 --- a/test-suite/bugs/closed/3287.v +++ b/test-suite/bugs/closed/3287.v @@ -6,6 +6,7 @@ Definition bar := true. End Foo. Recursive Extraction Foo.bar. +Extraction TestCompile Foo.bar. Module Foo'. Definition foo := (I,I). @@ -13,10 +14,6 @@ Definition bar := true. End Foo'. Recursive Extraction Foo'.bar. +Extraction TestCompile Foo'.bar. -Module Foo''. -Definition foo := (I,I). -Definition bar := true. -End Foo''. - -Extraction Foo.bar. +Extraction Foo'.bar. diff --git a/test-suite/bugs/closed/3923.v b/test-suite/bugs/closed/3923.v index 2fb0a5439..1d9488c6e 100644 --- a/test-suite/bugs/closed/3923.v +++ b/test-suite/bugs/closed/3923.v @@ -33,3 +33,4 @@ Axiom empty_fieldstore : cert_fieldstore. End MkCertRuntimeTypes. Extraction MkCertRuntimeTypes. (* Was leading to an uncaught Not_found *) +Extraction TestCompile MkCertRuntimeTypes. diff --git a/test-suite/bugs/closed/4616.v b/test-suite/bugs/closed/4616.v index a59975dbc..d6660e355 100644 --- a/test-suite/bugs/closed/4616.v +++ b/test-suite/bugs/closed/4616.v @@ -2,5 +2,6 @@ Require Coq.extraction.Extraction. Set Primitive Projections. Record Foo' := Foo { foo : Type }. -Axiom f : forall t : Foo', foo t. +Definition f := forall t : Foo', foo t. Extraction f. +Extraction TestCompile f. diff --git a/test-suite/bugs/closed/4709.v b/test-suite/bugs/closed/4709.v new file mode 100644 index 000000000..a9edcc804 --- /dev/null +++ b/test-suite/bugs/closed/4709.v @@ -0,0 +1,18 @@ + +(** Bug 4709 https://coq.inria.fr/bug/4709 + Extraction wasn't reducing primitive projections in types. *) + +Require Extraction. + +Set Primitive Projections. + +Record t := Foo { foo : Type }. +Definition ty := foo (Foo nat). + +(* Without proper reduction of primitive projections in + [extract_type], the type [ty] was extracted as [Tunknown]. + Let's check it isn't the case anymore. *) + +Parameter check : nat. +Extract Constant check => "(O:ty)". +Extraction TestCompile ty check. diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v index 5d8ca330a..e792a3623 100644 --- a/test-suite/bugs/closed/4710.v +++ b/test-suite/bugs/closed/4710.v @@ -4,7 +4,6 @@ Set Primitive Projections. Record Foo' := Foo { foo : nat }. Extraction foo. Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }. -Extraction Language Ocaml. Extraction foo2p. Definition bla (x : Foo2 0) := foo2p _ x. @@ -12,3 +11,5 @@ Extraction bla. Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x. Extraction bla'. + +Extraction TestCompile foo foo2p bla bla'. diff --git a/test-suite/bugs/closed/4720.v b/test-suite/bugs/closed/4720.v index 9265b60c1..704331e78 100644 --- a/test-suite/bugs/closed/4720.v +++ b/test-suite/bugs/closed/4720.v @@ -44,3 +44,7 @@ Recursive Extraction WithMod. Recursive Extraction WithDef. Recursive Extraction WithModPriv. + +(* Let's even check that all this extracted code is actually compilable: *) + +Extraction TestCompile WithMod WithDef WithModPriv. diff --git a/test-suite/bugs/closed/5177.v b/test-suite/bugs/closed/5177.v index 231d103a5..7c8af1e46 100644 --- a/test-suite/bugs/closed/5177.v +++ b/test-suite/bugs/closed/5177.v @@ -19,3 +19,4 @@ End MakeA. Require Extraction. Recursive Extraction MakeA. +Extraction TestCompile MakeA. diff --git a/test-suite/bugs/closed/5315.v b/test-suite/bugs/closed/5315.v new file mode 100644 index 000000000..f1f1b8c05 --- /dev/null +++ b/test-suite/bugs/closed/5315.v @@ -0,0 +1,10 @@ +Require Import Recdef. + +Function dumb_works (a:nat) {struct a} := + match (fun x => x) a with O => O | S n' => dumb_works n' end. + +Function dumb_nope (a:nat) {struct a} := + match (id (fun x => x)) a with O => O | S n' => dumb_nope n' end. + +(* This check is just present to ensure Function worked well *) +Check R_dumb_nope_complete.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5671.v b/test-suite/bugs/closed/5671.v new file mode 100644 index 000000000..c9a085045 --- /dev/null +++ b/test-suite/bugs/closed/5671.v @@ -0,0 +1,7 @@ +(* Fixing Meta-unclean specialize *) + +Require Import Setoid. +Axiom a : forall x, x=0 -> True. +Lemma lem (x y1 y2:nat) (H:x=0) (H0:eq y1 y2) : y1 = y2. +specialize a with (1:=H). clear H x. intros _. +setoid_rewrite H0. diff --git a/test-suite/output/Notations3.out b/test-suite/output/Notations3.out index ffea0819a..a9ae74fd6 100644 --- a/test-suite/output/Notations3.out +++ b/test-suite/output/Notations3.out @@ -109,3 +109,9 @@ fun x : ?A => x === x : forall x : ?A, x = x where ?A : [x : ?A |- Type] (x cannot be used) +{0, 1} + : nat * nat +{0, 1, 2} + : nat * (nat * nat) +{0, 1, 2, 3} + : nat * (nat * (nat * nat)) diff --git a/test-suite/output/Notations3.v b/test-suite/output/Notations3.v index 250aecafd..dee0f70f7 100644 --- a/test-suite/output/Notations3.v +++ b/test-suite/output/Notations3.v @@ -160,3 +160,11 @@ End Bug4765. Notation "x === x" := (eq_refl x) (only printing, at level 10). Check (fun x => eq_refl x). + +(**********************************************************************) +(* Test recursive notations with the recursive pattern repeated on the right *) + +Notation "{ x , .. , y , z }" := (pair x .. (pair y z) ..). +Check {0,1}. +Check {0,1,2}. +Check {0,1,2,3}. diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v index 4a509da89..0ee223250 100644 --- a/test-suite/success/extraction.v +++ b/test-suite/success/extraction.v @@ -545,47 +545,96 @@ Recursive Extraction test_proj. (*** TO SUM UP: ***) -(* Was previously producing a "test_extraction.ml" *) -Recursive Extraction - idnat id id' test2 test3 test4 test5 test6 test7 d d2 - d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 - test13 test19 test20 nat sumbool_rect c Finite tree - tree_size test14 test15 eta_c test16 test17 test18 bidon - tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 - tp1bis Truc oups test24 loop horibilis PropSet natbool - zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop - f_arity f_normal Boite boite1 boite2 test_boite Box box1 - zarb test_proj. +Module Everything. + Definition idnat := idnat. + Definition id := id. + Definition id' := id'. + Definition test2 := test2. + Definition test3 := test3. + Definition test4 := test4. + Definition test5 := test5. + Definition test6 := test6. + Definition test7 := test7. + Definition d := d. + Definition d2 := d2. + Definition d3 := d3. + Definition d4 := d4. + Definition d5 := d5. + Definition d6 := d6. + Definition test8 := test8. + Definition test9 := test9. + Definition test10 := test10. + Definition test11 := test11. + Definition test12 := test12. + Definition test13 := test13. + Definition test19 := test19. + Definition test20 := test20. + Definition nat := nat. + Definition sumbool_rect := sumbool_rect. + Definition c := c. + Definition Finite := Finite. + Definition tree := tree. + Definition tree_size := tree_size. + Definition test14 := test14. + Definition test15 := test15. + Definition eta_c := eta_c. + Definition test16 := test16. + Definition test17 := test17. + Definition test18 := test18. + Definition bidon := bidon. + Definition tb := tb. + Definition fbidon := fbidon. + Definition fbidon2 := fbidon2. + Definition test_0 := test_0. + Definition test_1 := test_1. + Definition eq_rect := eq_rect. + Definition tp1 := tp1. + Definition tp1bis := tp1bis. + Definition Truc := Truc. + Definition oups := oups. + Definition test24 := test24. + Definition loop := loop. + Definition horibilis := horibilis. + Definition PropSet := PropSet. + Definition natbool := natbool. + Definition zerotrue := zerotrue. + Definition zeroTrue := zeroTrue. + Definition zeroprop := zeroprop. + Definition test21 := test21. + Definition test22 := test22. + Definition test23 := test23. + Definition f := f. + Definition f_prop := f_prop. + Definition f_arity := f_arity. + Definition f_normal := f_normal. + Definition Boite := Boite. + Definition boite1 := boite1. + Definition boite2 := boite2. + Definition test_boite := test_boite. + Definition Box := Box. + Definition box1 := box1. + Definition zarb := zarb. + Definition test_proj := test_proj. +End Everything. + +(* Extraction "test_extraction.ml" Everything. *) +Recursive Extraction Everything. +(* Check that the previous OCaml code is compilable *) +Extraction TestCompile Everything. Extraction Language Haskell. -(* Was previously producing a "Test_extraction.hs" *) -Recursive Extraction - idnat id id' test2 test3 test4 test5 test6 test7 d d2 - d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 - test13 test19 test20 nat sumbool_rect c Finite tree - tree_size test14 test15 eta_c test16 test17 test18 bidon - tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 - tp1bis Truc oups test24 loop horibilis PropSet natbool - zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop - f_arity f_normal Boite boite1 boite2 test_boite Box box1 - zarb test_proj. +(* Extraction "Test_extraction.hs" Everything. *) +Recursive Extraction Everything. Extraction Language Scheme. -(* Was previously producing a "test_extraction.scm" *) -Recursive Extraction - idnat id id' test2 test3 test4 test5 test6 test7 d d2 - d3 d4 d5 d6 test8 id id' test9 test10 test11 test12 - test13 test19 test20 nat sumbool_rect c Finite tree - tree_size test14 test15 eta_c test16 test17 test18 bidon - tb fbidon fbidon2 fbidon2 test_0 test_1 eq eq_rect tp1 - tp1bis Truc oups test24 loop horibilis PropSet natbool - zerotrue zeroTrue zeroprop test21 test22 test23 f f_prop - f_arity f_normal Boite boite1 boite2 test_boite Box box1 - zarb test_proj. +(* Extraction "test_extraction.scm" Everything. *) +Recursive Extraction Everything. (*** Finally, a test more focused on everyday's life situations ***) Require Import ZArith. -Recursive Extraction two_or_two_plus_one Zdiv_eucl_exist. +Extraction Language Ocaml. +Recursive Extraction Z_modulo_2 Zdiv_eucl_exist. +Extraction TestCompile Z_modulo_2 Zdiv_eucl_exist. diff --git a/test-suite/success/extraction_dep.v b/test-suite/success/extraction_dep.v index e770cf779..fb0adabae 100644 --- a/test-suite/success/extraction_dep.v +++ b/test-suite/success/extraction_dep.v @@ -4,7 +4,7 @@ Require Coq.extraction.Extraction. (** NB: we should someday check the produced code instead of - simply running the commands. *) + extracting and just compiling. *) (** 1) Without signature ... *) @@ -20,6 +20,7 @@ End A. Definition testA := A.u + A.B.x. Recursive Extraction testA. (* without: v w *) +Extraction TestCompile testA. (** 1b) Same with an Include *) @@ -31,6 +32,7 @@ End Abis. Definition testAbis := Abis.u + Abis.y. Recursive Extraction testAbis. (* without: A B v w x *) +Extraction TestCompile testAbis. (** 2) With signature, we only keep elements mentionned in signature. *) @@ -46,3 +48,4 @@ End Ater. Definition testAter := Ater.u. Recursive Extraction testAter. (* with only: u v *) +Extraction TestCompile testAter. diff --git a/test-suite/success/extraction_impl.v b/test-suite/success/extraction_impl.v index 5bf807b1c..a38a688fb 100644 --- a/test-suite/success/extraction_impl.v +++ b/test-suite/success/extraction_impl.v @@ -2,7 +2,7 @@ (** Examples of extraction with manually-declared implicit arguments *) (** NB: we should someday check the produced code instead of - simply running the commands. *) + extracting and just compiling. *) Require Coq.extraction.Extraction. @@ -22,9 +22,11 @@ Proof. Defined. Recursive Extraction dnat_nat. +Extraction TestCompile dnat_nat. Extraction Implicit dnat_nat [n]. Recursive Extraction dnat_nat. +Extraction TestCompile dnat_nat. (** Same, with a Fixpoint *) @@ -35,9 +37,11 @@ Fixpoint dnat_nat' n (d:dnat n) := end. Recursive Extraction dnat_nat'. +Extraction TestCompile dnat_nat'. Extraction Implicit dnat_nat' [n]. Recursive Extraction dnat_nat'. +Extraction TestCompile dnat_nat'. (** Bug #4243, part 2 *) @@ -56,6 +60,7 @@ Defined. Extraction Implicit es [n]. Extraction Implicit enat_nat [n]. Recursive Extraction enat_nat. +Extraction TestCompile enat_nat. (** Same, with a Fixpoint *) @@ -67,6 +72,7 @@ Fixpoint enat_nat' n (e:enat n) : nat := Extraction Implicit enat_nat' [n]. Recursive Extraction enat_nat'. +Extraction TestCompile enat_nat'. (** Bug #4228 *) @@ -82,3 +88,4 @@ Extraction Implicit two_course [n]. End Food. Recursive Extraction Food.Meal. +Extraction TestCompile Food.Meal. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 789854b2d..576bdbf71 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -184,6 +184,7 @@ Definition term' (x : wrap nat) := let f := (@unwrap2 nat) in f x. Require Coq.extraction.Extraction. Recursive Extraction term term'. +Extraction TestCompile term term'. (*Unset Printing Primitive Projection Parameters.*) (* Primitive projections in the presence of let-ins (was not failing in beta3)*) diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index f1e519d03..3a8ca7b8d 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -170,7 +170,7 @@ COQMAKEFILE_VERSION:=@COQ_VERSION@ COQSRCLIBS?= $(foreach d,$(COQ_SRC_SUBDIRS), -I "$(COQLIB)$(d)") -CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) +CAMLFLAGS=$(OCAMLLIBS) $(COQSRCLIBS) -I $(CAMLP4LIB) $(OCAML_API_FLAGS) CAMLLIB:=$(shell "$(OCAMLFIND)" printconf stdlib) @@ -182,7 +182,7 @@ else CAMLP4EXTEND= endif -PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" compat5.cmo $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' +PP:=-pp '$(CAMLP4O) -I $(CAMLLIB) -I "$(COQLIB)/grammar" $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl' ifneq (,$(TIMING)) TIMING_ARG=-time diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 327f53520..0f38d1938 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -203,8 +203,12 @@ let generate_conf_coq_config oc args bypass_API = section oc "Coq configuration."; let src_dirs = if bypass_API then Coq_config.all_src_dirs - else Coq_config.api_dirs @ Coq_config.plugins_dirs @ ["-open API"] in + else Coq_config.api_dirs @ Coq_config.plugins_dirs in Envars.print_config ~prefix_var_name:"COQMF_" oc src_dirs; + if bypass_API then + Printf.fprintf oc "OCAML_API_FLAGS=\n" + else + Printf.fprintf oc "OCAML_API_FLAGS=-open API\n"; fprintf oc "COQMF_WINDRIVE=%s\n" (windrive Coq_config.coqlib) ;; diff --git a/tools/coqc.ml b/tools/coqc.ml index 5da203742..4595af6e8 100644 --- a/tools/coqc.ml +++ b/tools/coqc.ml @@ -86,16 +86,15 @@ let parse_args () = Envars.print_config stdout Coq_config.all_src_dirs; exit 0 - |"--print-version" :: _ -> + | ("-print-version" | "--print-version") :: _ -> Usage.machine_readable_version 0 (* Options for coqtop : a) options with 0 argument *) - | ("-notactics"|"-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" + | ("-bt"|"-debug"|"-nolib"|"-boot"|"-time"|"-profile-ltac" |"-batch"|"-noinit"|"-nois"|"-noglob"|"-no-glob" - |"-q"|"-full"|"-profile"|"-just-parsing"|"-echo" |"-unsafe"|"-quiet" - |"-silent"|"-m"|"-xml"|"-v7"|"-v8"|"-beautify"|"-strict-implicit" - |"-dont-load-proofs"|"-load-proofs"|"-force-load-proofs" + |"-q"|"-profile"|"-just-parsing"|"-echo" |"-quiet" + |"-silent"|"-m"|"-xml"|"-beautify"|"-strict-implicit" |"-impredicative-set"|"-vm"|"-native-compiler" |"-indices-matter"|"-quick"|"-type-in-type" |"-async-proofs-always-delegate"|"-async-proofs-never-reopen-branch" @@ -110,7 +109,7 @@ let parse_args () = |"-load-ml-source"|"-require"|"-load-ml-object" |"-init-file"|"-dump-glob"|"-compat"|"-coqlib"|"-top" |"-async-proofs-j" |"-async-proofs-private-flags" |"-async-proofs" |"-w" - |"-o"|"-profile-ltac-cutoff" + |"-o"|"-profile-ltac-cutoff" as o) :: rem -> begin match rem with diff --git a/tools/coqmktop.ml b/tools/coqmktop.ml index 30e098df5..28a3c791c 100644 --- a/tools/coqmktop.ml +++ b/tools/coqmktop.ml @@ -175,8 +175,6 @@ let parse_args () = | "-top" :: rem -> top := true ; parse (op,fl) rem | "-no-start" :: rem -> no_start:=true; parse (op, fl) rem | "-echo" :: rem -> echo := true ; parse (op,fl) rem - | ("-v8"|"-full" as o) :: rem -> - Printf.eprintf "warning: option %s deprecated\n" o; parse (op,fl) rem (* Extra options with arity 0 or 1, directly passed to ocamlc/ocamlopt *) | ("-noassert"|"-compact"|"-g"|"-p"|"-thread"|"-dtypes" as o) :: rem -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 515552fe7..8fe27b3b9 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -138,8 +138,6 @@ let set_toplevel_name dir = if Names.DirPath.is_empty dir then user_err Pp.(str "Need a non empty toplevel module name"); toplevel_name := dir -let remove_top_ml () = Mltop.remove () - let warn_deprecated_inputstate = CWarnings.create ~name:"deprecated-inputstate" ~category:"deprecated" (fun () -> strbrk "The inputstate option is deprecated and discouraged.") @@ -585,25 +583,10 @@ let parse_args arglist = |"-type-in-type" -> set_type_in_type () |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) - |"--print-version" -> Usage.machine_readable_version (exitcode ()) + |"-print-version"|"--print-version" -> Usage.machine_readable_version (exitcode ()) |"-where" -> print_where := true |"-xml" -> Flags.xml_export := true - (* Deprecated options *) - |"-byte" -> warning "option -byte deprecated, call with .byte suffix" - |"-opt" -> warning "option -opt deprecated, call with .opt suffix" - |"-full" -> warning "option -full deprecated" - |"-notactics" -> warning "Obsolete option \"-notactics\"."; remove_top_ml () - |"-emacs-U" -> - warning "Obsolete option \"-emacs-U\", use -emacs instead."; set_emacs () - |"-v7" -> user_err Pp.(str "This version of Coq does not support v7 syntax") - |"-v8" -> warning "Obsolete option \"-v8\"." - |"-lazy-load-proofs" -> warning "Obsolete option \"-lazy-load-proofs\"." - |"-dont-load-proofs" -> warning "Obsolete option \"-dont-load-proofs\"." - |"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"." - |"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ()) - |"-quality" -> warning "Obsolete option \"-quality\"." - (* Unknown option *) | s -> extras := s :: !extras end; diff --git a/toplevel/usage.ml b/toplevel/usage.ml index f8c7b114c..962bb4302 100644 --- a/toplevel/usage.ml +++ b/toplevel/usage.ml @@ -57,7 +57,7 @@ let print_usage_channel co command = \n -where print Coq's standard library location and exit\ \n -config, --config print Coq's configuration information and exit\ \n -v, --version print Coq version and exit\ -\n --print-version print Coq version in easy to parse format and exit\ +\n -print-version print Coq version in easy to parse format and exit\ \n -list-tags print highlight color tags known by Coq and exit\ \n\ \n -quiet unset display of extra information (implies -w \"-all\")\ diff --git a/vernac/explainErr.ml b/vernac/explainErr.ml index 793a4c580..2178a7caa 100644 --- a/vernac/explainErr.ml +++ b/vernac/explainErr.ml @@ -18,7 +18,7 @@ let guill s = str "\"" ++ str s ++ str "\"" (** Invariant : exceptions embedded in EvaluatedError satisfy Errors.noncritical *) -exception EvaluatedError of std_ppcmds * exn option +exception EvaluatedError of Pp.t * exn option (** Registration of generic errors Nota: explain_exn does NOT end with a newline anymore! diff --git a/vernac/explainErr.mli b/vernac/explainErr.mli index 944339d85..0cbd71fa4 100644 --- a/vernac/explainErr.mli +++ b/vernac/explainErr.mli @@ -7,7 +7,7 @@ (************************************************************************) (** Toplevel Exception *) -exception EvaluatedError of Pp.std_ppcmds * exn option +exception EvaluatedError of Pp.t * exn option (** Pre-explain a vernac interpretation error *) @@ -16,6 +16,6 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> Util.iexn -> Util.iexn (** General explain function. Should not be used directly now, see instead function [Errors.print] and variants *) -val explain_exn_default : exn -> Pp.std_ppcmds +val explain_exn_default : exn -> Pp.t -val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option Loc.located) option) -> unit +val register_additional_error_info : (Util.iexn -> (Pp.t option Loc.located) option) -> unit diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 784c6d338..0e5184905 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -783,7 +783,7 @@ let pr_constraints printenv env sigma evars cstrs = let explain_unsatisfiable_constraints env sigma constr comp = let (_, constraints) = Evd.extract_all_conv_pbs sigma in - let undef = Evd.undefined_map (Evarutil.nf_evar_map_undefined sigma) in + let undef = Evd.undefined_map sigma in (** Only keep evars that are subject to resolution and members of the given component. *) let is_kept evk evi = match comp with diff --git a/vernac/himsg.mli b/vernac/himsg.mli index b95ef8425..5b91f9e68 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -6,7 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Indtypes open Environ open Type_errors @@ -18,28 +17,28 @@ open Logic (** This module provides functions to explain the type errors. *) -val explain_type_error : env -> Evd.evar_map -> type_error -> std_ppcmds +val explain_type_error : env -> Evd.evar_map -> type_error -> Pp.t -val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> std_ppcmds +val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t -val explain_inductive_error : inductive_error -> std_ppcmds +val explain_inductive_error : inductive_error -> Pp.t -val explain_typeclass_error : env -> typeclass_error -> Pp.std_ppcmds +val explain_typeclass_error : env -> typeclass_error -> Pp.t -val explain_recursion_scheme_error : recursion_scheme_error -> std_ppcmds +val explain_recursion_scheme_error : recursion_scheme_error -> Pp.t -val explain_refiner_error : refiner_error -> std_ppcmds +val explain_refiner_error : refiner_error -> Pp.t val explain_pattern_matching_error : - env -> Evd.evar_map -> pattern_matching_error -> std_ppcmds + env -> Evd.evar_map -> pattern_matching_error -> Pp.t val explain_reduction_tactic_error : - Tacred.reduction_tactic_error -> std_ppcmds + Tacred.reduction_tactic_error -> Pp.t -val explain_module_error : Modops.module_typing_error -> std_ppcmds +val explain_module_error : Modops.module_typing_error -> Pp.t val explain_module_internalization_error : - Modintern.module_internalization_error -> std_ppcmds + Modintern.module_internalization_error -> Pp.t val map_pguard_error : ('c -> 'd) -> 'c pguard_error -> 'd pguard_error val map_ptype_error : ('c -> 'd) -> ('c, 'c) ptype_error -> ('d, 'd) ptype_error diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 567fc57fa..c0974d0a7 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -615,46 +615,71 @@ let define_keywords = function let distribute a ll = List.map (fun l -> a @ l) ll - (* Expand LIST1(t,sep) into the combination of t and t;sep;LIST1(t,sep) - as many times as expected in [n] argument *) -let rec expand_list_rule typ tkl x n i hds ll = - if Int.equal i n then + (* Expand LIST1(t,sep);sep;t;...;t (with the trailing pattern + occurring p times, possibly p=0) into the combination of + t;sep;t;...;t;sep;t (p+1 times) + t;sep;t;...;t;sep;t;sep;t (p+2 times) + ... + t;sep;t;...;t;sep;t;...;t;sep;t (p+n times) + t;sep;t;...;t;sep;t;...;t;sep;t;LIST1(t,sep) *) + +let expand_list_rule typ tkl x n p ll = + let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in + let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in + let tks = List.map (fun x -> GramConstrTerminal x) tkl in + let rec aux i hds ll = + if i < p then aux (i+1) (main :: tks @ hds) ll + else if Int.equal i (p+n) then let hds = - GramConstrListMark (n,true) :: hds + GramConstrListMark (p+n,true,p) :: hds @ [GramConstrNonTerminal (ETConstrList (typ,tkl), Some x)] in distribute hds ll else - let camlp4_message_name = Some (add_suffix x ("_"^string_of_int n)) in - let main = GramConstrNonTerminal (ETConstr typ, camlp4_message_name) in - let tks = List.map (fun x -> GramConstrTerminal x) tkl in - distribute (GramConstrListMark (i+1,false) :: hds @ [main]) ll @ - expand_list_rule typ tkl x n (i+1) (main :: tks @ hds) ll + distribute (GramConstrListMark (i+1,false,p) :: hds @ [main]) ll @ + aux (i+1) (main :: tks @ hds) ll in + aux 0 [] ll + +let is_constr_typ typ x etyps = + match List.assoc x etyps with + | ETConstr typ' -> typ = typ' + | _ -> false + +let include_possible_similar_trailing_pattern typ etyps sl l = + let rec aux n = function + | Terminal s :: sl, Terminal s'::l' when s = s' -> aux n (sl,l') + | [], NonTerminal x ::l' when is_constr_typ typ x etyps -> try_aux n l' + | _ -> raise Exit + and try_aux n l = + try aux (n+1) (sl,l) + with Exit -> n,l in + try_aux 0 l let make_production etyps symbols = - let prod = - List.fold_right - (fun t ll -> match t with - | NonTerminal m -> - let typ = List.assoc m etyps in - distribute [GramConstrNonTerminal (typ, Some m)] ll - | Terminal s -> - distribute [GramConstrTerminal (CLexer.terminal s)] ll - | Break _ -> - ll - | SProdList (x,sl) -> - let tkl = List.flatten - (List.map (function Terminal s -> [CLexer.terminal s] - | Break _ -> [] - | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in - match List.assoc x etyps with - | ETConstr typ -> expand_list_rule typ tkl x 1 0 [] ll - | ETBinder o -> - distribute - [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] ll - | _ -> - user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.")) - symbols [[]] in - List.map define_keywords prod + let rec aux = function + | [] -> [[]] + | NonTerminal m :: l -> + let typ = List.assoc m etyps in + distribute [GramConstrNonTerminal (typ, Some m)] (aux l) + | Terminal s :: l -> + distribute [GramConstrTerminal (CLexer.terminal s)] (aux l) + | Break _ :: l -> + aux l + | SProdList (x,sl) :: l -> + let tkl = List.flatten + (List.map (function Terminal s -> [CLexer.terminal s] + | Break _ -> [] + | _ -> anomaly (Pp.str "Found a non terminal token in recursive notation separator.")) sl) in + match List.assoc x etyps with + | ETConstr typ -> + let p,l' = include_possible_similar_trailing_pattern typ etyps sl l in + expand_list_rule typ tkl x 1 p (aux l') + | ETBinder o -> + distribute + [GramConstrNonTerminal (ETBinderList (o,tkl), Some x)] (aux l) + | _ -> + user_err Pp.(str "Components of recursive patterns in notation must be terms or binders.") in + let prods = aux symbols in + List.map define_keywords prods let rec find_symbols c_current c_next c_last = function | [] -> [] @@ -1056,7 +1081,7 @@ module SynData = struct extra : (string * string) list; (* XXX: Callback to printing, must remove *) - msgs : ((std_ppcmds -> unit) * std_ppcmds) list; + msgs : ((Pp.t -> unit) * Pp.t) list; (* Fields for internalization *) recvars : (Id.t * Id.t) list; diff --git a/vernac/metasyntax.mli b/vernac/metasyntax.mli index c9e37a4eb..9cd00cbcb 100644 --- a/vernac/metasyntax.mli +++ b/vernac/metasyntax.mli @@ -52,7 +52,7 @@ val add_syntactic_definition : Id.t -> Id.t list * constr_expr -> (** Print the Camlp4 state of a grammar *) -val pr_grammar : string -> Pp.std_ppcmds +val pr_grammar : string -> Pp.t type any_entry = AnyEntry : 'a Pcoq.Gram.entry -> any_entry diff --git a/vernac/mltop.mli b/vernac/mltop.mli index 3ecda656d..324a66d38 100644 --- a/vernac/mltop.mli +++ b/vernac/mltop.mli @@ -83,6 +83,6 @@ val declare_ml_modules : Vernacexpr.locality_flag -> string list -> unit (** {5 Utilities} *) -val print_ml_path : unit -> Pp.std_ppcmds -val print_ml_modules : unit -> Pp.std_ppcmds -val print_gc : unit -> Pp.std_ppcmds +val print_ml_path : unit -> Pp.t +val print_ml_modules : unit -> Pp.t +val print_gc : unit -> Pp.t diff --git a/vernac/obligations.mli b/vernac/obligations.mli index fa691ad1b..5614403ba 100644 --- a/vernac/obligations.mli +++ b/vernac/obligations.mli @@ -10,7 +10,6 @@ open Environ open Term open Evd open Names -open Pp open Globnames (* This is a hack to make it possible for Obligations to craft a Qed @@ -96,12 +95,12 @@ val try_solve_obligations : Names.Id.t option -> unit Proofview.tactic option -> val show_obligations : ?msg:bool -> Names.Id.t option -> unit -val show_term : Names.Id.t option -> std_ppcmds +val show_term : Names.Id.t option -> Pp.t val admit_obligations : Names.Id.t option -> unit exception NoObligations of Names.Id.t option -val explain_no_obligations : Names.Id.t option -> Pp.std_ppcmds +val explain_no_obligations : Names.Id.t option -> Pp.t val set_program_mode : bool -> unit diff --git a/vernac/topfmt.mli b/vernac/topfmt.mli index 6e006fc6c..afe76f6f8 100644 --- a/vernac/topfmt.mli +++ b/vernac/topfmt.mli @@ -37,8 +37,8 @@ val set_margin : int option -> unit val get_margin : unit -> int option (** Console display of feedback, we may add some location information *) -val std_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit -val emacs_logger : ?pre_hdr:Pp.std_ppcmds -> Feedback.level -> Pp.std_ppcmds -> unit +val std_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit +val emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit (** Color output *) val clear_styles : unit -> unit @@ -51,8 +51,8 @@ val init_terminal_output : color:bool -> unit (** Error printing *) (* To be deprecated when we can fully move to feedback-based error printing. *) -val pr_loc : Loc.t -> Pp.std_ppcmds -val print_err_exn : ?extra:Pp.std_ppcmds -> exn -> unit +val pr_loc : Loc.t -> Pp.t +val print_err_exn : ?extra:Pp.t -> exn -> unit (** [with_output_to_file file f x] executes [f x] with logging redirected to a file [file] *) diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 1556beb06..4f63ed6f4 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -65,7 +65,7 @@ let show_top_evars () = let pfts = Proof_global.give_me_the_proof () in let gls = Proof.V82.subgoals pfts in let sigma = gls.Evd.sigma in - Feedback.msg_notice (pr_evars_int sigma 1 (Evarutil.non_instantiated sigma)) + Feedback.msg_notice (pr_evars_int sigma 1 (Evd.undefined_map sigma)) let show_universes () = let pfts = Proof_global.give_me_the_proof () in @@ -2135,7 +2135,7 @@ let locate_if_not_already ?loc (e, info) = | Some l -> (e, info) exception HasNotFailed -exception HasFailed of std_ppcmds +exception HasFailed of Pp.t let with_fail b f = if not b then f () |