diff options
92 files changed, 644 insertions, 491 deletions
@@ -73,6 +73,10 @@ Tactics - The `romega` tactics have been deprecated; please use `lia` instead. +- Names of existential variables occurring in Ltac functions + (e.g. "?[n]" or "?n" in terms - not in patterns) are now interpreted + the same way as other variable names occurring in Ltac functions. + Focusing - Focusing bracket `{` now supports named goal selectors, @@ -129,6 +133,9 @@ Standard Library impacts users running Coq without the init library (`-nois` or `-noinit`) and also issuing `Require Import Coq.Init.Datatypes`. +- Added `Bvector.BVeq` that decides whether two `Bvector`s are equal. +- Added notations for `BVxor`, `BVand`, `BVor`, `BVeq` and `BVneg`. + Tools - Coq_makefile lets one override or extend the following variables from @@ -268,7 +268,7 @@ distclean: clean cleanconfig cacheclean timingclean voclean: find theories plugins test-suite \( -name '*.vo' -o -name '*.glob' -o -name "*.cmxs" \ -o -name "*.native" -o -name "*.cmx" -o -name "*.cmi" -o -name "*.o" \) -exec rm -f {} + - find theories plugins test-suite -name .coq-native -empty -exec rm -f {} + + find theories plugins test-suite -name .coq-native -empty -exec rm -rf {} + timingclean: find theories plugins test-suite \( -name '*.v.timing' -o -name '*.v.before-timing' \ diff --git a/checker/environ.ml b/checker/environ.ml index 74cf237763..b172acb126 100644 --- a/checker/environ.ml +++ b/checker/environ.ml @@ -183,7 +183,7 @@ let lookup_mind kn env = let add_mind kn mib env = if Mindmap_env.mem kn env.env_globals.env_inductives then - Printf.ksprintf anomaly ("Inductive %s is already defined.") + Printf.ksprintf anomaly ("Mutual inductive block %s is already defined.") (MutInd.to_string kn); let new_inds = Mindmap_env.add kn mib env.env_globals.env_inductives in let kn1,kn2 = MutInd.user kn, MutInd.canonical kn in diff --git a/checker/indtypes.ml b/checker/indtypes.ml index 8f11e01c33..1fd86bc368 100644 --- a/checker/indtypes.ml +++ b/checker/indtypes.ml @@ -595,8 +595,12 @@ let check_subtyping cumi paramsctxt env inds = (************************************************************************) (************************************************************************) +let print_mutind ind = + let kn = MutInd.user ind in + str (ModPath.to_string (KerName.modpath kn) ^ "." ^ Label.to_string (KerName.label kn)) + let check_inductive env kn mib = - Flags.if_verbose Feedback.msg_notice (str " checking ind: " ++ MutInd.print kn); + Flags.if_verbose Feedback.msg_notice (str " checking mutind block: " ++ print_mutind kn); (* check mind_constraints: should be consistent with env *) let env0 = match mib.mind_universes with diff --git a/checker/typeops.ml b/checker/typeops.ml index 138fe8bc95..e4c3f4ae4b 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -158,7 +158,7 @@ let judge_of_inductive_knowing_parameters env (ind,u) (paramstyp:constr array) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) + failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind)) in type_of_inductive_knowing_parameters env (specif,u) paramstyp @@ -172,7 +172,7 @@ let judge_of_constructor env (c,u) = let specif = try lookup_mind_specif env ind with Not_found -> - failwith ("Cannot find inductive: "^MutInd.to_string (fst ind)) + failwith ("Cannot find mutual inductive block: "^MutInd.to_string (fst ind)) in type_of_constructor (c,u) specif diff --git a/checker/validate.ml b/checker/validate.ml index f831875dd4..c214409a2c 100644 --- a/checker/validate.ml +++ b/checker/validate.ml @@ -85,6 +85,7 @@ let rec val_gen v ctx o = match v with | Fail s -> fail ctx o ("unexpected object " ^ s) | Annot (s,v) -> val_gen v (ctx/CtxAnnot s) o | Dyn -> val_dyn ctx o + | Proxy { contents = v } -> val_gen v ctx o (* Check that an object is a tuple (or a record). vs is an array of value representation for each field. Its size corresponds to the diff --git a/checker/values.ml b/checker/values.ml index 801874773a..35027d5bfb 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -45,6 +45,13 @@ type value = | String | Annot of string * value | Dyn + | Proxy of value ref + +let fix (f : value -> value) : value = + let self = ref Any in + let ans = f (Proxy self) in + let () = self := ans in + ans (** Some pseudo-constructors *) @@ -347,18 +354,16 @@ let v_states = v_pair Any v_frozen let v_state = Tuple ("state", [|v_states; Any; v_bool|]) let v_vcs = - let data = Opt Any in - let vcs = + let vcs self = Tuple ("vcs", [|Any; Any; Tuple ("dag", [|Any; Any; v_map Any (Tuple ("state_info", - [|Any; Any; Opt v_state; v_pair data Any|])) + [|Any; Any; Opt v_state; v_pair (Opt self) Any|])) |]) |]) in - let () = Obj.set_field (Obj.magic data) 0 (Obj.magic vcs) in - vcs + fix vcs let v_uuid = Any let v_request id doc = diff --git a/checker/values.mli b/checker/values.mli index 20b9d54a68..1b1437a469 100644 --- a/checker/values.mli +++ b/checker/values.mli @@ -20,6 +20,7 @@ type value = | String | Annot of string * value | Dyn + | Proxy of value ref val v_univopaques : value val v_libsum : value diff --git a/checker/votour.ml b/checker/votour.ml index bc820e23dd..1ea0de456e 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -152,6 +152,7 @@ let rec get_name ?(extra=false) = function |String -> "string" |Annot (s,v) -> s^"/"^get_name ~extra v |Dyn -> "<dynamic>" + | Proxy v -> get_name ~extra !v (** For tuples, its quite handy to display the inner 1st string (if any). Cf. [structure_body] for instance *) @@ -255,6 +256,7 @@ let rec get_children v o pos = match v with | _ -> raise Exit end |Fail s -> raise Forbidden + | Proxy v -> get_children !v o pos let get_children v o pos = try get_children v o pos diff --git a/configure.ml b/configure.ml index 1c2edefc5c..1b0c592e46 100644 --- a/configure.ml +++ b/configure.ml @@ -649,9 +649,8 @@ let camltag = match caml_version_list with 50: unexpected documentation comment: too common and annoying to avoid 56: unreachable match case: the [_ -> .] syntax doesn't exist in 4.02.3 58: "no cmx file was found in path": See https://github.com/ocaml/num/issues/9 - 59: "potential assignment to a non-mutable value": See Coq's issue #8043 *) -let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58-59" +let coq_warnings = "-w +a-4-9-27-41-42-44-45-48-50-58" let coq_warn_error = if !prefs.warn_error then "-warn-error +a" diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 4f3d793ed4..fdeb0abed4 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -1,3 +1,12 @@ +## Changes between Coq 8.9 and Coq 8.10 + +### ML API + +Termops: + +- Internal printing functions have been placed under the + `Termops.Internal` namespace. + ## Changes between Coq 8.8 and Coq 8.9 ### ML API diff --git a/dev/top_printers.ml b/dev/top_printers.ml index ab679a71ce..ced6ea2614 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -64,8 +64,14 @@ let ppwf_paths x = pp (Rtree.pp_tree prrecarg x) let envpp pp = let sigma,env = Pfedit.get_current_context () in pp env sigma let rawdebug = ref false let ppevar evk = pp (Evar.print evk) -let ppconstr x = pp (Termops.print_constr (EConstr.of_constr x)) -let ppeconstr x = pp (Termops.print_constr x) +let pr_constr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_constr_env env sigma t +let pr_econstr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_econstr_env env sigma t +let ppconstr x = pp (pr_constr x) +let ppeconstr x = pp (pr_econstr x) let ppconstr_expr x = pp (Ppconstr.pr_constr_expr x) let ppsconstr x = ppconstr (Mod_subst.force_constr x) let ppconstr_univ x = Constrextern.with_universes ppconstr x @@ -95,9 +101,9 @@ let ppidmapgen l = pp (pridmapgen l) let ppevarsubst = ppidmap (fun id0 -> prset (fun (c,copt,id) -> hov 0 - (Termops.print_constr (EConstr.of_constr c) ++ + (pr_constr c ++ (match copt with None -> mt () | Some c -> spc () ++ str "<expanded: " ++ - Termops.print_constr (EConstr.of_constr c) ++ str">") ++ + pr_constr c ++ str">") ++ (if id = id0 then mt () else spc () ++ str "<canonical: " ++ Id.print id ++ str ">")))) @@ -106,7 +112,7 @@ let ppididmap = ppidmap (fun _ -> Id.print) let prconstrunderbindersidmap = pridmap (fun _ (l,c) -> hov 1 (str"[" ++ prlist_with_sep spc Id.print l ++ str"]") - ++ str "," ++ spc () ++ Termops.print_constr c) + ++ str "," ++ spc () ++ pr_econstr c) let ppconstrunderbindersidmap l = pp (prconstrunderbindersidmap l) @@ -155,9 +161,9 @@ let ppdelta s = pp (Mod_subst.debug_pr_delta s) let pp_idpred s = pp (pr_idpred s) let pp_cpred s = pp (pr_cpred s) let pp_transparent_state s = pp (pr_transparent_state s) -let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> Termops.print_constr) n) -let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr n) -let pp_state_t n = pp (Reductionops.pr_state n) +let pp_stack_t n = pp (Reductionops.Stack.pr (EConstr.of_constr %> pr_econstr) n) +let pp_cst_stack_t n = pp (Reductionops.Cst_stack.pr Global.(env()) Evd.empty n) +let pp_state_t n = pp (Reductionops.pr_state Global.(env()) Evd.empty n) (* proof printers *) let pr_evar ev = Pp.int (Evar.repr ev) diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml index 47cfeb98d7..ea126e2756 100644 --- a/dev/vm_printers.ml +++ b/dev/vm_printers.ml @@ -10,7 +10,7 @@ let ppripos (ri,pos) = | Reloc_annot a -> let sp,i = a.ci.ci_ind in print_string - ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") + ("annot : MutInd("^(MutInd.to_string sp)^","^(string_of_int i)^")\n") | Reloc_const _ -> print_string "structured constant\n" | Reloc_getglobal kn -> diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst index daf34500bf..593afa8f20 100644 --- a/doc/sphinx/language/gallina-specification-language.rst +++ b/doc/sphinx/language/gallina-specification-language.rst @@ -522,7 +522,7 @@ The Vernacular ============== .. productionlist:: coq - decorated-sentence : [`decoration`] `sentence` + decorated-sentence : [ `decoration` … `decoration` ] `sentence` sentence : `assumption` : | `definition` : | `inductive` @@ -1438,7 +1438,7 @@ Attributes Any vernacular command can be decorated with a list of attributes, enclosed between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket) -and separated by commas ``,``. +and separated by commas ``,``. Multiple space-separated blocks may be provided. Each attribute has a name (an identifier) and may have a value. A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign), diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 837d3f10a2..be65ff7570 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -35,7 +35,7 @@ Displaying .. cmdv:: Print {? Term } @qualid\@@name This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the raw universe is printed. + An underscore means the usual name is printed. .. cmd:: About @qualid @@ -49,7 +49,7 @@ Displaying .. cmdv:: About @qualid\@@name This locally renames the polymorphic universes of :n:`@qualid`. - An underscore means the raw universe is printed. + An underscore means the usual name is printed. .. cmd:: Print All diff --git a/engine/termops.ml b/engine/termops.ml index 156d1370e3..efe1525c9a 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -22,6 +22,8 @@ module RelDecl = Context.Rel.Declaration module NamedDecl = Context.Named.Declaration module CompactedDecl = Context.Compacted.Declaration +module Internal = struct + (* Sorts and sort family *) let print_sort = function @@ -49,6 +51,8 @@ let pr_puniverses p u = if Univ.Instance.is_empty u then p else p ++ str"(*" ++ Univ.Instance.pr UnivNames.pr_with_global_universes u ++ str"*)" +(* Minimalistic constr printer, typically for debugging *) + let rec pr_constr c = match kind c with | Rel n -> str "#"++int n | Meta n -> str "Meta(" ++ int n ++ str ")" @@ -96,12 +100,16 @@ let rec pr_constr c = match kind c with cut() ++ str":=" ++ pr_constr bd) (Array.to_list fixl)) ++ str"}") -let term_printer = ref (fun _env _sigma c -> pr_constr (EConstr.Unsafe.to_constr c)) +let debug_print_constr c = pr_constr EConstr.Unsafe.(to_constr c) +let debug_print_constr_env env sigma c = pr_constr EConstr.(to_constr sigma c) +let term_printer = ref debug_print_constr_env + let print_constr_env env sigma t = !term_printer env sigma t let print_constr t = let env = Global.env () in let evd = Evd.from_env env in !term_printer env evd t + let set_print_constr f = term_printer := f module EvMap = Evar.Map @@ -1535,3 +1543,6 @@ let env_rel_context_chop k env = let ctx1,ctx2 = List.chop k rels in push_rel_context ctx2 (reset_with_named_context (named_context_val env) env), ctx1 +end + +include Internal diff --git a/engine/termops.mli b/engine/termops.mli index b967bb6abb..aa0f837938 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -311,12 +311,40 @@ val pr_metaset : Metaset.t -> Pp.t val pr_evar_universe_context : UState.t -> Pp.t val pr_evd_level : evar_map -> Univ.Level.t -> Pp.t -(** debug printer: do not use to display terms to the casual user... *) +module Internal : sig -val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit -val print_constr : constr -> Pp.t +(** NOTE: to print terms you always want to use functions in + Printer, not these ones which are for very special cases. *) + +(** debug printers: print raw form for terms, both with + evar-substitution and without. *) +val debug_print_constr : constr -> Pp.t +val debug_print_constr_env : env -> evar_map -> constr -> Pp.t + +(** Pretty-printer hook: [print_constr_env env sigma c] will pretty + print c if the pretty printing layer has been linked into the Coq + binary. *) val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t + +(** [set_print_constr f] sets f to be the pretty printer *) +val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit + +(** Printers for contexts *) val print_named_context : env -> Pp.t val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t + +val print_constr : constr -> Pp.t +[@@deprecated "use print_constr_env"] + +end + +val print_constr : constr -> Pp.t +[@@deprecated "use Internal.print_constr_env"] + +val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t +[@@deprecated "use Internal.print_constr_env"] + +val print_rel_context : env -> Pp.t +[@@deprecated "use Internal.print_rel_context"] diff --git a/engine/univNames.ml b/engine/univNames.ml index e861913de2..9e4c6e47fc 100644 --- a/engine/univNames.ml +++ b/engine/univNames.ml @@ -8,6 +8,7 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +open Util open Names open Univ open Nametab @@ -52,10 +53,10 @@ let empty_binders = Id.Map.empty let universe_binders_table = Summary.ref GlobRef.Map.empty ~name:"universe binders" -let universe_binders_of_global ref : universe_binders = +let universe_binders_of_global ref : Id.t list = try let l = GlobRef.Map.find ref !universe_binders_table in l - with Not_found -> Names.Id.Map.empty + with Not_found -> [] let cache_ubinder (_,(ref,l)) = universe_binders_table := GlobRef.Map.add ref l !universe_binders_table @@ -64,10 +65,28 @@ let subst_ubinder (subst,(ref,l as orig)) = let ref' = fst (Globnames.subst_global subst ref) in if ref == ref' then orig else ref', l +let name_universe lvl = + (** Best-effort naming from the string representation of the level. This is + completely hackish and should be solved in upper layers instead. *) + Id.of_string_soft (Level.to_string lvl) + let discharge_ubinder (_,(ref,l)) = + (** Expand polymorphic binders with the section context *) + let info = Lib.section_segment_of_reference ref in + let sec_inst = Array.to_list (Instance.to_array (info.Lib.abstr_subst)) in + let map lvl = match Level.name lvl with + | None -> (* Having Prop/Set/Var as section universes makes no sense *) + assert false + | Some na -> + try + let qid = Nametab.shortest_qualid_of_universe na in + snd (Libnames.repr_qualid qid) + with Not_found -> name_universe lvl + in + let l = List.map map sec_inst @ l in Some (Lib.discharge_global ref, l) -let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = +let ubinder_obj : GlobRef.t * Id.t list -> Libobject.obj = let open Libobject in declare_object { (default_object "universe binder") with cache_function = cache_ubinder; @@ -78,28 +97,35 @@ let ubinder_obj : GlobRef.t * universe_binders -> Libobject.obj = rebuild_function = (fun x -> x); } let register_universe_binders ref ubinders = - (* Add the polymorphic (section) universes *) - let ubinders = UnivIdMap.fold (fun lvl poly ubinders -> - let qid = Nametab.shortest_qualid_of_universe lvl in - let level = Level.make (fst lvl) (snd lvl) in - if poly then Id.Map.add (snd (Libnames.repr_qualid qid)) level ubinders - else ubinders) - !universe_map ubinders + (** TODO: change the API to register a [Name.t list] instead. This is the last + part of the code that depends on the internal representation of names in + abstract contexts, but removing it requires quite a rework of the + callers. *) + let univs = AUContext.instance (Global.universes_of_global ref) in + let revmap = Id.Map.fold (fun id lvl accu -> LMap.add lvl id accu) ubinders LMap.empty in + let map lvl = + try LMap.find lvl revmap + with Not_found -> name_universe lvl in - if not (Id.Map.is_empty ubinders) - then Lib.add_anonymous_leaf (ubinder_obj (ref,ubinders)) + let ubinders = Array.map_to_list map (Instance.to_array univs) in + if not (List.is_empty ubinders) then Lib.add_anonymous_leaf (ubinder_obj (ref, ubinders)) type univ_name_list = Names.lname list -let universe_binders_with_opt_names ref levels = function - | None -> universe_binders_of_global ref +let universe_binders_with_opt_names ref names = + let orig = universe_binders_of_global ref in + let udecl = match names with + | None -> orig | Some udecl -> - if Int.equal(List.length levels) (List.length udecl) - then - List.fold_left2 (fun acc { CAst.v = na} lvl -> match na with - | Anonymous -> acc - | Name na -> Names.Id.Map.add na lvl acc) - empty_binders udecl levels - else + try + List.map2 (fun orig {CAst.v = na} -> + match na with + | Anonymous -> orig + | Name id -> id) orig udecl + with Invalid_argument _ -> + let len = List.length orig in CErrors.user_err ~hdr:"universe_binders_with_opt_names" - Pp.(str "Universe instance should have length " ++ int (List.length levels)) + Pp.(str "Universe instance should have length " ++ int len) + in + let fold i acc na = Names.Id.Map.add na (Level.var i) acc in + List.fold_left_i fold 0 empty_binders udecl diff --git a/engine/univNames.mli b/engine/univNames.mli index 837beac267..d794d7b744 100644 --- a/engine/univNames.mli +++ b/engine/univNames.mli @@ -27,15 +27,14 @@ type universe_binders = Univ.Level.t Names.Id.Map.t val empty_binders : universe_binders val register_universe_binders : Names.GlobRef.t -> universe_binders -> unit -val universe_binders_of_global : Names.GlobRef.t -> universe_binders type univ_name_list = Names.lname list -(** [universe_binders_with_opt_names ref u l] +(** [universe_binders_with_opt_names ref l] - If [l] is [Some univs] return the universe binders naming the levels of [u] by [univs] (skipping Anonymous). - May error if the lengths mismatch. + If [l] is [Some univs] return the universe binders naming the bound levels + of [ref] by [univs] (skipping Anonymous). May error if the lengths mismatch. - Otherwise return [universe_binders_of_global ref]. *) + Otherwise return the bound universe names registered for [ref]. *) val universe_binders_with_opt_names : Names.GlobRef.t -> - Univ.Level.t list -> univ_name_list option -> universe_binders + univ_name_list option -> universe_binders diff --git a/engine/universes.ml b/engine/universes.ml index ee9668433c..c7e5f654a1 100644 --- a/engine/universes.ml +++ b/engine/universes.ml @@ -26,7 +26,6 @@ let is_polymorphic = UnivNames.is_polymorphic let empty_binders = UnivNames.empty_binders let register_universe_binders = UnivNames.register_universe_binders -let universe_binders_of_global = UnivNames.universe_binders_of_global let universe_binders_with_opt_names = UnivNames.universe_binders_with_opt_names diff --git a/engine/universes.mli b/engine/universes.mli index ad937471e9..7ca33f47a1 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -39,14 +39,12 @@ val empty_binders : universe_binders val register_universe_binders : Globnames.global_reference -> universe_binders -> unit [@@ocaml.deprecated "Use [UnivNames.register_universe_binders]"] -val universe_binders_of_global : Globnames.global_reference -> universe_binders -[@@ocaml.deprecated "Use [UnivNames.universe_binders_of_global]"] type univ_name_list = UnivNames.univ_name_list [@@ocaml.deprecated "Use [UnivNames.univ_name_list]"] val universe_binders_with_opt_names : Globnames.global_reference -> - Univ.Level.t list -> univ_name_list option -> universe_binders + univ_name_list option -> universe_binders [@@ocaml.deprecated "Use [UnivNames.universe_binders_with_opt_names]"] (** ****** Deprecated: moved to [UnivGen] *) diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ddc0a5c000..3996a1756c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -102,7 +102,7 @@ let _show_inactive_notations () = (function | NotationRule (scopt, ntn) -> Feedback.msg_notice (pr_notation ntn ++ show_scope scopt) - | SynDefRule kn -> Feedback.msg_notice (str (Names.KerName.to_string kn))) + | SynDefRule kn -> Feedback.msg_notice (str (string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn)))) !inactive_notations_table let deactivate_notation nr = @@ -135,8 +135,9 @@ let reactivate_notation nr = ++ str "is already active" ++ show_scope scopt ++ str ".") | SynDefRule kn -> + let s = string_of_qualid (Nametab.shortest_qualid_of_syndef Id.Set.empty kn) in Feedback.msg_warning - (str "Notation" ++ spc () ++ str (Names.KerName.to_string kn) + (str "Notation" ++ spc () ++ str s ++ spc () ++ str "is already active.") diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index fd9394025a..c4c96c9b55 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -281,7 +281,7 @@ let assoc_defined id env = match Environ.lookup_named id env with | LocalDef (_, c, _) -> c | _ -> raise Not_found -let ref_value_cache ({i_cache = cache} as infos) tab ref = +let ref_value_cache ({i_cache = cache;_} as infos) tab ref = try Some (KeyTable.find tab ref) with Not_found -> @@ -289,7 +289,7 @@ let ref_value_cache ({i_cache = cache} as infos) tab ref = let body = match ref with | RelKey n -> - let open Context.Rel.Declaration in + let open! Context.Rel.Declaration in let i = n - 1 in let (d, _) = try Range.get cache.i_rels i @@ -837,7 +837,7 @@ let eta_expand_ind_stack env ind m s (f, s') = arg1..argn ~= (proj1 t...projn t) where t = zip (f,s') *) let pars = mib.Declarations.mind_nparams in let right = fapp_stack (f, s') in - let (depth, args, s) = strip_update_shift_app m s in + let (depth, args, _s) = strip_update_shift_app m s in (** Try to drop the params, might fail on partially applied constructors. *) let argss = try_drop_parameters depth pars args in let hstack = Array.map (fun p -> @@ -925,7 +925,7 @@ and knht info e t stk = | Fix _ -> knh info (mk_clos2 e t) stk | Cast(a,_,_) -> knht info e a stk | Rel n -> knh info (clos_rel e n) stk - | Proj (p,c) -> knh info (mk_clos2 e t) stk + | Proj (_p,_c) -> knh info (mk_clos2 e t) stk | (Lambda _|Prod _|Construct _|CoFix _|Ind _| LetIn _|Const _|Var _|Evar _|Meta _|Sort _) -> (mk_clos2 e t, stk) @@ -952,7 +952,7 @@ let rec knr info tab m stk = (match ref_value_cache info tab (RelKey k) with Some v -> kni info tab v stk | None -> (set_norm m; (m,stk))) - | FConstruct((ind,c),u) -> + | FConstruct((_ind,c),_u) -> let use_match = red_set info.i_flags fMATCH in let use_fix = red_set info.i_flags fFIX in if use_match || use_fix then @@ -1018,7 +1018,7 @@ let rec zip_term zfun m stk = zip_term zfun h s | Zshift(n)::s -> zip_term zfun (lift n m) s - | Zupdate(rf)::s -> + | Zupdate(_rf)::s -> zip_term zfun m s (* Computes the strong normal form of a term. @@ -1038,7 +1038,7 @@ let rec kl info tab m = and norm_head info tab m = if is_val m then (incr prune; term_of_fconstr m) else match m.term with - | FLambda(n,tys,f,e) -> + | FLambda(_n,tys,f,e) -> let (e',rvtys) = List.fold_left (fun (e,ctxt) (na,ty) -> (subs_lift e, (na,kl info tab (mk_clos e ty))::ctxt)) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index ed3bd866a4..c63795b295 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -126,8 +126,8 @@ let compare e1 e2 = match e1, e2 with | FVrel r1, FVrel r2 -> Int.compare r1 r2 | FVrel _, (FVuniv_var _ | FVevar _) -> -1 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 -| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1 -| FVuniv_var i1, FVevar _ -> -1 +| FVuniv_var _i1, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var _i1, FVevar _ -> -1 | FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 | FVevar e1, FVevar e2 -> Evar.compare e1 e2 diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 5362f9a814..73620ae578 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -413,7 +413,7 @@ let code_makeblock ~stack_size ~arity ~tag cont = Kpush :: nest_block tag arity cont end -let compile_structured_constant cenv sc sz cont = +let compile_structured_constant _cenv sc sz cont = set_max_stack_size sz; Kconst sc :: cont @@ -534,7 +534,7 @@ let rec compile_lam env cenv lam sz cont = comp_app compile_structured_constant compile_get_univ cenv (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont - | Llet (id,def,body) -> + | Llet (_id,def,body) -> compile_lam env cenv def sz (Kpush :: compile_lam env (push_local sz cenv) body (sz+1) (add_pop 1 cont)) @@ -561,7 +561,7 @@ let rec compile_lam env cenv lam sz cont = | _ -> comp_app (compile_lam env) (compile_lam env) cenv f args sz cont end - | Lfix ((rec_args, init), (decl, types, bodies)) -> + | Lfix ((rec_args, init), (_decl, types, bodies)) -> let ndef = Array.length types in let rfv = ref empty_fv in let lbl_types = Array.make ndef Label.no in @@ -594,7 +594,7 @@ let rec compile_lam env cenv lam sz cont = (Kclosurerec(fv.size,init,lbl_types,lbl_bodies) :: cont) - | Lcofix(init, (decl,types,bodies)) -> + | Lcofix(init, (_decl,types,bodies)) -> let ndef = Array.length types in let lbl_types = Array.make ndef Label.no in let lbl_bodies = Array.make ndef Label.no in diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 31dede6f5d..c21ce22421 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -107,7 +107,7 @@ let rec pp_lam lam = | Lval _ -> str "values" | Lsort s -> pp_sort s | Lind ((mind,i), _) -> MutInd.print mind ++ str"#" ++ int i - | Lprim((kn,_u),ar,op,args) -> + | Lprim((kn,_u),_ar,_op,args) -> hov 1 (str "(PRIM " ++ pr_con kn ++ spc() ++ prlist_with_sep spc pp_lam (Array.to_list args) ++ @@ -215,7 +215,7 @@ let rec map_lam_with_binders g f n lam = let u' = map_uint g f n u in if u == u' then lam else Luint u' -and map_uint g f n u = +and map_uint _g f n u = match u with | UintVal _ -> u | UintDigits(args) -> @@ -532,7 +532,7 @@ struct size = 0; } - let extend v = + let extend (v : 'a t) = if v.size = Array.length v.elems then let new_size = min (2*v.size) Sys.max_array_length in if new_size <= v.size then raise (Invalid_argument "Vect.extend"); @@ -545,12 +545,12 @@ struct v.elems.(v.size) <- a; v.size <- v.size + 1 - let popn v n = + let popn (v : 'a t) n = v.size <- max 0 (v.size - n) let pop v = popn v 1 - let get_last v n = + let get_last (v : 'a t) n = if v.size <= n then raise (Invalid_argument "Vect.get:index out of bounds"); v.elems.(v.size - n - 1) @@ -715,7 +715,7 @@ let rec lambda_of_constr env c = and lambda_of_app env f args = match Constr.kind f with - | Const (kn,u as c) -> + | Const (kn,_u as c) -> let kn = get_alias env.global_env kn in (* spiwack: checks if there is a specific way to compile the constant if there is not, Not_found is raised, and the function diff --git a/kernel/constr.ml b/kernel/constr.ml index c73fe7fbde..b25f38d630 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -360,17 +360,17 @@ let destConst c = match kind c with (* Destructs an existential variable *) let destEvar c = match kind c with - | Evar (kn, a as r) -> r + | Evar (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a (co)inductive type named kn *) let destInd c = match kind c with - | Ind (kn, a as r) -> r + | Ind (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a constructor *) let destConstruct c = match kind c with - | Construct (kn, a as r) -> r + | Construct (_kn, _a as r) -> r | _ -> raise DestKO (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *) @@ -421,12 +421,12 @@ let fold f acc c = match kind c with | Lambda (_,t,c) -> f (f acc t) c | LetIn (_,b,t,c) -> f (f (f acc b) t) c | App (c,l) -> Array.fold_left f (f acc c) l - | Proj (p,c) -> f acc c + | Proj (_p,c) -> f acc c | Evar (_,l) -> Array.fold_left f acc l | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | Fix (_,(lna,tl,bl)) -> + | Fix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl - | CoFix (_,(lna,tl,bl)) -> + | CoFix (_,(_lna,tl,bl)) -> Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl (* [iter f c] iters [f] on the immediate subterms of [c]; it is @@ -441,7 +441,7 @@ let iter f c = match kind c with | Lambda (_,t,c) -> f t; f c | LetIn (_,b,t,c) -> f b; f t; f c | App (c,l) -> f c; Array.iter f l - | Proj (p,c) -> f c + | Proj (_p,c) -> f c | Evar (_,l) -> Array.iter f l | Case (_,p,c,bl) -> f p; f c; Array.iter f bl | Fix (_,(_,tl,bl)) -> Array.iter f tl; Array.iter f bl @@ -463,7 +463,7 @@ let iter_with_binders g f n c = match kind c with | App (c,l) -> f n c; Array.Fun1.iter f n l | Evar (_,l) -> Array.Fun1.iter f n l | Case (_,p,c,bl) -> f n p; f n c; Array.Fun1.iter f n bl - | Proj (p,c) -> f n c + | Proj (_p,c) -> f n c | Fix (_,(_,tl,bl)) -> Array.Fun1.iter f n tl; Array.Fun1.iter f (iterate g (Array.length tl) n) bl @@ -483,19 +483,19 @@ let fold_constr_with_binders g f n acc c = | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _) -> acc | Cast (c,_, t) -> f n (f n acc c) t - | Prod (na,t,c) -> f (g n) (f n acc t) c - | Lambda (na,t,c) -> f (g n) (f n acc t) c - | LetIn (na,b,t,c) -> f (g n) (f n (f n acc b) t) c + | Prod (_na,t,c) -> f (g n) (f n acc t) c + | Lambda (_na,t,c) -> f (g n) (f n acc t) c + | LetIn (_na,b,t,c) -> f (g n) (f n (f n acc b) t) c | App (c,l) -> Array.fold_left (f n) (f n acc c) l - | Proj (p,c) -> f n acc c + | Proj (_p,c) -> f n acc c | Evar (_,l) -> Array.fold_left (f n) acc l | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl | Fix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd | CoFix (_,(lna,tl,bl)) -> - let n' = CArray.fold_left2 (fun c n t -> g c) n lna tl in + let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in let fd = Array.map2 (fun t b -> (t,b)) tl bl in Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd @@ -963,11 +963,11 @@ let constr_ord_int f t1 t2 = | LetIn _, _ -> -1 | _, LetIn _ -> 1 | App (c1,l1), App (c2,l2) -> (f =? (Array.compare f)) c1 c2 l1 l2 | App _, _ -> -1 | _, App _ -> 1 - | Const (c1,u1), Const (c2,u2) -> Constant.CanOrd.compare c1 c2 + | Const (c1,_u1), Const (c2,_u2) -> Constant.CanOrd.compare c1 c2 | Const _, _ -> -1 | _, Const _ -> 1 - | Ind (ind1, u1), Ind (ind2, u2) -> ind_ord ind1 ind2 + | Ind (ind1, _u1), Ind (ind2, _u2) -> ind_ord ind1 ind2 | Ind _, _ -> -1 | _, Ind _ -> 1 - | Construct (ct1,u1), Construct (ct2,u2) -> constructor_ord ct1 ct2 + | Construct (ct1,_u1), Construct (ct2,_u2) -> constructor_ord ct1 ct2 | Construct _, _ -> -1 | _, Construct _ -> 1 | Case (_,p1,c1,bl1), Case (_,p2,c2,bl2) -> ((f =? f) ==? (Array.compare f)) p1 p2 c1 c2 bl1 bl2 @@ -1226,9 +1226,9 @@ let rec hash t = combinesmall 11 (combine (constructor_hash c) (Instance.hash u)) | Case (_ , p, c, bl) -> combinesmall 12 (combine3 (hash c) (hash p) (hash_term_array bl)) - | Fix (ln ,(_, tl, bl)) -> + | Fix (_ln ,(_, tl, bl)) -> combinesmall 13 (combine (hash_term_array bl) (hash_term_array tl)) - | CoFix(ln, (_, tl, bl)) -> + | CoFix(_ln, (_, tl, bl)) -> combinesmall 14 (combine (hash_term_array bl) (hash_term_array tl)) | Meta n -> combinesmall 15 n | Rel n -> combinesmall 16 n diff --git a/kernel/context.ml b/kernel/context.ml index 4a7204b75c..3d98381fbb 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -142,8 +142,8 @@ struct (** Reduce all terms in a given declaration to a single value. *) let fold_constr f decl acc = match decl with - | LocalAssum (n,ty) -> f ty acc - | LocalDef (n,v,ty) -> f ty (f v acc) + | LocalAssum (_n,ty) -> f ty acc + | LocalDef (_n,v,ty) -> f ty (f v acc) let to_tuple = function | LocalAssum (na, ty) -> na, None, ty @@ -151,7 +151,7 @@ struct let drop_body = function | LocalAssum _ as d -> d - | LocalDef (na, v, ty) -> LocalAssum (na, ty) + | LocalDef (na, _v, ty) -> LocalAssum (na, ty) end @@ -356,7 +356,7 @@ struct let drop_body = function | LocalAssum _ as d -> d - | LocalDef (id, v, ty) -> LocalAssum (id, ty) + | LocalDef (id, _v, ty) -> LocalAssum (id, ty) let of_rel_decl f = function | Rel.Declaration.LocalAssum (na,t) -> diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 7ef63c1860..c74f2ab318 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -42,7 +42,7 @@ let empty = { cst_trstate = Cpred.full; } -let get_strategy { var_opacity; cst_opacity } f = function +let get_strategy { var_opacity; cst_opacity; _ } f = function | VarKey id -> (try Id.Map.find id var_opacity with Not_found -> default) @@ -51,7 +51,7 @@ let get_strategy { var_opacity; cst_opacity } f = function with Not_found -> default) | RelKey _ -> Expand -let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = +let set_strategy ({ var_opacity; cst_opacity; _ } as oracle) k l = match k with | VarKey id -> let var_opacity = @@ -75,13 +75,13 @@ let set_strategy ({ var_opacity; cst_opacity } as oracle) k l = { oracle with cst_opacity; cst_trstate; } | RelKey _ -> CErrors.user_err Pp.(str "set_strategy: RelKey") -let fold_strategy f { var_opacity; cst_opacity; } accu = +let fold_strategy f { var_opacity; cst_opacity; _ } accu = let fvar id lvl accu = f (VarKey id) lvl accu in let fcst cst lvl accu = f (ConstKey cst) lvl accu in let accu = Id.Map.fold fvar var_opacity accu in Cmap.fold fcst cst_opacity accu -let get_transp_state { var_trstate; cst_trstate } = (var_trstate, cst_trstate) +let get_transp_state { var_trstate; cst_trstate; _ } = (var_trstate, cst_trstate) (* Unfold the first constant only if it is "more transparent" than the second one. In case of tie, use the recommended default. *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 657478a106..b361e36bbf 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -91,7 +91,7 @@ let update_case_info cache ci modlist = try let ind, n = match share cache (IndRef ci.ci_ind) modlist with - | (IndRef f,(u,l)) -> (f, Array.length l) + | (IndRef f,(_u,l)) -> (f, Array.length l) | _ -> assert false in { ci with ci_ind = ind; ci_npar = ci.ci_npar + n } with Not_found -> diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index bb9231d000..8bef6aec42 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -173,7 +173,7 @@ and slot_for_fv env fv = | Some (v, _) -> v end | FVevar evk -> val_of_evar evk - | FVuniv_var idu -> + | FVuniv_var _idu -> assert false and eval_to_patch env (buff,pl,fv) = @@ -192,5 +192,5 @@ and val_of_constr env c = | Some v -> eval_to_patch env (to_memory v) | None -> assert false -let set_transparent_const kn = () (* !?! *) -let set_opaque_const kn = () (* !?! *) +let set_transparent_const _kn = () (* !?! *) +let set_opaque_const _kn = () (* !?! *) diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 51ec3defb3..d995786d97 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -181,7 +181,7 @@ let subst_regular_ind_arity sub s = if uar' == s.mind_user_arity then s else { mind_user_arity = uar'; mind_sort = s.mind_sort } -let subst_template_ind_arity sub s = s +let subst_template_ind_arity _sub s = s (* FIXME records *) let subst_ind_arity = @@ -240,14 +240,14 @@ let inductive_polymorphic_context mib = let inductive_is_polymorphic mib = match mib.mind_universes with | Monomorphic_ind _ -> false - | Polymorphic_ind ctx -> true - | Cumulative_ind cumi -> true + | Polymorphic_ind _ctx -> true + | Cumulative_ind _cumi -> true let inductive_is_cumulative mib = match mib.mind_universes with | Monomorphic_ind _ -> false - | Polymorphic_ind ctx -> false - | Cumulative_ind cumi -> true + | Polymorphic_ind _ctx -> false + | Cumulative_ind _cumi -> true let inductive_make_projection ind mib ~proj_arg = match mib.mind_record with diff --git a/kernel/dune b/kernel/dune index 011af9c28c..a503238907 100644 --- a/kernel/dune +++ b/kernel/dune @@ -13,3 +13,8 @@ (documentation (package coq)) + +; In dev profile, we check the kernel against a more strict set of +; warnings. +(env + (dev (flags :standard -w +a-4-44-50))) diff --git a/kernel/environ.ml b/kernel/environ.ml index 3bfcaa7f52..dffcd70282 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -296,12 +296,12 @@ let eq_named_context_val c1 c2 = (* A local const is evaluable if it is defined *) -open Context.Named.Declaration - let named_type id env = + let open Context.Named.Declaration in get_type (lookup_named id env) let named_body id env = + let open Context.Named.Declaration in get_value (lookup_named id env) let evaluable_named id env = @@ -333,7 +333,7 @@ let fold_named_context f env ~init = let rec fold_right env = match match_named_context_val env.env_named_context with | None -> init - | Some (d, v, rem) -> + | Some (d, _v, rem) -> let env = reset_with_named_context rem env in f env d (fold_right env) @@ -415,7 +415,7 @@ let constant_type env (kn,u) = let cb = lookup_constant kn env in match cb.const_universes with | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty - | Polymorphic_const ctx -> + | Polymorphic_const _ctx -> let csts = constraints_of cb u in (subst_instance_constr u cb.const_type, csts) @@ -508,14 +508,14 @@ let get_projections env ind = Declareops.inductive_make_projections ind mib (* Mutual Inductives *) -let polymorphic_ind (mind,i) env = +let polymorphic_ind (mind,_i) env = Declareops.inductive_is_polymorphic (lookup_mind mind env) let polymorphic_pind (ind,u) env = if Univ.Instance.is_empty u then false else polymorphic_ind ind env -let type_in_type_ind (mind,i) env = +let type_in_type_ind (mind,_i) env = not (lookup_mind mind env).mind_typing_flags.check_universes let template_polymorphic_ind (mind,i) env = @@ -527,7 +527,7 @@ let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false else template_polymorphic_ind ind env -let add_mind_key kn (mind, _ as mind_key) env = +let add_mind_key kn (_mind, _ as mind_key) env = let new_inds = Mindmap_env.add kn mind_key env.env_globals.env_inductives in let new_globals = { env.env_globals with @@ -543,7 +543,7 @@ let lookup_constant_variables c env = let cmap = lookup_constant c env in Context.Named.to_vars cmap.const_hyps -let lookup_inductive_variables (kn,i) env = +let lookup_inductive_variables (kn,_i) env = let mis = lookup_mind kn env in Context.Named.to_vars mis.mind_hyps @@ -579,6 +579,7 @@ let global_vars_set env constr = contained in the types of the needed variables. *) let really_needed env needed = + let open! Context.Named.Declaration in Context.Named.fold_inside (fun need decl -> if Id.Set.mem (get_id decl) need then @@ -594,6 +595,7 @@ let really_needed env needed = (named_context env) let keep_hyps env needed = + let open Context.Named.Declaration in let really_needed = really_needed env needed in Context.Named.fold_outside (fun d nsign -> @@ -647,6 +649,7 @@ type unsafe_type_judgment = types punsafe_type_judgment exception Hyp_not_found let apply_to_hyp ctxt id f = + let open Context.Named.Declaration in let rec aux rtail ctxt = match match_named_context_val ctxt with | Some (d, v, ctxt) -> @@ -663,6 +666,7 @@ let remove_hyps ids check_context check_value ctxt = let rec remove_hyps ctxt = match match_named_context_val ctxt with | None -> empty_named_context_val, false | Some (d, v, rctxt) -> + let open Context.Named.Declaration in let (ans, seen) = remove_hyps rctxt in if Id.Set.mem (get_id d) ids then (ans, true) else if not seen then ctxt, false diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 7abf8027bd..b976469ff7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -242,7 +242,7 @@ let check_subtyping cumi paramsctxt env_ar inds = in let env = Environ.add_constraints subtyp_constraints env in (* process individual inductive types: *) - Array.iter (fun (id,cn,lc,(sign,arity)) -> + Array.iter (fun (_id,_cn,lc,(_sign,arity)) -> match arity with | RegularArity (_, full_arity, _) -> check_subtyping_arity_constructor env dosubst full_arity numparams true; @@ -368,7 +368,7 @@ let typecheck_inductive env mie = RegularArity (not is_natural,full_arity,defu) in let template_polymorphic () = - let _, s = + let _sign, s = try dest_arity env full_arity with NotArity -> raise (InductiveError (NotAnArity (env, full_arity))) in @@ -428,7 +428,7 @@ exception IllFormedInd of ill_formed_ind let mind_extract_params = decompose_prod_n_assum let explain_ind_err id ntyp env nparamsctxt c err = - let (lparams,c') = mind_extract_params nparamsctxt c in + let (_lparams,c') = mind_extract_params nparamsctxt c in match err with | LocalNonPos kt -> raise (InductiveError (NonPos (env,c',mkRel (kt+nparamsctxt)))) @@ -596,7 +596,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( discharged to the [check_positive_nested] function. *) if List.for_all (noccur_between n ntypes) largs then (nmr,mk_norec) else check_positive_nested ienv nmr (ind_kn, largs) - | err -> + | _err -> (** If an inductive of the mutually inductive block appears in any other way, then the positivy check gives up. *) @@ -613,7 +613,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( defined types, not one of the types of the mutually inductive block being defined). *) (* accesses to the environment are not factorised, but is it worth? *) - and check_positive_nested (env,n,ntypes,ra_env as ienv) nmr ((mi,u), largs) = + and check_positive_nested (env,n,ntypes,_ra_env as ienv) nmr ((mi,u), largs) = let (mib,mip) = lookup_mind_specif env mi in let auxnrecpar = mib.mind_nparams_rec in let auxnnonrecpar = mib.mind_nparams - auxnrecpar in @@ -664,7 +664,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( the type [c]) is checked to be the right (properly applied) inductive type. *) and check_constructors ienv check_head nmr c = - let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = + let rec check_constr_rec (env,n,ntypes,_ra_env as ienv) nmr lrec c = let x,largs = decompose_app (whd_all env c) in match kind x with @@ -813,7 +813,7 @@ let compute_projections (kn, i as ind) mib = in let projections decl (i, j, labs, pbs, letsubst) = match decl with - | LocalDef (na,c,t) -> + | LocalDef (_na,c,_t) -> (* From [params, field1,..,fieldj |- c(params,field1,..,fieldj)] to [params, x:I, field1,..,fieldj |- c(params,field1,..,fieldj)] *) let c = liftn 1 j c in @@ -841,7 +841,7 @@ let compute_projections (kn, i as ind) mib = (i + 1, j + 1, lab :: labs, projty :: pbs, fterm :: letsubst) | Anonymous -> raise UndefinableExpansion in - let (_, _, labs, pbs, letsubst) = + let (_, _, labs, pbs, _letsubst) = List.fold_right projections ctx (0, 1, [], [], paramsletsubst) in Array.of_list (List.rev labs), diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1d2f22b006..9bbcf07f7e 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -154,10 +154,10 @@ let make_subst env = let rec make subst = function | LocalDef _ :: sign, exp, args -> make subst (sign, exp, args) - | d::sign, None::exp, args -> + | _d::sign, None::exp, args -> let args = match args with _::args -> args | [] -> [] in make subst (sign, exp, args) - | d::sign, Some u::exp, a::args -> + | _d::sign, Some u::exp, a::args -> (* We recover the level of the argument, but we don't change the *) (* level in the corresponding type in the arity; this level in the *) (* arity is a global level which, at typing time, will be enforce *) @@ -165,7 +165,7 @@ let make_subst env = (* a useless extra constraint *) let s = Sorts.univ_of_sort (snd (dest_arity env (Lazy.force a))) in make (cons_subst u s subst) (sign, exp, args) - | LocalAssum (na,t) :: sign, Some u::exp, [] -> + | LocalAssum (_na,_t) :: sign, Some u::exp, [] -> (* No more argument here: we add the remaining universes to the *) (* substitution (when [u] is distinct from all other universes in the *) (* template, it is identity substitution otherwise (ie. when u is *) @@ -173,7 +173,7 @@ let make_subst env = (* update its image [x] by [sup x u] in order not to forget the *) (* dependency in [u] that remains to be fullfilled. *) make (remember_subst u subst) (sign, exp, []) - | sign, [], _ -> + | _sign, [], _ -> (* Uniform parameters are exhausted *) subst | [], _, _ -> @@ -199,7 +199,7 @@ let instantiate_universes env ctx ar argsorts = (* Type of an inductive type *) -let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = +let type_of_inductive_gen ?(polyprop=true) env ((_mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> @@ -215,12 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps = let type_of_inductive env pind = type_of_inductive_gen env pind [||] -let constrained_type_of_inductive env ((mib,mip),u as pind) = +let constrained_type_of_inductive env ((mib,_mip),u as pind) = let ty = type_of_inductive env pind in let cst = instantiate_inductive_constraints mib u in (ty, cst) -let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args = +let constrained_type_of_inductive_knowing_parameters env ((mib,_mip),u as pind) args = let ty = type_of_inductive_gen env pind args in let cst = instantiate_inductive_constraints mib u in (ty, cst) @@ -249,7 +249,7 @@ let type_of_constructor (cstr, u) (mib,mip) = if i > nconstr then user_err Pp.(str "Not enough constructors in the type."); constructor_instantiate (fst ind) u mib specif.(i-1) -let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) = +let constrained_type_of_constructor (_cstr,u as cstru) (mib,_mip as ind) = let ty = type_of_constructor cstru ind in let cst = instantiate_inductive_constraints mib u in (ty, cst) @@ -279,7 +279,7 @@ let inductive_sort_family mip = let mind_arity mip = mip.mind_arity_ctxt, inductive_sort_family mip -let get_instantiated_arity (ind,u) (mib,mip) params = +let get_instantiated_arity (_ind,u) (mib,mip) params = let sign, s = mind_arity mip in full_inductive_instantiate mib u params sign, s @@ -563,7 +563,7 @@ let check_inductive_codomain env p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,l' = decompose_app (whd_all env s) in + let i,_l' = decompose_app (whd_all env s) in isInd i (* The following functions are almost duplicated from indtypes.ml, except @@ -635,10 +635,10 @@ let get_recargs_approx env tree ind args = build_recargs_nested ienv tree (ind_kn, largs) | _ -> mk_norec end - | err -> + | _err -> mk_norec - and build_recargs_nested (env,ra_env as ienv) tree (((mind,i),u), largs) = + and build_recargs_nested (env,_ra_env as ienv) tree (((mind,i),u), largs) = (* If the inferred tree already disallows recursion, no need to go further *) if eq_wf_paths tree mk_norec then tree else @@ -676,7 +676,7 @@ let get_recargs_approx env tree ind args = (Rtree.mk_rec irecargs).(i) and build_recargs_constructors ienv trees c = - let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = + let rec recargs_constr_rec (env,_ra_env as ienv) trees lrec c = let x,largs = decompose_app (whd_all env c) in match kind x with @@ -685,7 +685,7 @@ let get_recargs_approx env tree ind args = let recarg = build_recargs ienv (List.hd trees) b in let ienv' = ienv_push_var ienv (na,b,mk_norec) in recargs_constr_rec ienv' (List.tl trees) (recarg::lrec) d - | hd -> + | _hd -> List.rev lrec in recargs_constr_rec ienv trees [] c @@ -794,7 +794,7 @@ let rec subterm_specif renv stack t = | Proj (p, c) -> let subt = subterm_specif renv stack c in (match subt with - | Subterm (s, wf) -> + | Subterm (_s, wf) -> (* We take the subterm specs of the constructor of the record *) let wf_args = (dest_subterms wf).(0) in (* We extract the tree of the projected argument *) @@ -964,7 +964,7 @@ let check_one_fix renv recpos trees def = else check_rec_call renv' [] body) bodies - | Const (kn,u as cu) -> + | Const (kn,_u as cu) -> if evaluable_constant kn renv.env then try List.iter (check_rec_call renv []) l with (FixGuardError _ ) -> @@ -983,7 +983,7 @@ let check_one_fix renv recpos trees def = check_rec_call renv [] a; check_rec_call (push_var_renv renv (x,a)) [] b - | CoFix (i,(_,typarray,bodies as recdef)) -> + | CoFix (_i,(_,typarray,bodies as recdef)) -> List.iter (check_rec_call renv []) l; Array.iter (check_rec_call renv []) typarray; let renv' = push_fix_renv renv recdef in @@ -992,13 +992,13 @@ let check_one_fix renv recpos trees def = | (Ind _ | Construct _) -> List.iter (check_rec_call renv []) l - | Proj (p, c) -> + | Proj (_p, c) -> List.iter (check_rec_call renv []) l; check_rec_call renv [] c | Var id -> begin - let open Context.Named.Declaration in + let open! Context.Named.Declaration in match lookup_named id renv.env with | LocalAssum _ -> List.iter (check_rec_call renv []) l @@ -1129,10 +1129,10 @@ let check_one_cofix env nbfix def deftype = raise (CoFixGuardError (env,UnguardedRecursiveCall t)) else if not(List.for_all (noccur_with_meta n nbfix) args) then raise (CoFixGuardError (env,NestedRecursiveOccurrences)) - | Construct ((_,i as cstr_kn),u) -> + | Construct ((_,i as cstr_kn),_u) -> let lra = vlra.(i-1) in let mI = inductive_of_constructor cstr_kn in - let (mib,mip) = lookup_mind_specif env mI in + let (mib,_mip) = lookup_mind_specif env mI in let realargs = List.skipn mib.mind_nparams args in let rec process_args_of_constr = function | (t::lr), (rar::lrar) -> @@ -1157,7 +1157,7 @@ let check_one_cofix env nbfix def deftype = else raise (CoFixGuardError (env,RecCallInTypeOfAbstraction a)) - | CoFix (j,(_,varit,vdefs as recdef)) -> + | CoFix (_j,(_,varit,vdefs as recdef)) -> if List.for_all (noccur_with_meta n nbfix) args then if Array.for_all (noccur_with_meta n nbfix) varit then @@ -1203,7 +1203,7 @@ let check_one_cofix env nbfix def deftype = (* The function which checks that the whole block of definitions satisfies the guarded condition *) -let check_cofix env (bodynum,(names,types,bodies as recdef)) = +let check_cofix env (_bodynum,(names,types,bodies as recdef)) = let flags = Environ.typing_flags env in if flags.check_guarded then let nbfix = Array.length bodies in diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index f1d08ef6dd..bff3092655 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -319,12 +319,12 @@ let subst_con sub cst = let subst_con_kn sub con = subst_con sub (con,Univ.Instance.empty) -let subst_pcon sub (con,u as pcon) = - try let con', can = subst_con0 sub pcon in +let subst_pcon sub (_con,u as pcon) = + try let con', _can = subst_con0 sub pcon in con',u with No_subst -> pcon -let subst_pcon_term sub (con,u as pcon) = +let subst_pcon_term sub (_con,u as pcon) = try let con', can = subst_con0 sub pcon in (con',u), can with No_subst -> pcon, mkConstU pcon @@ -441,7 +441,7 @@ let replace_mp_in_kn mpfrom mpto kn = let rec mp_in_mp mp mp1 = match mp1 with | _ when ModPath.equal mp1 mp -> true - | MPdot (mp2,l) -> mp_in_mp mp mp2 + | MPdot (mp2,_l) -> mp_in_mp mp mp2 | _ -> false let subset_prefixed_by mp resolver = diff --git a/kernel/modops.ml b/kernel/modops.ml index 9435f46c6b..424d329e09 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -138,7 +138,7 @@ let rec functor_smart_map fty f0 funct = match funct with let a' = f0 a in if a==a' then funct else NoFunctor a' let rec functor_iter fty f0 = function - |MoreFunctor (mbid,ty,e) -> fty ty; functor_iter fty f0 e + |MoreFunctor (_mbid,ty,e) -> fty ty; functor_iter fty f0 e |NoFunctor a -> f0 a (** {6 Misc operations } *) @@ -171,7 +171,7 @@ let implem_iter fs fa impl = match impl with (** {6 Substitutions of modular structures } *) -let id_delta x y = x +let id_delta x _y = x let subst_with_body sub = function |WithMod(id,mp) as orig -> @@ -200,7 +200,7 @@ let rec subst_structure sub do_delta sign = and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body = fun is_mod sub subst_impl do_delta mb -> - let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in + let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty; _ } = mb in let mp' = subst_mp sub mp in let sub = if ModPath.equal mp mp' then sub @@ -371,7 +371,7 @@ and strengthen_sig mp_from struc mp_to reso = match struc with let item' = l,SFBmodule mb' in let reso',rest' = strengthen_sig mp_from rest mp_to reso in add_delta_resolver reso' mb.mod_delta, item':: rest' - |(l,SFBmodtype mty as item) :: rest -> + |(_l,SFBmodtype _mty as item) :: rest -> let reso',rest' = strengthen_sig mp_from rest mp_to reso in reso',item::rest' @@ -628,7 +628,7 @@ let join_structure except otab s = let rec join_module : 'a. 'a generic_module_body -> unit = fun mb -> Option.iter join_expression mb.mod_type_alg; join_signature mb.mod_type - and join_field (l,body) = match body with + and join_field (_l,body) = match body with |SFBconst sb -> join_constant_body except otab sb |SFBmind _ -> () |SFBmodule m -> diff --git a/kernel/names.ml b/kernel/names.ml index 933cefe993..6d33f233e9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -207,7 +207,7 @@ struct let repr mbid = mbid - let to_string (i, s, p) = + let to_string (_i, s, p) = DirPath.to_string p ^ "." ^ s let debug_to_string (i, s, p) = @@ -328,7 +328,7 @@ module ModPath = struct let rec dp = function | MPfile sl -> sl | MPbound (_,_,dp) -> dp - | MPdot (mp,l) -> dp mp + | MPdot (mp,_l) -> dp mp module Self_Hashcons = struct type t = module_path @@ -420,7 +420,7 @@ module KerName = struct let hash kn = let h = kn.refhash in if h < 0 then - let { modpath = mp; dirpath = dp; knlabel = lbl; } = kn in + let { modpath = mp; dirpath = dp; knlabel = lbl; _ } = kn in let h = combine3 (ModPath.hash mp) (DirPath.hash dp) (Label.hash lbl) in (* Ensure positivity on all platforms. *) let h = h land 0x3FFFFFFF in @@ -623,8 +623,8 @@ let constr_modpath (ind,_) = ind_modpath ind let ith_mutual_inductive (mind, _) i = (mind, i) let ith_constructor_of_inductive ind i = (ind, i) -let inductive_of_constructor (ind, i) = ind -let index_of_constructor (ind, i) = i +let inductive_of_constructor (ind, _i) = ind +let index_of_constructor (_ind, i) = i let eq_ind (m1, i1) (m2, i2) = Int.equal i1 i2 && MutInd.equal m1 m2 let eq_user_ind (m1, i1) (m2, i2) = diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index eed25a4ca4..74b075f4a5 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1007,7 +1007,7 @@ let compile_prim decl cond paux = *) let rec opt_prim_aux paux = match paux with - | PAprim(prefix, kn, op, args) -> + | PAprim(_prefix, _kn, op, args) -> let args = Array.map opt_prim_aux args in app_prim (Coq_primitive(op,None)) args (* @@ -1071,7 +1071,7 @@ let ml_of_instance instance u = match t with | Lrel(id ,i) -> get_rel env id i | Lvar id -> get_var env id - | Lmeta(mv,ty) -> + | Lmeta(mv,_ty) -> let tyn = fresh_lname Anonymous in let i = push_symbol (SymbMeta mv) in MLapp(MLprimitive Mk_meta, [|get_meta_code i; MLlocal tyn|]) @@ -1184,7 +1184,7 @@ let ml_of_instance instance u = let lf,env_n = push_rels (empty_env env.env_univ ()) ids in let t_params = Array.make ndef [||] in let t_norm_f = Array.make ndef (Gnorm (l,-1)) in - let mk_let envi (id,def) t = MLlet (id,def,t) in + let mk_let _envi (id,def) t = MLlet (id,def,t) in let mk_lam_or_let (params,lets,env) (id,def) = let ln,env' = push_rel env id in match def with @@ -1217,7 +1217,7 @@ let ml_of_instance instance u = (Array.map (fun g -> mkMLapp (MLglobal g) fv_args') t_norm_f) in (* Compilation of fix *) let fv_args = fv_args env fvn fvr in - let lf, env = push_rels env ids in + let lf, _env = push_rels env ids in let lf_args = Array.map (fun id -> MLlocal id) lf in let mk_norm = MLapp(MLglobal norm, fv_args) in let mkrec i lname = @@ -1272,9 +1272,9 @@ let ml_of_instance instance u = let mk_norm = MLapp(MLglobal norm, fv_args) in let lnorm = fresh_lname Anonymous in let ltype = fresh_lname Anonymous in - let lf, env = push_rels env ids in + let lf, _env = push_rels env ids in let lf_args = Array.map (fun id -> MLlocal id) lf in - let upd i lname cont = + let upd i _lname cont = let paramsi = t_params.(i) in let pargsi = Array.map (fun id -> MLlocal id) paramsi in let uniti = fresh_lname Anonymous in @@ -1305,7 +1305,7 @@ let ml_of_instance instance u = (lname, paramsi, body) in MLletrec(Array.mapi mkrec lf, lf_args.(start)) *) - | Lmakeblock (prefix,(cn,u),_,args) -> + | Lmakeblock (prefix,(cn,_u),_,args) -> let args = Array.map (ml_of_lam env l) args in MLconstruct(prefix,cn,args) | Lconstruct (prefix, (cn,u)) -> @@ -1561,7 +1561,7 @@ let rec list_of_mp acc = function let list_of_mp mp = list_of_mp [] mp let string_of_kn kn = - let (mp,dp,l) = KerName.repr kn in + let (mp,_dp,l) = KerName.repr kn in let mp = list_of_mp mp in String.concat "_" mp ^ "_" ^ string_of_label l @@ -1987,7 +1987,7 @@ let compile_mind mb mind stack = (MLconstruct("", c, Array.map (fun id -> MLlocal id) args)))::acc in let constructors = Array.fold_left_i add_construct [] ob.mind_reloc_tbl in - let add_proj proj_arg acc pb = + let add_proj proj_arg acc _pb = let tbl = ob.mind_reloc_tbl in (* Building info *) let ci = { ci_ind = ind; ci_npar = nparams; @@ -2053,9 +2053,9 @@ let compile_mind_deps env prefix ~interactive let compile_deps env sigma prefix ~interactive init t = let rec aux env lvl init t = match kind t with - | Ind ((mind,_),u) -> compile_mind_deps env prefix ~interactive init mind + | Ind ((mind,_),_u) -> compile_mind_deps env prefix ~interactive init mind | Const c -> - let c,u = get_alias env c in + let c,_u = get_alias env c in let cb,(nameref,_) = lookup_constant_key c env in let (_, (_, const_updates)) = init in if is_code_loaded ~interactive nameref @@ -2074,11 +2074,11 @@ let compile_deps env sigma prefix ~interactive init t = let comp_stack = code@comp_stack in let const_updates = Cmap_env.add c (nameref, name) const_updates in comp_stack, (mind_updates, const_updates) - | Construct (((mind,_),_),u) -> compile_mind_deps env prefix ~interactive init mind + | Construct (((mind,_),_),_u) -> compile_mind_deps env prefix ~interactive init mind | Proj (p,c) -> let init = compile_mind_deps env prefix ~interactive init (Projection.mind p) in aux env lvl init c - | Case (ci, p, c, ac) -> + | Case (ci, _p, _c, _ac) -> let mind = fst ci.ci_ind in let init = compile_mind_deps env prefix ~interactive init mind in fold_constr_with_binders succ (aux env) lvl init t diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c75dde843e..054b6a2d17 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -25,9 +25,9 @@ let rec conv_val env pb lvl v1 v2 cu = | Vfun f1, Vfun f2 -> let v = mk_rel_accu lvl in conv_val env CONV (lvl+1) (f1 v) (f2 v) cu - | Vfun f1, _ -> + | Vfun _f1, _ -> conv_val env CONV lvl v1 (fun x -> v2 x) cu - | _, Vfun f2 -> + | _, Vfun _f2 -> conv_val env CONV lvl (fun x -> v1 x) v2 cu | Vaccu k1, Vaccu k2 -> conv_accu env pb lvl k1 k2 cu @@ -110,7 +110,7 @@ and conv_atom env pb lvl a1 a2 cu = else if not (Int.equal (Array.length f1) (Array.length f2)) then raise NotConvertible else conv_fix env lvl t1 f1 t2 f2 cu - | Aprod(_,d1,c1), Aprod(_,d2,c2) -> + | Aprod(_,d1,_c1), Aprod(_,d2,_c2) -> let cu = conv_val env CONV lvl d1 d2 cu in let v = mk_rel_accu lvl in conv_val env pb (lvl + 1) (d1 v) (d2 v) cu diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index ab40c643f9..70cb8691c6 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -142,7 +142,7 @@ let rec map_lam_with_binders g f n lam = let args' = Array.Smart.map (f n) args in if args == args' then lam else Levar (evk, args') -and map_uint g f n u = +and map_uint _g f n u = match u with | UintVal _ -> u | UintDigits(prefix,c,args) -> @@ -203,7 +203,7 @@ let can_subst lam = let can_merge_if bt bf = match bt, bf with - | Llam(idst,_), Llam(idsf,_) -> true + | Llam(_idst,_), Llam(_idsf,_) -> true | _ -> false let merge_if t bt bf = @@ -370,7 +370,7 @@ module Cache = let is_lazy env prefix t = match kind t with - | App (f,args) -> + | App (f,_args) -> begin match kind f with | Construct (c,_) -> let gr = GlobRef.IndRef (fst c) in @@ -431,7 +431,7 @@ let rec lambda_of_constr cache env sigma c = | Sort s -> Lsort s - | Ind (ind,u as pind) -> + | Ind (ind,_u as pind) -> let prefix = get_mind_prefix env (fst ind) in Lind (prefix, pind) @@ -529,7 +529,7 @@ let rec lambda_of_constr cache env sigma c = and lambda_of_app cache env sigma f args = match kind f with - | Const (kn,u as c) -> + | Const (_kn,_u as c) -> let kn,u = get_alias env c in let cb = lookup_constant kn env in (try diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index f784509b6f..b4126dd68c 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -40,7 +40,7 @@ let include_dirs () = [Filename.get_temp_dir_name (); coqlib () / "kernel"; coqlib () / "library"] (* Pointer to the function linking an ML object into coq's toplevel *) -let load_obj = ref (fun x -> () : string -> unit) +let load_obj = ref (fun _x -> () : string -> unit) let rt1 = ref (dummy_value ()) let rt2 = ref (dummy_value ()) @@ -113,7 +113,7 @@ let call_compiler ?profile:(profile=false) ml_filename = let res = CUnix.sys_command (ocamlfind ()) args in let res = match res with | Unix.WEXITED 0 -> true - | Unix.WEXITED n | Unix.WSIGNALED n | Unix.WSTOPPED n -> + | Unix.WEXITED _n | Unix.WSIGNALED _n | Unix.WSTOPPED _n -> warn_native_compiler_failed (Inl res); false in res, link_filename @@ -158,7 +158,7 @@ let call_linker ?(fatal=true) prefix f upds = (try if Dynlink.is_native then Dynlink.loadfile f else !load_obj f; register_native_file prefix - with Dynlink.Error e as exn -> + with Dynlink.Error _ as exn -> let exn = CErrors.push exn in if fatal then iraise exn else if !Flags.debug then Feedback.msg_debug CErrors.(iprint exn)); diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index edce9367fc..8ac3538fc5 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -29,7 +29,7 @@ and translate_field prefix mp env acc (l,x) = | SFBconst cb -> let con = Constant.make3 mp DirPath.empty l in (if !Flags.debug then - let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in + let msg = Printf.sprintf "Compiling constant %s..." (Constant.to_string con) in Feedback.msg_debug (Pp.str msg)); compile_constant_field env prefix con acc cb | SFBmind mb -> diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index f8b71e4564..303cb06c55 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -87,21 +87,21 @@ let discharge_direct_opaque ~cook_constr ci = function | Direct (d,cu) -> Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u)) -let join_opaque { opaque_val = prfs; opaque_dir = odp } = function +let join_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> ignore(Future.join cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then let fp = snd (Int.Map.find i prfs) in ignore(Future.join fp) -let uuid_opaque { opaque_val = prfs; opaque_dir = odp } = function +let uuid_opaque { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Some (Future.uuid cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then Some (Future.uuid (snd (Int.Map.find i prfs))) else None -let force_proof { opaque_val = prfs; opaque_dir = odp } = function +let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> fst(Future.force cu) | Indirect (l,dp,i) -> @@ -112,7 +112,7 @@ let force_proof { opaque_val = prfs; opaque_dir = odp } = function let c = Future.force pt in force_constr (List.fold_right subst_substituted l (from_val c)) -let force_constraints { opaque_val = prfs; opaque_dir = odp } = function +let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> snd(Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp @@ -121,14 +121,14 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp } = function | None -> Univ.ContextSet.empty | Some u -> Future.force u -let get_constraints { opaque_val = prfs; opaque_dir = odp } = function +let get_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Some(Future.chain cu snd) | Indirect (_,dp,i) -> if DirPath.equal dp odp then Some(Future.chain (snd (Int.Map.find i prfs)) snd) else !get_univ dp i -let get_proof { opaque_val = prfs; opaque_dir = odp } = function +let get_proof { opaque_val = prfs; opaque_dir = odp; _ } = function | Direct (_,cu) -> Future.chain cu fst | Indirect (l,dp,i) -> let pt = @@ -144,7 +144,7 @@ let a_constr = Future.from_val (mkRel 1) let a_univ = Future.from_val Univ.ContextSet.empty let a_discharge : cooking_info list = [] -let dump { opaque_val = otab; opaque_len = n } = +let dump { opaque_val = otab; opaque_len = n; _ } = let opaque_table = Array.make n a_constr in let univ_table = Array.make n a_univ in let disch_table = Array.make n a_discharge in diff --git a/kernel/reduction.ml b/kernel/reduction.ml index c701b53fe4..2abb4b485c 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -53,9 +53,9 @@ let compare_stack_shape stk1 stk2 = | (_, (Zupdate _|Zshift _)::s2) -> compare_rec bal stk1 s2 | (Zapp l1::s1, _) -> compare_rec (bal+Array.length l1) s1 stk2 | (_, Zapp l2::s2) -> compare_rec (bal-Array.length l2) stk1 s2 - | (Zproj p1::s1, Zproj p2::s2) -> + | (Zproj _p1::s1, Zproj _p2::s2) -> Int.equal bal 0 && compare_rec 0 s1 s2 - | (ZcaseT(c1,_,_,_)::s1, ZcaseT(c2,_,_,_)::s2) -> + | (ZcaseT(_c1,_,_,_)::s1, ZcaseT(_c2,_,_,_)::s2) -> Int.equal bal 0 (* && c1.ci_ind = c2.ci_ind *) && compare_rec 0 s1 s2 | (Zfix(_,a1)::s1, Zfix(_,a2)::s2) -> Int.equal bal 0 && compare_rec 0 a1 a2 && compare_rec 0 s1 s2 @@ -261,7 +261,7 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u s | Declarations.Polymorphic_ind _ -> cmp_instances u1 u2 s - | Declarations.Cumulative_ind cumi -> + | Declarations.Cumulative_ind _cumi -> let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s @@ -296,7 +296,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 cuniv = (match (z1,z2) with | (Zlapp a1,Zlapp a2) -> Array.fold_right2 f a1 a2 cu1 - | (Zlproj (c1,l1),Zlproj (c2,l2)) -> + | (Zlproj (c1,_l1),Zlproj (c2,_l2)) -> if not (Projection.Repr.equal c1 c2) then raise NotConvertible else cu1 @@ -498,7 +498,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = eqappr cv_pb l2r infos (lft1, r1) appr2 cuniv | None -> match c2 with - | FConstruct ((ind2,j2),u2) -> + | FConstruct ((ind2,_j2),_u2) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) @@ -515,7 +515,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = eqappr cv_pb l2r infos appr1 (lft2, r2) cuniv | None -> match c1 with - | FConstruct ((ind1,j1),u1) -> + | FConstruct ((ind1,_j1),_u1) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv @@ -554,14 +554,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv = else raise NotConvertible (* Eta expansion of records *) - | (FConstruct ((ind1,j1),u1), _) -> + | (FConstruct ((ind1,_j1),_u1), _) -> (try let v1, v2 = eta_expand_ind_stack (info_env infos.cnv_inf) ind1 hd1 v1 (snd appr2) in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv with Not_found -> raise NotConvertible) - | (_, FConstruct ((ind2,j2),u2)) -> + | (_, FConstruct ((ind2,_j2),_u2)) -> (try let v2, v1 = eta_expand_ind_stack (info_env infos.cnv_inf) ind2 hd2 v2 (snd appr1) @@ -659,14 +659,14 @@ let check_sort_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible | Set, Prop -> raise NotConvertible | Set, Type u -> check_pb Univ.type0_univ u - | Type u, Prop -> raise NotConvertible + | Type _u, Prop -> raise NotConvertible | Type u, Set -> check_pb u Univ.type0_univ | Type u0, Type u1 -> check_pb u0 u1 let checked_sort_cmp_universes env pb s0 s1 univs = check_sort_cmp_universes env pb s0 s1 univs; univs -let check_convert_instances ~flex u u' univs = +let check_convert_instances ~flex:_ u u' univs = if UGraph.check_eq_instances univs u u' then univs else raise NotConvertible @@ -707,7 +707,7 @@ let infer_cmp_universes env pb s0 s1 univs = | Prop, (Set | Type _) -> if not (is_cumul pb) then raise NotConvertible else univs | Set, Prop -> raise NotConvertible | Set, Type u -> infer_pb Univ.type0_univ u - | Type u, Prop -> raise NotConvertible + | Type _u, Prop -> raise NotConvertible | Type u, Set -> infer_pb u Univ.type0_univ | Type u0, Type u1 -> infer_pb u0 u1 @@ -781,7 +781,7 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta env univs t1 t2 = infer_conv_universes CUMUL l2r evars ts env univs t1 t2 -let default_conv cv_pb ?(l2r=false) env t1 t2 = +let default_conv cv_pb ?l2r:_ env t1 t2 = gen_conv cv_pb env t1 t2 let default_conv_leq = default_conv CUMUL @@ -912,7 +912,7 @@ let is_arity env c = with NotArity -> false let eta_expand env t ty = - let ctxt, codom = dest_prod env ty in + let ctxt, _codom = dest_prod env ty in let ctxt',t = dest_lam env t in let d = Context.Rel.nhyps ctxt - Context.Rel.nhyps ctxt' in let eta_args = List.rev_map mkRel (List.interval 1 d) in diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 74042f9e04..bfe68671a2 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -138,7 +138,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name t1 t2 = check_conv (NotConvertibleInductiveField name) - cst (inductive_is_polymorphic mib1) infer_conv_leq env t1 t2 + cst (inductive_is_polymorphic mib1) (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2 in let check_packet cst p1 p2 = @@ -162,10 +162,10 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 cst in let mind = MutInd.make1 kn1 in - let check_cons_types i cst p1 p2 = + let check_cons_types _i cst p1 p2 = Array.fold_left3 (fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst - (inductive_is_polymorphic mib1) infer_conv env t1 t2) + (inductive_is_polymorphic mib1) (infer_conv ?l2r:None ?evars:None ?ts:None) env t1 t2) cst p2.mind_consnames (arities_of_specif (mind, inst) (mib1, p1)) @@ -229,7 +229,7 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = let check_conv cst poly f = check_conv_error error cst poly f in let check_type poly cst env t1 t2 = let err = NotConvertibleTypeField (env, t1, t2) in - check_conv err cst poly infer_conv_leq env t1 t2 + check_conv err cst poly (infer_conv_leq ?l2r:None ?evars:None ?ts:None) env t1 t2 in match info1 with | Constant cb1 -> @@ -268,14 +268,14 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 = Anyway [check_conv] will handle that afterwards. *) let c1 = Mod_subst.force_constr lc1 in let c2 = Mod_subst.force_constr lc2 in - check_conv NotConvertibleBodyField cst poly infer_conv env c1 c2)) - | IndType ((kn,i),mind1) -> + check_conv NotConvertibleBodyField cst poly (infer_conv ?l2r:None ?evars:None ?ts:None) env c1 c2)) + | IndType ((_kn,_i),_mind1) -> CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by an inductive type. Hint: you can rename the " ^ "inductive type and give a definition to map the old name to the new " ^ "name.") - | IndConstr (((kn,i),j),mind1) -> + | IndConstr (((_kn,_i),_j),_mind1) -> CErrors.user_err Pp.(str @@ "The kernel does not recognize yet that a parameter can be " ^ "instantiated by a constructor. Hint: you can rename the " ^ diff --git a/kernel/term.ml b/kernel/term.ml index 4851a9c0d0..795cdeb040 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -54,13 +54,13 @@ let mkProd_wo_LetIn decl c = let open Context.Rel.Declaration in match decl with | LocalAssum (na,t) -> mkProd (na, t, c) - | LocalDef (na,b,t) -> subst1 b c + | LocalDef (_na,b,_t) -> subst1 b c let mkNamedProd_wo_LetIn decl c = let open Context.Named.Declaration in match decl with | LocalAssum (id,t) -> mkNamedProd id t c - | LocalDef (id,b,t) -> subst1 b (subst_var id c) + | LocalDef (id,b,_t) -> subst1 b (subst_var id c) (* non-dependent product t1 -> t2 *) let mkArrow t1 t2 = mkProd (Anonymous, t1, t2) @@ -81,7 +81,7 @@ let mkNamedLambda_or_LetIn decl c = (* prodn n [xn:Tn;..;x1:T1;Gamma] b = (x1:T1)..(xn:Tn)b *) let prodn n env b = let rec prodrec = function - | (0, env, b) -> b + | (0, _env, b) -> b | (n, ((v,t)::l), b) -> prodrec (n-1, l, mkProd (v,t,b)) | _ -> assert false in @@ -93,7 +93,7 @@ let compose_prod l b = prodn (List.length l) l b (* lamn n [xn:Tn;..;x1:T1;Gamma] b = [x1:T1]..[xn:Tn]b *) let lamn n env b = let rec lamrec = function - | (0, env, b) -> b + | (0, _env, b) -> b | (n, ((v,t)::l), b) -> lamrec (n-1, l, mkLambda (v,t,b)) | _ -> assert false in @@ -276,7 +276,7 @@ let decompose_prod_n_assum n = | Prod (x,t,c) -> prodec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> prodec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> prodec_rec l n c - | c -> user_err (str "decompose_prod_n_assum: not enough assumptions") + | _ -> user_err (str "decompose_prod_n_assum: not enough assumptions") in prodec_rec Context.Rel.empty n @@ -297,7 +297,7 @@ let decompose_lam_n_assum n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) n c | Cast (c,_,_) -> lamdec_rec l n c - | c -> user_err (str "decompose_lam_n_assum: not enough abstractions") + | _c -> user_err (str "decompose_lam_n_assum: not enough abstractions") in lamdec_rec Context.Rel.empty n @@ -313,7 +313,7 @@ let decompose_lam_n_decls n = | Lambda (x,t,c) -> lamdec_rec (Context.Rel.add (LocalAssum (x,t)) l) (n-1) c | LetIn (x,b,t,c) -> lamdec_rec (Context.Rel.add (LocalDef (x,b,t)) l) (n-1) c | Cast (c,_,_) -> lamdec_rec l n c - | c -> user_err (str "decompose_lam_n_decls: not enough abstractions") + | _ -> user_err (str "decompose_lam_n_decls: not enough abstractions") in lamdec_rec Context.Rel.empty n diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index f59e07098b..47247ff25e 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -73,7 +73,7 @@ type _ trust = let uniq_seff_rev = SideEffects.repr let uniq_seff l = let ans = List.rev (SideEffects.repr l) in - List.map_append (fun { eff } -> eff) ans + List.map_append (fun { eff ; _ } -> eff) ans let empty_seff = SideEffects.empty let add_seff mb eff effs = @@ -103,12 +103,7 @@ let inline_side_effects env body ctx side_eff = if List.is_empty side_eff then (body, ctx, sigs) else (** Second step: compute the lifts and substitutions to apply *) - let cname c = - let name = Constant.to_string c in - let map c = if c == '.' || c == '#' then '_' else c in - let name = String.map map name in - Name (Id.of_string name) - in + let cname c = Name (Label.to_id (Constant.label c)) in let fold (subst, var, ctx, args) (c, cb, b) = let (b, opaque) = match cb.const_body, b with | Def b, _ -> (Mod_subst.force_constr b, false) @@ -122,7 +117,7 @@ let inline_side_effects env body ctx side_eff = let subst = Cmap_env.add c (Inr var) subst in let ctx = Univ.ContextSet.union ctx univs in (subst, var + 1, ctx, (cname c, b, ty, opaque) :: args) - | Polymorphic_const auctx -> + | Polymorphic_const _auctx -> (** Inline the term to emulate universe polymorphism *) let subst = Cmap_env.add c (Inl b) subst in (subst, var, ctx, args) @@ -250,9 +245,9 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = delay even in the polymorphic case. *) | DefinitionEntry ({ const_entry_type = Some typ; const_entry_opaque = true; - const_entry_universes = Monomorphic_const_entry univs } as c) -> + const_entry_universes = Monomorphic_const_entry univs; _ } as c) -> let env = push_context_set ~strict:true univs env in - let { const_entry_body = body; const_entry_feedback = feedback_id } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in let tyj = infer_type env typ in let proofterm = Future.chain body (fun ((body,uctx),side_eff) -> @@ -288,8 +283,8 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = (** Other definitions have to be processed immediately. *) | DefinitionEntry c -> - let { const_entry_type = typ; const_entry_opaque = opaque } = c in - let { const_entry_body = body; const_entry_feedback = feedback_id } = c in + let { const_entry_type = typ; const_entry_opaque = opaque ; _ } = c in + let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let (body, ctx), side_eff = Future.join body in let body, ctx, _ = match trust with | Pure -> body, ctx, [] @@ -348,7 +343,7 @@ let record_aux env s_ty s_bo = (keep_hyps env s_bo)) in Aux_file.record_in_aux "context_used" v -let build_constant_declaration kn env result = +let build_constant_declaration _kn env result = let open Cooking in let typ = result.cook_type in let check declared inferred = @@ -478,7 +473,7 @@ let export_eff eff = (eff.seff_constant, eff.seff_body, eff.seff_role) let export_side_effects mb env c = - let { const_entry_body = body } = c in + let { const_entry_body = body; _ } = c in let _, eff = Future.force body in let ce = { c with const_entry_body = Future.chain body @@ -493,7 +488,7 @@ let export_side_effects mb env c = let seff, signatures = List.fold_left aux ([],[]) (uniq_seff_rev eff) in let trusted = check_signatures mb signatures in let push_seff env eff = - let { seff_constant = kn; seff_body = cb } = eff in + let { seff_constant = kn; seff_body = cb ; _ } = eff in let env = Environ.add_constant kn cb env in match cb.const_universes with | Polymorphic_const _ -> env @@ -511,7 +506,7 @@ let export_side_effects mb env c = if Int.equal sl 0 then let env, cbs = List.fold_left (fun (env,cbs) eff -> - let { seff_constant = kn; seff_body = ocb; seff_env = u } = eff in + let { seff_constant = kn; seff_body = ocb; seff_env = u ; _ } = eff in let ce = constant_entry_of_side_effect ocb u in let cb = translate_constant Pure env kn ce in let eff = { eff with @@ -543,7 +538,7 @@ let translate_recipe env kn r = let hcons = DirPath.is_empty dir in build_constant_declaration kn env (Cooking.cook_constant ~hcons r) -let translate_local_def env id centry = +let translate_local_def env _id centry = let open Cooking in let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in let centry = { diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 25c1cbff3a..7456ecea56 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -118,14 +118,14 @@ let check_hyps_inclusion env f c sign = (* Type of constants *) -let type_of_constant env (kn,u as cst) = +let type_of_constant env (kn,_u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in let ty, cu = constant_type env cst in let () = check_constraints cu env in ty -let type_of_constant_in env (kn,u as cst) = +let type_of_constant_in env (kn,_u as cst) = let cb = lookup_constant kn env in let () = check_hyps_inclusion env mkConstU cst cb.const_hyps in constant_type_in env cst @@ -142,7 +142,7 @@ let type_of_constant_in env (kn,u as cst) = and no upper constraint exists on the sort $s$, we don't need to compute $s$ *) -let type_of_abstraction env name var ty = +let type_of_abstraction _env name var ty = mkProd (name, var, ty) (* Type of an application. *) @@ -204,7 +204,7 @@ let sort_of_product env domsort rangsort = where j.uj_type is convertible to a sort s2 *) -let type_of_product env name s1 s2 = +let type_of_product env _name s1 s2 = let s = sort_of_product env s1 s2 in mkSort s @@ -247,7 +247,7 @@ let check_cast env c ct k expected_type = dynamic constraints of the form u<=v are enforced *) let type_of_inductive_knowing_parameters env (ind,u as indu) args = - let (mib,mip) as spec = lookup_mind_specif env ind in + let (mib,_mip) as spec = lookup_mind_specif env ind in check_hyps_inclusion env mkIndU indu mib.mind_hyps; let t,cst = Inductive.constrained_type_of_inductive_knowing_parameters env (spec,u) args @@ -264,7 +264,7 @@ let type_of_inductive env (ind,u as indu) = (* Constructors. *) -let type_of_constructor env (c,u as cu) = +let type_of_constructor env (c,_u as cu) = let () = let ((kn,_),_) = c in let mib = lookup_mind kn env in @@ -285,7 +285,7 @@ let check_branch_types env (ind,u) c ct lft explft = | Invalid_argument _ -> error_number_branches env (make_judge c ct) (Array.length explft) -let type_of_case env ci p pt c ct lf lft = +let type_of_case env ci p pt c ct _lf lft = let (pind, _ as indspec) = try find_rectype env ct with Not_found -> error_case_not_inductive env (make_judge c ct) in @@ -399,7 +399,7 @@ let rec execute env cstr = let lft = execute_array env lf in type_of_case env ci p pt c ct lf lft - | Fix ((vn,i as vni),recdef) -> + | Fix ((_vn,i as vni),recdef) -> let (fix_ty,recdef') = execute_recdef env recdef i in let fix = (vni,recdef') in check_fix env fix; fix_ty @@ -432,12 +432,12 @@ and execute_array env = Array.map (execute env) (* Derived functions *) -let universe_levels_of_constr env c = +let universe_levels_of_constr _env c = let rec aux s c = match kind c with - | Const (c, u) -> + | Const (_c, u) -> LSet.fold LSet.add (Instance.levels u) s - | Ind ((mind,_), u) | Construct (((mind,_),_), u) -> + | Ind ((_mind,_), u) | Construct (((_mind,_),_), u) -> LSet.fold LSet.add (Instance.levels u) s | Sort u when not (Sorts.is_small u) -> let u = Sorts.univ_of_sort u in @@ -530,7 +530,7 @@ let judge_of_product env x varj outj = make_judge (mkProd (x, varj.utj_val, outj.utj_val)) (mkSort (sort_of_product env varj.utj_type outj.utj_type)) -let judge_of_letin env name defj typj j = +let judge_of_letin _env name defj typj j = make_judge (mkLetIn (name, defj.uj_val, typj.utj_val, j.uj_val)) (subst1 defj.uj_val j.uj_type) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 95d71965df..9ff51fca55 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -194,7 +194,7 @@ let check_universes_invariants g = UMap.iter (fun l u -> match u with | Canonical u -> - UMap.iter (fun v strict -> + UMap.iter (fun v _strict -> incr n_edges; let v = repr g v in assert (topo_compare u v = -1); @@ -435,7 +435,7 @@ let reorder g u v = | n0::q0 -> (* Computing new root. *) let root, rank_rest = - List.fold_left (fun ((best, rank_rest) as acc) n -> + List.fold_left (fun ((best, _rank_rest) as acc) n -> if n.rank >= best.rank then n, best.rank else acc) (n0, min_int) q0 in @@ -809,7 +809,7 @@ let normalize_universes g = in UMap.fold (fun _ u g -> match u with - | Equiv u -> g + | Equiv _u -> g | Canonical u -> let _, u, g = get_ltle g u in let _, _, g = get_gtge g u in @@ -821,7 +821,7 @@ let constraints_of_universes g = let uf = UF.create () in let constraints_of u v acc = match v with - | Canonical {univ=u; ltle} -> + | Canonical {univ=u; ltle; _} -> UMap.fold (fun v strict acc-> let typ = if strict then Lt else Le in Constraint.add (u,typ,v) acc) ltle acc @@ -943,7 +943,7 @@ let check_eq_instances g t1 t2 = (** Pretty-printing *) let pr_arc prl = function - | _, Canonical {univ=u; ltle} -> + | _, Canonical {univ=u; ltle; _} -> if UMap.is_empty ltle then mt () else prl u ++ str " " ++ @@ -963,7 +963,7 @@ let pr_universes prl g = let dump_universes output g = let dump_arc u = function - | Canonical {univ=u; ltle} -> + | Canonical {univ=u; ltle; _} -> let u_str = Level.to_string u in UMap.iter (fun v strict -> let typ = if strict then Lt else Le in diff --git a/kernel/univ.ml b/kernel/univ.ml index 311477daca..61ad1d0a82 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -86,7 +86,7 @@ struct | Level (n,d) as x -> let d' = Names.DirPath.hcons d in if d' == d then x else Level (n,d') - | Var n as x -> x + | Var _n as x -> x open Hashset.Combine @@ -160,13 +160,6 @@ module Level = struct let compare u v = if u == v then 0 - else - let c = Int.compare (hash u) (hash v) in - if c == 0 then RawLevel.compare (data u) (data v) - else c - - let natural_compare u v = - if u == v then 0 else RawLevel.compare (data u) (data v) let to_string x = @@ -206,13 +199,13 @@ module LMap = struct include M let union l r = - merge (fun k l r -> + merge (fun _k l r -> match l, r with | Some _, _ -> l | _, _ -> r) l r let subst_union l r = - merge (fun k l r -> + merge (fun _k l r -> match l, r with | Some (Some _), _ -> l | Some None, None -> l @@ -365,14 +358,14 @@ struct else f v ++ str"+" ++ int n let is_level = function - | (v, 0) -> true + | (_v, 0) -> true | _ -> false let level = function | (v,0) -> Some v | _ -> None - let get_level (v,n) = v + let get_level (v,_n) = v let map f (v, n as x) = let v' = f v in @@ -582,7 +575,7 @@ struct prl u2 ++ fnl () ) c (str "") let universes_of c = - fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty + fold (fun (u1, _op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty end let universes_of_constraints = Constraint.universes_of @@ -907,7 +900,7 @@ let subst_instance_constraints s csts = type universe_instance = Instance.t type 'a puniverses = 'a * Instance.t -let out_punivs (x, y) = x +let out_punivs (x, _y) = x let in_punivs x = (x, Instance.empty) let eq_puniverses f (x, u) (y, u') = f x y && Instance.equal u u' @@ -932,8 +925,8 @@ struct let hcons (univs, cst) = (Instance.hcons univs, hcons_constraints cst) - let instance (univs, cst) = univs - let constraints (univs, cst) = cst + let instance (univs, _cst) = univs + let constraints (_univs, cst) = cst let union (univs, cst) (univs', cst') = Instance.append univs univs', Constraint.union cst cst' @@ -952,7 +945,9 @@ struct include UContext let repr (inst, cst) = - (Array.mapi (fun i l -> Level.var i) inst, cst) + (Array.mapi (fun i _l -> Level.var i) inst, cst) + + let pr f ?variance ctx = pr f ?variance (repr ctx) let instantiate inst (u, cst) = assert (Array.length u = Array.length inst); @@ -988,8 +983,8 @@ struct let hcons (univs, variance) = (* should variance be hconsed? *) (UContext.hcons univs, variance) - let univ_context (univs, subtypcst) = univs - let variance (univs, variance) = variance + let univ_context (univs, _subtypcst) = univs + let variance (_univs, variance) = variance (** This function takes a universe context representing constraints of an inductive and produces a CumulativityInfo.t with the @@ -1054,7 +1049,7 @@ struct (univs, cst) let sort_levels a = - Array.sort Level.natural_compare a; a + Array.sort Level.compare a; a let to_context (ctx, cst) = (Instance.of_array (sort_levels (Array.of_list (LSet.elements ctx))), cst) @@ -1066,8 +1061,8 @@ struct if is_empty ctx then mt() else h 0 (LSet.pr prl univs ++ str " |= ") ++ h 0 (v 0 (Constraint.pr prl cst)) - let constraints (univs, cst) = cst - let levels (univs, cst) = univs + let constraints (_univs, cst) = cst + let levels (univs, _cst) = univs let size (univs,_) = LSet.cardinal univs end @@ -1155,7 +1150,7 @@ let make_inverse_instance_subst i = LMap.empty arr let make_abstract_instance (ctx, _) = - Array.mapi (fun i l -> Level.var i) ctx + Array.mapi (fun i _l -> Level.var i) ctx let abstract_universes ctx = let instance = UContext.instance ctx in diff --git a/kernel/vars.ml b/kernel/vars.ml index 0f588a6302..9d5d79124b 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -66,7 +66,7 @@ let isMeta c = match Constr.kind c with let noccur_with_meta n m term = let rec occur_rec n c = match Constr.kind c with | Constr.Rel p -> if n<=p && p<n+m then raise LocalOccur - | Constr.App(f,cl) -> + | Constr.App(f,_cl) -> (match Constr.kind f with | Constr.Cast (c,_,_) when isMeta c -> () | Constr.Meta _ -> () @@ -188,7 +188,7 @@ let adjust_rel_to_rel_context sign n = let open RelDecl in match sign with | LocalAssum _ :: sign' -> let (n',p) = aux sign' in (n'+1,p) - | LocalDef (_,c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) + | LocalDef (_,_c,_)::sign' -> let (n',p) = aux sign' in (n'+1,if n'<n then p+1 else p) | [] -> (0,n) in snd (aux sign) diff --git a/kernel/vconv.ml b/kernel/vconv.ml index d19bea5199..5965853e1e 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -11,7 +11,7 @@ open Csymtable let compare_zipper z1 z2 = match z1, z2 with | Zapp args1, Zapp args2 -> Int.equal (nargs args1) (nargs args2) - | Zfix(f1,args1), Zfix(f2,args2) -> Int.equal (nargs args1) (nargs args2) + | Zfix(_f1,args1), Zfix(_f2,args2) -> Int.equal (nargs args1) (nargs args2) | Zswitch _, Zswitch _ | Zproj _, Zproj _ -> true | Zapp _ , _ | Zfix _, _ | Zswitch _, _ | Zproj _, _ -> false @@ -84,7 +84,7 @@ and conv_whd env pb k whd1 whd2 cu = and conv_atom env pb k a1 stk1 a2 stk2 cu = (* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *) match a1, a2 with - | Aind ((mi,i) as ind1) , Aind ind2 -> + | Aind ((mi,_i) as ind1) , Aind ind2 -> if eq_ind ind1 ind2 && compare_stack stk1 stk2 then if Environ.polymorphic_ind ind1 env then let mib = Environ.lookup_mind mi env in diff --git a/kernel/vm.ml b/kernel/vm.ml index 9917e94a35..eaf64ba4af 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -187,5 +187,5 @@ let apply_whd k whd = interprete (cofix_upd_code to_up) (cofix_upd_val to_up) (cofix_upd_env to_up) 0 | Vatom_stk(a,stk) -> apply_stack (val_of_atom a) stk v - | Vuniv_level lvl -> assert false + | Vuniv_level _lvl -> assert false diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 8edd49f77f..217ef4b8e5 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -100,7 +100,7 @@ let eq_structured_constant c1 c2 = match c1, c2 with | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false | Const_val v1, Const_val v2 -> eq_structured_values v1 v2 -| Const_val v1, _ -> false +| Const_val _v1, _ -> false let hash_structured_constant c = let open Hashset.Combine in @@ -245,7 +245,7 @@ type id_key = | RelKey of Int.t | EvarKey of Evar.t -let eq_id_key k1 k2 = match k1, k2 with +let eq_id_key (k1 : id_key) (k2 : id_key) = match k1, k2 with | ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 | VarKey id1, VarKey id2 -> Id.equal id1 id2 | RelKey n1, RelKey n2 -> Int.equal n1 n2 @@ -304,9 +304,9 @@ let uni_lvl_val (v : values) : Univ.Level.t = | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" | Vcofix _ -> str "Vcofix" - | Vconstr_const i -> str "Vconstr_const" - | Vconstr_block b -> str "Vconstr_block" - | Vatom_stk (a,stk) -> str "Vatom_stk" + | Vconstr_const _i -> str "Vconstr_const" + | Vconstr_block _b -> str "Vconstr_block" + | Vatom_stk (_a,_stk) -> str "Vatom_stk" | _ -> assert false in CErrors.anomaly @@ -444,7 +444,7 @@ struct type t = id_key let equal = eq_id_key open Hashset.Combine - let hash = function + let hash : t -> tag = function | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) @@ -658,7 +658,7 @@ and pr_whd w = | Vfix _ -> str "Vfix" | Vcofix _ -> str "Vcofix" | Vconstr_const i -> str "Vconstr_const(" ++ int i ++ str ")" - | Vconstr_block b -> str "Vconstr_block" + | Vconstr_block _b -> str "Vconstr_block" | Vatom_stk (a,stk) -> str "Vatom_stk(" ++ pr_atom a ++ str ", " ++ pr_stack stk ++ str ")" | Vuniv_level _ -> assert false) and pr_stack stk = @@ -668,6 +668,6 @@ and pr_stack stk = and pr_zipper z = Pp.(match z with | Zapp args -> str "Zapp(len = " ++ int (nargs args) ++ str ")" - | Zfix (f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" - | Zswitch s -> str "Zswitch(...)" + | Zfix (_f,args) -> str "Zfix(..., len=" ++ int (nargs args) ++ str ")" + | Zswitch _s -> str "Zswitch(...)" | Zproj c -> str "Zproj(" ++ Projection.Repr.print c ++ str ")") diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index ce620d5312..f26ec0f401 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -26,6 +26,10 @@ let init_size=5 let cc_verbose=ref false +let print_constr t = + let sigma, env = Pfedit.get_current_context () in + Printer.pr_econstr_env env sigma t + let debug x = if !cc_verbose then Feedback.msg_debug (x ()) @@ -483,10 +487,10 @@ let rec inst_pattern subst = function args t let pr_idx_term uf i = str "[" ++ int i ++ str ":=" ++ - Termops.print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" + print_constr (EConstr.of_constr (constr_of_term (term uf i))) ++ str "]" let pr_term t = str "[" ++ - Termops.print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" + print_constr (EConstr.of_constr (constr_of_term t)) ++ str "]" let rec add_term state t= let uf=state.uf in @@ -601,7 +605,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ + (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " == " ++ pr_term t ++ str "]")); add_equality state prf s t end @@ -609,7 +613,7 @@ let add_inst state (inst,int_subst) = begin debug (fun () -> (str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++ - (str " [" ++ Termops.print_constr (EConstr.of_constr prf) ++ str " : " ++ + (str " [" ++ print_constr (EConstr.of_constr prf) ++ str " : " ++ pr_term s ++ str " <> " ++ pr_term t ++ str "]")); add_disequality state (Hyp prf) s t end diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index 803d35d07c..b219ee25ca 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -272,6 +272,8 @@ let string_of_genarg_arg (ArgumentType arg) = in pr_sequence pr prods with Not_found -> + (* FIXME: This key, moreover printed with a low-level printer, + has no meaning user-side *) KerName.print key let pr_alias_gen pr_gen lev key l = diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 67ffae59cc..9f34df4608 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -1298,7 +1298,7 @@ and tactic_of_value ist vle = match appl with UnnamedAppl -> "An unnamed user-defined tactic" | GlbAppl apps -> - let nms = List.map (fun (kn,_) -> Names.KerName.to_string kn) apps in + let nms = List.map (fun (kn,_) -> string_of_qualid (Tacenv.shortest_qualid_of_tactic kn)) apps in match nms with [] -> assert false | kn::_ -> "The user-defined tactic \"" ^ kn ^ "\"" (* TODO: when do we not have a singleton? *) diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 48d677a864..6bab8d0353 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -12,7 +12,6 @@ open Util open Names open Pp open Tacexpr -open Termops let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () @@ -51,8 +50,8 @@ let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) let db_pr_goal gl = let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - let penv = print_named_context env in - let pc = print_constr_env env (Tacmach.New.project gl) concl in + let penv = Termops.Internal.print_named_context env in + let pc = Printer.pr_econstr_env env (Tacmach.New.project gl) concl in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () @@ -243,7 +242,7 @@ let db_constr debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Evaluated term: " ++ print_constr_env env sigma c) + msg_tac_debug (str "Evaluated term: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints the pattern rule *) @@ -268,7 +267,7 @@ let db_matched_hyp debug env sigma (id,_,c) ido = is_debug debug >>= fun db -> if db then msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++ - str " has been matched: " ++ print_constr_env env sigma c) + str " has been matched: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints the matched conclusion *) @@ -276,7 +275,7 @@ let db_matched_concl debug env sigma c = let open Proofview.NonLogical in is_debug debug >>= fun db -> if db then - msg_tac_debug (str "Conclusion has been matched: " ++ print_constr_env env sigma c) + msg_tac_debug (str "Conclusion has been matched: " ++ Printer.pr_econstr_env env sigma c) else return () (* Prints a success message when the goal has been matched *) diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index a7aae5bd31..e4a0910673 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -342,7 +342,7 @@ let interp_index ist gl idx = open Pltac -ARGUMENT EXTEND ssrindex TYPED AS ssrindex PRINTED BY pr_ssrindex +ARGUMENT EXTEND ssrindex PRINTED BY pr_ssrindex INTERPRETED BY interp_index | [ int_or_var(i) ] -> [ mk_index ~loc i ] END diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml index 20ea8b3667..aadb4fe5f6 100644 --- a/plugins/ssrmatching/ssrmatching.ml +++ b/plugins/ssrmatching/ssrmatching.ml @@ -1366,7 +1366,7 @@ let ssrpatterntac _ist arg gl = let concl0 = pf_concl gl in let concl0 = EConstr.Unsafe.to_constr concl0 in let (t, uc), concl_x = - fill_occ_pattern (Global.env()) sigma0 concl0 pat noindex 1 in + fill_occ_pattern (pf_env gl) sigma0 concl0 pat noindex 1 in 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 diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index fc24e9b3a9..265909980b 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -187,7 +187,7 @@ let _ = Goptions.declare_bool_option { Goptions.optwrite = (fun a -> debug_cbv:=a); } -let pr_key = function +let debug_pr_key = function | ConstKey (sp,_) -> Names.Constant.print sp | VarKey id -> Names.Id.print id | RelKey n -> Pp.(str "REL_" ++ int n) @@ -320,14 +320,14 @@ and norm_head_ref k info env stack normt = if red_set_ref (info_flags info.infos) normt then match ref_value_cache info.infos info.tab normt with | Some body -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt); strip_appl (shift_value k body) stack | None -> - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) else begin - if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ pr_key normt); + if !debug_cbv then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt); (VAL(0,make_constr_ref k normt),stack) end diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 6c52dacaa9..7d480b8d48 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -588,7 +588,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty (* Evar must be undefined since we have flushed evars *) let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (pr_state appr1 ++ cut () ++ pr_state appr2 ++ cut ())) in + Feedback.msg_notice (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in match (flex_kind_of_term (fst ts) env evd term1 sk1, flex_kind_of_term (fst ts) env evd term2 sk2) with | Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) -> @@ -1225,8 +1225,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in let () = if !debug_unification then let open Pp in - Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ print_constr t1 - ++ cut () ++ print_constr t2 ++ cut ())) in + Feedback.msg_notice (v 0 (str "Heuristic:" ++ spc () ++ + Termops.Internal.print_constr_env env evd t1 ++ cut () ++ + Termops.Internal.print_constr_env env evd t2 ++ cut ())) in let app_empty = Array.is_empty l1 && Array.is_empty l2 in match EConstr.kind evd term1, EConstr.kind evd term2 with | Evar (evk1,args1), (Rel _|Var _) when app_empty diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml index b452755b10..571be7466c 100644 --- a/pretyping/evardefine.ml +++ b/pretyping/evardefine.ml @@ -201,4 +201,4 @@ let lift_tycon n = Option.map (lift n) let pr_tycon env sigma = function None -> str "None" - | Some t -> Termops.print_constr_env env sigma t + | Some t -> Termops.Internal.print_constr_env env sigma t diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml index 12788e5ec5..63a66b471b 100644 --- a/pretyping/globEnv.ml +++ b/pretyping/globEnv.ml @@ -55,16 +55,16 @@ let env env = env.static_env let vars_of_env env = Id.Set.union (Id.Map.domain env.lvar.ltac_genargs) (vars_of_env env.static_env) -let ltac_interp_name { ltac_idents ; ltac_genargs } = function - | Anonymous -> Anonymous - | Name id as na -> - try Name (Id.Map.find id ltac_idents) - with Not_found -> - if Id.Map.mem id ltac_genargs then - user_err (str "Ltac variable" ++ spc () ++ Id.print id ++ - spc () ++ str "is not bound to an identifier." ++ - spc () ++str "It cannot be used in a binder.") - else na +let ltac_interp_id { ltac_idents ; ltac_genargs } id = + try Id.Map.find id ltac_idents + with Not_found -> + if Id.Map.mem id ltac_genargs then + user_err (str "Ltac variable" ++ spc () ++ Id.print id ++ + spc () ++ str "is not bound to an identifier." ++ + spc () ++str "It cannot be used in a binder.") + else id + +let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar) let push_rel sigma d env = let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in @@ -140,7 +140,7 @@ let protected_get_type_of env sigma c = try Retyping.get_type_of ~lax:true env sigma c with Retyping.RetypeError _ -> user_err - (str "Cannot reinterpret " ++ quote (print_constr c) ++ + (str "Cannot reinterpret " ++ quote (Termops.Internal.print_constr_env env sigma c) ++ str " in the current environment.") let invert_ltac_bound_name env id0 id = @@ -182,6 +182,8 @@ let interp_ltac_variable ?loc typing_fun env sigma id = end; raise Not_found +let interp_ltac_id env id = ltac_interp_id env.lvar id + module ConstrInterpObj = struct type ('r, 'g, 't) obj = diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli index 4038523211..70a7ee6e2f 100644 --- a/pretyping/globEnv.mli +++ b/pretyping/globEnv.mli @@ -76,6 +76,11 @@ val hide_variable : t -> Name.t -> Id.t -> t val interp_ltac_variable : ?loc:Loc.t -> (t -> Glob_term.glob_constr -> unsafe_judgment) -> t -> evar_map -> Id.t -> unsafe_judgment +(** Interp an identifier as an ltac variable bound to an identifier, + or as the identifier itself if not bound to an ltac variable *) + +val interp_ltac_id : t -> Id.t -> Id.t + (** Interpreting a generic argument, typically a "ltac:(...)", taking into account the possible renaming *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index ec0ff73062..0fa573b9a6 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -358,7 +358,7 @@ let make_case_or_project env sigma indf ci pred c branches = not (has_dependent_elim mib) then user_err ~hdr:"make_case_or_project" Pp.(str"Dependent case analysis not allowed" ++ - str" on inductive type " ++ Names.MutInd.print (fst ind)) + str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind)) in let branch = branches.(0) in let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8774cdf080..162adf0626 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -480,6 +480,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref | GEvar (id, inst) -> (* Ne faudrait-il pas s'assurer que hyps est bien un sous-contexte du contexte courant, et qu'il n'y a pas de Rel "caché" *) + let id = interp_ltac_id env id in let evk = try Evd.evar_key id !evdref with Not_found -> @@ -499,6 +500,11 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) evdref { uj_val = e_new_evar env evdref ~src:(loc,k) ty; uj_type = ty } | GHole (k, naming, None) -> + let open Namegen in + let naming = match naming with + | IntroIdentifier id -> IntroIdentifier (interp_ltac_id env id) + | IntroAnonymous -> IntroAnonymous + | IntroFresh id -> IntroFresh (interp_ltac_id env id) in let ty = match tycon with | Some ty -> ty @@ -978,9 +984,9 @@ and pretype_instance k0 resolve_tc env evdref loc hyps evk update = pr_existential_key !evdref evk ++ strbrk " in current context: binding for " ++ Id.print id ++ strbrk " is not convertible to its expected definition (cannot unify " ++ - quote (print_constr_env !!env !evdref b) ++ + quote (Termops.Internal.print_constr_env !!env !evdref b) ++ strbrk " and " ++ - quote (print_constr_env !!env !evdref c) ++ + quote (Termops.Internal.print_constr_env !!env !evdref c) ++ str ").") | Some b, None -> user_err ?loc (str "Cannot interpret " ++ diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index bd41e61b34..c25416405e 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -229,7 +229,7 @@ let warn_projection_no_head_constant = let env = Termops.push_rels_assum sign env in let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) in let proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - let term_pp = Termops.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in + let term_pp = Termops.Internal.print_constr_env env (Evd.from_env env) (EConstr.of_constr t) in strbrk "Projection value has no head constant: " ++ term_pp ++ strbrk " in canonical instance " ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") @@ -295,8 +295,12 @@ let add_canonical_structure warn o = in match ocs with | None -> object_table := GlobRef.Map.add proj ((pat,s)::l) !object_table; | Some (c, cs) -> - let old_can_s = (Termops.print_constr (EConstr.of_constr cs.o_DEF)) - and new_can_s = (Termops.print_constr (EConstr.of_constr s.o_DEF)) in + (* XXX: Undesired global access to env *) + let env = Global.env () in + let sigma = Evd.from_env env in + let old_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr cs.o_DEF)) + and new_can_s = (Termops.Internal.print_constr_env env sigma (EConstr.of_constr s.o_DEF)) + in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) @@ -334,19 +338,19 @@ let error_not_structure ref description = user_err ~hdr:"object_declare" (str"Could not declare a canonical structure " ++ (Id.print (basename_of_global ref) ++ str"." ++ spc() ++ - str(description))) + description)) let check_and_decompose_canonical_structure ref = let sp = match ref with ConstRef sp -> sp - | _ -> error_not_structure ref "Expected an instance of a record or structure." + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let env = Global.env () in let u = Univ.make_abstract_instance (Environ.constant_context env sp) in let vc = match Environ.constant_opt_value_in env (sp, u) with | Some vc -> vc - | None -> error_not_structure ref "Could not find its value in the global environment." in + | None -> error_not_structure ref (str "Could not find its value in the global environment.") in let env = Global.env () in let evd = Evd.from_env env in let body = snd (splay_lam (Global.env()) evd (EConstr.of_constr vc)) in @@ -354,18 +358,18 @@ let check_and_decompose_canonical_structure ref = let f,args = match kind body with | App (f,args) -> f,args | _ -> - error_not_structure ref "Expected a record or structure constructor applied to arguments." in + error_not_structure ref (str "Expected a record or structure constructor applied to arguments.") in let indsp = match kind f with | Construct ((indsp,1),u) -> indsp - | _ -> error_not_structure ref "Expected an instance of a record or structure." in + | _ -> error_not_structure ref (str "Expected an instance of a record or structure.") in let s = try lookup_structure indsp with Not_found -> error_not_structure ref - ("Could not find the record or structure " ^ (MutInd.to_string (fst indsp))) in + (str "Could not find the record or structure " ++ Termops.Internal.print_constr_env env evd (EConstr.mkInd indsp)) in let ntrue_projs = List.count snd s.s_PROJKIND in if s.s_EXPECTEDPARAM + ntrue_projs > Array.length args then - error_not_structure ref "Got too few arguments to the record or structure constructor."; + error_not_structure ref (str "Got too few arguments to the record or structure constructor."); (sp,indsp) let declare_canonical_structure ref = diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index f4c8a6cd66..e8c3b3e2b3 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -254,9 +254,9 @@ module Cst_stack = struct (applist (cst, List.rev params)) t) cst_l c - let pr l = + let pr env sigma l = let open Pp in - let p_c c = Termops.print_constr c in + let p_c c = Termops.Internal.print_constr_env env sigma c in prlist_with_sep pr_semicolon (fun (c,params,args) -> hov 1 (str"(" ++ p_c c ++ str ")" ++ spc () ++ pr_sequence p_c params ++ spc () ++ str "(args:" ++ @@ -341,6 +341,7 @@ struct | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list + (* Debugging printer *) let rec pr_member pr_c member = let open Pp in let pr_c x = hov 1 (pr_c x) in @@ -351,7 +352,7 @@ struct prvect_with_sep (pr_bar) pr_c br ++ str ")" | Proj (p,cst) -> - str "ZProj(" ++ Constant.print (Projection.constant p) ++ str ")" + str "ZProj(" ++ Constant.debug_print (Projection.constant p) ++ str ")" | Fix (f,args,cst) -> str "ZFix(" ++ Termops.pr_fix pr_c f ++ pr_comma () ++ pr pr_c args ++ str ")" @@ -368,11 +369,11 @@ struct let open Pp in match c with | Cst_const (c, u) -> - if Univ.Instance.is_empty u then Constant.print c - else str"(" ++ Constant.print c ++ str ", " ++ + if Univ.Instance.is_empty u then Constant.debug_print c + else str"(" ++ Constant.debug_print c ++ str ", " ++ Univ.Instance.pr Univ.Level.pr u ++ str")" | Cst_proj p -> - str".(" ++ Constant.print (Projection.constant p) ++ str")" + str".(" ++ Constant.debug_print (Projection.constant p) ++ str")" let empty = [] let is_empty = CList.is_empty @@ -614,9 +615,9 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -let pr_state (tm,sk) = +let pr_state env sigma (tm,sk) = let open Pp in - let pr c = Termops.print_constr c in + let pr c = Termops.Internal.print_constr_env env sigma c in h 0 (pr tm ++ str "|" ++ cut () ++ Stack.pr pr sk) (*************************************) @@ -854,10 +855,10 @@ let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma = let rec whrec cst_l (x, stack) = let () = if !debug_RAKAM then let open Pp in - let pr c = Termops.print_constr c in + let pr c = Termops.Internal.print_constr_env env sigma c in Feedback.msg_notice (h 0 (str "<<" ++ pr x ++ - str "|" ++ cut () ++ Cst_stack.pr cst_l ++ + str "|" ++ cut () ++ Cst_stack.pr env sigma cst_l ++ str "|" ++ cut () ++ Stack.pr pr stack ++ str ">>")) in diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index dd3cd26f0f..c0ff6723f6 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -60,7 +60,7 @@ module Cst_stack : sig val best_cst : t -> (constr * constr list) option val best_replace : Evd.evar_map -> constr -> t -> constr -> constr val reference : Evd.evar_map -> t -> Constant.t option - val pr : t -> Pp.t + val pr : env -> Evd.evar_map -> t -> Pp.t end module Stack : sig @@ -140,7 +140,7 @@ type contextual_state_reduction_function = type state_reduction_function = contextual_state_reduction_function type local_state_reduction_function = evar_map -> state -> state -val pr_state : state -> Pp.t +val pr_state : env -> evar_map -> state -> Pp.t (** {6 Reduction Function Operators } *) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index fc1f6fc81e..e223674579 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -684,8 +684,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e and cN = Evarutil.whd_head_evar sigma curn in let () = if !debug_unification then - Feedback.msg_debug (print_constr_env curenv sigma cM ++ str" ~= " ++ print_constr_env curenv sigma cN) - in + Feedback.msg_debug ( + Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++ + Termops.Internal.print_constr_env curenv sigma cN) + in match (EConstr.kind sigma cM, EConstr.kind sigma cN) with | Meta k1, Meta k2 -> if Int.equal k1 k2 then substn else diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 9ed985195f..66f748454d 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -71,17 +71,17 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref udecl = - let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in - let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in + let typ, univs = Global.type_of_global_in_context (Global.env ()) ref in + let inst = Univ.make_abstract_instance univs in + let bl = UnivNames.universe_binders_with_opt_names ref udecl in + let sigma = Evd.from_ctx (UState.of_binders bl) in let typ = EConstr.of_constr typ in let typ = if reduce then let env = Global.env () in - let sigma = Evd.from_env env in let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in - let univs = Global.universes_of_global ref in let variance = match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> @@ -91,19 +91,14 @@ let print_ref reduce ref udecl = | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) end in - let inst = Univ.AUContext.instance univs in - let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in - let bl = UnivNames.universe_binders_with_opt_names ref - (Array.to_list (Univ.Instance.to_array inst)) udecl in - let sigma = Evd.from_ctx (UState.of_binders bl) in let inst = if Global.is_polymorphic ref - then Printer.pr_universe_instance sigma (Univ.UContext.instance univs) + then Printer.pr_universe_instance sigma inst else mt () in hov 0 (pr_global ref ++ inst ++ str " :" ++ spc () ++ pr_letype_env env sigma typ ++ - Printer.pr_universe_ctx sigma ?variance univs) + Printer.pr_abstract_universe_ctx sigma ?variance univs) (********************************) (** Printing implicit arguments *) @@ -552,48 +547,31 @@ let print_typed_body env evd (val_0,typ) = let print_instance sigma cb = if Declareops.constant_is_polymorphic cb then let univs = Declareops.constant_polymorphic_context cb in - let inst = Univ.AUContext.instance univs in + let inst = Univ.make_abstract_instance univs in pr_universe_instance sigma inst else mt() let print_constant with_values sep sp udecl = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in - let typ = - match cb.const_universes with - | Monomorphic_const _ -> cb.const_type - | Polymorphic_const univs -> - let inst = Univ.AUContext.instance univs in - Vars.subst_instance_constr inst cb.const_type - in - let univs, ulist = - let open Entries in + let typ = cb.const_type in + let univs = let open Univ in let otab = Global.opaque_tables () in match cb.const_body with - | Undef _ | Def _ -> - begin - match cb.const_universes with - | Monomorphic_const ctx -> Monomorphic_const_entry ctx, [] - | Polymorphic_const ctx -> - let inst = AUContext.instance ctx in - Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)), - Array.to_list (Instance.to_array inst) - end + | Undef _ | Def _ -> cb.const_universes | OpaqueDef o -> let body_uctxs = Opaqueproof.force_constraints otab o in match cb.const_universes with | Monomorphic_const ctx -> - Monomorphic_const_entry (ContextSet.union body_uctxs ctx), [] + Monomorphic_const (ContextSet.union body_uctxs ctx) | Polymorphic_const ctx -> assert(ContextSet.is_empty body_uctxs); - let inst = AUContext.instance ctx in - Polymorphic_const_entry (UContext.make (inst, AUContext.instantiate inst ctx)), - Array.to_list (Instance.to_array inst) + Polymorphic_const ctx in let ctx = UState.of_binders - (UnivNames.universe_binders_with_opt_names (ConstRef sp) ulist udecl) + (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in @@ -605,7 +583,6 @@ let print_constant with_values sep sp udecl = str" ]" ++ Printer.pr_constant_universes sigma univs | Some (c, ctx) -> - let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_constant_universes sigma univs) @@ -712,11 +689,6 @@ let print_eval x = !object_pr.print_eval x (**** Printing declarations and judgments *) (**** Abstract layer *****) -let print_typed_value x = - let env = Global.env () in - let sigma = Evd.from_env env in - print_typed_value_in_env env sigma x - let print_judgment env sigma {uj_val=trm;uj_type=typ} = print_typed_value_in_env env sigma (trm, typ) @@ -852,11 +824,9 @@ let print_opaque_name env sigma qid = print_inductive sp None | ConstructRef cstr as gr -> let ty, ctx = Global.type_of_global_in_context env gr in - let inst = Univ.AUContext.instance ctx in - let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in let open EConstr in - print_typed_value (mkConstruct cstr, ty) + print_typed_value_in_env env sigma (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> print_named_decl env sigma diff --git a/printing/printer.ml b/printing/printer.ml index 67d71332b0..6cd4daa374 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -192,7 +192,7 @@ let pr_constr_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) -let _ = Termops.set_print_constr +let _ = Termops.Internal.set_print_constr (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t)) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" @@ -270,9 +270,16 @@ let pr_universe_ctx sigma ?variance c = else mt() +let pr_abstract_universe_ctx sigma ?variance c = + if !Detyping.print_universes && not (Univ.AUContext.is_empty c) then + fnl()++pr_in_comment (fun c -> v 0 + (Univ.pr_abstract_universe_context (Termops.pr_evd_level sigma) ?variance c)) c + else + mt() + let pr_constant_universes sigma = function - | Entries.Monomorphic_const_entry ctx -> pr_universe_ctx_set sigma ctx - | Entries.Polymorphic_const_entry ctx -> pr_universe_ctx sigma ctx + | Declarations.Monomorphic_const ctx -> pr_universe_ctx_set sigma ctx + | Declarations.Polymorphic_const ctx -> pr_abstract_universe_ctx sigma ctx let pr_cumulativity_info sigma cumi = if !Detyping.print_universes @@ -282,6 +289,14 @@ let pr_cumulativity_info sigma cumi = else mt() +let pr_abstract_cumulativity_info sigma cumi = + if !Detyping.print_universes + && not (Univ.AUContext.is_empty (Univ.ACumulativityInfo.univ_context cumi)) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_abstract_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + else + mt() + (**********************************************************************) (* Global references *) @@ -944,9 +959,16 @@ let pr_assumptionset env sigma s = let safe_pr_constant env kn = try pr_constant env kn with Not_found -> + (* FIXME? *) let mp,_,lab = Constant.repr3 kn in str (ModPath.to_string mp) ++ str "." ++ Label.print lab in + let safe_pr_inductive env kn = + try pr_inductive env (kn,0) + with Not_found -> + (* FIXME? *) + MutInd.print kn + in let safe_pr_ltype env sigma typ = try str " : " ++ pr_ltype_env env sigma typ with e when CErrors.noncritical e -> mt () @@ -961,7 +983,7 @@ let pr_assumptionset env sigma s = | Constant kn -> safe_pr_constant env kn ++ safe_pr_ltype env sigma typ | Positive m -> - hov 2 (MutInd.print m ++ spc () ++ strbrk"is positive.") + hov 2 (safe_pr_inductive env m ++ spc () ++ strbrk"is positive.") | Guarded kn -> hov 2 (safe_pr_constant env kn ++ spc () ++ strbrk"is positive.") in diff --git a/printing/printer.mli b/printing/printer.mli index 518c5b930b..96db7091a6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -123,9 +123,12 @@ val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t +val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> + Univ.AUContext.t -> Pp.t val pr_universe_ctx_set : evar_map -> Univ.ContextSet.t -> Pp.t -val pr_constant_universes : evar_map -> Entries.constant_universes_entry -> Pp.t +val pr_constant_universes : evar_map -> Declarations.constant_universes -> Pp.t val pr_cumulativity_info : evar_map -> Univ.CumulativityInfo.t -> Pp.t +val pr_abstract_cumulativity_info : evar_map -> Univ.ACumulativityInfo.t -> Pp.t (** Printing global references using names as short as possible *) diff --git a/printing/printmod.ml b/printing/printmod.ml index e2d9850bf8..1fc308ac99 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -90,9 +90,7 @@ let build_ind_type env mip = Inductive.type_of_inductive env mip let print_one_inductive env sigma mib ((_,i) as ind) = - let u = if Declareops.inductive_is_polymorphic mib then - Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) - else Univ.Instance.empty in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in @@ -111,16 +109,6 @@ let print_one_inductive env sigma mib ((_,i) as ind) = str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes -let instantiate_cumulativity_info cumi = - let open Univ in - let univs = ACumulativityInfo.univ_context cumi in - let expose ctx = - let inst = AUContext.instance ctx in - let cst = AUContext.instantiate inst ctx in - UContext.make (inst, cst) - in - CumulativityInfo.make (expose univs, ACumulativityInfo.variance cumi) - let print_mutual_inductive env mind mib udecl = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in @@ -131,14 +119,7 @@ let print_mutual_inductive env mind mib udecl = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let univs = - let open Univ in - if Declareops.inductive_is_polymorphic mib then - Array.to_list (Instance.to_array - (AUContext.instance (Declareops.inductive_polymorphic_context mib))) - else [] - in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) univs udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative @@ -150,8 +131,7 @@ let print_mutual_inductive env mind mib udecl = match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> - Printer.pr_cumulativity_info - sigma (instantiate_cumulativity_info cumi)) + Printer.pr_abstract_cumulativity_info sigma cumi) let get_fields = let rec prodec_rec l subst c = @@ -167,11 +147,7 @@ let get_fields = prodec_rec [] [] let print_record env mind mib udecl = - let u = - if Declareops.inductive_is_polymorphic mib then - Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) - else Univ.Instance.empty - in + let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in let mip = mib.mind_packets.(0) in let params = Inductive.inductive_paramdecls (mib,u) in let nparamdecls = Context.Rel.length params in @@ -181,8 +157,7 @@ let print_record env mind mib udecl = let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) - (Array.to_list (Univ.Instance.to_array u)) udecl in + let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in @@ -210,8 +185,7 @@ let print_record env mind mib udecl = match mib.mind_universes with | Monomorphic_ind _ | Polymorphic_ind _ -> str "" | Cumulative_ind cumi -> - Printer.pr_cumulativity_info - sigma (instantiate_cumulativity_info cumi) + Printer.pr_abstract_cumulativity_info sigma cumi ) let pr_mutual_inductive_body env mind mib udecl = @@ -315,12 +289,6 @@ let print_body is_impl env mp (l,body) = | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> let ctx = Declareops.constant_polymorphic_context cb in - let u = - if Declareops.constant_is_polymorphic cb then - Univ.AUContext.instance ctx - else Univ.Instance.empty - in - let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in (match cb.const_body with | Def _ -> def "Definition" ++ spc () | OpaqueDef _ when is_impl -> def "Theorem" ++ spc () @@ -328,18 +296,17 @@ let print_body is_impl env mp (l,body) = (match env with | None -> mt () | Some env -> + let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in + let sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ - hov 0 (Printer.pr_ltype_env env (Evd.from_env env) - (Vars.subst_instance_constr u - cb.const_type)) ++ + hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ hov 2 (str ":= " ++ - Printer.pr_lconstr_env env (Evd.from_env env) - (Vars.subst_instance_constr u (Mod_subst.force_constr l))) + Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l)) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx (Evd.from_env env) ctx) + Printer.pr_abstract_universe_ctx sigma ctx) | SFBmind mib -> try let env = Option.get env in diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 79b7e1599b..95e908c4dd 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -575,8 +575,8 @@ let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma let pr_clenv clenv = h 0 - (str"TEMPL: " ++ print_constr clenv.templval.rebus ++ - str" : " ++ print_constr clenv.templtyp.rebus ++ fnl () ++ + (str"TEMPL: " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templval.rebus ++ + str" : " ++ Termops.Internal.print_constr_env clenv.env clenv.evd clenv.templtyp.rebus ++ fnl () ++ pr_evar_map (Some 2) clenv.evd) (****************************************************************) diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 092bb5c276..182b38d350 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -127,8 +127,8 @@ open Pp let db_pr_goal sigma g = let env = Goal.V82.env sigma g in - let penv = print_named_context env in - let pc = print_constr_env env sigma (Goal.V82.concl sigma g) in + let penv = Termops.Internal.print_named_context env in + let pc = Termops.Internal.print_constr_env env sigma (Goal.V82.concl sigma g) in str" " ++ hv 0 (penv ++ fnl () ++ str "============================" ++ fnl () ++ str" " ++ pc) ++ fnl () diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 3456d13bbe..f3581f17dd 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -693,8 +693,9 @@ module Search = struct let msg = match fst ie with | Pretype_errors.PretypeError (env, evd, Pretype_errors.CannotUnify (x,y,_)) -> - str"Cannot unify " ++ print_constr_env env evd x ++ str" and " ++ - print_constr_env env evd y + str"Cannot unify " ++ + Printer.pr_econstr_env env evd x ++ str" and " ++ + Printer.pr_econstr_env env evd y | ReachedLimitEx -> str "Proof-search reached its limit." | NoApplicableEx -> str "Proof-search failed." | e -> CErrors.iprint ie diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 837865e644..596feeec8b 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -655,12 +655,11 @@ module New = struct | _ -> let name_elim = match EConstr.kind sigma elim with - | Const (kn, _) -> Constant.to_string kn - | Var id -> Id.to_string id - | _ -> "\b" + | Const _ | Var _ -> str " " ++ Printer.pr_econstr_env (pf_env gl) sigma elim + | _ -> mt () in user_err ~hdr:"Tacticals.general_elim_then_using" - (str "The elimination combinator " ++ str name_elim ++ str " is unknown.") + (str "The elimination combinator " ++ name_elim ++ str " is unknown.") in let elimclause' = clenv_fchain ~with_univs:false indmv elimclause indclause in let branchsigns = compute_constructor_signatures ~rec_flag ind in diff --git a/test-suite/output/UnivBinders.out b/test-suite/output/UnivBinders.out index 926114a1e1..f8f11d7cf6 100644 --- a/test-suite/output/UnivBinders.out +++ b/test-suite/output/UnivBinders.out @@ -86,10 +86,10 @@ Type@{M} -> Type@{N} -> Type@{E} (* E M N |= *) foo is universe polymorphic -foo@{Top.16 Top.17 Top.18} = -Type@{Top.17} -> Type@{Top.18} -> Type@{Top.16} - : Type@{max(Top.16+1,Top.17+1,Top.18+1)} -(* Top.16 Top.17 Top.18 |= *) +foo@{u Top.17 v} = +Type@{Top.17} -> Type@{v} -> Type@{u} + : Type@{max(u+1,Top.17+1,v+1)} +(* u Top.17 v |= *) foo is universe polymorphic NonCumulative Inductive Empty@{E} : Type@{E} := @@ -129,11 +129,19 @@ insec@{v} = Type@{u} -> Type@{v} (* v |= *) insec is universe polymorphic +NonCumulative Inductive insecind@{k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{k} + +For inseccstr: Argument scope is [type_scope] insec@{u v} = Type@{u} -> Type@{v} : Type@{max(u+1,v+1)} (* u v |= *) insec is universe polymorphic +NonCumulative Inductive insecind@{u k} : Type@{k+1} := + inseccstr : Type@{k} -> insecind@{u k} + +For inseccstr: Argument scope is [type_scope] inmod@{u} = Type@{u} : Type@{u+1} (* u |= *) @@ -155,24 +163,24 @@ inmod@{u} -> Type@{v} (* u v |= *) Applied.infunct is universe polymorphic -axfoo@{i Top.48 Top.49} : Type@{Top.48} -> Type@{i} -(* i Top.48 Top.49 |= *) +axfoo@{i Top.55 Top.56} : Type@{Top.55} -> Type@{i} +(* i Top.55 Top.56 |= *) axfoo is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo -axbar@{i Top.48 Top.49} : Type@{Top.49} -> Type@{i} -(* i Top.48 Top.49 |= *) +axbar@{i Top.55 Top.56} : Type@{Top.56} -> Type@{i} +(* i Top.55 Top.56 |= *) axbar is universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axbar -axfoo' : Type@{Top.51} -> Type@{axbar'.i} +axfoo' : Type@{Top.58} -> Type@{axbar'.i} axfoo' is not universe polymorphic Argument scope is [type_scope] Expands to: Constant Top.axfoo' -axbar' : Type@{Top.51} -> Type@{axbar'.i} +axbar' : Type@{Top.58} -> Type@{axbar'.i} axbar' is not universe polymorphic Argument scope is [type_scope] diff --git a/test-suite/output/UnivBinders.v b/test-suite/output/UnivBinders.v index f806a9f4f7..9aebce1b9a 100644 --- a/test-suite/output/UnivBinders.v +++ b/test-suite/output/UnivBinders.v @@ -122,8 +122,12 @@ Section SomeSec. Universe u. Definition insec@{v} := Type@{u} -> Type@{v}. Print insec. + + Inductive insecind@{k} := inseccstr : Type@{k} -> insecind. + Print insecind. End SomeSec. Print insec. +Print insecind. Module SomeMod. Definition inmod@{u} := Type@{u}. diff --git a/test-suite/output/ltac_missing_args.out b/test-suite/output/ltac_missing_args.out index 7326f137c2..8a00cd3fe5 100644 --- a/test-suite/output/ltac_missing_args.out +++ b/test-suite/output/ltac_missing_args.out @@ -1,25 +1,25 @@ The command has indeed failed with message: -The user-defined tactic "Top.foo" was not fully applied: +The user-defined tactic "foo" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "bar" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.bar" was not fully applied: +The user-defined tactic "bar" was not fully applied: There are missing arguments for variables y and _, an argument was provided for variable x. The command has indeed failed with message: -The user-defined tactic "Top.baz" was not fully applied: +The user-defined tactic "baz" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.qux" was not fully applied: +The user-defined tactic "qux" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.mydo" was not fully applied: +The user-defined tactic "mydo" was not fully applied: There is a missing argument for variable _, no arguments at all were provided. The command has indeed failed with message: @@ -31,7 +31,7 @@ An unnamed user-defined tactic was not fully applied: There is a missing argument for variable _, no arguments at all were provided. The command has indeed failed with message: -The user-defined tactic "Top.rec" was not fully applied: +The user-defined tactic "rec" was not fully applied: There is a missing argument for variable x, no arguments at all were provided. The command has indeed failed with message: diff --git a/test-suite/ssr/ssrpattern.v b/test-suite/ssr/ssrpattern.v new file mode 100644 index 0000000000..422bb95fdf --- /dev/null +++ b/test-suite/ssr/ssrpattern.v @@ -0,0 +1,7 @@ +Require Import ssrmatching. + +Goal forall n, match n with 0 => 0 | _ => 0 end = 0. +Proof. + intro n. + ssrpattern (match _ with 0 => _ | S n' => _ end). +Abort. diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v index 83fb3d0c8e..241d4eb200 100644 --- a/test-suite/success/attribute-syntax.v +++ b/test-suite/success/attribute-syntax.v @@ -1,4 +1,4 @@ -From Coq Require Program. +From Coq Require Program.Wf. Section Scope. @@ -21,3 +21,13 @@ Fixpoint f (n: nat) {wf lt n} : nat := _. #[deprecated(since="8.9.0")] Ltac foo := foo. + +Module M. + #[local] #[polymorphic] Definition zed := Type. + + #[local, polymorphic] Definition kats := Type. +End M. +Check M.zed@{_}. +Fail Check zed. +Check M.kats@{_}. +Fail Check kats. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index 4404ff3f16..448febed25 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -377,3 +377,30 @@ f y true. Abort. End LtacNames. + +(* Test binding of the name of existential variables in Ltac *) + +Module EvarNames. + +Ltac pick x := eexists ?[x]. +Goal exists y, y = 0. +pick foo. +[foo]:exact 0. +auto. +Qed. + +Ltac goal x := refine ?[x]. + +Goal forall n, n + 0 = n. +Proof. + induction n; [ goal Base | goal Rec ]. + [Base]: { + easy. + } + [Rec]: { + simpl. + now f_equal. + } +Qed. + +End EvarNames. diff --git a/theories/Bool/Bvector.v b/theories/Bool/Bvector.v index aecdb59dbe..3d615485b9 100644 --- a/theories/Bool/Bvector.v +++ b/theories/Bool/Bvector.v @@ -70,6 +70,8 @@ Definition BVor := @Vector.map2 _ _ _ orb. Definition BVxor := @Vector.map2 _ _ _ xorb. +Definition BVeq m n := @Vector.eqb bool eqb m n. + Definition BshiftL (n:nat) (bv:Bvector (S n)) (carry:bool) := Bcons carry n (Vector.shiftout bv). @@ -99,3 +101,13 @@ Fixpoint BshiftRa_iter (n:nat) (bv:Bvector (S n)) (p:nat) : Bvector (S n) := End BOOLEAN_VECTORS. +Module BvectorNotations. +Declare Scope Bvector_scope. +Delimit Scope Bvector_scope with Bvector. +Notation "^~ x" := (Bneg _ x) (at level 35, right associativity) : Bvector_scope. +Infix "^&" := (BVand _) (at level 40, left associativity) : Bvector_scope. +Infix "^⊕" := (BVxor _) (at level 45, left associativity) : Bvector_scope. +Infix "^|" := (BVor _) (at level 50, left associativity) : Bvector_scope. +Infix "=?" := (BVeq _ _) (at level 70, no associativity) : Bvector_scope. +Open Scope Bvector_scope. +End BvectorNotations. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index e33aa38173..3bf3925b4b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -543,7 +543,7 @@ let eqI ind l = and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff with Not_found -> user_err ~hdr:"AutoIndDecl.eqI" - (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed."); + (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed."); in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 650b28ea67..7dd5471f3f 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -83,11 +83,10 @@ GRAMMAR EXTEND Gram ] ; decorated_vernac: - [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) } - | fv = vernac -> { fv } ] - ] + [ [ a = LIST0 quoted_attributes ; fv = vernac -> + { let (f, v) = fv in (List.append (List.flatten a) f, v) } ] ] ; - attributes: + quoted_attributes: [ [ "#[" ; a = attribute_list ; "]" -> { a } ] ] ; diff --git a/vernac/himsg.ml b/vernac/himsg.ml index e7b2a0e8a6..71155d7921 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -896,7 +896,8 @@ let explain_not_match_error = function quote (Printer.safe_pr_lconstr_env env (Evd.from_env env) t2) | IncompatibleConstraints cst -> str " the expected (polymorphic) constraints do not imply " ++ - let cst = Univ.AUContext.instantiate (Univ.AUContext.instance cst) cst in + let cst = Univ.UContext.constraints (Univ.AUContext.repr cst) in + (** FIXME: provide a proper naming for the bound variables *) quote (Univ.pr_constraints (Termops.pr_evd_level Evd.empty) cst) let explain_signature_mismatch l spec why = diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index 13c8830b84..9cbaa8af9b 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -114,8 +114,8 @@ type hint_mode = Hints.hint_mode = [@@ocaml.deprecated "Please use [Hints.hint_mode]"] type 'a hint_info_gen = 'a Typeclasses.hint_info_gen = - { hint_priority : int option; - hint_pattern : 'a option } + { hint_priority : int option; [@ocaml.deprecated "Use Typeclasses.hint_priority"] + hint_pattern : 'a option [@ocaml.deprecated "Use Typeclasses.hint_pattern"] } [@@ocaml.deprecated "Please use [Typeclasses.hint_info_gen]"] type hint_info_expr = Hints.hint_info_expr @@ -151,7 +151,9 @@ type search_restriction = type rec_flag = bool (* true = Rec; false = NoRec *) type verbose_flag = bool (* true = Verbose; false = Silent *) -type opacity_flag = Proof_global.opacity_flag = Opaque | Transparent +type opacity_flag = Proof_global.opacity_flag = + Opaque [@ocaml.deprecated "Use Proof_global.Opaque"] + | Transparent [@ocaml.deprecated "Use Proof_global.Transparent"] [@ocaml.deprecated "Please use [Proof_global.opacity_flag]"] type coercion_flag = bool (* true = AddCoercion false = NoCoercion *) type instance_flag = bool option |