diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-06-12 16:20:15 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-06-12 16:43:33 +0200 |
| commit | 9097e9a84cf3841cd5fac81a7fe309ae2dec246f (patch) | |
| tree | 7358a5db6e5f6f17974cc61b4491248f30a332b4 | |
| parent | 013c0232953f1f5832c30940119da05847e99ce2 (diff) | |
| parent | b6feaafc7602917a8ef86fb8adc9651ff765e710 (diff) | |
Merge PR#718: API cleanup: aliases
85 files changed, 712 insertions, 632 deletions
diff --git a/API/API.mli b/API/API.mli index d844e8bf5..20a637c1f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -84,18 +84,19 @@ sig end type universe_context = UContext.t + [@@ocaml.deprecated "alias of API.Names.UContext.t"] module LSet : module type of struct include Univ.LSet end module ContextSet : sig type t = Univ.ContextSet.t val empty : t - val of_context : universe_context -> t - val to_context : t -> universe_context + val of_context : UContext.t -> t + val to_context : t -> UContext.t end type 'a in_universe_context_set = 'a * ContextSet.t - type 'a in_universe_context = 'a * universe_context + type 'a in_universe_context = 'a * UContext.t type constraint_type = Univ.constraint_type module Universe : @@ -105,7 +106,10 @@ sig end type universe_context_set = ContextSet.t + [@@ocaml.deprecated "alias of API.Names.ContextSet.t"] + type universe_set = LSet.t + [@@ocaml.deprecated "alias of API.Names.LSet.t"] type 'a constraint_function = 'a -> 'a -> Constraint.t -> Constraint.t type universe_subst = Univ.universe_subst @@ -156,11 +160,13 @@ sig type evaluable_global_reference = Names.evaluable_global_reference = | EvalVarRef of Id.t | EvalConstRef of Names.Constant.t + module Name : module type of struct include Names.Name end type name = Name.t = | Anonymous | Name of Id.t + [@@ocaml.deprecated "alias of API.Name.t"] module DirPath : sig @@ -212,6 +218,7 @@ sig end type kernel_name = KerName.t + [@@ocaml.deprecated "alias of API.Names.KerName.t"] module Constant : sig @@ -281,17 +288,19 @@ sig val cst_full_transparent_state : transparent_state val pr_kn : KerName.t -> Pp.std_ppcmds + [@@ocaml.deprecated "alias of API.Names.KerName.print"] val eq_constant : Constant.t -> Constant.t -> bool + [@@ocaml.deprecated "alias of API.Names.Constant.equal"] type module_path = ModPath.t = | MPfile of DirPath.t | MPbound of MBId.t - | MPdot of module_path * Label.t + | MPdot of ModPath.t * Label.t + [@@ocaml.deprecated "alias of API.Names.ModPath.t"] type variable = Id.t - - type constant = Constant.t + [@@ocaml.deprecated "alias of API.Names.Id.t"] type 'a tableKey = 'a Names.tableKey = | ConstKey of 'a @@ -299,46 +308,70 @@ sig | RelKey of Int.t val id_of_string : string -> Id.t + [@@ocaml.deprecated "alias of API.Names.Id.of_string"] val string_of_id : Id.t -> string + [@@ocaml.deprecated "alias of API.Names.Id.to_string"] type mutual_inductive = MutInd.t + [@@ocaml.deprecated "alias of API.Names.MutInd.t"] val eq_mind : MutInd.t -> MutInd.t -> bool + [@@ocaml.deprecated "alias of API.Names.MutInd.equal"] val repr_con : Constant.t -> ModPath.t * DirPath.t * Label.t + [@@ocaml.deprecated "alias of API.Names.Constant.repr3"] val repr_mind : MutInd.t -> ModPath.t * DirPath.t * Label.t + [@@ocaml.deprecated "alias of API.Names.MutInd.repr3"] val initial_path : ModPath.t + [@@ocaml.deprecated "alias of API.Names.ModPath.initial"] val con_label : Constant.t -> Label.t + [@@ocaml.deprecated "alias of API.Names.Constant.label"] val mind_label : MutInd.t -> Label.t + [@@ocaml.deprecated "alias of API.Names.MutInd.label"] val string_of_mp : ModPath.t -> string + [@@ocaml.deprecated "alias of API.Names.ModPath.to_string"] val mind_of_kn : KerName.t -> MutInd.t + [@@ocaml.deprecated "alias of API.Names.MutInd.make1"] + + type constant = Constant.t + [@@ocaml.deprecated "alias of API.Names.Constant.t"] val mind_modpath : MutInd.t -> ModPath.t + [@@ocaml.deprecated "alias of API.Names.MutInd.modpath"] val canonical_mind : MutInd.t -> KerName.t + [@@ocaml.deprecated "alias of API.Names.MutInd.canonical"] val user_mind : MutInd.t -> KerName.t + [@@ocaml.deprecated "alias of API.Names.MutInd.user"] val repr_kn : KerName.t -> ModPath.t * DirPath.t * Label.t + [@@ocaml.deprecated "alias of API.Names.KerName.repr"] val constant_of_kn : KerName.t -> Constant.t + [@@ocaml.deprecated "alias of API.Names.Constant.make1"] val user_con : Constant.t -> KerName.t + [@@ocaml.deprecated "alias of API.Names.Constant.user"] val modpath : KerName.t -> ModPath.t + [@@ocaml.deprecated "alias of API.Names.KerName.modpath"] val canonical_con : Constant.t -> KerName.t + [@@ocaml.deprecated "alias of API.Names.Constant.canonical"] val make_kn : ModPath.t -> DirPath.t -> Label.t -> KerName.t + [@@ocaml.deprecated "alias of API.Names.KerName.make"] 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 @@ -564,14 +597,16 @@ end module Term : sig type sorts_family = Sorts.family = InProp | InSet | InType + [@@deprecated "alias of API.Sorts.family"] type metavariable = Prelude.metavariable type contents = Sorts.contents = Pos | Null type sorts = Sorts.t = - | Prop of contents - | Type of Univ.Universe.t + | Prop of contents + | Type of Univ.Universe.t + [@@ocaml.deprecated "alias of API.Sorts.t"] type constr = Prelude.constr type types = Prelude.types @@ -632,7 +667,9 @@ sig type cofixpoint = int * rec_declaration val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term val applistc : constr -> constr list -> constr + val applist : constr * constr list -> constr + [@@ocaml.deprecated "(sort of an) alias of API.Term.applistc"] val mkArrow : types -> types -> constr val mkRel : int -> constr @@ -727,12 +764,16 @@ sig val kind_of_type : types -> (constr, types) kind_of_type val is_prop_sort : Sorts.t -> bool + [@@ocaml.deprecated "alias of API.Sorts.is_prop"] type existential_key = Prelude.evar val family_of_sort : Sorts.t -> Sorts.family + val compare : constr -> constr -> int + val constr_ord : constr -> constr -> int + [@@ocaml.deprecated "alias of API.Term.compare"] val destInd : constr -> Names.inductive puniverses val univ_of_sort : Sorts.t -> Univ.Universe.t @@ -1052,7 +1093,7 @@ sig mind_nparams_rec : int; mind_params_ctxt : Context.Rel.t; mind_polymorphic : bool; - mind_universes : Univ.universe_context; + mind_universes : Univ.UContext.t; mind_private : bool option; mind_typing_flags : Declarations.typing_flags; } @@ -1213,7 +1254,7 @@ sig const_entry_feedback : Stateid.t option; const_entry_type : Term.types option; const_entry_polymorphic : bool; - const_entry_universes : Univ.universe_context; + const_entry_universes : Univ.UContext.t; const_entry_opaque : bool; const_entry_inline_code : bool } type parameter_entry = Context.Named.t option * bool * Term.types Univ.in_universe_context * inline @@ -1415,7 +1456,7 @@ sig val evar_ident : Prelude.evar -> evar_map -> Names.Id.t option val extract_all_conv_pbs : evar_map -> evar_map * evar_constraint list val universe_context : ?names:(Names.Id.t Loc.located) list -> evar_map -> - (Names.Id.t * Univ.Level.t) list * Univ.universe_context + (Names.Id.t * Univ.Level.t) list * Univ.UContext.t val nf_constraints : evar_map -> evar_map val from_ctx : UState.t -> evar_map @@ -1460,10 +1501,13 @@ sig val evars_of_term : Term.constr -> Evar.Set.t val evar_universe_context_of : Univ.ContextSet.t -> UState.t + [@@ocaml.deprecated "alias of API.UState.of_context_set"] val evar_context_universe_context : UState.t -> Univ.UContext.t + [@@ocaml.deprecated "alias of API.UState.context"] type evar_universe_context = UState.t + [@@ocaml.deprecated "alias of API.UState.t"] val existential_opt_value : evar_map -> Term.existential -> Term.constr option val existential_value : evar_map -> Term.existential -> Term.constr @@ -1733,7 +1777,7 @@ sig val new_type_evar : Environ.env -> Evd.evar_map -> ?src:Evar_kinds.t Loc.located -> ?filter:Evd.Filter.t -> ?naming:Misctypes.intro_pattern_naming_expr -> ?principal:bool -> Evd.rigid -> - Evd.evar_map * (EConstr.constr * Term.sorts) + Evd.evar_map * (EConstr.constr * Sorts.t) val nf_evars_universes : Evd.evar_map -> Term.constr -> Term.constr val safe_evar_value : Evd.evar_map -> Term.existential -> Term.constr option val evd_comb1 : (Evd.evar_map -> 'b -> Evd.evar_map * 'a) -> Evd.evar_map ref -> 'b -> 'a @@ -1822,6 +1866,8 @@ sig val destConstructRef : Globnames.global_reference -> Names.constructor val reference_of_constr : Term.constr -> global_reference + [@@ocaml.deprecated "alias of API.Globnames.global_of_constr"] + val is_global : global_reference -> Term.constr -> bool end @@ -2588,7 +2634,7 @@ sig val unsafe_type_of_global : Globnames.global_reference -> Term.types val constr_of_global : Prelude.global_reference -> Term.constr val universes_of_constr : Term.constr -> Univ.LSet.t - val restrict_universe_context : Univ.universe_context_set -> Univ.universe_set -> Univ.universe_context_set + val restrict_universe_context : Univ.ContextSet.t -> Univ.LSet.t -> Univ.ContextSet.t val new_univ_level : Names.DirPath.t -> Univ.Level.t val unsafe_constr_of_global : Globnames.global_reference -> Term.constr Univ.in_universe_context val new_sort_in_family : Sorts.family -> Sorts.t @@ -2696,7 +2742,7 @@ sig Term.constr Univ.in_universe_context_set -> Names.Constant.t val definition_entry : ?fix_exn:Future.fix_exn -> ?opaque:bool -> ?inline:bool -> ?types:Term.types -> - ?poly:Decl_kinds.polymorphic -> ?univs:Univ.universe_context -> + ?poly:Decl_kinds.polymorphic -> ?univs:Univ.UContext.t -> ?eff:Safe_typing.private_constants -> Term.constr -> Safe_typing.private_constants Entries.definition_entry val definition_message : Names.Id.t -> unit val declare_variable : Names.Id.t -> variable_declaration -> Libnames.object_name @@ -3286,8 +3332,10 @@ end module Tacmach : sig type tactic = Proof_type.tactic + [@@ocaml.deprecated "alias for API.Proof_type.tactic"] type 'a sigma = 'a Evd.sigma + [@@ocaml.deprecated "alias of API.Evd.sigma"] val re_sig : 'a -> Evd.evar_map -> 'a Evd.sigma @@ -3325,21 +3373,21 @@ sig val pf_reduce : (Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr) -> Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr - val pf_conv_x : Proof_type.goal sigma -> EConstr.constr -> EConstr.constr -> bool + val pf_conv_x : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool - val pf_is_matching : Proof_type.goal sigma -> Pattern.constr_pattern -> EConstr.constr -> bool + val pf_is_matching : Proof_type.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool - val pf_hyps_types : Proof_type.goal sigma -> (Names.Id.t * EConstr.types) list + val pf_hyps_types : Proof_type.goal Evd.sigma -> (Names.Id.t * EConstr.types) list - val pr_gls : Proof_type.goal sigma -> Pp.std_ppcmds + val pr_gls : Proof_type.goal Evd.sigma -> Pp.std_ppcmds - val pf_nf_betaiota : Proof_type.goal sigma -> EConstr.constr -> EConstr.constr + val pf_nf_betaiota : Proof_type.goal Evd.sigma -> EConstr.constr -> EConstr.constr - val pf_last_hyp : Proof_type.goal sigma -> EConstr.named_declaration + val pf_last_hyp : Proof_type.goal Evd.sigma -> EConstr.named_declaration - val pf_nth_hyp_id : Proof_type.goal sigma -> int -> Names.Id.t + val pf_nth_hyp_id : Proof_type.goal Evd.sigma -> int -> Names.Id.t - val sig_it : 'a sigma -> 'a + val sig_it : 'a Evd.sigma -> 'a module New : sig @@ -3550,13 +3598,14 @@ sig val free_rels : Evd.evar_map -> EConstr.constr -> Int.Set.t val occur_term : Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool + [@@ocaml.deprecated "alias of API.Termops.dependent"] 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 : Evd.evar_universe_context -> Pp.std_ppcmds + val pr_evar_universe_context : UState.t -> Pp.std_ppcmds end module Locality : @@ -3812,6 +3861,7 @@ end module Ppconstr : sig val pr_name : Names.Name.t -> Pp.std_ppcmds + [@@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 @@ -4088,7 +4138,9 @@ sig val onLastHypId : (Names.Id.t -> tactic) -> tactic val onNthHypId : int -> (Names.Id.t -> tactic) -> tactic val onNLastHypsId : int -> (Names.Id.t list -> tactic) -> tactic + val tclTHENSEQ : tactic list -> tactic + [@@ocaml.deprecated "alias of API.Tacticals.tclTHENLIST"] val nLastDecls : int -> Proof_type.goal Evd.sigma -> EConstr.named_context @@ -4274,7 +4326,7 @@ sig | Res_pf_THEN_trivial_fail of 'a | Unfold_nth of Names.evaluable_global_reference | Extern of Genarg.glob_generic_argument - type raw_hint = EConstr.constr * EConstr.types * Univ.universe_context_set + type raw_hint = EConstr.constr * EConstr.types * Univ.ContextSet.t type 'a with_metadata = 'a Hints.with_metadata = private { pri : int; poly : Decl_kinds.polymorphic; @@ -4563,8 +4615,10 @@ sig val atompart_of_id : Names.Id.t -> string val pr_id : Names.Id.t -> Pp.std_ppcmds + [@@ocaml.deprecated "alias of API.Names.Id.print"] val pr_name : Names.Name.t -> Pp.std_ppcmds + [@@ocaml.deprecated "alias of API.Names.Name.print"] val name_fold : (Names.Id.t -> 'a -> 'a) -> Names.Name.t -> 'a -> 'a val name_app : (Names.Id.t -> Names.Id.t) -> Names.Name.t -> Names.Name.t @@ -4593,8 +4647,14 @@ end module Constr : sig type t = Term.constr - type constr = t - type types = t + [@@ocaml.deprecated "alias of API.Term.constr"] + + type constr = Term.constr + [@@ocaml.deprecated "alias of API.Term.constr"] + + type types = Term.constr + [@@ocaml.deprecated "alias of API.Term.types"] + type cast_kind = Term.cast_kind = | VMcast | NATIVEcast @@ -4618,14 +4678,30 @@ sig | Fix of ('constr, 'types) Term.pfixpoint | CoFix of ('constr, 'types) Term.pcofixpoint | Proj of Names.Projection.t * 'constr - val equal : constr -> constr -> bool - val mkIndU : Term.pinductive -> constr - val mkConstU : Term.pconstant -> constr - val mkConst : Names.Constant.t -> constr - val mkVar : Names.Id.t -> constr - val compare : constr -> constr -> int - val mkApp : constr * constr array -> constr + [@@ocaml.deprecated "alias of API.Term.cast_kind"] + + val equal : Term.constr -> Term.constr -> bool + [@@ocaml.deprecated "alias of API.Term.eq_constr"] + + val mkIndU : Term.pinductive -> Term.constr + [@@ocaml.deprecated "alias of API.Term.mkIndU"] + + val mkConstU : Term.pconstant -> Term.constr + [@@ocaml.deprecated "alias of API.Term.mkConstU"] + + val mkConst : Names.Constant.t -> Term.constr + [@@ocaml.deprecated "alias of API.Term.mkConst"] + + val mkVar : Names.Id.t -> Term.constr + [@@ocaml.deprecated "alias of API.Term.mkVar"] + + val compare : Term.constr -> Term.constr -> int + [@@ocaml.deprecated "alias of API.Term.constr_ord"] + + val mkApp : Term.constr * Term.constr array -> Term.constr + [@@ocaml.deprecated "alias of API.Term.mkApp"] end +[@@ocaml.deprecated "alias of API.Term"] module Coq_config : sig @@ -4667,7 +4743,7 @@ sig val interp_fixpoint : structured_fixpoint_expr list -> Vernacexpr.decl_notation list -> - recursive_preentry * Vernacexpr.lident list option * Evd.evar_universe_context * + recursive_preentry * Vernacexpr.lident list option * UState.t * (EConstr.rel_context * Impargs.manual_implicits * int option) list val extract_mutual_inductive_declaration_components : diff --git a/API/PROPERTIES b/API/PROPERTIES new file mode 100644 index 000000000..cd942e202 --- /dev/null +++ b/API/PROPERTIES @@ -0,0 +1,8 @@ +0 : All API elements, i.e.: + - modules + - module types + - functions & values + - types + are present if and only if are needed for implementing Coq plugins. + +1 : Individual API elements are not aliased. diff --git a/dev/top_printers.ml b/dev/top_printers.ml index a1b3c81b9..6ae5125f6 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -37,7 +37,7 @@ let pp x = Pp.pp_with !Topfmt.std_ft x let ppfuture kx = pp (Future.print (fun _ -> str "_") kx) (* name printers *) -let ppid id = pp (pr_id id) +let ppid id = pp (Id.print id) let pplab l = pp (pr_lab l) let ppmbid mbid = pp (str (MBId.debug_to_string mbid)) let ppdir dir = pp (pr_dirpath dir) @@ -79,12 +79,12 @@ let ppbigint n = pp (str (Bigint.to_string n));; let prset pr l = str "[" ++ hov 0 (prlist_with_sep spc pr l) ++ str "]" let ppintset l = pp (prset int (Int.Set.elements l)) -let ppidset l = pp (prset pr_id (Id.Set.elements l)) +let ppidset l = pp (prset Id.print (Id.Set.elements l)) let prset' pr l = str "[" ++ hov 0 (prlist_with_sep pr_comma pr l) ++ str "]" let pridmap pr l = - let pr (id,b) = pr_id id ++ str "=>" ++ pr id b in + let pr (id,b) = Id.print id ++ str "=>" ++ pr id b in prset' pr (Id.Map.fold (fun a b l -> (a,b)::l) l []) let ppidmap pr l = pp (pridmap pr l) @@ -95,10 +95,10 @@ let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ Termops.print_constr (EConstr.of_constr c) ++ str">") ++ (if id = id0 then mt () - else spc () ++ str "<canonical: " ++ pr_id id ++ str ">")))) + else spc () ++ str "<canonical: " ++ Id.print id ++ str ">")))) -let prididmap = pridmap (fun _ -> pr_id) -let ppididmap = ppidmap (fun _ -> pr_id) +let prididmap = pridmap (fun _ -> Id.print) +let ppididmap = ppidmap (fun _ -> Id.print) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") @@ -132,15 +132,15 @@ let safe_pr_global = function int i ++ str ")") | ConstructRef ((kn,i),j) -> pp (str "INDREF(" ++ debug_pr_mind kn ++ str "," ++ int i ++ str "," ++ int j ++ str ")") - | VarRef id -> pp (str "VARREF(" ++ pr_id id ++ str ")") + | VarRef id -> pp (str "VARREF(" ++ Id.print id ++ str ")") let ppglobal x = try pp(pr_global x) with _ -> safe_pr_global x let ppconst (sp,j) = - pp (str"#" ++ pr_kn sp ++ str"=" ++ pr_lconstr j.uj_val) + pp (str"#" ++ KerName.print sp ++ str"=" ++ pr_lconstr j.uj_val) let ppvar ((id,a)) = - pp (str"#" ++ pr_id id ++ str":" ++ pr_lconstr a) + pp (str"#" ++ Id.print id ++ str":" ++ pr_lconstr a) let genppj f j = let (c,t) = f j in (c ++ str " : " ++ t) @@ -538,21 +538,21 @@ let encode_path ?loc prefix mpdir suffix id = let dir = match mpdir with | None -> [] | Some (mp,dir) -> - (DirPath.repr (dirpath_of_string (string_of_mp mp))@ + (DirPath.repr (dirpath_of_string (ModPath.to_string mp))@ DirPath.repr dir) in Qualid (Loc.tag ?loc @@ make_qualid (DirPath.make (List.rev (Id.of_string prefix::dir@suffix))) id) let raw_string_of_ref ?loc _ = function | ConstRef cst -> - let (mp,dir,id) = repr_con cst in + let (mp,dir,id) = Constant.repr3 cst in encode_path ?loc "CST" (Some (mp,dir)) [] (Label.to_id id) | IndRef (kn,i) -> - let (mp,dir,id) = repr_mind kn in + let (mp,dir,id) = MutInd.repr3 kn in encode_path ?loc "IND" (Some (mp,dir)) [Label.to_id id] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> - let (mp,dir,id) = repr_mind kn in + let (mp,dir,id) = MutInd.repr3 kn in encode_path ?loc "CSTR" (Some (mp,dir)) [Label.to_id id;Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) @@ -561,14 +561,14 @@ let raw_string_of_ref ?loc _ = function let short_string_of_ref ?loc _ = function | VarRef id -> Ident (Loc.tag ?loc id) - | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_con cst))) - | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (repr_mind kn))) + | ConstRef cst -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (Constant.repr3 cst))) + | IndRef (kn,0) -> Ident (Loc.tag ?loc @@ Label.to_id (pi3 (MutInd.repr3 kn))) | IndRef (kn,i) -> - encode_path ?loc "IND" None [Label.to_id (pi3 (repr_mind kn))] + encode_path ?loc "IND" None [Label.to_id (pi3 (MutInd.repr3 kn))] (Id.of_string ("_"^string_of_int i)) | ConstructRef ((kn,i),j) -> encode_path ?loc "CSTR" None - [Label.to_id (pi3 (repr_mind kn));Id.of_string ("_"^string_of_int i)] + [Label.to_id (pi3 (MutInd.repr3 kn));Id.of_string ("_"^string_of_int i)] (Id.of_string ("_"^string_of_int j)) (* Anticipate that printers can be used from ocamldebug and that diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp index 7d309cf0d..1c2009ece 100644 --- a/grammar/q_util.mlp +++ b/grammar/q_util.mlp @@ -57,8 +57,8 @@ let mlexpr_of_option f = function | Some e -> <:expr< Some $f e$ >> let mlexpr_of_name f = function - | None -> <:expr< Anonymous >> - | Some e -> <:expr< Name $f e$ >> + | None -> <:expr< API.Names.Name.Anonymous >> + | Some e -> <:expr< API.Names.Name.Name $f e$ >> let symbol_of_string s = <:expr< Grammar_API.Extend.Atoken (Grammar_API.CLexer.terminal $str:s$) >> diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 970bc0fcc..ea53d00d7 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -83,7 +83,7 @@ type flags = {fastcomputation : bool} (* The [proactive] knowledge contains the mapping [field->entry]. *) module Proactive = - Map.Make (struct type t = field let compare = compare end) + Map.Make (struct type t = field let compare = Pervasives.compare end) type proactive = entry Proactive.t diff --git a/kernel/term.ml b/kernel/term.ml index 07a85329e..b90718358 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -143,7 +143,8 @@ let leq_constr_univs = Constr.leq_constr_univs let eq_constr_nounivs = Constr.eq_constr_nounivs let kind_of_term = Constr.kind -let constr_ord = Constr.compare +let compare = Constr.compare +let constr_ord = compare let fold_constr = Constr.fold let map_puniverses = Constr.map_puniverses let map_constr = Constr.map diff --git a/kernel/term.mli b/kernel/term.mli index 241ef322f..e729439f0 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -447,9 +447,12 @@ val eq_constr_nounivs : constr -> constr -> bool val kind_of_term : constr -> (constr, types, Sorts.t, Univ.Instance.t) kind_of_term (** Alias for [Constr.kind] *) -val constr_ord : constr -> constr -> int +val compare : constr -> constr -> int (** Alias for [Constr.compare] *) +val constr_ord : constr -> constr -> int +(** Alias for [Term.compare] *) + val fold_constr : ('a -> constr -> 'a) -> 'a -> constr -> 'a (** Alias for [Constr.fold] *) diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index e8589f2ce..5c7cad7ff 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -136,7 +136,7 @@ let family_eq f1 f2 = match f1, f2 with type term= Symb of constr - | Product of sorts * sorts + | Product of Sorts.t * Sorts.t | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) @@ -270,7 +270,7 @@ type state = mutable rew_depth:int; mutable changed:bool; by_type: Int.Set.t Typehash.t; - mutable gls:Proof_type.goal Tacmach.sigma} + mutable gls:Proof_type.goal Evd.sigma} let dummy_node = { @@ -457,13 +457,13 @@ let rec canonize_name sigma c = let func c = canonize_name sigma (EConstr.of_constr c) in match kind_of_term c with | Const (kn,u) -> - let canon_const = constant_of_kn (canonical_con kn) in + let canon_const = Constant.make1 (Constant.canonical kn) in (mkConstU (canon_const,u)) | Ind ((kn,i),u) -> - let canon_mind = mind_of_kn (canonical_mind kn) in + let canon_mind = MutInd.make1 (MutInd.canonical kn) in (mkIndU ((canon_mind,i),u)) | Construct (((kn,i),j),u) -> - let canon_mind = mind_of_kn (canonical_mind kn) in + let canon_mind = MutInd.make1 (MutInd.canonical kn) in mkConstructU (((canon_mind,i),j),u) | Prod (na,t,ct) -> mkProd (na,func t, func ct) @@ -475,7 +475,7 @@ let rec canonize_name sigma c = mkApp (func ct,Array.smartmap func l) | Proj(p,c) -> let p' = Projection.map (fun kn -> - constant_of_kn (canonical_con kn)) p in + Constant.make1 (Constant.canonical kn)) p in (mkProj (p', func c)) | _ -> c diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli index 871de7253..505029992 100644 --- a/plugins/cc/ccalgo.mli +++ b/plugins/cc/ccalgo.mli @@ -31,7 +31,7 @@ type cinfo = type term = Symb of constr - | Product of sorts * sorts + | Product of Sorts.t * Sorts.t | Eps of Id.t | Appli of term*term | Constructor of cinfo (* constructor arity + nhyps *) @@ -129,7 +129,7 @@ val axioms : forest -> (term * term) Constrhash.t val epsilons : forest -> pa_constructor list -val empty : int -> Proof_type.goal Tacmach.sigma -> state +val empty : int -> Proof_type.goal Evd.sigma -> state val add_term : state -> term -> int diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index e8b2d7615..1ce1660b3 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -66,7 +66,7 @@ let rec decompose_term env sigma t= | Construct c -> let (((mind,i_ind),i_con),u)= c in let u = EInstance.kind sigma u in - let canon_mind = mind_of_kn (canonical_mind mind) in + let canon_mind = MutInd.make1 (MutInd.canonical mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in let nargs=constructor_nallargs_env env (canon_ind,i_con) in @@ -76,16 +76,16 @@ let rec decompose_term env sigma t= | Ind c -> let (mind,i_ind),u = c in let u = EInstance.kind sigma u in - let canon_mind = mind_of_kn (canonical_mind mind) in - let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u))) + let canon_mind = MutInd.make1 (MutInd.canonical mind) in + let canon_ind = canon_mind,i_ind in (Symb (Term.mkIndU (canon_ind,u))) | Const (c,u) -> let u = EInstance.kind sigma u in - let canon_const = constant_of_kn (canonical_con c) in - (Symb (Constr.mkConstU (canon_const,u))) + let canon_const = Constant.make1 (Constant.canonical c) in + (Symb (Term.mkConstU (canon_const,u))) | Proj (p, c) -> - let canon_const kn = constant_of_kn (canonical_con kn) in + let canon_const kn = Constant.make1 (Constant.canonical kn) in let p' = Projection.map canon_const p in - (Appli (Symb (Constr.mkConst (Projection.constant p')), decompose_term env sigma c)) + (Appli (Symb (Term.mkConst (Projection.constant p')), decompose_term env sigma c)) | _ -> let t = Termops.strip_outer_cast sigma t in if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found @@ -198,7 +198,7 @@ let make_prb gls depth additionnal_terms = (fun decl -> let id = NamedDecl.get_id decl in begin - let cid=Constr.mkVar id in + let cid=Term.mkVar id in match litteral_of_constr env sigma (NamedDecl.get_type decl) with `Eq (t,a,b) -> add_equality state cid a b | `Neq (t,a,b) -> add_disequality state (Hyp cid) a b diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml index 9c3f97696..e66bf7e1b 100644 --- a/plugins/extraction/common.ml +++ b/plugins/extraction/common.ml @@ -10,6 +10,7 @@ open API open Pp open Util open Names +open ModPath open Namegen open Nameops open Libnames @@ -45,7 +46,7 @@ let pp_apply2 st par args = let pr_binding = function | [] -> mt () - | l -> str " " ++ prlist_with_sep (fun () -> str " ") pr_id l + | l -> str " " ++ prlist_with_sep (fun () -> str " ") Id.print l let pp_tuple_light f = function | [] -> mt () @@ -274,8 +275,8 @@ let params_ren_add, params_ren_mem = seen at this level. *) -type visible_layer = { mp : module_path; - params : module_path list; +type visible_layer = { mp : ModPath.t; + params : ModPath.t list; mutable content : Label.t KMap.t; } let pop_visible, push_visible, get_visible = diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli index 4c9b1e1a5..004019e16 100644 --- a/plugins/extraction/common.mli +++ b/plugins/extraction/common.mli @@ -50,20 +50,20 @@ type phase = Pre | Impl | Intf val set_phase : phase -> unit val get_phase : unit -> phase -val opened_libraries : unit -> module_path list +val opened_libraries : unit -> ModPath.t list type kind = Term | Type | Cons | Mod val pp_global : kind -> global_reference -> string -val pp_module : module_path -> string +val pp_module : ModPath.t -> string -val top_visible_mp : unit -> module_path +val top_visible_mp : unit -> ModPath.t (* In [push_visible], the [module_path list] corresponds to module parameters, the innermost one coming first in the list *) -val push_visible : module_path -> module_path list -> unit +val push_visible : ModPath.t -> ModPath.t list -> unit val pop_visible : unit -> unit -val get_duplicate : module_path -> Label.t -> string option +val get_duplicate : ModPath.t -> Label.t -> string option type reset_kind = AllButExternal | Everything @@ -73,7 +73,7 @@ val set_keywords : Id.Set.t -> unit (** For instance: [mk_ind "Coq.Init.Datatypes" "nat"] *) -val mk_ind : string -> string -> mutual_inductive +val mk_ind : string -> string -> MutInd.t (** Special hack for constants of type Ascii.ascii : if an [Extract Inductive ascii => char] has been declared, then diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml index 688bcd025..40ef6601d 100644 --- a/plugins/extraction/extract_env.ml +++ b/plugins/extraction/extract_env.ml @@ -11,6 +11,7 @@ open Miniml open Term open Declarations open Names +open ModPath open Libnames open Globnames open Pp @@ -28,13 +29,13 @@ open Common let toplevel_env () = let get_reference = function | (_,kn), Lib.Leaf o -> - let mp,_,l = repr_kn kn in + let mp,_,l = KerName.repr kn in begin match Libobject.object_tag o with | "CONSTANT" -> - let constant = Global.lookup_constant (constant_of_kn kn) in + let constant = Global.lookup_constant (Constant.make1 kn) in Some (l, SFBconst constant) | "INDUCTIVE" -> - let inductive = Global.lookup_mind (mind_of_kn kn) in + let inductive = Global.lookup_mind (MutInd.make1 kn) in Some (l, SFBmind inductive) | "MODULE" -> let modl = Global.lookup_module (MPdot (mp, l)) in @@ -73,21 +74,21 @@ module type VISIT = sig (* Add the module_path and all its prefixes to the mp visit list. We'll keep all fields of these modules. *) - val add_mp_all : module_path -> unit + val add_mp_all : ModPath.t -> unit (* Add reference / ... in the visit lists. These functions silently add the mp of their arg in the mp list *) val add_ref : global_reference -> unit - val add_kn : kernel_name -> unit + val add_kn : KerName.t -> unit val add_decl_deps : ml_decl -> unit val add_spec_deps : ml_spec -> unit (* Test functions: is a particular object a needed dependency for the current extraction ? *) - val needed_ind : mutual_inductive -> bool - val needed_cst : constant -> bool - val needed_mp : module_path -> bool - val needed_mp_all : module_path -> bool + val needed_ind : MutInd.t -> bool + val needed_cst : Constant.t -> bool + val needed_mp : ModPath.t -> bool + val needed_mp_all : ModPath.t -> bool end module Visit : VISIT = struct @@ -102,8 +103,8 @@ module Visit : VISIT = struct v.kn <- KNset.empty; v.mp <- MPset.empty; v.mp_all <- MPset.empty - let needed_ind i = KNset.mem (user_mind i) v.kn - let needed_cst c = KNset.mem (user_con c) v.kn + let needed_ind i = KNset.mem (MutInd.user i) v.kn + let needed_cst c = KNset.mem (Constant.user c) v.kn let needed_mp mp = MPset.mem mp v.mp || MPset.mem mp v.mp_all let needed_mp_all mp = MPset.mem mp v.mp_all let add_mp mp = @@ -112,10 +113,10 @@ module Visit : VISIT = struct check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp; v.mp_all <- MPset.add mp v.mp_all - let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) + let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (KerName.modpath kn) let add_ref = function - | ConstRef c -> add_kn (user_con c) - | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (user_mind ind) + | ConstRef c -> add_kn (Constant.user c) + | IndRef (ind,_) | ConstructRef ((ind,_),_) -> add_kn (MutInd.user ind) | VarRef _ -> assert false let add_decl_deps = decl_iter_references add_ref add_ref add_ref let add_spec_deps = spec_iter_references add_ref add_ref add_ref diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli index 1e7a6ba5b..4f0ed953c 100644 --- a/plugins/extraction/extract_env.mli +++ b/plugins/extraction/extract_env.mli @@ -21,12 +21,12 @@ val extraction_library : bool -> Id.t -> unit (* For debug / external output via coqtop.byte + Drop : *) val mono_environment : - global_reference list -> module_path list -> Miniml.ml_structure + global_reference list -> ModPath.t list -> Miniml.ml_structure (* Used by the Relation Extraction plugin *) val print_one_decl : - Miniml.ml_structure -> module_path -> Miniml.ml_decl -> Pp.std_ppcmds + Miniml.ml_structure -> ModPath.t -> Miniml.ml_decl -> Pp.std_ppcmds (* Used by Extraction Compute *) diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index f1a50e7eb..2b7199a76 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -32,7 +32,7 @@ open Context.Rel.Declaration exception I of inductive_kind (* A set of all fixpoint functions currently being extracted *) -let current_fixpoints = ref ([] : constant list) +let current_fixpoints = ref ([] : Constant.t list) let none = Evd.empty @@ -256,7 +256,7 @@ let rec extract_type env db j c args = let reason = if lvl == TypeScheme then Ktype else Kprop in Tarr (Tdummy reason, mld))) | Sort _ -> Tdummy Ktype (* The two logical cases. *) - | _ when sort_of env (applist (c, args)) == InProp -> Tdummy Kprop + | _ when sort_of env (applistc c args) == InProp -> Tdummy Kprop | Rel n -> (match lookup_rel n env with | LocalDef (_,t,_) -> extract_type env db j (lift n t) args @@ -277,7 +277,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> mlt | Def _ when is_custom r -> mlt | Def lbody -> - let newc = applist (Mod_subst.force_constr lbody, args) in + let newc = applistc (Mod_subst.force_constr lbody) args in let mlt' = extract_type env db j newc [] in (* ML type abbreviations interact badly with Coq *) (* reduction, so [mlt] and [mlt'] might be different: *) @@ -291,7 +291,7 @@ let rec extract_type env db j c args = | Undef _ | OpaqueDef _ -> Tunknown (* Brutal approx ... *) | Def lbody -> (* We try to reduce. *) - let newc = applist (Mod_subst.force_constr lbody, args) in + let newc = applistc (Mod_subst.force_constr lbody) args in extract_type env db j newc [])) | Ind ((kn,i),u) -> let s = (extract_ind env kn).ind_packets.(i).ip_sign in @@ -362,14 +362,14 @@ and extract_really_ind env kn mib = (cf Vector and bug #2570) *) let equiv = if lang () != Ocaml || - (not (modular ()) && at_toplevel (mind_modpath kn)) || - KerName.equal (canonical_mind kn) (user_mind kn) + (not (modular ()) && at_toplevel (MutInd.modpath kn)) || + KerName.equal (MutInd.canonical kn) (MutInd.user kn) then NoEquiv else begin - ignore (extract_ind env (mind_of_kn (canonical_mind kn))); - Equiv (canonical_mind kn) + ignore (extract_ind env (MutInd.make1 (MutInd.canonical kn))); + Equiv (MutInd.canonical kn) end in (* Everything concerning parameters. *) @@ -865,7 +865,7 @@ let decomp_lams_eta_n n m env c t = (* we'd better keep rels' as long as possible. *) let rels = (List.firstn d rels) @ rels' in let eta_args = List.rev_map mkRel (List.interval 1 d) in - rels, applist (lift d c,eta_args) + rels, applistc (lift d c) eta_args (* Let's try to identify some situation where extracted code will allow generalisation of type variables *) diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index 2b4b05a95..26268fb17 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -15,18 +15,18 @@ open Declarations open Environ open Miniml -val extract_constant : env -> constant -> constant_body -> ml_decl +val extract_constant : env -> Constant.t -> constant_body -> ml_decl -val extract_constant_spec : env -> constant -> constant_body -> ml_spec +val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option val extract_fixpoint : - env -> constant array -> (constr, types) prec_declaration -> ml_decl + env -> Constant.t array -> (constr, types) prec_declaration -> ml_decl -val extract_inductive : env -> mutual_inductive -> ml_ind +val extract_inductive : env -> MutInd.t -> ml_ind (** For extraction compute *) diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4 index 6cba83ef9..76b435410 100644 --- a/plugins/extraction/g_extraction.ml4 +++ b/plugins/extraction/g_extraction.ml4 @@ -20,7 +20,6 @@ open Genarg open Stdarg open Pp open Names -open Nameops open Table open Extract_env @@ -35,7 +34,7 @@ END let pr_int_or_id _ _ _ = function | ArgInt i -> int i - | ArgId id -> pr_id id + | ArgId id -> Id.print id ARGUMENT EXTEND int_or_id PRINTED BY pr_int_or_id diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml index 8cdfb3499..4bd207a98 100644 --- a/plugins/extraction/haskell.ml +++ b/plugins/extraction/haskell.ml @@ -13,7 +13,6 @@ open Pp open CErrors open Util open Names -open Nameops open Globnames open Table open Miniml @@ -94,7 +93,7 @@ let preamble mod_name comment used_modules usf = let pp_abst = function | [] -> (mt ()) | l -> (str "\\" ++ - prlist_with_sep (fun () -> (str " ")) pr_id l ++ + prlist_with_sep (fun () -> (str " ")) Id.print l ++ str " ->" ++ spc ()) (*s The pretty-printer for haskell syntax *) @@ -110,7 +109,7 @@ let rec pp_type par vl t = let rec pp_rec par = function | Tmeta _ | Tvar' _ -> assert false | Tvar i -> - (try pr_id (List.nth vl (pred i)) + (try Id.print (List.nth vl (pred i)) with Failure _ -> (str "a" ++ int i)) | Tglob (r,[]) -> pp_global Type r | Tglob (IndRef(kn,0),l) @@ -149,7 +148,7 @@ let rec pp_expr par env args = (* Try to survive to the occurrence of a Dummy rel. TODO: we should get rid of this hack (cf. #592) *) let id = if Id.equal id dummy_name then Id.of_string "__" else id in - apply (pr_id id) + apply (Id.print id) | MLapp (f,args') -> let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f @@ -160,7 +159,7 @@ let rec pp_expr par env args = apply2 st | MLletin (id,a1,a2) -> let i,env' = push_vars [id_of_mlid id] env in - let pp_id = pr_id (List.hd i) + let pp_id = Id.print (List.hd i) and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in let pp_def = @@ -224,10 +223,10 @@ and pp_cons_pat par r ppl = and pp_gen_pat par ids env = function | Pcons (r,l) -> pp_cons_pat par r (List.map (pp_gen_pat true ids env) l) - | Pusual r -> pp_cons_pat par r (List.map pr_id ids) + | Pusual r -> pp_cons_pat par r (List.map Id.print ids) | Ptuple l -> pp_boxed_tuple (pp_gen_pat false ids env) l | Pwild -> str "_" - | Prel n -> pr_id (get_db_name n env) + | Prel n -> Id.print (get_db_name n env) and pp_one_pat env (ids,p,t) = let ids',env' = push_vars (List.rev_map id_of_mlid ids) env in @@ -252,10 +251,10 @@ and pp_fix par env i (ids,bl) args = (v 0 (v 1 (str "let {" ++ fnl () ++ prvect_with_sep (fun () -> str ";" ++ fnl ()) - (fun (fi,ti) -> pp_function env (pr_id fi) ti) + (fun (fi,ti) -> pp_function env (Id.print fi) ti) (Array.map2 (fun a b -> a,b) ids bl) ++ str "}") ++ - fnl () ++ str "in " ++ pp_apply (pr_id ids.(i)) false args)) + fnl () ++ str "in " ++ pp_apply (Id.print ids.(i)) false args)) and pp_function env f t = let bl,t' = collect_lams t in @@ -267,19 +266,19 @@ and pp_function env f t = (*s Pretty-printing of inductive types declaration. *) let pp_logical_ind packet = - pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ + pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++ pp_comment (str "with constructors : " ++ - prvect_with_sep spc pr_id packet.ip_consnames) + prvect_with_sep spc Id.print packet.ip_consnames) let pp_singleton kn packet = let name = pp_global Type (IndRef (kn,0)) in let l = rename_tvars keywords packet.ip_vars in hov 2 (str "type " ++ name ++ spc () ++ - prlist_with_sep spc pr_id l ++ + prlist_with_sep spc Id.print l ++ (if not (List.is_empty l) then str " " else mt ()) ++ str "=" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ - pr_id packet.ip_consnames.(0))) + Id.print packet.ip_consnames.(0))) let pp_one_ind ip pl cv = let pl = rename_tvars keywords pl in @@ -331,7 +330,7 @@ let pp_decl = function let ids,s = find_type_custom r in prlist (fun id -> str (id^" ")) ids ++ str "=" ++ spc () ++ str s with Not_found -> - prlist (fun id -> pr_id id ++ str " ") l ++ + prlist (fun id -> Id.print id ++ str " ") l ++ if t == Taxiom then str "= () -- AXIOM TO BE REALIZED" ++ fnl () else str "=" ++ spc () ++ pp_type false l t in diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli index 28226f225..ec28f4996 100644 --- a/plugins/extraction/miniml.mli +++ b/plugins/extraction/miniml.mli @@ -83,7 +83,7 @@ type ml_ind_packet = { type equiv = | NoEquiv - | Equiv of kernel_name + | Equiv of KerName.t | RenEquiv of string type ml_ind = { @@ -138,13 +138,13 @@ and ml_pattern = (*s ML declarations. *) type ml_decl = - | Dind of mutual_inductive * ml_ind + | Dind of MutInd.t * ml_ind | Dtype of global_reference * Id.t list * ml_type | Dterm of global_reference * ml_ast * ml_type | Dfix of global_reference array * ml_ast array * ml_type array type ml_spec = - | Sind of mutual_inductive * ml_ind + | Sind of MutInd.t * ml_ind | Stype of global_reference * Id.t list * ml_type option | Sval of global_reference * ml_type @@ -154,14 +154,14 @@ type ml_specif = | Smodtype of ml_module_type and ml_module_type = - | MTident of module_path + | MTident of ModPath.t | MTfunsig of MBId.t * ml_module_type * ml_module_type - | MTsig of module_path * ml_module_sig + | MTsig of ModPath.t * ml_module_sig | MTwith of ml_module_type * ml_with_declaration and ml_with_declaration = | ML_With_type of Id.t list * Id.t list * ml_type - | ML_With_module of Id.t list * module_path + | ML_With_module of Id.t list * ModPath.t and ml_module_sig = (Label.t * ml_specif) list @@ -171,9 +171,9 @@ type ml_structure_elem = | SEmodtype of ml_module_type and ml_module_expr = - | MEident of module_path + | MEident of ModPath.t | MEfunctor of MBId.t * ml_module_type * ml_module_expr - | MEstruct of module_path * ml_module_structure + | MEstruct of ModPath.t * ml_module_structure | MEapply of ml_module_expr * ml_module_expr and ml_module_structure = (Label.t * ml_structure_elem) list @@ -185,9 +185,9 @@ and ml_module = (* NB: we do not translate the [mod_equiv] field, since [mod_equiv = mp] implies that [mod_expr = MEBident mp]. Same with [msb_equiv]. *) -type ml_structure = (module_path * ml_module_structure) list +type ml_structure = (ModPath.t * ml_module_structure) list -type ml_signature = (module_path * ml_module_sig) list +type ml_signature = (ModPath.t * ml_module_sig) list type ml_flat_structure = ml_structure_elem list @@ -203,10 +203,10 @@ type language_descr = { (* Concerning the source file *) file_suffix : string; - file_naming : module_path -> string; + file_naming : ModPath.t -> string; (* the second argument is a comment to add to the preamble *) preamble : - Id.t -> std_ppcmds option -> module_path list -> unsafe_needs -> + Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs -> std_ppcmds; pp_struct : ml_structure -> std_ppcmds; @@ -214,7 +214,7 @@ type language_descr = { sig_suffix : string option; (* the second argument is a comment to add to the preamble *) sig_preamble : - Id.t -> std_ppcmds option -> module_path list -> unsafe_needs -> + Id.t -> std_ppcmds option -> ModPath.t list -> unsafe_needs -> std_ppcmds; pp_sig : ml_signature -> std_ppcmds; diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml index 5a50899c6..3a70a5020 100644 --- a/plugins/extraction/mlutil.ml +++ b/plugins/extraction/mlutil.ml @@ -29,9 +29,9 @@ let dummy_name = Id.of_string "_" let anonymous = Id anonymous_name let id_of_name = function - | Anonymous -> anonymous_name - | Name id when Id.equal id dummy_name -> anonymous_name - | Name id -> id + | Name.Anonymous -> anonymous_name + | Name.Name id when Id.equal id dummy_name -> anonymous_name + | Name.Name id -> id let id_of_mlid = function | Dummy -> dummy_name @@ -1488,7 +1488,7 @@ let inline_test r t = let con_of_string s = let d, id = Libnames.split_dirpath (dirpath_of_string s) in - Constant.make2 (MPfile d) (Label.of_id id) + Constant.make2 (ModPath.MPfile d) (Label.of_id id) let manual_inline_set = List.fold_right (fun x -> Cset_env.add (con_of_string x)) diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli index 2655dfc89..6924dc9ff 100644 --- a/plugins/extraction/mlutil.mli +++ b/plugins/extraction/mlutil.mli @@ -49,7 +49,7 @@ end (*s Utility functions over ML types without meta *) -val type_mem_kn : mutual_inductive -> ml_type -> bool +val type_mem_kn : MutInd.t -> ml_type -> bool val type_maxvar : ml_type -> int diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml index 2b1e81060..6c38813e4 100644 --- a/plugins/extraction/modutil.ml +++ b/plugins/extraction/modutil.ml @@ -8,6 +8,7 @@ open API open Names +open ModPath open Globnames open CErrors open Util @@ -111,7 +112,7 @@ let ind_iter_references do_term do_cons do_type kn ind = do_type (IndRef ip); if lang () == Ocaml then (match ind.ind_equiv with - | Miniml.Equiv kne -> do_type (IndRef (mind_of_kn kne, snd ip)); + | Miniml.Equiv kne -> do_type (IndRef (MutInd.make1 kne, snd ip)); | _ -> ()); Array.iteri (fun j -> cons_iter (ip,j+1)) p.ip_types in diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli index 45e890be0..9a67baa96 100644 --- a/plugins/extraction/modutil.mli +++ b/plugins/extraction/modutil.mli @@ -26,7 +26,7 @@ val signature_of_structure : ml_structure -> ml_signature val mtyp_of_mexpr : ml_module_expr -> ml_module_type -val msid_of_mt : ml_module_type -> module_path +val msid_of_mt : ml_module_type -> ModPath.t val get_decl_in_structure : global_reference -> ml_structure -> ml_decl @@ -37,5 +37,5 @@ val get_decl_in_structure : global_reference -> ml_structure -> ml_decl optimizations. The first argument is the list of objects we want to appear. *) -val optimize_struct : global_reference list * module_path list -> +val optimize_struct : global_reference list * ModPath.t list -> ml_structure -> ml_structure diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml index 83abaf508..16feaf4d6 100644 --- a/plugins/extraction/ocaml.ml +++ b/plugins/extraction/ocaml.ml @@ -13,7 +13,7 @@ open Pp open CErrors open Util open Names -open Nameops +open ModPath open Globnames open Table open Miniml @@ -29,7 +29,7 @@ let pp_tvar id = str ("'" ^ Id.to_string id) let pp_abst = function | [] -> mt () | l -> - str "fun " ++ prlist_with_sep (fun () -> str " ") pr_id l ++ + str "fun " ++ prlist_with_sep (fun () -> str " ") Id.print l ++ str " ->" ++ spc () let pp_parameters l = @@ -183,7 +183,7 @@ let rec pp_expr par env args = (* Try to survive to the occurrence of a Dummy rel. TODO: we should get rid of this hack (cf. #592) *) let id = if Id.equal id dummy_name then Id.of_string "__" else id in - apply (pr_id id) + apply (Id.print id) | MLapp (f,args') -> let stl = List.map (pp_expr true env []) args' in pp_expr par env (stl @ args) f @@ -195,7 +195,7 @@ let rec pp_expr par env args = apply2 st | MLletin (id,a1,a2) -> let i,env' = push_vars [id_of_mlid id] env in - let pp_id = pr_id (List.hd i) + let pp_id = Id.print (List.hd i) and pp_a1 = pp_expr false env [] a1 and pp_a2 = pp_expr (not par && expr_needs_par a2) env' [] a2 in hv 0 (apply2 (pp_letin pp_id pp_a1 pp_a2)) @@ -331,10 +331,10 @@ and pp_cons_pat r ppl = and pp_gen_pat ids env = function | Pcons (r, l) -> pp_cons_pat r (List.map (pp_gen_pat ids env) l) - | Pusual r -> pp_cons_pat r (List.map pr_id ids) + | Pusual r -> pp_cons_pat r (List.map Id.print ids) | Ptuple l -> pp_boxed_tuple (pp_gen_pat ids env) l | Pwild -> str "_" - | Prel n -> pr_id (get_db_name n env) + | Prel n -> Id.print (get_db_name n env) and pp_ifthenelse env expr pv = match pv with | [|([],tru,the);([],fal,els)|] when @@ -373,7 +373,7 @@ and pp_function env t = v 0 (pp_pat env' pv) else pr_binding (List.rev bl) ++ - str " = match " ++ pr_id (List.hd bl) ++ str " with" ++ fnl () ++ + str " = match " ++ Id.print (List.hd bl) ++ str " with" ++ fnl () ++ v 0 (pp_pat env' pv) | _ -> pr_binding (List.rev bl) ++ @@ -388,10 +388,10 @@ and pp_fix par env i (ids,bl) args = (v 0 (str "let rec " ++ prvect_with_sep (fun () -> fnl () ++ str "and ") - (fun (fi,ti) -> pr_id fi ++ pp_function env ti) + (fun (fi,ti) -> Id.print fi ++ pp_function env ti) (Array.map2 (fun id b -> (id,b)) ids bl) ++ fnl () ++ - hov 2 (str "in " ++ pp_apply (pr_id ids.(i)) false args))) + hov 2 (str "in " ++ pp_apply (Id.print ids.(i)) false args))) (* Ad-hoc double-newline in v boxes, with enough negative whitespace to avoid indenting the intermediate blank line *) @@ -432,7 +432,7 @@ let pp_Dfix (rv,c,t) = let pp_equiv param_list name = function | NoEquiv, _ -> mt () | Equiv kn, i -> - str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (mind_of_kn kn,i)) + str " = " ++ pp_parameters param_list ++ pp_global Type (IndRef (MutInd.make1 kn,i)) | RenEquiv ren, _ -> str " = " ++ pp_parameters param_list ++ str (ren^".") ++ name @@ -452,10 +452,10 @@ let pp_one_ind prefix ip_equiv pl name cnames ctyps = else fnl () ++ v 0 (prvecti pp_constructor ctyps) let pp_logical_ind packet = - pp_comment (pr_id packet.ip_typename ++ str " : logical inductive") ++ + pp_comment (Id.print packet.ip_typename ++ str " : logical inductive") ++ fnl () ++ pp_comment (str "with constructors : " ++ - prvect_with_sep spc pr_id packet.ip_consnames) ++ + prvect_with_sep spc Id.print packet.ip_consnames) ++ fnl () let pp_singleton kn packet = @@ -464,7 +464,7 @@ let pp_singleton kn packet = hov 2 (str "type " ++ pp_parameters l ++ name ++ str " =" ++ spc () ++ pp_type false l (List.hd packet.ip_types.(0)) ++ fnl () ++ pp_comment (str "singleton inductive, whose constructor was " ++ - pr_id packet.ip_consnames.(0))) + Id.print packet.ip_consnames.(0))) let pp_record kn fields ip_equiv packet = let ind = IndRef (kn,0) in diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 607ca1b3a..b82c5257e 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -8,9 +8,9 @@ open API open Names +open ModPath open Term open Declarations -open Nameops open Namegen open Libobject open Goptions @@ -36,14 +36,14 @@ module Refset' = Refset_env let occur_kn_in_ref kn = function | IndRef (kn',_) - | ConstructRef ((kn',_),_) -> Names.eq_mind kn kn' + | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' | ConstRef _ -> false | VarRef _ -> assert false let repr_of_r = function - | ConstRef kn -> repr_con kn + | ConstRef kn -> Constant.repr3 kn | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> repr_mind kn + | ConstructRef ((kn,_),_) -> MutInd.repr3 kn | VarRef _ -> assert false let modpath_of_r r = @@ -65,7 +65,7 @@ let raw_string_of_modfile = function | _ -> assert false let is_toplevel mp = - ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ()) + ModPath.equal mp ModPath.initial || ModPath.equal mp (Lib.current_mp ()) let at_toplevel mp = is_modfile mp || is_toplevel mp @@ -265,8 +265,8 @@ let safe_basename_of_global r = anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.") in match r with - | ConstRef kn -> Label.to_id (con_label kn) - | IndRef (kn,0) -> Label.to_id (mind_label kn) + | ConstRef kn -> Label.to_id (Constant.label kn) + | IndRef (kn,0) -> Label.to_id (MutInd.label kn) | IndRef (kn,i) -> (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename with Not_found -> last_chance r) @@ -287,8 +287,8 @@ let safe_pr_long_global r = try Printer.pr_global r with Not_found -> match r with | ConstRef kn -> - let mp,_,l = repr_con kn in - str ((string_of_mp mp)^"."^(Label.to_string l)) + let mp,_,l = Constant.repr3 kn in + str ((ModPath.to_string mp)^"."^(Label.to_string l)) | _ -> assert false let pr_long_mp mp = @@ -417,7 +417,7 @@ let error_singleton_become_prop id og = str " (or in its mutual block)" | None -> mt () in - err (str "The informative inductive type " ++ pr_id id ++ + err (str "The informative inductive type " ++ Id.print id ++ str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++ str "This happens when a sort-polymorphic singleton inductive type\n" ++ str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++ @@ -722,7 +722,7 @@ let add_implicits r l = let i = List.index Name.equal (Name id) names in Int.Set.add i s with Not_found -> - err (str "No argument " ++ pr_id id ++ str " for " ++ + err (str "No argument " ++ Id.print id ++ str " for " ++ safe_pr_global r) in let ints = List.fold_left add_arg Int.Set.empty l in @@ -800,7 +800,7 @@ let extraction_blacklist l = (* Printing part *) let print_extraction_blacklist () = - prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table) + prlist_with_sep fnl Id.print (Id.Set.elements !blacklist_table) (* Reset part *) diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index cd1667bdb..cfe75bf4e 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -22,22 +22,22 @@ val safe_basename_of_global : global_reference -> Id.t val warning_axioms : unit -> unit val warning_opaques : bool -> unit -val warning_ambiguous_name : ?loc:Loc.t -> qualid * module_path * global_reference -> unit +val warning_ambiguous_name : ?loc:Loc.t -> qualid * ModPath.t * global_reference -> unit val warning_id : string -> unit val error_axiom_scheme : global_reference -> int -> 'a val error_constant : global_reference -> 'a val error_inductive : global_reference -> 'a val error_nb_cons : unit -> 'a -val error_module_clash : module_path -> module_path -> 'a -val error_no_module_expr : module_path -> 'a +val error_module_clash : ModPath.t -> ModPath.t -> 'a +val error_no_module_expr : ModPath.t -> 'a val error_singleton_become_prop : Id.t -> global_reference option -> 'a val error_unknown_module : qualid -> 'a val error_scheme : unit -> 'a val error_not_visible : global_reference -> 'a -val error_MPfile_as_mod : module_path -> bool -> 'a +val error_MPfile_as_mod : ModPath.t -> bool -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit -val check_loaded_modfile : module_path -> unit +val check_loaded_modfile : ModPath.t -> unit val msg_of_implicit : kill_reason -> string val err_or_warn_remaining_implicit : kill_reason -> unit @@ -45,22 +45,22 @@ val info_file : string -> unit (*s utilities about [module_path] and [kernel_names] and [global_reference] *) -val occur_kn_in_ref : mutual_inductive -> global_reference -> bool -val repr_of_r : global_reference -> module_path * DirPath.t * Label.t -val modpath_of_r : global_reference -> module_path +val occur_kn_in_ref : MutInd.t -> global_reference -> bool +val repr_of_r : global_reference -> ModPath.t * DirPath.t * Label.t +val modpath_of_r : global_reference -> ModPath.t val label_of_r : global_reference -> Label.t -val base_mp : module_path -> module_path -val is_modfile : module_path -> bool -val string_of_modfile : module_path -> string -val file_of_modfile : module_path -> string -val is_toplevel : module_path -> bool -val at_toplevel : module_path -> bool -val mp_length : module_path -> int -val prefixes_mp : module_path -> MPset.t +val base_mp : ModPath.t -> ModPath.t +val is_modfile : ModPath.t -> bool +val string_of_modfile : ModPath.t -> string +val file_of_modfile : ModPath.t -> string +val is_toplevel : ModPath.t -> bool +val at_toplevel : ModPath.t -> bool +val mp_length : ModPath.t -> int +val prefixes_mp : ModPath.t -> MPset.t val common_prefix_from_list : - module_path -> module_path list -> module_path option -val get_nth_label_mp : int -> module_path -> Label.t -val labels_of_ref : global_reference -> module_path * Label.t list + ModPath.t -> ModPath.t list -> ModPath.t option +val get_nth_label_mp : int -> ModPath.t -> Label.t +val labels_of_ref : global_reference -> ModPath.t * Label.t list (*s Some table-related operations *) @@ -72,16 +72,16 @@ val labels_of_ref : global_reference -> module_path * Label.t list [mutual_inductive_body] as checksum. In both case, we should ideally also check the env *) -val add_typedef : constant -> constant_body -> ml_type -> unit -val lookup_typedef : constant -> constant_body -> ml_type option +val add_typedef : Constant.t -> constant_body -> ml_type -> unit +val lookup_typedef : Constant.t -> constant_body -> ml_type option -val add_cst_type : constant -> constant_body -> ml_schema -> unit -val lookup_cst_type : constant -> constant_body -> ml_schema option +val add_cst_type : Constant.t -> constant_body -> ml_schema -> unit +val lookup_cst_type : Constant.t -> constant_body -> ml_schema option -val add_ind : mutual_inductive -> mutual_inductive_body -> ml_ind -> unit -val lookup_ind : mutual_inductive -> mutual_inductive_body -> ml_ind option +val add_ind : MutInd.t -> mutual_inductive_body -> ml_ind -> unit +val lookup_ind : MutInd.t -> mutual_inductive_body -> ml_ind option -val add_inductive_kind : mutual_inductive -> inductive_kind -> unit +val add_inductive_kind : MutInd.t -> inductive_kind -> unit val is_coinductive : global_reference -> bool val is_coinductive_type : ml_type -> bool (* What are the fields of a record (empty for a non-record) *) @@ -89,10 +89,10 @@ val get_record_fields : global_reference -> global_reference option list val record_fields_of_type : ml_type -> global_reference option list -val add_recursors : Environ.env -> mutual_inductive -> unit +val add_recursors : Environ.env -> MutInd.t -> unit val is_recursor : global_reference -> bool -val add_projection : int -> constant -> inductive -> unit +val add_projection : int -> Constant.t -> inductive -> unit val is_projection : global_reference -> bool val projection_arity : global_reference -> int val projection_info : global_reference -> inductive * int (* arity *) diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 4a93e01dc..435ca1986 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,7 +7,6 @@ (************************************************************************) open API -open Term open EConstr open CErrors open Util @@ -58,11 +57,11 @@ end module OrderedConstr= struct - type t=Constr.t - let compare=constr_ord + type t=Term.constr + let compare=Term.compare end -type h_item = global_reference * (int*Constr.t) option +type h_item = global_reference * (int*Term.constr) option module Hitem= struct diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli index c43a91cee..e24eca7cb 100644 --- a/plugins/firstorder/sequent.mli +++ b/plugins/firstorder/sequent.mli @@ -11,11 +11,11 @@ open EConstr open Formula open Globnames -module OrderedConstr: Set.OrderedType with type t=Constr.t +module OrderedConstr: Set.OrderedType with type t=Term.constr -module CM: CSig.MapS with type key=Constr.t +module CM: CSig.MapS with type key=Term.constr -type h_item = global_reference * (int*Constr.t) option +type h_item = global_reference * (int*Term.constr) option module History: Set.S with type elt = h_item diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml index 24fd8dd88..e1adebe8d 100644 --- a/plugins/firstorder/unify.ml +++ b/plugins/firstorder/unify.ml @@ -55,12 +55,12 @@ let unif evd t1 t2= | Meta i,_ -> let t=subst_meta !sigma nt2 in if Int.Set.is_empty (free_rels evd t) && - not (occur_term evd (EConstr.mkMeta i) t) then + not (dependent evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | _,Meta i -> let t=subst_meta !sigma nt1 in if Int.Set.is_empty (free_rels evd t) && - not (occur_term evd (EConstr.mkMeta i) t) then + not (dependent evd (EConstr.mkMeta i) t) then bind i t else raise (UFAIL(nt1,nt2)) | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index 2af79aec9..b44307590 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -77,8 +77,8 @@ let flin_emult a f = type ineq = Rlt | Rle | Rgt | Rge let string_of_R_constant kn = - match Names.repr_con kn with - | MPfile dir, sec_dir, id when + match Constant.repr3 kn with + | ModPath.MPfile dir, sec_dir, id when sec_dir = DirPath.empty && DirPath.to_string dir = "Coq.Reals.Rdefinitions" -> Label.to_string id diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index 023cbad43..ef894b239 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -106,7 +106,7 @@ let make_refl_eq constructor type_of_t t = type pte_info = { - proving_tac : (Id.t list -> Tacmach.tactic); + proving_tac : (Id.t list -> Proof_type.tactic); is_valid : constr -> bool } @@ -688,7 +688,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id = let build_proof (interactive_proof:bool) - (fnames:constant list) + (fnames:Constant.t list) ptes_infos dyn_infos : tactic = @@ -708,13 +708,13 @@ let build_proof let term_eq = make_refl_eq (Lazy.force refl_equal) type_of_term t in - tclTHENSEQ + tclTHENLIST [ Proofview.V82.of_tactic (generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps))); thin dyn_infos.rec_hyps; Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None); (fun g -> observe_tac "toto" ( - tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t); + tclTHENLIST [Proofview.V82.of_tactic (Simple.case t); (fun g' -> let g'_nb_prod = nb_prod (project g') (pf_concl g') in let nb_instanciate_partial = g'_nb_prod - g_nb_prod in @@ -982,14 +982,14 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num let eqn = mkApp(Lazy.force eq,[|type_of_f;eq_lhs;eq_rhs|]) in let lemma_type = it_mkProd_or_LetIn eqn type_ctxt in (* Pp.msgnl (str "lemma type " ++ Printer.pr_lconstr lemma_type ++ fnl () ++ str "f_body " ++ Printer.pr_lconstr f_body); *) - let f_id = Label.to_id (con_label (fst (destConst evd f))) in + let f_id = Label.to_id (Constant.label (fst (destConst evd f))) in let prove_replacement = - tclTHENSEQ + tclTHENLIST [ tclDO (nb_params + rec_args_num + 1) (Proofview.V82.of_tactic intro); observe_tac "" (fun g -> let rec_id = pf_nth_hyp_id g 1 in - tclTHENSEQ + tclTHENLIST [observe_tac "generalize_non_dep in generate_equation_lemma" (generalize_non_dep rec_id); observe_tac "h_case" (Proofview.V82.of_tactic (simplest_case (mkVar rec_id))); (Proofview.V82.of_tactic intros_reflexivity)] g @@ -1019,7 +1019,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a let finfos = find_Function_infos (fst (destConst !evd f)) (*FIXME*) in mkConst (Option.get finfos.equation_lemma) with (Not_found | Option.IsNone as e) -> - let f_id = Label.to_id (con_label (fst (destConst !evd f))) in + let f_id = Label.to_id (Constant.label (fst (destConst !evd f))) in (*i The next call to mk_equation_id is valid since we will construct the lemma Ensures by: obvious i*) @@ -1242,7 +1242,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam other_fix_infos 0) in let first_tac : tactic = (* every operations until fix creations *) - tclTHENSEQ + tclTHENLIST [ observe_tac "introducing params" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.params))); observe_tac "introducing predictes" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.predicates))); observe_tac "introducing branches" (Proofview.V82.of_tactic (intros_using (List.rev_map id_of_decl princ_info.branches))); @@ -1260,7 +1260,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam in let fix_info = Id.Map.find pte ptes_to_fix in let nb_args = fix_info.nb_realargs in - tclTHENSEQ + tclTHENLIST [ (* observe_tac ("introducing args") *) (tclDO nb_args (Proofview.V82.of_tactic intro)); (fun g -> (* replacement of the function by its body *) @@ -1279,7 +1279,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam eq_hyps = [] } in - tclTHENSEQ + tclTHENLIST [ observe_tac "do_replace" (do_replace evd @@ -1322,7 +1322,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam ] gl with Not_found -> let nb_args = min (princ_info.nargs) (List.length ctxt) in - tclTHENSEQ + tclTHENLIST [ tclDO nb_args (Proofview.V82.of_tactic intro); (fun g -> (* replacement of the function by its body *) @@ -1343,7 +1343,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam } in let fname = destConst (project g) (fst (decompose_app (project g) (List.hd (List.rev pte_args)))) in - tclTHENSEQ + tclTHENLIST [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]); let do_prove = build_proof @@ -1402,7 +1402,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic = fun gls -> (* let hid = next_ident_away_in_goal h_id (pf_ids_of_hyps gls) in *) (* let ids = hid::pf_ids_of_hyps gls in *) - tclTHENSEQ + tclTHENLIST [ (* generalize [lemma]; *) (* h_intro hid; *) @@ -1457,13 +1457,13 @@ let rec rewrite_eqs_in_eqs eqs = let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic = fun gls -> - (tclTHENSEQ + (tclTHENLIST [ backtrack_eqs_until_hrec hrec eqs; (* observe_tac ("new_prove_with_tcc ( applying "^(Id.to_string hrec)^" )" ) *) (tclTHENS (* We must have exactly ONE subgoal !*) (Proofview.V82.of_tactic (apply (mkVar hrec))) - [ tclTHENSEQ + [ tclTHENLIST [ (Proofview.V82.of_tactic (keep (tcc_hyps@eqs))); (Proofview.V82.of_tactic (apply (Lazy.force acc_inv))); @@ -1617,7 +1617,7 @@ let prove_principle_for_gen (Id.of_string "prov") hyps in - tclTHENSEQ + tclTHENLIST [ Proofview.V82.of_tactic (generalize [lemma]); Proofview.V82.of_tactic (Simple.intro hid); @@ -1636,7 +1636,7 @@ let prove_principle_for_gen ] gls in - tclTHENSEQ + tclTHENLIST [ observe_tac "start_tac" start_tac; h_intros diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli index 069f767dd..5bb288678 100644 --- a/plugins/funind/functional_principles_proofs.mli +++ b/plugins/funind/functional_principles_proofs.mli @@ -4,17 +4,17 @@ open Names val prove_princ_for_struct : Evd.evar_map ref -> bool -> - int -> constant array -> EConstr.constr array -> int -> Tacmach.tactic + int -> Constant.t array -> EConstr.constr array -> int -> Proof_type.tactic val prove_principle_for_gen : - constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *) + Constant.t * Constant.t * Constant.t -> (* name of the function, the functional and the fixpoint equation *) Indfun_common.tcc_lemma_value ref -> (* a pointer to the obligation proofs lemma *) bool -> (* is that function uses measure *) int -> (* the number of recursive argument *) EConstr.types -> (* the type of the recursive argument *) EConstr.constr -> (* the wf relation used to prove the function *) - Tacmach.tactic + Proof_type.tactic (* val is_pte : rel_declaration -> bool *) diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml index fd4b52b65..70245a8b1 100644 --- a/plugins/funind/functional_principles_types.ml +++ b/plugins/funind/functional_principles_types.ml @@ -150,7 +150,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type = ([],[]) in let new_f,binders_to_remove_from_f = compute_new_princ_type remove env f in - applist(new_f, new_args), + applistc new_f new_args, list_union_eq eq_constr binders_to_remove_from_f binders_to_remove | LetIn(x,v,t,b) -> compute_new_princ_type_for_letin remove env x v t b @@ -330,7 +330,7 @@ let generate_functional_principle (evd: Evd.evar_map ref) match new_princ_name with | Some (id) -> id,id | None -> - let id_of_f = Label.to_id (con_label (fst f)) in + let id_of_f = Label.to_id (Constant.label (fst f)) in id_of_f,Indrec.make_elimination_ident id_of_f (family_of_sort type_sort) in let names = ref [new_princ_name] in @@ -389,14 +389,14 @@ let generate_functional_principle (evd: Evd.evar_map ref) exception Not_Rec let get_funs_constant mp dp = - let get_funs_constant const e : (Names.constant*int) array = + let get_funs_constant const e : (Names.Constant.t*int) array = match kind_of_term ((strip_lam e)) with | Fix((_,(na,_,_))) -> Array.mapi (fun i na -> match na with | Name id -> - let const = make_con mp dp (Label.of_id id) in + let const = Constant.make3 mp dp (Label.of_id id) in const,i | Anonymous -> anomaly (Pp.str "Anonymous fix.") @@ -656,7 +656,7 @@ let build_case_scheme fa = user_err ~hdr:"FunInd.build_case_scheme" (str "Cannot find " ++ Libnames.pr_reference f) in let first_fun,u = destConst funs in - let funs_mp,funs_dp,_ = Names.repr_con first_fun in + let funs_mp,funs_dp,_ = Constant.repr3 first_fun in let first_fun_kn = try fst (find_Function_infos first_fun).graph_ind with Not_found -> raise No_graph_found in let this_block_funs_indexes = get_funs_constant funs_mp funs_dp first_fun in let this_block_funs = Array.map (fun (c,_) -> (c,u)) this_block_funs_indexes in diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli index bf1906bfb..bb2b2d918 100644 --- a/plugins/funind/functional_principles_types.mli +++ b/plugins/funind/functional_principles_types.mli @@ -18,7 +18,7 @@ val generate_functional_principle : (* induction principle on rel *) types -> (* *) - sorts array option -> + Sorts.t array option -> (* Name of the new principle *) (Id.t) option -> (* the compute functions to use *) @@ -28,10 +28,10 @@ val generate_functional_principle : (* The tactic to use to make the proof w.r the number of params *) - (EConstr.constr array -> int -> Tacmach.tactic) -> + (EConstr.constr array -> int -> Proof_type.tactic) -> unit -val compute_new_princ_type_from_rel : constr array -> sorts array -> +val compute_new_princ_type_from_rel : constr array -> Sorts.t array -> types -> types diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index d9cd026d8..1258c9286 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -166,7 +166,7 @@ VERNAC COMMAND EXTEND Function END let pr_fun_scheme_arg (princ_name,fun_name,s) = - Nameops.pr_id princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ + Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++ Libnames.pr_reference fun_name ++ spc() ++ str "Sort " ++ Ppconstr.pr_glob_sort s diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml index eae72d9e8..a7481370a 100644 --- a/plugins/funind/glob_termops.ml +++ b/plugins/funind/glob_termops.ml @@ -579,8 +579,8 @@ let ids_of_pat = ids_of_pat Id.Set.empty let id_of_name = function - | Names.Anonymous -> Id.of_string "x" - | Names.Name x -> x + | Anonymous -> Id.of_string "x" + | Name x -> x (* TODO: finish Rec caes *) let ids_of_glob_constr c = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index f277c563a..d12aa7f42 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -65,7 +65,7 @@ let functional_induction with_clean c princl pat = (or f_rec, f_rect) i*) let princ_name = Indrec.make_elimination_ident - (Label.to_id (con_label c')) + (Label.to_id (Constant.label c')) (Tacticals.elimination_sort_of_goal g) in try @@ -342,8 +342,8 @@ let error_error names e = let generate_principle (evd:Evd.evar_map ref) pconstants on_error is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof - (continue_proof : int -> Names.constant array -> EConstr.constr array -> int -> - Tacmach.tactic) : unit = + (continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int -> + Proof_type.tactic) : unit = let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in let funs_args = List.map fst fun_bodies in @@ -446,7 +446,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp let generate_correction_proof_wf f_ref tcc_lemma_ref is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation - (_: int) (_:Names.constant array) (_:EConstr.constr array) (_:int) : Tacmach.tactic = + (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic = Functional_principles_proofs.prove_principle_for_gen (f_ref,functional_ref,eq_ref) tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation @@ -899,14 +899,14 @@ let make_graph (f_ref:global_reference) = in l | _ -> - let id = Label.to_id (con_label c) in + let id = Label.to_id (Constant.label c) in [(((Loc.tag id),None),(None,Constrexpr.CStructRec),nal_tas,t,Some b),[]] in - let mp,dp,_ = repr_con c in + let mp,dp,_ = Constant.repr3 c in do_generate_principle [c,Univ.Instance.empty] error_error false false expr_list; (* We register the infos *) List.iter - (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (make_con mp dp (Label.of_id id))) + (fun ((((_,id),_),_,_,_,_),_) -> add_Function false (Constant.make3 mp dp (Label.of_id id))) expr_list) let do_generate_principle = do_generate_principle [] warning_error true diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli index a82a8b360..33420d813 100644 --- a/plugins/funind/indfun.mli +++ b/plugins/funind/indfun.mli @@ -16,7 +16,7 @@ val functional_induction : EConstr.constr -> (EConstr.constr * EConstr.constr bindings) option -> Tacexpr.or_and_intro_pattern option -> - Proof_type.goal Tacmach.sigma -> Proof_type.goal list Evd.sigma + Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma val make_graph : Globnames.global_reference -> unit diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 8f62231ae..7558ac7ac 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -109,7 +109,7 @@ let const_of_id id = try Constrintern.locate_reference princ_ref with Not_found -> CErrors.user_err ~hdr:"IndFun.const_of_id" - (str "cannot find " ++ Nameops.pr_id id) + (str "cannot find " ++ Id.print id) let def_of_const t = match (Term.kind_of_term t) with @@ -217,14 +217,14 @@ let with_full_print f a = type function_info = { - function_constant : constant; + function_constant : Constant.t; graph_ind : inductive; - equation_lemma : constant option; - correctness_lemma : constant option; - completeness_lemma : constant option; - rect_lemma : constant option; - rec_lemma : constant option; - prop_lemma : constant option; + equation_lemma : Constant.t option; + correctness_lemma : Constant.t option; + completeness_lemma : Constant.t option; + rect_lemma : Constant.t option; + rec_lemma : Constant.t option; + prop_lemma : Constant.t option; is_general : bool; (* Has this function been defined using general recursive definition *) } @@ -389,7 +389,7 @@ let update_Function finfo = let add_Function is_general f = - let f_id = Label.to_id (con_label f) in + let f_id = Label.to_id (Constant.label f) in let equation_lemma = find_or_none (mk_equation_id f_id) and correctness_lemma = find_or_none (mk_correct_id f_id) and completeness_lemma = find_or_none (mk_complete_id f_id) @@ -548,5 +548,5 @@ let compose_prod l b = prodn (List.length l) l b type tcc_lemma_value = | Undefined - | Value of Constr.constr + | Value of Term.constr | Not_needed diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli index aa42b2ab9..6b40c9171 100644 --- a/plugins/funind/indfun_common.mli +++ b/plugins/funind/indfun_common.mli @@ -23,7 +23,7 @@ val array_get_start : 'a array -> 'a array val id_of_name : Name.t -> Id.t val locate_ind : Libnames.reference -> inductive -val locate_constant : Libnames.reference -> constant +val locate_constant : Libnames.reference -> Constant.t val locate_with_msg : Pp.std_ppcmds -> (Libnames.reference -> 'a) -> Libnames.reference -> 'a @@ -70,21 +70,21 @@ val with_full_print : ('a -> 'b) -> 'a -> 'b type function_info = { - function_constant : constant; + function_constant : Constant.t; graph_ind : inductive; - equation_lemma : constant option; - correctness_lemma : constant option; - completeness_lemma : constant option; - rect_lemma : constant option; - rec_lemma : constant option; - prop_lemma : constant option; + equation_lemma : Constant.t option; + correctness_lemma : Constant.t option; + completeness_lemma : Constant.t option; + rect_lemma : Constant.t option; + rec_lemma : Constant.t option; + prop_lemma : Constant.t option; is_general : bool; } -val find_Function_infos : constant -> function_info +val find_Function_infos : Constant.t -> function_info val find_Function_of_graph : inductive -> function_info (* WARNING: To be used just after the graph definition !!! *) -val add_Function : bool -> constant -> unit +val add_Function : bool -> Constant.t -> unit val update_Function : function_info -> unit @@ -123,5 +123,5 @@ val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t type tcc_lemma_value = | Undefined - | Value of Constr.constr + | Value of Term.constr | Not_needed diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 8152e181a..ebdb490e3 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -218,7 +218,7 @@ let rec generate_fresh_id x avoid i = \end{enumerate} *) -let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : tactic = +let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Proof_type.tactic = fun g -> (* first of all we recreate the lemmas types to be used as predicates of the induction principle that is~: @@ -342,7 +342,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes in (* observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); *) ( - tclTHENSEQ + tclTHENLIST [ observe_tac("h_intro_patterns ") (let l = (List.nth intro_pats (pred i)) in match l with @@ -415,7 +415,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes in (params_bindings@lemmas_bindings) in - tclTHENSEQ + tclTHENLIST [ observe_tac "principle" (Proofview.V82.of_tactic (assert_by (Name principle_id) @@ -468,7 +468,7 @@ let tauto = let rec intros_with_rewrite g = observe_tac "intros_with_rewrite" intros_with_rewrite_aux g -and intros_with_rewrite_aux : tactic = +and intros_with_rewrite_aux : Proof_type.tactic = fun g -> let eq_ind = make_eq () in let sigma = project g in @@ -480,16 +480,16 @@ and intros_with_rewrite_aux : tactic = if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2) then let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g + tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g)) - then tclTHENSEQ[ + then tclTHENLIST[ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]); tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) ))) (pf_ids_of_hyps g); intros_with_rewrite ] g else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g)) - then tclTHENSEQ[ + then tclTHENLIST[ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]); tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) ))) (pf_ids_of_hyps g); @@ -498,7 +498,7 @@ and intros_with_rewrite_aux : tactic = else if isVar sigma args.(1) then let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); + tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); generalize_dependent_of (destVar sigma args.(1)) id; tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); intros_with_rewrite @@ -507,7 +507,7 @@ and intros_with_rewrite_aux : tactic = else if isVar sigma args.(2) then let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); + tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id); generalize_dependent_of (destVar sigma args.(2)) id; tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id))); intros_with_rewrite @@ -516,7 +516,7 @@ and intros_with_rewrite_aux : tactic = else begin let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ[ + tclTHENLIST[ Proofview.V82.of_tactic (Simple.intro id); tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id))); intros_with_rewrite @@ -525,12 +525,12 @@ and intros_with_rewrite_aux : tactic = | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Universes.constr_of_global @@ Coqlib.build_coq_False ())) -> Proofview.V82.of_tactic tauto g | Case(_,_,v,_) -> - tclTHENSEQ[ + tclTHENLIST[ Proofview.V82.of_tactic (simplest_case v); intros_with_rewrite ] g | LetIn _ -> - tclTHENSEQ[ + tclTHENLIST[ Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags @@ -542,10 +542,10 @@ and intros_with_rewrite_aux : tactic = ] g | _ -> let id = pf_get_new_id (Id.of_string "y") g in - tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g + tclTHENLIST [ Proofview.V82.of_tactic (Simple.intro id);intros_with_rewrite] g end | LetIn _ -> - tclTHENSEQ[ + tclTHENLIST[ Proofview.V82.of_tactic (reduce (Genredexpr.Cbv {Redops.all_flags @@ -562,7 +562,7 @@ let rec reflexivity_with_destruct_cases g = try match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with | Case(_,_,v,_) -> - tclTHENSEQ[ + tclTHENLIST[ Proofview.V82.of_tactic (simplest_case v); Proofview.V82.of_tactic intros; observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases @@ -582,7 +582,7 @@ let rec reflexivity_with_destruct_cases g = if Equality.discriminable (pf_env g) (project g) t1 t2 then Proofview.V82.of_tactic (Equality.discrHyp id) g else if Equality.injectable (pf_env g) (project g) t1 t2 - then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g + then tclTHENLIST [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite] g else tclIDTAC g | _ -> tclIDTAC g ) @@ -629,7 +629,7 @@ let rec reflexivity_with_destruct_cases g = *) -let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = +let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.tactic = fun g -> (* We compute the types of the different mutually recursive lemmas in $\zeta$ normal form @@ -673,7 +673,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = using [f_equation] if it is recursive (that is the graph is infinite or unfold if the graph is finite *) - let rewrite_tac j ids : tactic = + let rewrite_tac j ids : Proof_type.tactic = let graph_def = graphs.(j) in let infos = try find_Function_infos (fst (destConst (project g) funcs.(j))) @@ -686,7 +686,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = try Option.get (infos).equation_lemma with Option.IsNone -> anomaly (Pp.str "Cannot find equation lemma.") in - tclTHENSEQ[ + tclTHENLIST[ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids; Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma)); (* Don't forget to $\zeta$ normlize the term since the principles @@ -722,7 +722,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = end in let this_branche_ids = List.nth intro_pats (pred i) in - tclTHENSEQ[ + tclTHENLIST[ (* we expand the definition of the function *) observe_tac "rewrite_tac" (rewrite_tac this_ind_number this_branche_ids); (* introduce hypothesis with some rewrite *) @@ -735,7 +735,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = let params_names = fst (List.chop princ_infos.nparams args_names) in let open EConstr in let params = List.map mkVar params_names in - tclTHENSEQ + tclTHENLIST [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]); observe_tac "h_generalize" (Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)])); @@ -807,7 +807,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( in Array.iteri (fun i f_as_constant -> - let f_id = Label.to_id (con_label (fst f_as_constant)) in + let f_id = Label.to_id (Constant.label (fst f_as_constant)) in (*i The next call to mk_correct_id is valid since we are constructing the lemma Ensures by: obvious i*) @@ -872,7 +872,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) ( in Array.iteri (fun i f_as_constant -> - let f_id = Label.to_id (con_label (fst f_as_constant)) in + let f_id = Label.to_id (Constant.label (fst f_as_constant)) in (*i The next call to mk_complete_id is valid since we are constructing the lemma Ensures by: obvious i*) @@ -923,7 +923,7 @@ let revert_graph kn post_tac hid g = | None -> tclIDTAC g | Some f_complete -> let f_args,res = Array.chop (Array.length args - 1) args in - tclTHENSEQ + tclTHENLIST [ Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]); thin [hid]; @@ -953,7 +953,7 @@ let revert_graph kn post_tac hid g = \end{enumerate} *) -let functional_inversion kn hid fconst f_correct : tactic = +let functional_inversion kn hid fconst f_correct : Proof_type.tactic = fun g -> let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in let sigma = project g in @@ -968,7 +968,7 @@ let functional_inversion kn hid fconst f_correct : tactic = ((fun hid -> tclIDTAC),f_args,args.(1)) | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2) in - tclTHENSEQ[ + tclTHENLIST [ pre_tac hid; Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]); thin [hid]; diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index 290d0bb91..c75f7f868 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -893,7 +893,7 @@ let find_Function_infos_safe (id:Id.t): Indfun_common.function_info = locate_constant f_ref in try find_Function_infos (kn_of_id id) with Not_found -> - user_err ~hdr:"indfun" (Nameops.pr_id id ++ str " has no functional scheme") + user_err ~hdr:"indfun" (Id.print id ++ str " has no functional scheme") (** [merge id1 id2 args1 args2 id] builds and declares a new inductive type called [id], representing the merged graphs of both graphs diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index bd74d2cf6..20abde82f 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -77,7 +77,7 @@ let def_of_const t = | _ -> raise Not_found) with Not_found -> anomaly (str "Cannot find definition of constant " ++ - (Id.print (Label.to_id (con_label (fst sp)))) ++ str ".") + (Id.print (Label.to_id (Constant.label (fst sp)))) ++ str ".") ) |_ -> assert false @@ -172,7 +172,7 @@ let simpl_iter clause = clause (* Others ugly things ... *) -let (value_f:Constr.constr list -> global_reference -> Constr.constr) = +let (value_f:Term.constr list -> global_reference -> Term.constr) = let open Term in fun al fterm -> let rev_x_id_l = @@ -204,7 +204,7 @@ let (value_f:Constr.constr list -> global_reference -> Constr.constr) = let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in it_mkLambda_or_LetIn body context -let (declare_f : Id.t -> logical_kind -> Constr.constr list -> global_reference -> global_reference) = +let (declare_f : Id.t -> logical_kind -> Term.constr list -> global_reference -> global_reference) = fun f_id kind input_type fterm_ref -> declare_fun f_id kind (value_f input_type fterm_ref);; @@ -313,7 +313,7 @@ let check_not_nested sigma forbidden e = | Var x -> if Id.List.mem x forbidden then user_err ~hdr:"Recdef.check_not_nested" - (str "check_not_nested: failure " ++ pr_id x) + (str "check_not_nested: failure " ++ Id.print x) | Meta _ | Evar _ | Sort _ -> () | Cast(e,_,t) -> check_not_nested e;check_not_nested t | Prod(_,t,b) -> check_not_nested t;check_not_nested b @@ -450,7 +450,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Lambda(n,t,b) -> begin @@ -458,7 +458,7 @@ let rec travel_aux jinfo continuation_tac (expr_info:constr infos) g = check_not_nested sigma (expr_info.f_id::expr_info.forbidden_ids) expr_info.info; jinfo.otherS () expr_info continuation_tac expr_info g with e when CErrors.noncritical e -> - user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ pr_id expr_info.f_id) + user_err ~hdr:"Recdef.travel" (str "the term " ++ Printer.pr_leconstr expr_info.info ++ str " can not contain a recursive call to " ++ Id.print expr_info.f_id) end | Case(ci,t,a,l) -> begin @@ -683,7 +683,7 @@ let pf_typel l tac = introduced back later; the result is the pair of the tactic and the list of hypotheses that have been generalized and cleared. *) let mkDestructEq : - Id.t list -> constr -> goal sigma -> tactic * Id.t list = + Id.t list -> constr -> goal Evd.sigma -> tactic * Id.t list = fun not_on_hyp expr g -> let hyps = pf_hyps g in let to_revert = @@ -691,7 +691,7 @@ let mkDestructEq : (fun decl -> let open Context.Named.Declaration in let id = get_id decl in - if Id.List.mem id not_on_hyp || not (Termops.occur_term (project g) expr (get_type decl)) + if Id.List.mem id not_on_hyp || not (Termops.dependent (project g) expr (get_type decl)) then None else Some id) hyps in let to_revert_constr = List.rev_map mkVar to_revert in let type_of_expr = pf_unsafe_type_of g expr in @@ -850,7 +850,7 @@ let rec prove_le g = try let matching_fun = pf_is_matching g - (Pattern.PApp(Pattern.PRef (reference_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in + (Pattern.PApp(Pattern.PRef (Globnames.global_of_constr (EConstr.Unsafe.to_constr (le ()))),[|Pattern.PVar (destVar sigma x);Pattern.PMeta None|])) in let (h,t) = List.find (fun (_,t) -> matching_fun t) (pf_hyps_types g) in let y = @@ -870,7 +870,7 @@ let rec make_rewrite_list expr_info max = function | [] -> tclIDTAC | (_,p,hp)::l -> observe_tac (str "make_rewrite_list") (tclTHENS - (observe_tac (str "rewrite heq on " ++ pr_id p ) ( + (observe_tac (str "rewrite heq on " ++ Id.print p ) ( (fun g -> let sigma = project g in let t_eq = compute_renamed_type g (mkVar hp) in @@ -965,7 +965,7 @@ let rec destruct_hex expr_info acc l = onNthHypId 1 (fun hp -> onNthHypId 2 (fun p -> observe_tac - (str "destruct_hex after " ++ pr_id hp ++ spc () ++ pr_id p) + (str "destruct_hex after " ++ Id.print hp ++ spc () ++ Id.print p) (destruct_hex expr_info ((v,p,hp)::acc) l) ) ) @@ -1457,7 +1457,7 @@ let start_equation (f:global_reference) (term_f:global_reference) let (com_eqn : int -> Id.t -> global_reference -> global_reference -> global_reference - -> Constr.constr -> unit) = + -> Term.constr -> unit) = fun nb_arg eq_name functional_ref f_ref terminate_ref equation_lemma_type -> let open CVars in let opacity = diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4 index 63057c3ae..07b8746fb 100644 --- a/plugins/ltac/coretactics.ml4 +++ b/plugins/ltac/coretactics.ml4 @@ -10,12 +10,12 @@ open API open Util -open Names open Locus open Misctypes open Genredexpr open Stdarg open Extraargs +open Names DECLARE PLUGIN "coretactics" @@ -307,7 +307,7 @@ let initial_atomic () = let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in let iter (s, t) = let body = TacAtom (Loc.tag t) in - Tacenv.register_ltac false false (Id.of_string s) body + Tacenv.register_ltac false false (Names.Id.of_string s) body in let () = List.iter iter [ "red", TacReduce(Red false,nocl); @@ -317,7 +317,7 @@ let initial_atomic () = "intros", TacIntroPattern (false,[]); ] in - let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in + let iter (s, t) = Tacenv.register_ltac false false (Names.Id.of_string s) t in List.iter iter [ "idtac",TacId []; "fail", TacFail(TacLocal,ArgArg 0,[]); diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml index 958f43bd7..a299e11f8 100644 --- a/plugins/ltac/evar_tactics.ml +++ b/plugins/ltac/evar_tactics.ml @@ -87,16 +87,16 @@ let let_evar name typ = let _ = Typing.e_sort_of env sigma typ in let sigma = !sigma in let id = match name with - | Names.Anonymous -> + | Name.Anonymous -> let id = Namegen.id_of_name_using_hdchar env sigma typ name in Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env)) - | Names.Name id -> id + | Name.Name id -> id in let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere) + (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere) end - + let hget_evar n = let open EConstr in Proofview.Goal.nf_enter begin fun gl -> @@ -108,6 +108,5 @@ let hget_evar n = if n <= 0 then user_err Pp.(str "Incorrect existential variable index."); let ev = List.nth evl (n-1) in let ev_type = EConstr.existential_type sigma ev in - Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl)) + Tactics.change_concl (mkLetIn (Name.Anonymous,mkEvar ev,ev_type,concl)) end - diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4 index b26fd78ef..44f33ab80 100644 --- a/plugins/ltac/extraargs.ml4 +++ b/plugins/ltac/extraargs.ml4 @@ -85,7 +85,7 @@ let pr_int_list_full _prc _prlc _prt l = pr_int_list l let pr_occurrences _prc _prlc _prt l = match l with | ArgArg x -> pr_int_list x - | ArgVar (loc, id) -> Nameops.pr_id id + | ArgVar (loc, id) -> Id.print id let occurrences_of = function | [] -> NoOccurrences @@ -201,8 +201,8 @@ let pr_gen_place pr_id = function | HypLocation (id,InHypValueOnly) -> str "in (Value of " ++ pr_id id ++ str ")" -let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id) -let pr_place _ _ _ = pr_gen_place Nameops.pr_id +let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Id.print id) +let pr_place _ _ _ = pr_gen_place Id.print let pr_hloc = pr_loc_place () () () let intern_place ist = function @@ -238,7 +238,7 @@ ARGUMENT EXTEND hloc END -let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m +let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m ARGUMENT EXTEND rename TYPED AS ident * ident diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4 index 9f53c44a4..18d7b818c 100644 --- a/plugins/ltac/extratactics.ml4 +++ b/plugins/ltac/extratactics.ml4 @@ -464,8 +464,8 @@ open Evar_tactics (* TODO: add support for some test similar to g_constr.name_colon so that expressions like "evar (list A)" do not raise a syntax error *) TACTIC EXTEND evar - [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ] -| [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ] + [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name.Name id) typ ] +| [ "evar" constr(typ) ] -> [ let_evar Name.Anonymous typ ] END TACTIC EXTEND instantiate @@ -516,7 +516,7 @@ let cache_transitivity_lemma (_,(left,lem)) = let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref) -let inTransitivity : bool * Constr.constr -> obj = +let inTransitivity : bool * Term.constr -> obj = declare_object {(default_object "TRANSITIVITY-STEPS") with cache_function = cache_transitivity_lemma; open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o); @@ -684,7 +684,7 @@ let hResolve id c occ t = let sigma = Evd.merge_universe_context sigma ctx in let t_constr_type = Retyping.get_type_of env sigma t_constr in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) - (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl))) + (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl))) end let hResolve_auto id c t = diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4 index 68b63f02c..dfd8e88a9 100644 --- a/plugins/ltac/g_auto.ml4 +++ b/plugins/ltac/g_auto.ml4 @@ -17,7 +17,6 @@ open Pcoq.Prim open Pcoq.Constr open Pltac open Hints -open Names DECLARE PLUGIN "g_auto" diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 3d7d5e3fe..905cfd02a 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -12,7 +12,6 @@ open API open Class_tactics open Stdarg open Tacarg -open Names DECLARE PLUGIN "g_class" diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4 index e91e25111..570cd4e69 100644 --- a/plugins/ltac/g_eqdecide.ml4 +++ b/plugins/ltac/g_eqdecide.ml4 @@ -16,7 +16,6 @@ open API open Eqdecide -open Names DECLARE PLUGIN "g_eqdecide" diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4 index 7855fbcfc..4bab31b85 100644 --- a/plugins/ltac/g_ltac.ml4 +++ b/plugins/ltac/g_ltac.ml4 @@ -231,8 +231,8 @@ GEXTEND Gram | "multimatch" -> General ] ] ; input_fun: - [ [ "_" -> Anonymous - | l = ident -> Name l ] ] + [ [ "_" -> Name.Anonymous + | l = ident -> Name.Name l ] ] ; let_clause: [ [ id = identref; ":="; te = tactic_expr -> @@ -399,7 +399,7 @@ let pr_ltac_selector = function | SelectNth i -> int i ++ str ":" | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str "]" ++ str ":" -| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":" +| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" | SelectAll -> str "all" ++ str ":" VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector @@ -469,14 +469,14 @@ let pr_ltac_production_item = function | None -> mt () | Some sep -> str "," ++ spc () ++ quote (str sep) in - str arg ++ str "(" ++ Nameops.pr_id id ++ sep ++ str ")" + str arg ++ str "(" ++ Id.print id ++ sep ++ str ")" VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item | [ string(s) ] -> [ Tacentries.TacTerm s ] | [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) ] | [ ident(nt) ] -> - [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ] + [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ] END VERNAC COMMAND EXTEND VernacTacticNotation @@ -499,7 +499,7 @@ let pr_ltac_ref = Libnames.pr_reference let pr_tacdef_body tacdef_body = let id, redef, body = match tacdef_body with - | TacticDefinition ((_,id), body) -> Nameops.pr_id id, false, body + | TacticDefinition ((_,id), body) -> Id.print id, false, body | TacticRedefinition (id, body) -> pr_ltac_ref id, true, body in let idl, body = @@ -507,8 +507,8 @@ let pr_tacdef_body tacdef_body = | Tacexpr.TacFun (idl,b) -> idl,b | _ -> [], body in id ++ - prlist (function Anonymous -> str " _" - | Name id -> spc () ++ Nameops.pr_id id) idl + prlist (function Name.Anonymous -> str " _" + | Name.Name id -> spc () ++ Id.print id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ Pptactic.pr_raw_tactic body diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4 index e94cf1c63..a971fc79f 100644 --- a/plugins/ltac/g_tactic.ml4 +++ b/plugins/ltac/g_tactic.ml4 @@ -477,7 +477,7 @@ GEXTEND Gram | -> None ] ] ; as_name: - [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ] + [ [ "as"; id = ident ->Names.Name.Name id | -> Names.Name.Anonymous ] ] ; by_tactic: [ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac @@ -540,7 +540,7 @@ GEXTEND Gram TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd)) | IDENT "pose"; (id,b) = bindings_with_parameters -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,b,Locusops.nowhere,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None)) | IDENT "pose"; b = constr; na = as_name -> TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None)) | IDENT "epose"; (id,b) = bindings_with_parameters -> @@ -548,7 +548,7 @@ GEXTEND Gram | IDENT "epose"; b = constr; na = as_name -> TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None)) | IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> - TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,c,p,true,None)) + TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None)) | IDENT "set"; c = constr; na = as_name; p = clause_dft_concl -> TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None)) | IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl -> @@ -600,9 +600,9 @@ GEXTEND Gram TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c)) | IDENT "generalize"; c = constr -> - TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)]) + TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)]) | IDENT "generalize"; c = constr; l = LIST1 constr -> - let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in + let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l))) | IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs; na = as_name; diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index c84a7c00a..8300a55e3 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -335,11 +335,11 @@ type 'a extra_genarg_printer = | ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id) let pr_ltac_constant kn = - if !Flags.in_debugger then pr_kn kn + if !Flags.in_debugger then KerName.print kn else try pr_qualid (Nametab.shortest_qualid_of_tactic kn) with Not_found -> (* local tactic not accessible anymore *) - str "<" ++ pr_kn kn ++ str ">" + str "<" ++ KerName.print kn ++ str ">" let pr_evaluable_reference_env env = function | EvalVarRef id -> pr_id id @@ -482,7 +482,7 @@ type 'a extra_genarg_printer = | SelectNth i -> int i ++ str ":" | SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++ str "]" ++ str ":" - | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":" + | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":" | SelectAll -> str "all" ++ str ":" let pr_lazy = function diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 0fbb9df2d..020b3048f 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -247,7 +247,7 @@ let string_of_call ck = (match ck with | Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s | Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst - | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id + | Tacexpr.LtacVarCall (id, t) -> Names.Id.print id | Tacexpr.LtacAtomCall te -> (Pptactic.pr_glob_tactic (Global.env ()) (Tacexpr.TacAtom (Loc.tag te))) diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml index 9069635c1..3927ca7ce 100644 --- a/plugins/ltac/rewrite.ml +++ b/plugins/ltac/rewrite.ml @@ -427,7 +427,7 @@ let split_head = function | [] -> assert(false) let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') = - pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y') + pb == pb' || (ty == ty' && Term.eq_constr x x' && Term.eq_constr y y') let problem_inclusion x y = List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x @@ -957,7 +957,7 @@ let fold_match ?(force=false) env sigma c = let unfold_match env sigma sk app = match EConstr.kind sigma app with - | App (f', args) when eq_constant (fst (destConst sigma f')) sk -> + | App (f', args) when Constant.equal (fst (destConst sigma f')) sk -> let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in let v = EConstr.of_constr v in Reductionops.whd_beta sigma (mkApp (v, args)) @@ -1371,7 +1371,7 @@ module Strategies = fail cs let inj_open hint = (); fun sigma -> - let ctx = Evd.evar_universe_context_of hint.Autorewrite.rew_ctx in + let ctx = UState.of_context_set hint.Autorewrite.rew_ctx in let sigma = Evd.merge_universe_context sigma ctx in (sigma, (EConstr.of_constr hint.Autorewrite.rew_lemma, NoBindings)) @@ -1472,7 +1472,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul let evars = (!evdref, Evar.Set.empty) in let evars, cstr = let prop, (evars, arrow) = - if is_prop_sort sort then true, app_poly_sort true env evars impl [||] + if Sorts.is_prop sort then true, app_poly_sort true env evars impl [||] else false, app_poly_sort false env evars TypeGlobal.arrow [||] in match is_hyp with @@ -1965,7 +1965,7 @@ let add_morphism_infer glob m n = if Lib.is_modtype () then let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id (Entries.ParameterEntry - (None,poly,(instance,Evd.evar_context_universe_context uctx),None), + (None,poly,(instance,UState.context uctx),None), Decl_kinds.IsAssumption Decl_kinds.Logical) in add_instance (Typeclasses.new_instance diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli index 77286452b..d7f92fd6e 100644 --- a/plugins/ltac/rewrite.mli +++ b/plugins/ltac/rewrite.mli @@ -8,7 +8,6 @@ open API open Names -open Constr open Environ open EConstr open Constrexpr @@ -39,7 +38,7 @@ type ('constr,'redexpr) strategy_ast = type rewrite_proof = | RewPrf of constr * constr - | RewCast of cast_kind + | RewCast of Term.cast_kind type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *) diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml index 14e5aa72a..117a16b0a 100644 --- a/plugins/ltac/taccoerce.ml +++ b/plugins/ltac/taccoerce.ml @@ -132,8 +132,8 @@ let coerce_var_to_ident fresh env sigma v = let coerce_to_ident_not_fresh env sigma v = let g = sigma in let id_of_name = function - | Names.Anonymous -> Id.of_string "x" - | Names.Name x -> x in + | Name.Anonymous -> Id.of_string "x" + | Name.Name x -> x in let v = Value.normalize v in let fail () = raise (CannotCoerceTo "an identifier") in if has_type v (topwit wit_intro_pattern) then diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml index dbc32c2f6..270225e23 100644 --- a/plugins/ltac/tacentries.ml +++ b/plugins/ltac/tacentries.ml @@ -419,7 +419,7 @@ let is_defined_tac kn = let warn_unusable_identifier = CWarnings.create ~name:"unusable-identifier" ~category:"parsing" - (fun id -> strbrk "The Ltac name" ++ spc () ++ pr_id id ++ spc () ++ + (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++ strbrk "may be unusable because of a conflict with a notation.") let register_ltac local tacl = @@ -427,7 +427,7 @@ let register_ltac local tacl = match tactic_body with | Tacexpr.TacticDefinition ((loc,id), body) -> let kn = Lib.make_kn id in - let id_pp = pr_id id in + let id_pp = Id.print id in let () = if is_defined_tac kn then CErrors.user_err ?loc (str "There is already an Ltac named " ++ id_pp ++ str".") @@ -475,7 +475,7 @@ let register_ltac local tacl = let iter (def, tac) = match def with | NewTac id -> Tacenv.register_ltac false local id tac; - Flags.if_verbose Feedback.msg_info (Nameops.pr_id id ++ str " is defined") + Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined") | UpdateTac kn -> Tacenv.redefine_ltac local kn tac; let name = Nametab.shortest_qualid_of_tactic kn in diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 85d3944b1..9d8094205 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -92,7 +92,7 @@ type value = Val.t (** Abstract application, to print ltac functions *) type appl = | UnnamedAppl (** For generic applications: nothing is printed *) - | GlbAppl of (Names.kernel_name * Val.t list) list + | GlbAppl of (Names.KerName.t * Val.t list) list (** For calls to global constants, some may alias other. *) let push_appl appl args = match appl with @@ -257,7 +257,7 @@ let pr_closure env ist body = let pr_sep () = fnl () in let pr_iarg (id, arg) = let arg = pr_argument_type arg in - hov 0 (pr_id id ++ spc () ++ str ":" ++ spc () ++ arg) + hov 0 (Id.print id ++ spc () ++ str ":" ++ spc () ++ arg) in let pp_iargs = v 0 (prlist_with_sep pr_sep pr_iarg (Id.Map.bindings ist)) in pp_body ++ fnl() ++ str "in environment " ++ fnl() ++ pp_iargs @@ -314,7 +314,7 @@ let append_trace trace v = let coerce_to_tactic loc id v = let v = Value.normalize v in let fail () = user_err ?loc - (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.") + (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.") in let v = Value.normalize v in if has_type v (topwit wit_tacvalue) then @@ -369,7 +369,7 @@ let debugging_exception_step ist signal_anomaly e pp = pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) let error_ltac_variable ?loc id env v s = - user_err ?loc (str "Ltac variable " ++ pr_id id ++ + user_err ?loc (str "Ltac variable " ++ Id.print id ++ strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++ strbrk "which cannot be coerced to " ++ str s ++ str".") @@ -403,7 +403,7 @@ let interp_int ist locid = try try_interp_ltac_var coerce_to_int ist None locid with Not_found -> user_err ?loc:(fst locid) ~hdr:"interp_int" - (str "Unbound variable " ++ pr_id (snd locid) ++ str".") + (str "Unbound variable " ++ Id.print (snd locid) ++ str".") let interp_int_or_var ist = function | ArgVar locid -> interp_int ist locid @@ -782,7 +782,7 @@ let interp_may_eval f ist env sigma = function with | Not_found -> user_err ?loc ~hdr:"interp_may_eval" - (str "Unbound context identifier" ++ pr_id s ++ str".")) + (str "Unbound context identifier" ++ Id.print s ++ str".")) | ConstrTypeOf c -> let (sigma,c_interp) = f ist env sigma c in let (sigma, t) = Typing.type_of ~refresh:true env sigma c_interp in @@ -858,7 +858,7 @@ let rec message_of_value v = end else if has_type v (topwit wit_var) then let id = out_gen (topwit wit_var) v in - Ftactic.enter begin fun gl -> Ftactic.return (pr_id id) end + Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end else match Value.to_list v with | Some l -> Ftactic.List.map message_of_value l >>= fun l -> @@ -873,7 +873,7 @@ let interp_message_token ist = function | MsgIdent (loc,id) -> let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in match v with - | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (pr_id id ++ str" not found.")) + | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found.")) | Some v -> message_of_value v let interp_message ist l = @@ -1010,7 +1010,7 @@ let interp_destruction_arg ist gl arg = | keep,ElimOnAnonHyp n as x -> x | keep,ElimOnIdent (loc,id) -> let error () = user_err ?loc - (strbrk "Cannot coerce " ++ pr_id id ++ + (strbrk "Cannot coerce " ++ Id.print id ++ strbrk " neither to a quantified hypothesis nor to a term.") in let try_cast_id id' = @@ -1021,7 +1021,7 @@ let interp_destruction_arg ist gl arg = try (sigma, (constr_of_id env id', NoBindings)) with Not_found -> user_err ?loc ~hdr:"interp_destruction_arg" ( - pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") + Id.print id ++ strbrk " binds to " ++ Id.print id' ++ strbrk " which is neither a declared nor a quantified hypothesis.") end) in try @@ -1088,7 +1088,7 @@ let read_pattern lfun ist env sigma = function let cons_and_check_name id l = if Id.List.mem id l then user_err ~hdr:"read_match_goal_hyps" ( - str "Hypothesis pattern-matching variable " ++ pr_id id ++ + str "Hypothesis pattern-matching variable " ++ Id.print id ++ str " used twice in the same pattern.") else id::l diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 8126421c7..b909c930d 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -12,8 +12,6 @@ open Names open Pp open Tacexpr open Termops -open Nameops - let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () @@ -259,14 +257,14 @@ let db_pattern_rule debug num r = (* Prints the hypothesis pattern identifier if it exists *) let hyp_bound = function | Anonymous -> str " (unbound)" - | Name id -> str " (bound to " ++ pr_id id ++ str ")" + | Name id -> str " (bound to " ++ Id.print id ++ str ")" (* Prints a matched hypothesis *) let db_matched_hyp debug env sigma (id,_,c) ido = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++ + msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++ str " has been matched: " ++ print_constr_env env sigma c) else return () @@ -361,7 +359,7 @@ let explain_ltac_call_trace last trace loc = | Tacexpr.LtacMLCall t -> quote (Pptactic.pr_glob_tactic (Global.env()) t) | Tacexpr.LtacVarCall (id,t) -> - quote (Nameops.pr_id id) ++ strbrk " (bound to " ++ + quote (Id.print id) ++ strbrk " (bound to " ++ Pptactic.pr_glob_tactic (Global.env()) t ++ str ")" | Tacexpr.LtacAtomCall te -> quote (Pptactic.pr_glob_tactic (Global.env()) @@ -372,7 +370,7 @@ let explain_ltac_call_trace last trace loc = strbrk " (with " ++ prlist_with_sep pr_comma (fun (id,c) -> - pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) + Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c) (List.rev (Id.Map.bindings vars)) ++ str ")" else mt()) in diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 13492ed51..5eacb1a95 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -197,7 +197,7 @@ let flatten_contravariant_disj _ ist = let make_unfold name = let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in - let const = Constant.make2 (MPfile dir) (Label.make name) in + let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in (Locus.AllOccurrences, ArgArg (EvalConstRef const, None)) let u_iff = make_unfold "iff" diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml index 03041ea0a..fba1966df 100644 --- a/plugins/micromega/coq_micromega.ml +++ b/plugins/micromega/coq_micromega.ml @@ -20,8 +20,7 @@ open API open Pp open Mutils open Goptions - -module Term = EConstr +open Names (** * Debug flag @@ -110,8 +109,8 @@ type 'cst atom = 'cst Micromega.formula type 'cst formula = | TT | FF - | X of Term.constr - | A of 'cst atom * tag * Term.constr + | X of EConstr.constr + | A of 'cst atom * tag * EConstr.constr | C of 'cst formula * 'cst formula | D of 'cst formula * 'cst formula | N of 'cst formula @@ -329,9 +328,6 @@ let selecti s m = module M = struct - open Constr - open EConstr - (** * Location of the Coq libraries. *) @@ -603,10 +599,10 @@ struct let get_left_construct sigma term = match EConstr.kind sigma term with - | Constr.Construct((_,i),_) -> (i,[| |]) - | Constr.App(l,rst) -> + | Term.Construct((_,i),_) -> (i,[| |]) + | Term.App(l,rst) -> (match EConstr.kind sigma l with - | Constr.Construct((_,i),_) -> (i,rst) + | Term.Construct((_,i),_) -> (i,rst) | _ -> raise ParseError ) | _ -> raise ParseError @@ -627,7 +623,7 @@ struct let rec dump_nat x = match x with | Mc.O -> Lazy.force coq_O - | Mc.S p -> Term.mkApp(Lazy.force coq_S,[| dump_nat p |]) + | Mc.S p -> EConstr.mkApp(Lazy.force coq_S,[| dump_nat p |]) let rec parse_positive sigma term = let (i,c) = get_left_construct sigma term in @@ -640,28 +636,28 @@ struct let rec dump_positive x = match x with | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_positive p |]) - | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_positive p |]) + | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_positive p |]) + | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_positive p |]) let pp_positive o x = Printf.fprintf o "%i" (CoqToCaml.positive x) let dump_n x = match x with | Mc.N0 -> Lazy.force coq_N0 - | Mc.Npos p -> Term.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) + | Mc.Npos p -> EConstr.mkApp(Lazy.force coq_Npos,[| dump_positive p|]) let rec dump_index x = match x with | Mc.XH -> Lazy.force coq_xH - | Mc.XO p -> Term.mkApp(Lazy.force coq_xO,[| dump_index p |]) - | Mc.XI p -> Term.mkApp(Lazy.force coq_xI,[| dump_index p |]) + | Mc.XO p -> EConstr.mkApp(Lazy.force coq_xO,[| dump_index p |]) + | Mc.XI p -> EConstr.mkApp(Lazy.force coq_xI,[| dump_index p |]) let pp_index o x = Printf.fprintf o "%i" (CoqToCaml.index x) let pp_n o x = output_string o (string_of_int (CoqToCaml.n x)) let dump_pair t1 t2 dump_t1 dump_t2 (x,y) = - Term.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|]) + EConstr.mkApp(Lazy.force coq_pair,[| t1 ; t2 ; dump_t1 x ; dump_t2 y|]) let parse_z sigma term = let (i,c) = get_left_construct sigma term in @@ -674,23 +670,23 @@ struct let dump_z x = match x with | Mc.Z0 ->Lazy.force coq_ZERO - | Mc.Zpos p -> Term.mkApp(Lazy.force coq_POS,[| dump_positive p|]) - | Mc.Zneg p -> Term.mkApp(Lazy.force coq_NEG,[| dump_positive p|]) + | Mc.Zpos p -> EConstr.mkApp(Lazy.force coq_POS,[| dump_positive p|]) + | Mc.Zneg p -> EConstr.mkApp(Lazy.force coq_NEG,[| dump_positive p|]) let pp_z o x = Printf.fprintf o "%s" (Big_int.string_of_big_int (CoqToCaml.z_big_int x)) let dump_num bd1 = - Term.mkApp(Lazy.force coq_Qmake, - [|dump_z (CamlToCoq.bigint (numerator bd1)) ; - dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |]) + EConstr.mkApp(Lazy.force coq_Qmake, + [|dump_z (CamlToCoq.bigint (numerator bd1)) ; + dump_positive (CamlToCoq.positive_big_int (denominator bd1)) |]) let dump_q q = - Term.mkApp(Lazy.force coq_Qmake, - [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|]) + EConstr.mkApp(Lazy.force coq_Qmake, + [| dump_z q.Micromega.qnum ; dump_positive q.Micromega.qden|]) let parse_q sigma term = match EConstr.kind sigma term with - | Constr.App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then + | Term.App(c, args) -> if EConstr.eq_constr sigma c (Lazy.force coq_Qmake) then {Mc.qnum = parse_z sigma args.(0) ; Mc.qden = parse_positive sigma args.(1) } else raise ParseError | _ -> raise ParseError @@ -713,13 +709,13 @@ struct match cst with | Mc.C0 -> Lazy.force coq_C0 | Mc.C1 -> Lazy.force coq_C1 - | Mc.CQ q -> Term.mkApp(Lazy.force coq_CQ, [| dump_q q |]) - | Mc.CZ z -> Term.mkApp(Lazy.force coq_CZ, [| dump_z z |]) - | Mc.CPlus(x,y) -> Term.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CMinus(x,y) -> Term.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CMult(x,y) -> Term.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |]) - | Mc.CInv t -> Term.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |]) - | Mc.COpp t -> Term.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |]) + | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_CQ, [| dump_q q |]) + | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_CZ, [| dump_z z |]) + | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_CPlus, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_CMinus, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_CMult, [| dump_Rcst x ; dump_Rcst y |]) + | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_CInv, [| dump_Rcst t |]) + | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_COpp, [| dump_Rcst t |]) let rec parse_Rcst sigma term = let (i,c) = get_left_construct sigma term in @@ -746,8 +742,8 @@ struct let rec dump_list typ dump_elt l = match l with - | [] -> Term.mkApp(Lazy.force coq_nil,[| typ |]) - | e :: l -> Term.mkApp(Lazy.force coq_cons, + | [] -> EConstr.mkApp(Lazy.force coq_nil,[| typ |]) + | e :: l -> EConstr.mkApp(Lazy.force coq_cons, [| typ; dump_elt e;dump_list typ dump_elt l|]) let pp_list op cl elt o l = @@ -777,27 +773,27 @@ struct let dump_expr typ dump_z e = let rec dump_expr e = match e with - | Mc.PEX n -> mkApp(Lazy.force coq_PEX,[| typ; dump_var n |]) - | Mc.PEc z -> mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |]) - | Mc.PEadd(e1,e2) -> mkApp(Lazy.force coq_PEadd, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> mkApp(Lazy.force coq_PEsub, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> mkApp(Lazy.force coq_PEopp, - [| typ; dump_expr e|]) - | Mc.PEmul(e1,e2) -> mkApp(Lazy.force coq_PEmul, - [| typ; dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> mkApp(Lazy.force coq_PEpow, - [| typ; dump_expr e; dump_n n|]) + | Mc.PEX n -> EConstr.mkApp(Lazy.force coq_PEX,[| typ; dump_var n |]) + | Mc.PEc z -> EConstr.mkApp(Lazy.force coq_PEc,[| typ ; dump_z z |]) + | Mc.PEadd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEadd, + [| typ; dump_expr e1;dump_expr e2|]) + | Mc.PEsub(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEsub, + [| typ; dump_expr e1;dump_expr e2|]) + | Mc.PEopp e -> EConstr.mkApp(Lazy.force coq_PEopp, + [| typ; dump_expr e|]) + | Mc.PEmul(e1,e2) -> EConstr.mkApp(Lazy.force coq_PEmul, + [| typ; dump_expr e1;dump_expr e2|]) + | Mc.PEpow(e,n) -> EConstr.mkApp(Lazy.force coq_PEpow, + [| typ; dump_expr e; dump_n n|]) in dump_expr e let dump_pol typ dump_c e = let rec dump_pol e = match e with - | Mc.Pc n -> mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|]) - | Mc.Pinj(p,pol) -> mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|]) - | Mc.PX(pol1,p,pol2) -> mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in + | Mc.Pc n -> EConstr.mkApp(Lazy.force coq_Pc, [|typ ; dump_c n|]) + | Mc.Pinj(p,pol) -> EConstr.mkApp(Lazy.force coq_Pinj , [| typ ; dump_positive p ; dump_pol pol|]) + | Mc.PX(pol1,p,pol2) -> EConstr.mkApp(Lazy.force coq_PX, [| typ ; dump_pol pol1 ; dump_positive p ; dump_pol pol2|]) in dump_pol e let pp_pol pp_c o e = @@ -816,17 +812,17 @@ struct let z = Lazy.force typ in let rec dump_cone e = match e with - | Mc.PsatzIn n -> mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |]) - | Mc.PsatzMulC(e,c) -> mkApp(Lazy.force coq_PsatzMultC, - [| z; dump_pol z dump_z e ; dump_cone c |]) - | Mc.PsatzSquare e -> mkApp(Lazy.force coq_PsatzSquare, - [| z;dump_pol z dump_z e|]) - | Mc.PsatzAdd(e1,e2) -> mkApp(Lazy.force coq_PsatzAdd, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzMulE(e1,e2) -> mkApp(Lazy.force coq_PsatzMulE, - [| z; dump_cone e1; dump_cone e2|]) - | Mc.PsatzC p -> mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|]) - | Mc.PsatzZ -> mkApp( Lazy.force coq_PsatzZ,[| z|]) in + | Mc.PsatzIn n -> EConstr.mkApp(Lazy.force coq_PsatzIn,[| z; dump_nat n |]) + | Mc.PsatzMulC(e,c) -> EConstr.mkApp(Lazy.force coq_PsatzMultC, + [| z; dump_pol z dump_z e ; dump_cone c |]) + | Mc.PsatzSquare e -> EConstr.mkApp(Lazy.force coq_PsatzSquare, + [| z;dump_pol z dump_z e|]) + | Mc.PsatzAdd(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzAdd, + [| z; dump_cone e1; dump_cone e2|]) + | Mc.PsatzMulE(e1,e2) -> EConstr.mkApp(Lazy.force coq_PsatzMulE, + [| z; dump_cone e1; dump_cone e2|]) + | Mc.PsatzC p -> EConstr.mkApp(Lazy.force coq_PsatzC,[| z; dump_z p|]) + | Mc.PsatzZ -> EConstr.mkApp(Lazy.force coq_PsatzZ,[| z|]) in dump_cone e let pp_psatz pp_z o e = @@ -869,10 +865,10 @@ struct Printf.fprintf o"(%a %a %a)" (pp_expr pp_z) l pp_op op (pp_expr pp_z) r let dump_cstr typ dump_constant {Mc.flhs = e1 ; Mc.fop = o ; Mc.frhs = e2} = - Term.mkApp(Lazy.force coq_Build, - [| typ; dump_expr typ dump_constant e1 ; - dump_op o ; - dump_expr typ dump_constant e2|]) + EConstr.mkApp(Lazy.force coq_Build, + [| typ; dump_expr typ dump_constant e1 ; + dump_op o ; + dump_expr typ dump_constant e2|]) let assoc_const sigma x l = try @@ -906,8 +902,8 @@ struct let parse_zop gl (op,args) = let sigma = gl.sigma in match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> + | Term.Const (x,_) -> (assoc_const sigma op zop_table, args.(0) , args.(1)) + | Term.Ind((n,0),_) -> if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_Z) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError @@ -916,8 +912,8 @@ struct let parse_rop gl (op,args) = let sigma = gl.sigma in match EConstr.kind sigma op with - | Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) - | Ind((n,0),_) -> + | Term.Const (x,_) -> (assoc_const sigma op rop_table, args.(0) , args.(1)) + | Term.Ind((n,0),_) -> if EConstr.eq_constr sigma op (Lazy.force coq_Eq) && is_convertible gl args.(0) (Lazy.force coq_R) then (Mc.OpEq, args.(1), args.(2)) else raise ParseError @@ -928,7 +924,7 @@ struct let is_constant sigma t = (* This is an approx *) match EConstr.kind sigma t with - | Construct(i,_) -> true + | Term.Construct(i,_) -> true | _ -> false type 'a op = @@ -949,14 +945,14 @@ struct module Env = struct - type t = constr list + type t = EConstr.constr list let compute_rank_add env sigma v = let rec _add env n v = match env with | [] -> ([v],n) | e::l -> - if eq_constr sigma e v + if EConstr.eq_constr sigma e v then (env,n) else let (env,n) = _add l ( n+1) v in @@ -970,7 +966,7 @@ struct match env with | [] -> raise (Invalid_argument "get_rank") | e::l -> - if eq_constr sigma e v + if EConstr.eq_constr sigma e v then n else _get_rank l (n+1) in _get_rank env 1 @@ -1011,10 +1007,10 @@ struct try (Mc.PEc (parse_constant term) , env) with ParseError -> match EConstr.kind sigma term with - | App(t,args) -> + | Term.App(t,args) -> ( match EConstr.kind sigma t with - | Const c -> + | Term.Const c -> ( match assoc_ops sigma t ops_spec with | Binop f -> combine env f (args.(0),args.(1)) | Opp -> let (expr,env) = parse_expr env args.(0) in @@ -1077,13 +1073,13 @@ struct let rec rconstant sigma term = match EConstr.kind sigma term with - | Const x -> + | Term.Const x -> if EConstr.eq_constr sigma term (Lazy.force coq_R0) then Mc.C0 else if EConstr.eq_constr sigma term (Lazy.force coq_R1) then Mc.C1 else raise ParseError - | App(op,args) -> + | Term.App(op,args) -> begin try (* the evaluation order is important in the following *) @@ -1152,7 +1148,7 @@ struct if debug then Feedback.msg_debug (Pp.str "parse_arith: " ++ Printer.pr_leconstr cstr ++ fnl ()); match EConstr.kind sigma cstr with - | App(op,args) -> + | Term.App(op,args) -> let (op,lhs,rhs) = parse_op gl (op,args) in let (e1,env) = parse_expr sigma env lhs in let (e2,env) = parse_expr sigma env rhs in @@ -1207,29 +1203,29 @@ struct let rec xparse_formula env tg term = match EConstr.kind sigma term with - | App(l,rst) -> + | Term.App(l,rst) -> (match rst with - | [|a;b|] when eq_constr sigma l (Lazy.force coq_and) -> + | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_and) -> let f,env,tg = xparse_formula env tg a in let g,env, tg = xparse_formula env tg b in mkformula_binary mkC term f g,env,tg - | [|a;b|] when eq_constr sigma l (Lazy.force coq_or) -> + | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_or) -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkD term f g,env,tg - | [|a|] when eq_constr sigma l (Lazy.force coq_not) -> + | [|a|] when EConstr.eq_constr sigma l (Lazy.force coq_not) -> let (f,env,tg) = xparse_formula env tg a in (N(f), env,tg) - | [|a;b|] when eq_constr sigma l (Lazy.force coq_iff) -> + | [|a;b|] when EConstr.eq_constr sigma l (Lazy.force coq_iff) -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkIff term f g,env,tg | _ -> parse_atom env tg term) - | Prod(typ,a,b) when Vars.noccurn sigma 1 b -> + | Term.Prod(typ,a,b) when EConstr.Vars.noccurn sigma 1 b -> let f,env,tg = xparse_formula env tg a in let g,env,tg = xparse_formula env tg b in mkformula_binary mkI term f g,env,tg - | _ when eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg) - | _ when eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg) + | _ when EConstr.eq_constr sigma term (Lazy.force coq_True) -> (TT,env,tg) + | _ when EConstr.eq_constr sigma term (Lazy.force coq_False) -> (FF,env,tg) | _ when is_prop term -> X(term),env,tg | _ -> raise ParseError in @@ -1238,14 +1234,14 @@ struct let dump_formula typ dump_atom f = let rec xdump f = match f with - | TT -> mkApp(Lazy.force coq_TT,[|typ|]) - | FF -> mkApp(Lazy.force coq_FF,[|typ|]) - | C(x,y) -> mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|]) - | D(x,y) -> mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|]) - | I(x,_,y) -> mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|]) - | N(x) -> mkApp(Lazy.force coq_Neg,[|typ ; xdump x|]) - | A(x,_,_) -> mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|]) - | X(t) -> mkApp(Lazy.force coq_X,[|typ ; t|]) in + | TT -> EConstr.mkApp(Lazy.force coq_TT,[|typ|]) + | FF -> EConstr.mkApp(Lazy.force coq_FF,[|typ|]) + | C(x,y) -> EConstr.mkApp(Lazy.force coq_And,[|typ ; xdump x ; xdump y|]) + | D(x,y) -> EConstr.mkApp(Lazy.force coq_Or,[|typ ; xdump x ; xdump y|]) + | I(x,_,y) -> EConstr.mkApp(Lazy.force coq_Impl,[|typ ; xdump x ; xdump y|]) + | N(x) -> EConstr.mkApp(Lazy.force coq_Neg,[|typ ; xdump x|]) + | A(x,_,_) -> EConstr.mkApp(Lazy.force coq_Atom,[|typ ; dump_atom x|]) + | X(t) -> EConstr.mkApp(Lazy.force coq_X,[|typ ; t|]) in xdump f @@ -1285,15 +1281,15 @@ struct type 'cst dump_expr = (* 'cst is the type of the syntactic constants *) { - interp_typ : constr; - dump_cst : 'cst -> constr; - dump_add : constr; - dump_sub : constr; - dump_opp : constr; - dump_mul : constr; - dump_pow : constr; - dump_pow_arg : Mc.n -> constr; - dump_op : (Mc.op2 * Term.constr) list + interp_typ : EConstr.constr; + dump_cst : 'cst -> EConstr.constr; + dump_add : EConstr.constr; + dump_sub : EConstr.constr; + dump_opp : EConstr.constr; + dump_mul : EConstr.constr; + dump_pow : EConstr.constr; + dump_pow_arg : Mc.n -> EConstr.constr; + dump_op : (Mc.op2 * EConstr.constr) list } let dump_zexpr = lazy @@ -1327,8 +1323,8 @@ let dump_qexpr = lazy let add = Lazy.force coq_Rplus in let one = Lazy.force coq_R1 in - let mk_add x y = mkApp(add,[|x;y|]) in - let mk_mult x y = mkApp(mult,[|x;y|]) in + let mk_add x y = EConstr.mkApp(add,[|x;y|]) in + let mk_mult x y = EConstr.mkApp(mult,[|x;y|]) in let two = mk_add one one in @@ -1351,13 +1347,13 @@ let rec dump_Rcst_as_R cst = match cst with | Mc.C0 -> Lazy.force coq_R0 | Mc.C1 -> Lazy.force coq_R1 - | Mc.CQ q -> Term.mkApp(Lazy.force coq_IQR, [| dump_q q |]) - | Mc.CZ z -> Term.mkApp(Lazy.force coq_IZR, [| dump_z z |]) - | Mc.CPlus(x,y) -> Term.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CMinus(x,y) -> Term.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CMult(x,y) -> Term.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) - | Mc.CInv t -> Term.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |]) - | Mc.COpp t -> Term.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |]) + | Mc.CQ q -> EConstr.mkApp(Lazy.force coq_IQR, [| dump_q q |]) + | Mc.CZ z -> EConstr.mkApp(Lazy.force coq_IZR, [| dump_z z |]) + | Mc.CPlus(x,y) -> EConstr.mkApp(Lazy.force coq_Rplus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) + | Mc.CMinus(x,y) -> EConstr.mkApp(Lazy.force coq_Rminus, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) + | Mc.CMult(x,y) -> EConstr.mkApp(Lazy.force coq_Rmult, [| dump_Rcst_as_R x ; dump_Rcst_as_R y |]) + | Mc.CInv t -> EConstr.mkApp(Lazy.force coq_Rinv, [| dump_Rcst_as_R t |]) + | Mc.COpp t -> EConstr.mkApp(Lazy.force coq_Ropp, [| dump_Rcst_as_R t |]) let dump_rexpr = lazy @@ -1386,7 +1382,7 @@ let dump_rexpr = lazy let prodn n env b = let rec prodrec = function | (0, env, b) -> b - | (n, ((v,t)::l), b) -> prodrec (n-1, l, mkProd (v,t,b)) + | (n, ((v,t)::l), b) -> prodrec (n-1, l, EConstr.mkProd (v,t,b)) | _ -> assert false in prodrec (n,env,b) @@ -1400,32 +1396,32 @@ let make_goal_of_formula sigma dexpr form = let props = prop_env_of_formula sigma form in - let vars_n = List.map (fun (_,i) -> (Names.id_of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in - let props_n = List.mapi (fun i _ -> (Names.id_of_string (Printf.sprintf "__p%i" (i+1))) , Term.mkProp) props in + let vars_n = List.map (fun (_,i) -> (Names.Id.of_string (Printf.sprintf "__x%i" i)) , dexpr.interp_typ) vars_idx in + let props_n = List.mapi (fun i _ -> (Names.Id.of_string (Printf.sprintf "__p%i" (i+1))) , EConstr.mkProp) props in let var_name_pos = List.map2 (fun (idx,_) (id,_) -> id,idx) vars_idx vars_n in let dump_expr i e = let rec dump_expr = function - | Mc.PEX n -> mkRel (i+(List.assoc (CoqToCaml.positive n) vars_idx)) + | Mc.PEX n -> EConstr.mkRel (i+(List.assoc (CoqToCaml.positive n) vars_idx)) | Mc.PEc z -> dexpr.dump_cst z - | Mc.PEadd(e1,e2) -> mkApp(dexpr.dump_add, + | Mc.PEadd(e1,e2) -> EConstr.mkApp(dexpr.dump_add, [| dump_expr e1;dump_expr e2|]) - | Mc.PEsub(e1,e2) -> mkApp(dexpr.dump_sub, + | Mc.PEsub(e1,e2) -> EConstr.mkApp(dexpr.dump_sub, [| dump_expr e1;dump_expr e2|]) - | Mc.PEopp e -> mkApp(dexpr.dump_opp, - [| dump_expr e|]) - | Mc.PEmul(e1,e2) -> mkApp(dexpr.dump_mul, - [| dump_expr e1;dump_expr e2|]) - | Mc.PEpow(e,n) -> mkApp(dexpr.dump_pow, - [| dump_expr e; dexpr.dump_pow_arg n|]) + | Mc.PEopp e -> EConstr.mkApp(dexpr.dump_opp, + [| dump_expr e|]) + | Mc.PEmul(e1,e2) -> EConstr.mkApp(dexpr.dump_mul, + [| dump_expr e1;dump_expr e2|]) + | Mc.PEpow(e,n) -> EConstr.mkApp(dexpr.dump_pow, + [| dump_expr e; dexpr.dump_pow_arg n|]) in dump_expr e in let mkop op e1 e2 = try - Term.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|]) + EConstr.mkApp(List.assoc op dexpr.dump_op, [| e1; e2|]) with Not_found -> - Term.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in + EConstr.mkApp(Lazy.force coq_Eq,[|dexpr.interp_typ ; e1 ;e2|]) in let dump_cstr i { Mc.flhs ; Mc.fop ; Mc.frhs } = mkop fop (dump_expr i flhs) (dump_expr i frhs) in @@ -1434,13 +1430,13 @@ let make_goal_of_formula sigma dexpr form = match f with | TT -> Lazy.force coq_True | FF -> Lazy.force coq_False - | C(x,y) -> mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) - | D(x,y) -> mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) - | I(x,_,y) -> mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) - | N(x) -> mkArrow (xdump pi xi x) (Lazy.force coq_False) + | C(x,y) -> EConstr.mkApp(Lazy.force coq_and,[|xdump pi xi x ; xdump pi xi y|]) + | D(x,y) -> EConstr.mkApp(Lazy.force coq_or,[| xdump pi xi x ; xdump pi xi y|]) + | I(x,_,y) -> EConstr.mkArrow (xdump pi xi x) (xdump (pi+1) (xi+1) y) + | N(x) -> EConstr.mkArrow (xdump pi xi x) (Lazy.force coq_False) | A(x,_,_) -> dump_cstr xi x | X(t) -> let idx = Env.get_rank props sigma t in - mkRel (pi+idx) in + EConstr.mkRel (pi+idx) in let nb_vars = List.length vars_n in let nb_props = List.length props_n in @@ -1449,12 +1445,12 @@ let make_goal_of_formula sigma dexpr form = let subst_prop p = let idx = Env.get_rank props sigma p in - mkVar (Names.id_of_string (Printf.sprintf "__p%i" idx)) in + EConstr.mkVar (Names.Id.of_string (Printf.sprintf "__p%i" idx)) in let form' = map_prop subst_prop form in - (prodn nb_props (List.map (fun (x,y) -> Names.Name x,y) props_n) - (prodn nb_vars (List.map (fun (x,y) -> Names.Name x,y) vars_n) + (prodn nb_props (List.map (fun (x,y) -> Name.Name x,y) props_n) + (prodn nb_vars (List.map (fun (x,y) -> Name.Name x,y) vars_n) (xdump (List.length vars_n) 0 form)), List.rev props_n, List.rev var_name_pos,form') @@ -1469,7 +1465,7 @@ let make_goal_of_formula sigma dexpr form = | [] -> acc | (e::l) -> let (name,expr,typ) = e in - xset (Term.mkNamedLetIn + xset (EConstr.mkNamedLetIn (Names.Id.of_string name) expr typ acc) l in xset concl l @@ -1545,10 +1541,10 @@ let coq_VarMap = let rec dump_varmap typ m = match m with - | Mc.Empty -> Term.mkApp(Lazy.force coq_Empty,[| typ |]) - | Mc.Leaf v -> Term.mkApp(Lazy.force coq_Leaf,[| typ; v|]) + | Mc.Empty -> EConstr.mkApp(Lazy.force coq_Empty,[| typ |]) + | Mc.Leaf v -> EConstr.mkApp(Lazy.force coq_Leaf,[| typ; v|]) | Mc.Node(l,o,r) -> - Term.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) + EConstr.mkApp (Lazy.force coq_Node, [| typ; dump_varmap typ l; o ; dump_varmap typ r |]) let vm_of_list env = @@ -1570,15 +1566,15 @@ let rec pp_varmap o vm = let rec dump_proof_term = function | Micromega.DoneProof -> Lazy.force coq_doneProof | Micromega.RatProof(cone,rst) -> - Term.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|]) + EConstr.mkApp(Lazy.force coq_ratProof, [| dump_psatz coq_Z dump_z cone; dump_proof_term rst|]) | Micromega.CutProof(cone,prf) -> - Term.mkApp(Lazy.force coq_cutProof, + EConstr.mkApp(Lazy.force coq_cutProof, [| dump_psatz coq_Z dump_z cone ; dump_proof_term prf|]) | Micromega.EnumProof(c1,c2,prfs) -> - Term.mkApp (Lazy.force coq_enumProof, - [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; - dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) + EConstr.mkApp (Lazy.force coq_enumProof, + [| dump_psatz coq_Z dump_z c1 ; dump_psatz coq_Z dump_z c2 ; + dump_list (Lazy.force coq_proofTerm) dump_proof_term prfs |]) let rec size_of_psatz = function @@ -1638,11 +1634,11 @@ let parse_goal gl parse_arith env hyps term = * The datastructures that aggregate theory-dependent proof values. *) type ('synt_c, 'prf) domain_spec = { - typ : Term.constr; (* is the type of the interpretation domain - Z, Q, R*) - coeff : Term.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) - dump_coeff : 'synt_c -> Term.constr ; - proof_typ : Term.constr ; - dump_proof : 'prf -> Term.constr + typ : EConstr.constr; (* is the type of the interpretation domain - Z, Q, R*) + coeff : EConstr.constr ; (* is the type of the syntactic coeffs - Z , Q , Rcst *) + dump_coeff : 'synt_c -> EConstr.constr ; + proof_typ : EConstr.constr ; + dump_proof : 'prf -> EConstr.constr } let zz_domain_spec = lazy { @@ -1707,7 +1703,7 @@ let topo_sort_constr l = let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic*) = (* let ids = Util.List.map_i (fun i _ -> (Names.Id.of_string ("__v"^(string_of_int i)))) 0 env in *) - let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in + let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.coeff spec.dump_coeff) ff in let vm = dump_varmap (spec.typ) (vm_of_list env) in (* todo : directly generate the proof term - or generalize before conversion? *) @@ -1717,8 +1713,8 @@ let micromega_order_change spec cert cert_typ env ff (*: unit Proofview.tactic* Tactics.change_concl (set [ - ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); + ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); + ("__varmap", vm, EConstr.mkApp(Lazy.force coq_VarMap, [|spec.typ|])); ("__wit", cert, cert_typ) ] (Tacmach.New.pf_concl gl)) @@ -1842,20 +1838,20 @@ let abstract_formula hyps f = | A(a,t,term) -> if TagSet.mem t hyps then A(a,t,term) else X(term) | C(f1,f2) -> (match xabs f1 , xabs f2 with - | X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_and, [|a1;a2|])) + | X a1 , X a2 -> X (EConstr.mkApp(Lazy.force coq_and, [|a1;a2|])) | f1 , f2 -> C(f1,f2) ) | D(f1,f2) -> (match xabs f1 , xabs f2 with - | X a1 , X a2 -> X (Term.mkApp(Lazy.force coq_or, [|a1;a2|])) + | X a1 , X a2 -> X (EConstr.mkApp(Lazy.force coq_or, [|a1;a2|])) | f1 , f2 -> D(f1,f2) ) | N(f) -> (match xabs f with - | X a -> X (Term.mkApp(Lazy.force coq_not, [|a|])) + | X a -> X (EConstr.mkApp(Lazy.force coq_not, [|a|])) | f -> N f) | I(f1,hyp,f2) -> (match xabs f1 , hyp, xabs f2 with | X a1 , Some _ , af2 -> af2 - | X a1 , None , X a2 -> X (Term.mkArrow a1 a2) + | X a1 , None , X a2 -> X (EConstr.mkArrow a1 a2) | af1 , _ , af2 -> I(af1,hyp,af2) ) | FF -> FF @@ -1909,7 +1905,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 if debug then begin Feedback.msg_notice (Pp.str "Formula....\n") ; - let formula_typ = (Term.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in + let formula_typ = (EConstr.mkApp(Lazy.force coq_Cstr, [|spec.coeff|])) in let ff = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff in Feedback.msg_notice (Printer.pr_leconstr ff); @@ -1934,7 +1930,7 @@ let micromega_tauto negate normalise unsat deduce spec prover env polys1 polys2 if debug then begin Feedback.msg_notice (Pp.str "\nAFormula\n") ; - let formula_typ = (Term.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in + let formula_typ = (EConstr.mkApp( Lazy.force coq_Cstr,[| spec.coeff|])) in let ff' = dump_formula formula_typ (dump_cstr spec.typ spec.dump_coeff) ff' in Feedback.msg_notice (Printer.pr_leconstr ff'); @@ -1992,11 +1988,11 @@ let micromega_gen let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in + let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; micromega_order_change spec res' - (Term.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in + (EConstr.mkApp(Lazy.force coq_list, [|spec.proof_typ|])) env' ff_arith ] in let goal_props = List.rev (prop_env_of_formula sigma ff') in @@ -2015,8 +2011,8 @@ let micromega_gen [ kill_arith; (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map Term.mkVar ids)); - Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args)) + [(Tactics.generalize (List.map EConstr.mkVar ids)); + Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) ] ) ] with @@ -2044,9 +2040,9 @@ let micromega_order_changer cert env ff = let coeff = Lazy.force coq_Rcst in let dump_coeff = dump_Rcst in let typ = Lazy.force coq_R in - let cert_typ = (Term.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in + let cert_typ = (EConstr.mkApp(Lazy.force coq_list, [|Lazy.force coq_QWitness |])) in - let formula_typ = (Term.mkApp (Lazy.force coq_Cstr,[| coeff|])) in + let formula_typ = (EConstr.mkApp (Lazy.force coq_Cstr,[| coeff|])) in let ff = dump_formula formula_typ (dump_cstr coeff dump_coeff) ff in let vm = dump_varmap (typ) (vm_of_list env) in Proofview.Goal.nf_enter begin fun gl -> @@ -2055,8 +2051,8 @@ let micromega_order_changer cert env ff = (Tactics.change_concl (set [ - ("__ff", ff, Term.mkApp(Lazy.force coq_Formula, [|formula_typ |])); - ("__varmap", vm, Term.mkApp + ("__ff", ff, EConstr.mkApp(Lazy.force coq_Formula, [|formula_typ |])); + ("__varmap", vm, EConstr.mkApp (gen_constant_in_modules "VarMap" [["Coq" ; "micromega" ; "VarMap"] ; ["VarMap"]] "t", [|typ|])); ("__wit", cert, cert_typ) @@ -2107,7 +2103,7 @@ let micromega_genr prover tac = let intro_props = Tacticals.New.tclTHENLIST (List.map intro props) in let ipat_of_name id = Some (Loc.tag @@ Misctypes.IntroNaming (Misctypes.IntroIdentifier id)) in let goal_name = fresh_id [] (Names.Id.of_string "__arith") gl in - let env' = List.map (fun (id,i) -> Term.mkVar id,i) vars in + let env' = List.map (fun (id,i) -> EConstr.mkVar id,i) vars in let tac_arith = Tacticals.New.tclTHENLIST [ intro_props ; intro_vars ; micromega_order_changer res' env' ff_arith ] in @@ -2129,8 +2125,8 @@ let micromega_genr prover tac = [ kill_arith; (Tacticals.New.tclTHENLIST - [(Tactics.generalize (List.map Term.mkVar ids)); - Tactics.exact_check (Term.applist (Term.mkVar goal_name, arith_args)) + [(Tactics.generalize (List.map EConstr.mkVar ids)); + Tactics.exact_check (EConstr.applist (EConstr.mkVar goal_name, arith_args)) ] ) ] diff --git a/plugins/nsatz/g_nsatz.ml4 b/plugins/nsatz/g_nsatz.ml4 index 589c13907..5a6d72036 100644 --- a/plugins/nsatz/g_nsatz.ml4 +++ b/plugins/nsatz/g_nsatz.ml4 @@ -10,7 +10,6 @@ open API open Ltac_plugin -open Names DECLARE PLUGIN "nsatz_plugin" diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli index d6eb1b406..c0dad72ad 100644 --- a/plugins/nsatz/nsatz.mli +++ b/plugins/nsatz/nsatz.mli @@ -7,4 +7,4 @@ (************************************************************************) open API -val nsatz_compute : Constr.t -> unit Proofview.tactic +val nsatz_compute : Term.constr -> unit Proofview.tactic diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 8cea98783..2fcf076f1 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -26,7 +26,7 @@ open Stdarg let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make2 (MPfile dp) (Label.make name) in + let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in let tac = Tacenv.interp_ltac kn in Tacinterp.eval_tactic tac diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml index a81b8944c..15d0f5f37 100644 --- a/plugins/quote/quote.ml +++ b/plugins/quote/quote.ml @@ -169,8 +169,8 @@ exchange ?1 and ?2 in the example above) module ConstrSet = Set.Make( struct - type t = Constr.constr - let compare = constr_ord + type t = Term.constr + let compare = Term.compare end) type inversion_scheme = { @@ -387,7 +387,7 @@ let rec sort_subterm gl l = | h::t -> insert h (sort_subterm gl t) module Constrhash = Hashtbl.Make - (struct type t = Constr.constr + (struct type t = Term.constr let equal = Term.eq_constr let hash = Term.hash_constr end) diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml index 4db4bdc2c..06c80a825 100644 --- a/plugins/romega/const_omega.ml +++ b/plugins/romega/const_omega.ml @@ -7,6 +7,7 @@ *************************************************************************) open API +open Names let module_refl_name = "ReflOmegaCore" let module_refl_path = ["Coq"; "romega"; module_refl_name] @@ -39,7 +40,7 @@ let destructurate t = | Term.Ind (isp,_), args -> Kapp (string_of_global (Globnames.IndRef isp), args) | Term.Var id, [] -> Kvar(Names.Id.to_string id) - | Term.Prod (Names.Anonymous,typ,body), [] -> Kimp(typ,body) + | Term.Prod (Anonymous,typ,body), [] -> Kimp(typ,body) | _ -> Kufo exception DestConstApp @@ -244,7 +245,7 @@ let minus = lazy (z_constant "Z.sub") let recognize_pos t = let rec loop t = let f,l = dest_const_apply t in - match Names.Id.to_string f,l with + match Id.to_string f,l with | "xI",[t] -> Bigint.add Bigint.one (Bigint.mult Bigint.two (loop t)) | "xO",[t] -> Bigint.mult Bigint.two (loop t) | "xH",[] -> Bigint.one @@ -255,7 +256,7 @@ let recognize_pos t = let recognize_Z t = try let f,l = dest_const_apply t in - match Names.Id.to_string f,l with + match Id.to_string f,l with | "Zpos",[t] -> recognize_pos t | "Zneg",[t] -> Option.map Bigint.neg (recognize_pos t) | "Z0",[] -> Some Bigint.zero diff --git a/plugins/romega/g_romega.ml4 b/plugins/romega/g_romega.ml4 index 30d93654b..53f6f42c8 100644 --- a/plugins/romega/g_romega.ml4 +++ b/plugins/romega/g_romega.ml4 @@ -19,7 +19,7 @@ open Stdarg let eval_tactic name = let dp = DirPath.make (List.map Id.of_string ["PreOmega"; "omega"; "Coq"]) in - let kn = KerName.make2 (MPfile dp) (Label.make name) in + let kn = KerName.make2 (ModPath.MPfile dp) (Label.make name) in let tac = Tacenv.interp_ltac kn in Tacinterp.eval_tactic tac diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index b9678fadf..f84eebadc 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -301,7 +301,7 @@ let rtauto_tac gls= build_form formula; build_proof [] 0 prf|]) in let term= - applist (main,List.rev_map (fun (id,_) -> mkVar id) hyps) in + applistc main (List.rev_map (fun (id,_) -> mkVar id) hyps) in let build_end_time=System.get_time () in let _ = if !verbose then begin diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli index c01e63505..ac260e51a 100644 --- a/plugins/rtauto/refl_tauto.mli +++ b/plugins/rtauto/refl_tauto.mli @@ -14,11 +14,11 @@ type atom_env= mutable env:(Term.constr*int) list} val make_form : atom_env -> - Proof_type.goal Tacmach.sigma -> EConstr.types -> Proof_search.form + Proof_type.goal Evd.sigma -> EConstr.types -> Proof_search.form val make_hyps : atom_env -> - Proof_type.goal Tacmach.sigma -> + Proof_type.goal Evd.sigma -> EConstr.types list -> EConstr.named_context -> (Names.Id.t * Proof_search.form) list diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index a107b5948..ee75d2908 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -152,7 +152,7 @@ let ic_unsafe c = (*FIXME remove *) EConstr.of_constr (fst (Constrintern.interp_constr env sigma c)) let decl_constant na ctx c = - let open Constr in + let open Term in let vars = Universes.universes_of_constr c in let ctx = Universes.restrict_universe_context (Univ.ContextSet.of_context ctx) vars in mkConst(declare_constant (Id.of_string na) @@ -283,7 +283,7 @@ let my_reference c = let znew_ring_path = DirPath.make (List.map Id.of_string ["InitialRing";plugin_dir;"Coq"]) let zltac s = - lazy(make_kn (MPfile znew_ring_path) DirPath.empty (Label.make s)) + lazy(KerName.make (ModPath.MPfile znew_ring_path) DirPath.empty (Label.make s)) let mk_cst l s = lazy (Coqlib.coq_reference "newring" l s);; let pol_cst s = mk_cst [plugin_dir;"Ring_polynom"] s ;; @@ -347,7 +347,11 @@ let _ = add_map "ring" let pr_constr c = pr_econstr c -module Cmap = Map.Make(Constr) +module M = struct + type t = Term.constr + let compare = Term.compare +end +module Cmap = Map.Make(M) let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table" let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table" @@ -770,7 +774,7 @@ let new_field_path = DirPath.make (List.map Id.of_string ["Field_tac";plugin_dir;"Coq"]) let field_ltac s = - lazy(make_kn (MPfile new_field_path) DirPath.empty (Label.make s)) + lazy(KerName.make (ModPath.MPfile new_field_path) DirPath.empty (Label.make s)) let _ = add_map "field" @@ -930,7 +934,7 @@ let field_equality evd r inv req = inv_m_lem let add_field_theory0 name fth eqth morphth cst_tac inj (pre,post) power sign odiv = - let open Constr in + let open Term in check_required_library (cdir@["Field_tac"]); let (sigma,fth) = ic fth in let env = Global.env() in diff --git a/plugins/setoid_ring/newring_ast.mli b/plugins/setoid_ring/newring_ast.mli index 46572acd0..b7afd2eff 100644 --- a/plugins/setoid_ring/newring_ast.mli +++ b/plugins/setoid_ring/newring_ast.mli @@ -7,7 +7,7 @@ (************************************************************************) open API -open Constr +open Term open Libnames open Constrexpr open Tacexpr diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 4ddd38365..0f4b86d10 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -94,10 +94,10 @@ type ssrintrosarg = Tacexpr.raw_tactic_expr * ssripats type ssrfwdid = Id.t (** Binders (for fwd tactics) *) type 'term ssrbind = - | Bvar of name - | Bdecl of name list * 'term - | Bdef of name * 'term option * 'term - | Bstruct of name + | Bvar of Name.t + | Bdecl of Name.t list * 'term + | Bdef of Name.t * 'term option * 'term + | Bstruct of Name.t | Bcast of 'term (* We use an intermediate structure to correctly render the binder list *) (* abbreviations. We use a list of hints to extract the binders and *) diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 38ee4be45..d389f7085 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -13,7 +13,7 @@ open Grammar_API open Util open Names open Evd -open Constr +open Term open Termops open Printer open Locusops @@ -133,7 +133,7 @@ let tac_on_all gl tac = (* Used to thread data between intro patterns at run time *) type tac_ctx = { - tmp_ids : (Id.t * name ref) list; + tmp_ids : (Id.t * Name.t ref) list; wild_ids : Id.t list; delayed_clears : Id.t list; } @@ -308,7 +308,7 @@ let is_internal_name s = List.exists (fun p -> p s) !internal_names let tmp_tag = "_the_" let tmp_post = "_tmp_" let mk_tmp_id i = - id_of_string (Printf.sprintf "%s%s%s" tmp_tag (CString.ordinal i) tmp_post) + Id.of_string (Printf.sprintf "%s%s%s" tmp_tag (CString.ordinal i) tmp_post) let new_tmp_id ctx = let id = mk_tmp_id (1 + List.length ctx.tmp_ids) in let orig = ref Anonymous in @@ -318,7 +318,7 @@ let new_tmp_id ctx = let mk_internal_id s = let s' = Printf.sprintf "_%s_" s in let s' = String.map (fun c -> if c = ' ' then '_' else c) s' in - add_internal_name ((=) s'); id_of_string s' + add_internal_name ((=) s'); Id.of_string s' let same_prefix s t n = let rec loop i = i = n || s.[i] = t.[i] && loop (i + 1) in loop 0 @@ -327,7 +327,7 @@ let skip_digits s = let n = String.length s in let rec loop i = if i < n && is_digit s.[i] then loop (i + 1) else i in loop -let mk_tagged_id t i = id_of_string (Printf.sprintf "%s%d_" t i) +let mk_tagged_id t i = Id.of_string (Printf.sprintf "%s%d_" t i) let is_tagged t s = let n = String.length s - 1 and m = String.length t in m < n && s.[n] = '_' && same_prefix s t m && skip_digits s m = n @@ -341,7 +341,7 @@ let ssr_anon_hyp = "Hyp" let wildcard_tag = "_the_" let wildcard_post = "_wildcard_" let mk_wildcard_id i = - id_of_string (Printf.sprintf "%s%s%s" wildcard_tag (CString.ordinal i) wildcard_post) + Id.of_string (Printf.sprintf "%s%s%s" wildcard_tag (CString.ordinal i) wildcard_post) let has_wildcard_tag s = let n = String.length s in let m = String.length wildcard_tag in let m' = String.length wildcard_post in @@ -357,15 +357,15 @@ let new_wild_id ctx = let discharged_tag = "_discharged_" let mk_discharged_id id = - id_of_string (Printf.sprintf "%s%s_" discharged_tag (string_of_id id)) + Id.of_string (Printf.sprintf "%s%s_" discharged_tag (Id.to_string id)) let has_discharged_tag s = let m = String.length discharged_tag and n = String.length s - 1 in m < n && s.[n] = '_' && same_prefix s discharged_tag m let _ = add_internal_name has_discharged_tag -let is_discharged_id id = has_discharged_tag (string_of_id id) +let is_discharged_id id = has_discharged_tag (Id.to_string id) let max_suffix m (t, j0 as tj0) id = - let s = string_of_id id in let n = String.length s - 1 in + let s = Id.to_string id in let n = String.length s - 1 in let dn = String.length t - 1 - n in let i0 = j0 - dn in if not (i0 >= m && s.[n] = '_' && same_prefix s t m) then tj0 else let rec loop i = @@ -385,7 +385,7 @@ let mk_anon_id t gl = let rec loop i j = let d = !s.[i] in if not (is_digit d) then i + 1, j else loop (i - 1) (if d = '0' then j else i) in - let m, j = loop (n - 1) n in m, (!s, j), id_of_string !s in + let m, j = loop (n - 1) n in m, (!s, j), Id.of_string !s in let gl_ids = pf_ids_of_hyps gl in if not (List.mem id0 gl_ids) then id0 else let s, i = List.fold_left (max_suffix m) si0 gl_ids in @@ -403,7 +403,7 @@ let convert_concl t = Tactics.convert_concl t Term.DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with - | Constr.Prod(_,src,tgt) -> + | Term.Prod(_,src,tgt) -> Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl | _ -> CErrors.anomaly (str "gentac creates no product") @@ -602,7 +602,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let rec loopP evlist c i = function | (_, (n, t, _)) :: evl -> let t = get evlist (i - 1) t in - let n = Name (id_of_string (ssr_anon_hyp ^ string_of_int n)) in + let n = Name (Id.of_string (ssr_anon_hyp ^ string_of_int n)) in loopP evlist (mkProd (n, t, c)) (i - 1) evl | [] -> c in let rec loop c i = function @@ -626,13 +626,13 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let nb_evar_deps = function | Name id -> - let s = string_of_id id in + let s = Id.to_string id in if not (is_tagged evar_tag s) then 0 else let m = String.length evar_tag in (try int_of_string (String.sub s m (String.length s - 1 - m)) with _ -> 0) | _ -> 0 -let pf_type_id gl t = id_of_string (Namegen.hdchar (pf_env gl) (project gl) t) +let pf_type_id gl t = Id.of_string (Namegen.hdchar (pf_env gl) (project gl) t) let pfe_type_of gl t = let sigma, ty = pf_type_of gl t in re_sig (sig_it gl) sigma, ty @@ -691,7 +691,7 @@ let pf_merge_uc_of sigma gl = let rec constr_name sigma c = match EConstr.kind sigma c with | Var id -> Name id | Cast (c', _, _) -> constr_name sigma c' - | Const (cn,_) -> Name (Label.to_id (con_label cn)) + | Const (cn,_) -> Name (Label.to_id (Constant.label cn)) | App (c', _) -> constr_name sigma c' | _ -> Anonymous @@ -703,9 +703,9 @@ let pf_mkprod gl c ?(name=constr_name (project gl) c) cl = let pf_abs_prod name gl c cl = pf_mkprod gl c ~name (Termops.subst_term (project gl) c cl) (** look up a name in the ssreflect internals module *) -let ssrdirpath = DirPath.make [id_of_string "ssreflect"] -let ssrqid name = Libnames.make_qualid ssrdirpath (id_of_string name) -let ssrtopqid name = Libnames.qualid_of_ident (id_of_string name) +let ssrdirpath = DirPath.make [Id.of_string "ssreflect"] +let ssrqid name = Libnames.make_qualid ssrdirpath (Id.of_string name) +let ssrtopqid name = Libnames.qualid_of_ident (Id.of_string name) let locate_reference qid = Smartlocate.global_of_extended_global (Nametab.locate_extended qid) let mkSsrRef name = @@ -814,7 +814,7 @@ let ssr_n_tac seed n gl = let name = if n = -1 then seed else ("ssr" ^ seed ^ string_of_int n) in let fail msg = CErrors.user_err (Pp.str msg) in let tacname = - try Nametab.locate_tactic (Libnames.qualid_of_ident (id_of_string name)) + try Nametab.locate_tactic (Libnames.qualid_of_ident (Id.of_string name)) with Not_found -> try Nametab.locate_tactic (ssrqid name) with Not_found -> if n = -1 then fail "The ssreflect library was not loaded" @@ -1082,7 +1082,7 @@ let introid ?(orig=ref Anonymous) name = tclTHEN (fun gl -> let anontac decl gl = let id = match RelDecl.get_name decl with | Name id -> - if is_discharged_id id then id else mk_anon_id (string_of_id id) gl + if is_discharged_id id then id else mk_anon_id (Id.to_string id) gl | _ -> mk_anon_id ssr_anon_hyp gl in introid id gl diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 1b6a700b2..7a4b47a46 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -57,7 +57,7 @@ type 'a tac_a = (goal * 'a) sigma -> (goal * 'a) list sigma (* Thread around names to be cleared or generalized back, and the speed *) type tac_ctx = { - tmp_ids : (Id.t * name ref) list; + tmp_ids : (Id.t * Name.t ref) list; wild_ids : Id.t list; (* List of variables to be cleared at the end of the sentence *) delayed_clears : Id.t list; @@ -175,17 +175,17 @@ val pf_abs_evars : Proof_type.goal Evd.sigma -> evar_map * EConstr.t -> int * EConstr.t * Evar.t list * - Evd.evar_universe_context + UState.t val pf_abs_evars2 : (* ssr2 *) Proof_type.goal Evd.sigma -> Evar.t list -> evar_map * EConstr.t -> int * EConstr.t * Evar.t list * - Evd.evar_universe_context + UState.t val pf_abs_cterm : Proof_type.goal Evd.sigma -> int -> EConstr.t -> EConstr.t val pf_merge_uc : - Evd.evar_universe_context -> 'a Evd.sigma -> 'a Evd.sigma + UState.t -> 'a Evd.sigma -> 'a Evd.sigma val pf_merge_uc_of : evar_map -> 'a Evd.sigma -> 'a Evd.sigma val constr_name : evar_map -> EConstr.t -> Name.t @@ -196,14 +196,14 @@ val pfe_type_of : Proof_type.goal Evd.sigma -> EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types val pf_abs_prod : - Names.name -> + Name.t -> Proof_type.goal Evd.sigma -> EConstr.t -> EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types val pf_mkprod : Proof_type.goal Evd.sigma -> EConstr.t -> - ?name:Names.name -> + ?name:Name.t -> EConstr.t -> Proof_type.goal Evd.sigma * EConstr.types val mkSsrRRef : string -> Glob_term.glob_constr * 'a option @@ -229,7 +229,7 @@ val is_tagged : string -> string -> bool val has_discharged_tag : string -> bool val ssrqid : string -> Libnames.qualid val new_tmp_id : - tac_ctx -> (Names.Id.t * Names.name ref) * tac_ctx + tac_ctx -> (Names.Id.t * Name.t ref) * tac_ctx val mk_anon_id : string -> Proof_type.goal Evd.sigma -> Id.t val pf_abs_evars_pirrel : Proof_type.goal Evd.sigma -> @@ -286,7 +286,7 @@ val pf_abs_ssrterm : ist -> Proof_type.goal Evd.sigma -> ssrterm -> - evar_map * EConstr.t * Evd.evar_universe_context * int + evar_map * EConstr.t * UState.t * int val pf_interp_ty : ?resolve_typeclasses:bool -> @@ -294,7 +294,7 @@ val pf_interp_ty : Proof_type.goal Evd.sigma -> Ssrast.ssrtermkind * (Glob_term.glob_constr * Constrexpr.constr_expr option) -> - int * EConstr.t * EConstr.t * Evd.evar_universe_context + int * EConstr.t * EConstr.t * UState.t val ssr_n_tac : string -> int -> v82tac val donetac : int -> v82tac @@ -362,7 +362,7 @@ val pf_interp_gen_aux : (Ssrast.ssrhyp list option * Ssrmatching_plugin.Ssrmatching.occ) * Ssrmatching_plugin.Ssrmatching.cpattern -> bool * Ssrmatching_plugin.Ssrmatching.pattern * EConstr.t * - EConstr.t * Ssrast.ssrhyp list * Evd.evar_universe_context * + EConstr.t * Ssrast.ssrhyp list * UState.t * Proof_type.goal Evd.sigma val is_name_in_ipats : @@ -377,7 +377,7 @@ val mk_profiler : string -> profiler (** Basic tactics *) -val introid : ?orig:name ref -> Id.t -> v82tac +val introid : ?orig:Name.t ref -> Id.t -> v82tac val intro_anon : v82tac val intro_all : v82tac diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index dbe13aec9..b0fe89897 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -343,9 +343,9 @@ let pirrel_rewrite pred rdx rdx_ty new_rdx dir (sigma, c) c_ty gl = let elim, gl = pf_fresh_global (Indrec.lookup_eliminator ind sort) gl in if dir = R2L then elim, gl else (* taken from Coq's rewrite *) let elim, _ = Term.destConst elim in - let mp,dp,l = repr_con (constant_of_kn (canonical_con elim)) in + let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical elim)) in let l' = Label.of_id (Nameops.add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (canonical_con (make_con mp dp l')) in + let c1' = Global.constant_of_delta_kn (Constant.canonical (Constant.make3 mp dp l')) in mkConst c1', gl in let elim = EConstr.of_constr elim in let proof = EConstr.mkApp (elim, [| rdx_ty; new_rdx; pred; p; rdx; c |]) in diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml index 2b10f2f35..660c2e776 100644 --- a/plugins/ssr/ssrfwd.ml +++ b/plugins/ssr/ssrfwd.ml @@ -201,7 +201,7 @@ let havetac ist let assert_is_conv gl = try Proofview.V82.of_tactic (convert_concl (EConstr.it_mkProd_or_LetIn concl ctx)) gl with _ -> errorstrm (str "Given proof term is not of type " ++ - pr_econstr (EConstr.mkArrow (EConstr.mkVar (id_of_string "_")) concl)) in + pr_econstr (EConstr.mkArrow (EConstr.mkVar (Id.of_string "_")) concl)) in gl, ty, Tacticals.tclTHEN assert_is_conv (Proofview.V82.of_tactic (Tactics.apply t)), id, itac_c | FwdHave, false, false -> let skols = List.flatten (List.map (function diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml index 96a75ba27..4a9dddd2b 100644 --- a/plugins/ssr/ssripats.ml +++ b/plugins/ssr/ssripats.ml @@ -117,7 +117,7 @@ let delayed_clear force rest clr gl = let ren_clr, ren = List.split (List.map (fun x -> let x = hyp_id x in - let x' = mk_anon_id (string_of_id x) gl in + let x' = mk_anon_id (Id.to_string x) gl in x', (x, x')) clr) in let ctx = { ctx with delayed_clears = ren_clr @ ctx.delayed_clears } in let gl = push_ctx ctx gl in @@ -133,7 +133,7 @@ let with_defective maintac deps clr ist gl = let top_id = match EConstr.kind_of_type (project gl) (pf_concl gl) with | ProdType (Name id, _, _) - when has_discharged_tag (string_of_id id) -> id + when has_discharged_tag (Id.to_string id) -> id | _ -> top_id in let top_gen = mkclr clr, cpattern_of_id top_id in tclTHEN (introid top_id) (maintac deps top_gen ist) gl @@ -143,7 +143,7 @@ let with_defective_a maintac deps clr ist gl = let top_id = match EConstr.kind_of_type sigma (without_ctx pf_concl gl) with | ProdType (Name id, _, _) - when has_discharged_tag (string_of_id id) -> id + when has_discharged_tag (Id.to_string id) -> id | _ -> top_id in let top_gen = mkclr clr, cpattern_of_id top_id in tclTHEN_a (tac_ctx (introid top_id)) (maintac deps top_gen ist) gl diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 5fd377233..3ea8c2431 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -1465,7 +1465,7 @@ let ssr_id_of_string loc s = else Feedback.msg_warning (str ( "The name " ^ s ^ " fits the _xxx_ format used for anonymous variables.\n" ^ "Scripts with explicit references to anonymous variables are fragile.")) - end; id_of_string s + end; Id.of_string s let ssr_null_entry = Gram.Entry.of_parser "ssr_null" (fun _ -> ()) @@ -1555,7 +1555,7 @@ END let ssrautoprop gl = try let tacname = - try Nametab.locate_tactic (qualid_of_ident (id_of_string "ssrautoprop")) + try Nametab.locate_tactic (qualid_of_ident (Id.of_string "ssrautoprop")) with Not_found -> Nametab.locate_tactic (ssrqid "ssrautoprop") in let tacexpr = Loc.tag @@ Tacexpr.Reference (ArgArg (Loc.tag @@ tacname)) in Proofview.V82.of_tactic (eval_tactic (Tacexpr.TacArg tacexpr)) gl @@ -2320,7 +2320,7 @@ let test_idcomma = Gram.Entry.of_parser "test_idcomma" accept_idcomma GEXTEND Gram GLOBAL: ssr_idcomma; ssr_idcomma: [ [ test_idcomma; - ip = [ id = IDENT -> Some (id_of_string id) | "_" -> None ]; "," -> + ip = [ id = IDENT -> Some (Id.of_string id) | "_" -> None ]; "," -> Some ip ] ]; END diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 67b705190..b586d05e1 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -10,7 +10,6 @@ open API open Names -open Constr open Termops open Tacmach open Misctypes @@ -103,10 +102,10 @@ let endclausestac id_map clseq gl_id cl0 gl = | ids, dc' -> forced && ids = [] && (not hide_goal || dc' = [] && c_hidden) in let rec unmark c = match EConstr.kind (project gl) c with - | Var id when hidden_clseq clseq && id = gl_id -> cl0 - | Prod (Name id, t, c') when List.mem_assoc id id_map -> + | Term.Var id when hidden_clseq clseq && id = gl_id -> cl0 + | Term.Prod (Name id, t, c') when List.mem_assoc id id_map -> EConstr.mkProd (Name (orig_id id), unmark t, unmark c') - | LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> + | Term.LetIn (Name id, v, t, c') when List.mem_assoc id id_map -> EConstr.mkLetIn (Name (orig_id id), unmark v, unmark t, unmark c') | _ -> EConstr.map (project gl) unmark c in let utac hyp = diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 6fbfbf03c..4c8827bf8 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -355,7 +355,7 @@ let coerce_search_pattern_to_sort hpat = let coerce hp coe_index = let coe = Classops.get_coercion_value coe_index in try - let coe_ref = reference_of_constr coe in + let coe_ref = global_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] with _ -> diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 051a9fb4e..796b6f43e 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -400,7 +400,7 @@ type pattern_class = | KpatLam | KpatRigid | KpatFlex - | KpatProj of constant + | KpatProj of Constant.t type tpattern = { up_k : pattern_class; @@ -421,7 +421,7 @@ let isRigid c = match kind_of_term c with | Prod _ | Sort _ | Lambda _ | Case _ | Fix _ | CoFix _ -> true | _ -> false -let hole_var = mkVar (id_of_string "_") +let hole_var = mkVar (Id.of_string "_") let pr_constr_pat c0 = let rec wipe_evar c = if isEvar c then hole_var else map_constr wipe_evar c in @@ -448,7 +448,7 @@ let evars_for_FO ~hack env sigma0 (ise0:evar_map) c0 = Context.Named.fold_inside abs_dc ~init:([], (put evi.evar_concl)) dc in let m = Evarutil.new_meta () in ise := meta_declare m t !ise; - sigma := Evd.define k (applist (mkMeta m, a)) !sigma; + sigma := Evd.define k (applistc (mkMeta m) a) !sigma; put (existential_value !sigma ex) end | _ -> map_constr put c in @@ -465,7 +465,7 @@ let mk_tpattern ?p_origin ?(hack=false) env sigma0 (ise, t) ok dir p = | Const (p,_) -> let np = proj_nparams p in if np = 0 || np > List.length a then KpatConst, f, a else - let a1, a2 = List.chop np a in KpatProj p, applist(f, a1), a2 + let a1, a2 = List.chop np a in KpatProj p, (applistc f a1), a2 | Proj (p,arg) -> KpatProj (Projection.constant p), f, a | Var _ | Ind _ | Construct _ -> KpatFixed, f, a | Evar (k, _) -> @@ -571,7 +571,7 @@ let filter_upat_FO i0 f n u fpats = | KpatFlex -> i0 := n; true in if ok then begin if !i0 < np then i0 := np; (u, np) :: fpats end else fpats -exception FoundUnif of (evar_map * evar_universe_context * tpattern) +exception FoundUnif of (evar_map * UState.t * tpattern) (* Note: we don't update env as we descend into the term, as the primitive *) (* unification procedure always rejects subterms with bound variables. *) @@ -714,7 +714,7 @@ type find_P = k:subst -> constr type conclude = unit -> - constr * ssrdir * (Evd.evar_map * Evd.evar_universe_context * constr) + constr * ssrdir * (Evd.evar_map * UState.t * constr) (* upats_origin makes a better error message only *) let mk_tpattern_matcher ?(all_instances=false) @@ -905,7 +905,7 @@ let glob_cpattern gs p = pp(lazy(str"globbing pattern: " ++ pr_term p)); let glob x = snd (glob_ssrterm gs (mk_lterm x)) in let encode k s l = - let name = Name (id_of_string ("_ssrpat_" ^ s)) in + let name = Name (Id.of_string ("_ssrpat_" ^ s)) in k, (mkRCast mkRHole (mkRLambda name mkRHole (mkRApp mkRHole l)), None) in let bind_in t1 t2 = let mkCHole = mkCHole ~loc:None in let n = Name (destCVar t1) in @@ -1131,9 +1131,9 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty = sigma in let red = let rec decode_red (ist,red) = let open CAst in match red with | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None)) - when let id = string_of_id id in let len = String.length id in + when let id = Id.to_string id in let len = String.length id in (len > 8 && String.sub id 0 8 = "_ssrpat_") -> - let id = string_of_id id in let len = String.length id in + let id = Id.to_string id in let len = String.length id in (match String.sub id 8 (len - 8), t with | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x) | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id) @@ -1377,7 +1377,7 @@ let ssrpatterntac _ist (arg_ist,arg) gl = let t = EConstr.of_constr t in let concl_x = EConstr.of_constr concl_x in let gl, tty = pf_type_of gl t in - let concl = EConstr.mkLetIn (Name (id_of_string "selected"), t, tty, concl_x) in + let concl = EConstr.mkLetIn (Name (Id.of_string "selected"), t, tty, concl_x) in Proofview.V82.of_tactic (convert_concl concl DEFAULTcast) gl (* Register "ssrpattern" tactic *) diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index 088dd021e..c2bf12cb6 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -154,7 +154,7 @@ type find_P = instantiation, the proof term and the ssrdit stored in the tpattern @raise UserEerror if too many occurrences were specified *) type conclude = - unit -> constr * ssrdir * (evar_map * Evd.evar_universe_context * constr) + unit -> constr * ssrdir * (evar_map * UState.t * constr) (** [mk_tpattern_matcher b o sigma0 occ sigma_tplist] creates a pair a function [find_P] and [conclude] with the behaviour explained above. @@ -224,12 +224,12 @@ val pf_unify_HO : goal sigma -> EConstr.constr -> EConstr.constr -> goal sigma on top of the former APIs *) val tag_of_cpattern : cpattern -> char val loc_of_cpattern : cpattern -> Loc.t option -val id_of_pattern : pattern -> Names.variable option +val id_of_pattern : pattern -> Names.Id.t option val is_wildcard : cpattern -> bool -val cpattern_of_id : Names.variable -> cpattern +val cpattern_of_id : Names.Id.t -> cpattern val pr_constr_pat : constr -> Pp.std_ppcmds -val pf_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma -val pf_unsafe_merge_uc : Evd.evar_universe_context -> goal Evd.sigma -> goal Evd.sigma +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 (* One can also "Set SsrMatchingDebug" from a .v *) val debug : bool -> unit diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml index f116e3a64..fb657c47c 100644 --- a/plugins/syntax/numbers_syntax.ml +++ b/plugins/syntax/numbers_syntax.ml @@ -25,9 +25,9 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l) let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id) let make_mind mp id = Names.MutInd.make2 mp (Label.make id) -let make_mind_mpfile dir id = make_mind (MPfile (make_dir dir)) id +let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id let make_mind_mpdot dir modname id = - let mp = MPdot (MPfile (make_dir dir), Label.make modname) + let mp = ModPath.MPdot (ModPath.MPfile (make_dir dir), Label.make modname) in make_mind mp id diff --git a/vernac/search.ml b/vernac/search.ml index 916015800..0ff78f439 100644 --- a/vernac/search.ml +++ b/vernac/search.ml @@ -142,7 +142,7 @@ module ConstrPriority = struct -(3*(num_symbols t) + size t) let compare (_,_,_,p1) (_,_,_,p2) = - compare p1 p2 + Pervasives.compare p1 p2 end module PriorityQueue = Heap.Functional(ConstrPriority) |