diff options
63 files changed, 236 insertions, 202 deletions
@@ -73,6 +73,7 @@ Vernacular Commands was removed. Use Local as a prefix instead. - For the Extraction Language command, "OCaml" is spelled correctly. The older "Ocaml" is still accepted, but deprecated. +- Using “Require” inside a section is deprecated. Universes @@ -86,6 +87,8 @@ Universes more information. - Fix #5726: Notations that start with `Type` now support universe instances with `@{u}`. +- `with Definition` now understands universe declarations + (like `@{u| Set < u}`). Checker @@ -110,6 +113,8 @@ Standard Library Coq.Numbers.DecimalString providing a type of decimal numbers, some facts about them, and conversions between decimal numbers and nat, positive, N, Z, and string. +- Added [Coq.Strings.String.concat] to concatenate a list of strings + inserting a separator between each item - Some deprecated aliases are now emitting warnings when used. diff --git a/Makefile.doc b/Makefile.doc index 894ef9a99..9fd93651d 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -387,10 +387,10 @@ install-doc-index-urls: OCAMLDOCDIR=dev/ocamldoc -DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \ - ./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \ - ./parsing/*.mli ./proofs/*.mli \ - ./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli) +DOCMLLIBS= $(CORECMA:.cma=_MLLIB_DEPENDENCIES) $(PLUGINSCMO:.cmo=_MLPACK_DEPENDENCIES) +DOCMLS=$(foreach lib,$(DOCMLLIBS),$(addsuffix .ml, $($(lib)))) + +DOCMLIS=$(wildcard $(addsuffix /*.mli, $(SRCDIRS))) # Defining options to generate dependencies graphs DOT=dot @@ -434,7 +434,12 @@ OCAMLDOC_MLLIBD = $(OCAMLFIND) ocamldoc -rectypes $(MLINCLUDES) $(ODOCDOTOPTS) - $(OCAMLDOC_MLLIBD) ml-doc: - $(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) -d $(OCAMLDOCDIR) $(MLSTATICFILES) + $(SHOW)'OCAMLDOC -html' + $(HIDE)mkdir -p $(OCAMLDOCDIR)/html/implementation + $(HIDE)$(OCAMLFIND) ocamldoc -charset utf-8 -html -rectypes -I +threads $(MLINCLUDES) $(COQIDEFLAGS) \ + $(DOCMLS) -d $(OCAMLDOCDIR)/html/implementation -colorize-code \ + -t "Coq mls documentation" \ + -css-style ../style.css parsing/parsing.dot : | parsing/parsing.mllib.d $(OCAMLDOC_MLLIBD) diff --git a/checker/univ.mli b/checker/univ.mli index 3876e7bbc..935f0a2b8 100644 --- a/checker/univ.mli +++ b/checker/univ.mli @@ -84,7 +84,7 @@ val check_eq : universe check_function val initial_universes : universes (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared diff --git a/clib/option.ml b/clib/option.ml index c2e2e7097..21913e8f7 100644 --- a/clib/option.ml +++ b/clib/option.ml @@ -44,7 +44,7 @@ let hash f = function exception IsNone (** [get x] returns [y] where [x] is [Some y]. - @raise [IsNone] if [x] equals [None]. *) + @raise IsNone if [x] equals [None]. *) let get = function | Some y -> y | _ -> raise IsNone diff --git a/doc/LICENSE b/doc/LICENSE index ada22e669..0aa0d629e 100644 --- a/doc/LICENSE +++ b/doc/LICENSE @@ -25,16 +25,6 @@ the PostScript, PDF and html outputs) are copyright (c) INRIA distributed under the terms of the Lesser General Public License version 2.1 or later. -The FAQ (Coq for the Clueless) is a work by Pierre Castéran, Hugo -Herbelin, Florent Kirchner, Benjamin Monate, and Julien Narboux. All -documents (the LaTeX source and the PostScript, PDF and html outputs) -are copyright (c) INRIA 2004-2006. The material connected to the FAQ -(Coq for the Clueless) may be distributed only subject to the terms -and conditions set forth in the Open Publication License, v1.0 or -later (the latest version is presently available at -http://www.opencontent.org/openpub/). Options A and B are *not* -elected. - The Tutorial on [Co-]Inductive Types in Coq is a work by Pierre Castéran and Eduardo Gimenez. All related documents (the LaTeX and BibTeX sources and the PostScript, PDF and html outputs) are copyright diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index c4c0435c5..0a4d0ef9a 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -1156,16 +1156,6 @@ without having to cut manually the proof in smaller lemmas. It may be useful to generate lemmas minimal w.r.t. the assumptions they depend on. This can be obtained thanks to the option below. -\begin{quote} -\optindex{Shrink Abstract} -{\tt Set Shrink Abstract} -\end{quote} -\emph{Deprecated since 8.7} - -When set (default), all lemmas generated through \texttt{abstract {\tacexpr}} -and \texttt{transparent\_abstract {\tacexpr}} are quantified only over the -variables that appear in the term constructed by \texttt{\tacexpr}. - \begin{Variants} \item \texttt{abstract {\tacexpr} using {\ident}}.\\ Give explicitly the name of the auxiliary lemma. diff --git a/engine/evd.mli b/engine/evd.mli index 55b8e3a83..ed3316c16 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -320,8 +320,8 @@ exception UniversesDiffer val add_universe_constraints : evar_map -> Universes.Constraints.t -> evar_map (** Add the given universe unification constraints to the evar map. - @raises UniversesDiffer in case a first-order unification fails. - @raises UniverseInconsistency + @raise UniversesDiffer in case a first-order unification fails. + @raise UniverseInconsistency . *) (** {5 Extra data} diff --git a/engine/proofview.ml b/engine/proofview.ml index 25c8e2d80..8a844bbf5 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -127,7 +127,7 @@ let focus_context (left,right) = (** This (internal) function extracts a sublist between two indices, and returns this sublist together with its context: if it returns - [(a,(b,c))] then [a] is the sublist and (rev b)@a@c is the + [(a,(b,c))] then [a] is the sublist and [(rev b) @ a @ c] is the original list. The focused list has lenght [j-i-1] and contains the goals from number [i] to number [j] (both included) the first goal of the list being numbered [1]. [focus_sublist i j l] raises @@ -572,8 +572,8 @@ let tclDISPATCHL tacs = tclDISPATCHGEN CList.rev tacs (** [extend_to_list startxs rx endxs l] builds a list - [startxs@[rx,...,rx]@endxs] of the same length as [l]. Raises - [SizeMismatch] if [startxs@endxs] is already longer than [l]. *) + [startxs @ [rx,...,rx] @ endxs] of the same length as [l]. Raises + [SizeMismatch] if [startxs @ endxs] is already longer than [l]. *) let extend_to_list startxs rx endxs l = (* spiwack: I use [l] essentially as a natural number *) let rec duplicate acc = function diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 84162ca89..918e12e5c 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1077,7 +1077,7 @@ type 'a raw_cases_pattern_expr_r = | RCPatAlias of 'a raw_cases_pattern_expr * Misctypes.lname | RCPatCstr of Globnames.global_reference * 'a raw_cases_pattern_expr list * 'a raw_cases_pattern_expr list - (** [RCPatCstr (loc, c, l1, l2)] represents ((@c l1) l2) *) + (** [RCPatCstr (loc, c, l1, l2)] represents [((@ c l1) l2)] *) | RCPatAtom of (Misctypes.lident * (Notation_term.tmp_scope_name option * Notation_term.scope_name list)) option | RCPatOr of 'a raw_cases_pattern_expr list and 'a raw_cases_pattern_expr = ('a raw_cases_pattern_expr_r, 'a) DAst.t diff --git a/interp/modintern.ml b/interp/modintern.ml index 92264fb72..887685585 100644 --- a/interp/modintern.ml +++ b/interp/modintern.ml @@ -62,18 +62,19 @@ let lookup_module lqid = fst (lookup_module_or_modtype Module lqid) let transl_with_decl env = function | CWith_Module ((_,fqid),qid) -> WithMod (fqid,lookup_module qid), Univ.ContextSet.empty - | CWith_Definition ((_,fqid),c) -> - let sigma = Evd.from_env env in + | CWith_Definition ((_,fqid),udecl,c) -> + let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in let c, ectx = interp_constr env sigma c in - if Flags.is_universe_polymorphism () then - let ctx = UState.context ectx in - let inst, ctx = Univ.abstract_universes ctx in - let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in - let c = EConstr.to_constr sigma c in - WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty - else - let c = EConstr.to_constr sigma c in - WithDef (fqid,(c, None)), UState.context_set ectx + begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with + | Entries.Polymorphic_const_entry ctx -> + let inst, ctx = Univ.abstract_universes ctx in + let c = EConstr.Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in + let c = EConstr.to_constr sigma c in + WithDef (fqid,(c, Some ctx)), Univ.ContextSet.empty + | Entries.Monomorphic_const_entry ctx -> + let c = EConstr.to_constr sigma c in + WithDef (fqid,(c, None)), ctx + end let loc_of_module l = l.CAst.loc diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml index 474b80ec4..31f811bc8 100644 --- a/intf/constrexpr.ml +++ b/intf/constrexpr.ml @@ -17,6 +17,11 @@ open Decl_kinds (** [constr_expr] is the abstract syntax tree produced by the parser *) +type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl + +type ident_decl = lident * universe_decl_expr option +type name_decl = lname * universe_decl_expr option + type notation = string type explicitation = @@ -51,7 +56,7 @@ type cases_pattern_expr_r = | CPatAlias of cases_pattern_expr * lname | CPatCstr of reference * cases_pattern_expr list option * cases_pattern_expr list - (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *) + (** [CPatCstr (_, c, Some l1, l2)] represents [(@ c l1) l2] *) | CPatAtom of reference option | CPatOr of cases_pattern_expr list | CPatNotation of notation * cases_pattern_notation_substitution @@ -121,7 +126,7 @@ and recursion_order_expr = | CWfRec of constr_expr | CMeasureRec of constr_expr * constr_expr option (** measure, relation *) -(** Anonymous defs allowed ?? *) +(* Anonymous defs allowed ?? *) and local_binder_expr = | CLocalAssum of lname list * binder_kind * constr_expr | CLocalDef of lname * constr_expr * constr_expr option @@ -139,7 +144,7 @@ type constr_pattern_expr = constr_expr type with_declaration_ast = | CWith_Module of Id.t list Loc.located * qualid Loc.located - | CWith_Definition of Id.t list Loc.located * constr_expr + | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr type module_ast_r = | CMident of qualid diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 7e9bc8caa..0a6e5b3b3 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -160,11 +160,6 @@ type option_ref_value = (** Identifier and optional list of bound universes and constraints. *) -type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl - -type ident_decl = lident * universe_decl_expr option -type name_decl = lname * universe_decl_expr option - type sort_expr = Sorts.family type definition_expr = @@ -536,3 +531,14 @@ type vernac_when = | VtNow | VtLater type vernac_classification = vernac_type * vernac_when + + +(** Deprecated stuff *) +type universe_decl_expr = Constrexpr.universe_decl_expr +[@@ocaml.deprecated "alias of Constrexpr.universe_decl_expr"] + +type ident_decl = Constrexpr.ident_decl +[@@ocaml.deprecated "alias of Constrexpr.ident_decl"] + +type name_decl = Constrexpr.name_decl +[@@ocaml.deprecated "alias of Constrexpr.name_decl"] diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index c5a8c7b23..11faef02c 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -798,7 +798,7 @@ let drop_parameters depth n argstk = s. @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 71453a04b..b9c71d72a 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -216,7 +216,7 @@ val whd_stack : s. @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> diff --git a/kernel/environ.mli b/kernel/environ.mli index 51388b8f3..4e6ac1e72 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -201,7 +201,7 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) (** Add universe constraints to the environment. - @raises UniverseInconsistency + @raise UniverseInconsistency . *) val add_constraints : Univ.Constraint.t -> env -> env diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index 97745771e..d4fba63fb 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -43,7 +43,7 @@ val check_constraint : t -> univ_constraint -> bool val check_constraints : Constraint.t -> t -> bool (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared diff --git a/lib/lib.mllib b/lib/lib.mllib index b2260ba09..089185942 100644 --- a/lib/lib.mllib +++ b/lib/lib.mllib @@ -15,7 +15,6 @@ CWarnings Rtree System Explore -RTree CProfile Future Spawn diff --git a/library/summary.ml b/library/summary.ml index 6ca871555..7ef19fbfb 100644 --- a/library/summary.ml +++ b/library/summary.ml @@ -89,6 +89,16 @@ let unfreeze_single name state = Pp.(seq [str "Error unfreezing summary "; str name; fnl (); CErrors.iprint e]); iraise e +let warn_summary_out_of_scope = + let name = "summary-out-of-scope" in + let category = "dev" in + let default = CWarnings.Disabled in + CWarnings.create ~name ~category ~default (fun name -> + Pp.str (Printf.sprintf + "A Coq plugin was loaded inside a local scope (such as a Section). It is recommended to load plugins at the start of the file. Summary entry: %s" + name) + ) + let unfreeze_summaries ?(partial=false) { summaries; ml_module } = (* The unfreezing of [ml_modules_summary] has to be anticipated since it * may modify the content of [summaries] by loading new ML modules *) @@ -101,7 +111,7 @@ let unfreeze_summaries ?(partial=false) { summaries; ml_module } = try decl.unfreeze_function String.Map.(find name summaries) with Not_found -> if not partial then begin - Feedback.msg_warning Pp.(str "Summary was captured out of module scope for entry " ++ str name); + warn_summary_out_of_scope name; decl.init_function () end; in diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 595a60f33..feaef3161 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -12,10 +12,10 @@ open Pp open CErrors open Util open Names +open Vernacexpr open Constrexpr open Constrexpr_ops open Extend -open Vernacexpr open Decl_kinds open Declarations open Misctypes @@ -142,7 +142,7 @@ let name_of_ident_decl : ident_decl -> name_decl = (* Gallina declarations *) GEXTEND Gram GLOBAL: gallina gallina_ext thm_token def_body of_type_with_opt_coercion - record_field decl_notation rec_definition ident_decl; + record_field decl_notation rec_definition ident_decl univ_decl; gallina: (* Definition, Theorem, Variable, Axiom, ... *) @@ -557,8 +557,8 @@ GEXTEND Gram [ [ qid = qualid -> CAst.make ~loc:!@loc @@ CMident (snd qid) | "("; me = module_expr; ")" -> me ] ] ; with_declaration: - [ [ "Definition"; fqid = fullyqualid; ":="; c = Constr.lconstr -> - CWith_Definition (fqid,c) + [ [ "Definition"; fqid = fullyqualid; udecl = OPT univ_decl; ":="; c = Constr.lconstr -> + CWith_Definition (fqid,udecl,c) | IDENT "Module"; fqid = fullyqualid; ":="; qid = qualid -> CWith_Module (fqid,qid) ] ] diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 9aae251f1..258c4bb11 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -442,6 +442,7 @@ module Prim = let name = Gram.entry_create "Prim.name" let identref = Gram.entry_create "Prim.identref" + let univ_decl = Gram.entry_create "Prim.univ_decl" let ident_decl = Gram.entry_create "Prim.ident_decl" let pattern_ident = Gram.entry_create "pattern_ident" let pattern_identref = Gram.entry_create "pattern_identref" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 8592968dc..e66aa4ade 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -198,6 +198,7 @@ module Prim : val ident : Id.t Gram.entry val name : lname Gram.entry val identref : lident Gram.entry + val univ_decl : universe_decl_expr Gram.entry val ident_decl : ident_decl Gram.entry val pattern_ident : Id.t Gram.entry val pattern_identref : lident Gram.entry diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v index 264b48a08..c403f7c5a 100644 --- a/plugins/extraction/ExtrOcamlNatBigInt.v +++ b/plugins/extraction/ExtrOcamlNatBigInt.v @@ -46,7 +46,7 @@ Extract Constant EqNat.eq_nat_decide => "Big.eq". Extract Constant Peano_dec.eq_nat_dec => "Big.eq". -Extract Constant Compare_dec.nat_compare => +Extract Constant Nat.compare => "Big.compare_case Eq Lt Gt". Extract Constant Compare_dec.leb => "Big.le". diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v index 35af71417..a2f809a0c 100644 --- a/plugins/extraction/ExtrOcamlNatInt.v +++ b/plugins/extraction/ExtrOcamlNatInt.v @@ -59,7 +59,7 @@ Extract Inlined Constant EqNat.eq_nat_decide => "(=)". Extract Inlined Constant Peano_dec.eq_nat_dec => "(=)". -Extract Constant Compare_dec.nat_compare => +Extract Constant Nat.compare => "fun n m -> if n=m then Eq else if n<m then Lt else Gt". Extract Inlined Constant Compare_dec.leb => "(<=)". Extract Inlined Constant Compare_dec.le_lt_dec => "(<=)". diff --git a/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v index 543a37ff8..f066ea462 100644 --- a/plugins/micromega/RingMicromega.v +++ b/plugins/micromega/RingMicromega.v @@ -21,6 +21,7 @@ Require Import List. Require Import Bool. Require Import OrderedRing. Require Import Refl. +Require Coq.micromega.Tauto. Set Implicit Arguments. @@ -796,7 +797,7 @@ Definition xnormalise (t:Formula C) : list (NFormula) := | OpLe => (psub lhs rhs ,Strict) :: nil end. -Require Import Coq.micromega.Tauto. +Import Coq.micromega.Tauto. Definition cnf_normalise (t:Formula C) : cnf (NFormula) := List.map (fun x => x::nil) (xnormalise t). diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 85e2a5b23..c5a09d677 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -30,6 +30,7 @@ Require Export Ncring_initial. Require Export Ncring_tac. Require Export Integral_domain. Require Import DiscrR. +Require Import ZArith. Declare ML Module "nsatz_plugin". @@ -56,9 +57,8 @@ simpl. simpl; cring. Qed. (* adpatation du code de Benjamin aux setoides *) -Require Import ZArith. -Require Export Ring_polynom. -Require Export InitialRing. +Export Ring_polynom. +Export InitialRing. Definition PolZ := Pol Z. Definition PEZ := PExpr Z. diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v index db17c0d65..19b3ab397 100644 --- a/plugins/rtauto/Rtauto.v +++ b/plugins/rtauto/Rtauto.v @@ -11,7 +11,7 @@ Require Export List. Require Export Bintree. -Require Import Bool. +Require Import Bool BinPos. Declare ML Module "rtauto_plugin". @@ -98,8 +98,6 @@ match F with | F_push H hyps0 F0 => interp_ctx hyps0 F0 ([[H]] -> G) end. -Require Export BinPos. - Ltac wipe := intros;simpl;constructor. Lemma compose0 : diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 5163ec7b3..43c29a08a 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -460,7 +460,7 @@ let red_product_skip_id env sigma c = match EConstr.kind sigma c with let ssrevaltac ist gtac = Tacinterp.tactic_of_value ist gtac -(** Open term to lambda-term coercion {{{ ************************************) +(** Open term to lambda-term coercion *)(* {{{ ************************************) (* This operation takes a goal gl and an open term (sigma, t), and *) (* returns a term t' where all the new evars in sigma are abstracted *) @@ -768,7 +768,7 @@ let discharge_hyp (id', (id, mode)) gl = let cl' = Vars.subst_var id (pf_concl gl) in match pf_get_hyp gl id, mode with | NamedDecl.LocalAssum (_, t), _ | NamedDecl.LocalDef (_, _, t), "(" -> - Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false (EConstr.of_constr (mkProd (Name id', t, cl'))) + Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true (EConstr.of_constr (mkProd (Name id', t, cl'))) [EConstr.of_constr (mkVar id)]) gl | NamedDecl.LocalDef (_, v, t), _ -> Proofview.V82.of_tactic @@ -1000,7 +1000,7 @@ let refine_with ?(first_goes_last=false) ?beta ?(with_evars=true) oc gl = try applyn ~with_evars ~with_shelve:true ?beta n (EConstr.of_constr oc) gl with e when CErrors.noncritical e -> raise dependent_apply_error -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; @@ -1128,7 +1128,7 @@ let interp_clr sigma = function (** Basic tacticals *) -(** Multipliers {{{ ***********************************************************) +(** Multipliers *)(* {{{ ***********************************************************) (* tactical *) @@ -1168,7 +1168,7 @@ let tclMULT = function let old_cleartac clr = check_hyps_uniq [] clr; Proofview.V82.of_tactic (Tactics.clear (hyps_ids clr)) let cleartac clr = check_hyps_uniq [] clr; Tactics.clear (hyps_ids clr) -(** }}} *) +(* }}} *) (** Generalize tactic *) @@ -1199,7 +1199,7 @@ let pf_interp_gen_aux gl to_ind ((oclr, occ), t) = false, pat, EConstr.mkProd (constr_name (project gl) c, pty, Tacmach.pf_concl gl), p, clr,ucst,gl else CErrors.user_err ?loc:(loc_of_cpattern t) (str "generalized term didn't match") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) +let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:true x xs) let genclrtac cl cs clr = let tclmyORELSE tac1 tac2 gl = diff --git a/plugins/ssr/ssrcommon.mli b/plugins/ssr/ssrcommon.mli index 7c16e1ba9..2b8f1d540 100644 --- a/plugins/ssr/ssrcommon.mli +++ b/plugins/ssr/ssrcommon.mli @@ -414,6 +414,8 @@ val clr_of_wgen : val unfold : EConstr.t list -> unit Proofview.tactic +val apply_type : EConstr.types -> EConstr.t list -> Proofview.V82.tac + (* New code ****************************************************************) (* To call old code *) diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 33ebe26b6..717657a24 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -30,8 +30,6 @@ module RelDecl = Context.Rel.Declaration (** The "case" and "elim" tactic *) -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - (* TASSI: given the type of an elimination principle, it finds the higher order * argument (index), it computes it's arity and the arity of the eliminator and * checks if the eliminator is recursive or not *) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index 00c971237..859513d5c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -372,8 +372,6 @@ let is_construct_ref sigma c r = EConstr.isConstruct sigma c && eq_gr (ConstructRef (fst(EConstr.destConstruct sigma c))) r let is_ind_ref sigma c r = EConstr.isInd sigma c && eq_gr (IndRef (fst(EConstr.destInd sigma c))) r -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - let rwcltac cl rdx dir sr gl = let n, r_n,_, ucst = pf_abs_evars gl sr in let r_n' = pf_abs_cterm gl n r_n in diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v index 96b6ed295..ac2c78249 100644 --- a/plugins/ssr/ssrfun.v +++ b/plugins/ssr/ssrfun.v @@ -165,7 +165,7 @@ Require Import ssreflect. (* rev_right_loop inv op <-> op, inv obey the inverse loop reverse right *) (* axiom: (x op y) op (inv y) = x for all x, y. *) (* Note that familiar "cancellation" identities like x + y - y = x or *) -(* x - y + x = x are respectively instances of right_loop and rev_right_loop *) +(* x - y + y = x are respectively instances of right_loop and rev_right_loop *) (* The corresponding lemmas will use the K and NK/VK suffixes, respectively. *) (* *) (* - Morphisms for functions and relations: *) @@ -639,6 +639,9 @@ End Injections. Lemma Some_inj {T} : injective (@Some T). Proof. by move=> x y []. Qed. +(* Force implicits to use as a view. *) +Prenex Implicits Some_inj. + (* cancellation lemmas for dependent type casts. *) Lemma esymK T x y : cancel (@esym T x y) (@esym T y x). Proof. by case: y /. Qed. diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4 index 70f73c1fe..2bed8b624 100644 --- a/plugins/ssr/ssrparser.ml4 +++ b/plugins/ssr/ssrparser.ml4 @@ -952,7 +952,7 @@ let pr_ssrhint _ _ = pr_hint ARGUMENT EXTEND ssrhint TYPED AS ssrhintarg PRINTED BY pr_ssrhint | [ ] -> [ nohint ] END -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) (* We can't make "in" into a general tactical because this would create a *) (* crippling conflict with the ltac let .. in construct. Hence, we add *) @@ -1438,7 +1438,7 @@ let tactic_expr = Pltac.tactic_expr let old_tac = V82.tactic -(** Name generation {{{ *******************************************************) +(** Name generation *)(* {{{ *******************************************************) (* Since Coq now does repeated internal checks of its external lexical *) (* rules, we now need to carve ssreflect reserved identifiers out of *) @@ -1490,7 +1490,7 @@ let _ = add_internal_name (is_tagged perm_tag) (* We must not anonymize context names discharged by the "in" tactical. *) -(** Tactical extensions. {{{ **************************************************) +(** Tactical extensions. *)(* {{{ **************************************************) (* The TACTIC EXTEND facility can't be used for defining new user *) (* tacticals, because: *) diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index 21ad6e6ce..9cc4f5cec 100644 --- a/plugins/ssr/ssrtacticals.ml +++ b/plugins/ssr/ssrtacticals.ml @@ -59,7 +59,7 @@ let tclSEQAT ist atac1 dir (ivar, ((_, atacs2), atac3)) = | L2R, pad, tacs2 -> Tacticals.tclTHENSFIRSTn tac1 (Array.of_list (pad @ tacs2)) tac3 | R2L, pad, tacs2 -> Tacticals.tclTHENSLASTn tac1 tac3 (Array.of_list (tacs2 @ pad)) -(** The "in" pseudo-tactical {{{ **********************************************) +(** The "in" pseudo-tactical *)(* {{{ **********************************************) let hidden_goal_tag = "the_hidden_goal" @@ -127,8 +127,6 @@ let endclausestac id_map clseq gl_id cl0 gl = if List.for_all not_hyp' all_ids && not c_hidden then mktac [] gl else errorstrm Pp.(str "tampering with discharged assumptions of \"in\" tactical") -let apply_type x xs = Proofview.V82.of_tactic (Tactics.apply_type ~typecheck:false x xs) - let tclCLAUSES tac (gens, clseq) gl = if clseq = InGoal || clseq = InSeqGoal then tac gl else let clr_gens = pf_clauseids gl gens clseq in diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index f37452613..e3941c1c5 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -49,7 +49,7 @@ let frozen_lexer = CLexer.get_keyword_state () ;; (* global syntactic changes and vernacular commands *) -(** Alternative notations for "match" and anonymous arguments. {{{ ************) +(** Alternative notations for "match" and anonymous arguments. *)(* {{{ ************) (* Syntax: *) (* if <term> is <pattern> then ... else ... *) @@ -127,7 +127,7 @@ GEXTEND Gram END (* }}} *) -(** Vernacular commands: Prenex Implicits and Search {{{ **********************) +(** Vernacular commands: Prenex Implicits and Search *)(* {{{ **********************) (* This should really be implemented as an extension to the implicit *) (* arguments feature, but unfortuately that API is sealed. The current *) @@ -461,7 +461,7 @@ END (* }}} *) -(** View hint database and View application. {{{ ******************************) +(** View hint database and View application. *)(* {{{ ******************************) (* There are three databases of lemmas used to mediate the application *) (* of reflection lemmas: one for forward chaining, one for backward *) diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index 1f1a63dac..62c35d6df 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -70,7 +70,7 @@ let _ = Goptions.optwrite = debug } let pp s = !pp_ref s -(** Utils {{{ *****************************************************************) +(** Utils *)(* {{{ *****************************************************************) let env_size env = List.length (Environ.named_context env) let safeDestApp c = match kind c with App (f, a) -> f, a | _ -> c, [| |] @@ -179,7 +179,7 @@ let nf_evar sigma c = (* }}} *) -(** Profiling {{{ *************************************************************) +(** Profiling *)(* {{{ *************************************************************) type profiler = { profile : 'a 'b. ('a -> 'b) -> 'a -> 'b; reset : unit -> unit; diff --git a/plugins/ssrmatching/ssrmatching.mli b/plugins/ssrmatching/ssrmatching.mli index cd5676f28..07d0f9757 100644 --- a/plugins/ssrmatching/ssrmatching.mli +++ b/plugins/ssrmatching/ssrmatching.mli @@ -74,7 +74,7 @@ val interp_cpattern : pattern (** The set of occurrences to be matched. The boolean is set to true - * to signal the complement of this set (i.e. {-1 3}) *) + * to signal the complement of this set (i.e. \{-1 3\}) *) type occ = (bool * int list) option (** [subst e p t i]. [i] is the number of binders diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 16d75685d..3b56513f5 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -278,7 +278,7 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con (** [infer_conv] Adds necessary universe constraints to the evar map. pb defaults to CUMUL and ts to a full transparent state. - @raises UniverseInconsistency iff catch_incon is set to false, + @raise UniverseInconsistency iff catch_incon is set to false, otherwise returns false in that case. *) val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli index 242eb802f..305d045b1 100644 --- a/pretyping/univdecls.mli +++ b/pretyping/univdecls.mli @@ -14,8 +14,8 @@ type universe_decl = val default_univ_decl : universe_decl -val interp_univ_decl : Environ.env -> Vernacexpr.universe_decl_expr -> +val interp_univ_decl : Environ.env -> Constrexpr.universe_decl_expr -> Evd.evar_map * universe_decl -val interp_univ_decl_opt : Environ.env -> Vernacexpr.universe_decl_expr option -> +val interp_univ_decl_opt : Environ.env -> Constrexpr.universe_decl_expr option -> Evd.evar_map * universe_decl diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 8551d040d..2b7d643d6 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -233,9 +233,9 @@ open Decl_kinds hov 2 (keyword "Hint "++ pph ++ opth) let pr_with_declaration pr_c = function - | CWith_Definition (id,c) -> + | CWith_Definition (id,udecl,c) -> let p = pr_c c in - keyword "Definition" ++ spc() ++ pr_lfqid id ++ str" := " ++ p + keyword "Definition" ++ spc() ++ pr_lfqid id ++ pr_universe_decl udecl ++ str" := " ++ p | CWith_Module (id,qid) -> keyword "Module" ++ spc() ++ pr_lfqid id ++ str" := " ++ pr_located pr_qualid qid diff --git a/tactics/auto.ml b/tactics/auto.ml index 3eea1a74f..0c0d9bcfc 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -42,9 +42,9 @@ let compute_secvars gl = open Unification -let auto_core_unif_flags_of st1 st2 useeager = { +let auto_core_unif_flags_of st1 st2 = { modulo_conv_on_closed_terms = Some st1; - use_metas_eagerly_in_conv_on_closed_terms = useeager; + use_metas_eagerly_in_conv_on_closed_terms = false; use_evars_eagerly_in_conv_on_closed_terms = false; modulo_delta = st2; modulo_delta_types = full_transparent_state; @@ -57,8 +57,8 @@ let auto_core_unif_flags_of st1 st2 useeager = { modulo_eta = true; } -let auto_unif_flags_of st1 st2 useeager = - let flags = auto_core_unif_flags_of st1 st2 useeager in { +let auto_unif_flags_of st1 st2 = + let flags = auto_core_unif_flags_of st1 st2 in { core_unify_flags = flags; merge_unify_flags = flags; subterm_unify_flags = { flags with modulo_delta = empty_transparent_state }; @@ -67,7 +67,7 @@ let auto_unif_flags_of st1 st2 useeager = } let auto_unif_flags = - auto_unif_flags_of full_transparent_state empty_transparent_state false + auto_unif_flags_of full_transparent_state empty_transparent_state (* Try unification with the precompiled clause, then use registered Apply *) @@ -291,10 +291,10 @@ let tclTRY_dbg d tac = de Hint impérative a été remplacée par plusieurs bases fonctionnelles *) let flags_of_state st = - auto_unif_flags_of st st false + auto_unif_flags_of st st let auto_flags_of_state st = - auto_unif_flags_of full_transparent_state st false + auto_unif_flags_of full_transparent_state st let hintmap_of sigma secvars hdc concl = match hdc with diff --git a/tactics/equality.ml b/tactics/equality.ml index 236db1dcc..98f627f21 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -56,18 +56,7 @@ type inj_flags = { injection_pattern_l2r_order : bool; } -let discriminate_introduction = ref true - -let discr_do_intro () = !discriminate_introduction - open Goptions -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "automatic introduction of hypotheses by discriminate"; - optkey = ["Discriminate";"Introduction"]; - optread = (fun () -> !discriminate_introduction); - optwrite = (:=) discriminate_introduction } let use_injection_pattern_l2r_order = function | None -> true @@ -1080,13 +1069,10 @@ let discrClause with_evars = onClause (discrSimpleClause with_evars) let discrEverywhere with_evars = tclTHEN (Proofview.tclUNIT ()) (* Delay the interpretation of side-effect *) - (if discr_do_intro () then - (tclTHEN - (tclREPEAT introf) - (tryAllHyps + (tclTHEN + (tclREPEAT introf) + (tryAllHyps (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings))))) - else (* <= 8.2 compat *) - tryAllHypsAndConcl (discrSimpleClause with_evars)) let discr_tac with_evars = function | None -> discrEverywhere with_evars diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index a59046a67..b012a7ecd 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -511,10 +511,10 @@ let coq_eqdec ~sum ~rev = mkPattern (mkGAppRef sum args) ) -(** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *) +(** [{ ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 }] *) let coq_eqdec_inf_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:false -(** { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } *) +(** [{ ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 }] *) let coq_eqdec_inf_rev_pattern = coq_eqdec ~sum:coq_sumbool_ref ~rev:true (** %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index b99a45103..b41df7f75 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -89,18 +89,6 @@ let _ = optread = (fun () -> !universal_lemma_under_conjunctions) ; optwrite = (fun b -> universal_lemma_under_conjunctions := b) } -(* Shrinking of abstract proofs. *) - -let shrink_abstract = ref true - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "shrinking of abstracted proofs"; - optkey = ["Shrink"; "Abstract"]; - optread = (fun () -> !shrink_abstract) ; - optwrite = (fun b -> shrink_abstract := b) } - (* The following boolean governs what "intros []" do on examples such as "forall x:nat*nat, x=x"; if true, it behaves as "intros [? ?]"; if false, it behaves as "intro H; case H; clear H" for fresh H. @@ -4986,10 +4974,7 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let (_, info) = CErrors.push src in iraise (e, info) in - let const, args = - if !shrink_abstract then shrink_entry sign const - else (const, List.rev (Context.Named.to_instance Constr.mkVar sign)) - in + let const, args = shrink_entry sign const in let args = List.map EConstr.of_constr args in let cd = Entries.DefinitionEntry { const with Entries.const_entry_opaque = opaque } in let decl = (cd, if opaque then IsProof Lemma else IsDefinition Definition) in diff --git a/test-suite/bugs/closed/2245.v b/test-suite/bugs/closed/2245.v new file mode 100644 index 000000000..f0162f3b2 --- /dev/null +++ b/test-suite/bugs/closed/2245.v @@ -0,0 +1,11 @@ +Module Type Test. + +Section Sec. +Variables (A:Type). +Context (B:Type). +End Sec. + +Fail Check B. (* used to be found !!! *) +Fail Check A. + +End Test. diff --git a/test-suite/bugs/closed/6634.v b/test-suite/bugs/closed/6634.v new file mode 100644 index 000000000..7f33afcc2 --- /dev/null +++ b/test-suite/bugs/closed/6634.v @@ -0,0 +1,6 @@ +From Coq Require Import ssreflect. + +Lemma normalizeP (p : tt = tt) : p = p. +Proof. +Fail move: {2} tt p. +Abort. diff --git a/test-suite/bugs/closed/6910.v b/test-suite/bugs/closed/6910.v new file mode 100644 index 000000000..5167a5364 --- /dev/null +++ b/test-suite/bugs/closed/6910.v @@ -0,0 +1,5 @@ +From Coq Require Import ssreflect ssrfun. + +(* We should be able to use Some_inj as a view: *) +Lemma foo (x y : nat) : Some x = Some y -> x = y. +Proof. by move/Some_inj. Qed. diff --git a/test-suite/modules/WithDefUBinders.v b/test-suite/modules/WithDefUBinders.v new file mode 100644 index 000000000..e68345516 --- /dev/null +++ b/test-suite/modules/WithDefUBinders.v @@ -0,0 +1,15 @@ + +Set Universe Polymorphism. +Module Type T. + Axiom foo@{u v|u < v} : Type@{v}. +End T. + +Module M : T with Definition foo@{u v} := Type@{u} : Type@{v}. + Definition foo@{u v} := Type@{u} : Type@{v}. +End M. + +Fail Module M' : T with Definition foo := Type. + +(* Without the binder expression we have to do trickery to get the + universes in the right order. *) +Module M' : T with Definition foo := let t := Type in t. diff --git a/test-suite/success/shrink_abstract.v b/test-suite/success/shrink_abstract.v index 3f6b9cb39..916bb846a 100644 --- a/test-suite/success/shrink_abstract.v +++ b/test-suite/success/shrink_abstract.v @@ -1,5 +1,3 @@ -Set Shrink Abstract. - Definition foo : forall (n m : nat), bool. Proof. pose (p := 0). diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 9fd52866e..238ac7df0 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -28,6 +28,8 @@ intentional type theory, Journal of Symbolic Logic 70(2):488-514, 2005. [[Werner97]] Benjamin Werner, Sets in Types, Types in Sets, TACS, 1997. *) +Require Import RelationClasses Logic. + Set Implicit Arguments. Local Unset Intuition Negation Unfolding. @@ -125,8 +127,6 @@ Definition DependentFunctionalRelReification_on (A:Type) (B:A -> Type) := formulation of choice); Note also a typo in its intended formulation in [[Werner97]]. *) -Require Import RelationClasses Logic. - Definition RepresentativeFunctionalChoice_on := forall R:A->A->Prop, (Equivalence R) -> diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v index a50140628..a79ddead2 100644 --- a/theories/Sets/Multiset.v +++ b/theories/Sets/Multiset.v @@ -11,6 +11,7 @@ (* G. Huet 1-9-95 *) Require Import Permut Setoid. +Require Plus. (* comm. and ass. of plus *) Set Implicit Arguments. @@ -69,9 +70,6 @@ Section multiset_defs. unfold meq; unfold munion; simpl; auto. Qed. - - Require Plus. (* comm. and ass. of plus *) - Lemma munion_comm : forall x y:multiset, meq (munion x y) (munion y x). Proof. unfold meq; unfold multiplicity; unfold munion. diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v index 95ba93232..7940bda1a 100644 --- a/theories/Sets/Uniset.v +++ b/theories/Sets/Uniset.v @@ -13,7 +13,7 @@ (* G. Huet 1-9-95 *) (* Updated Papageno 12/98 *) -Require Import Bool. +Require Import Bool Permut. Set Implicit Arguments. @@ -140,8 +140,6 @@ Hint Resolve seq_right. (** Here we should make uniset an abstract datatype, by hiding [Charac], [union], [charac]; all further properties are proved abstractly *) -Require Import Permut. - Lemma union_rotate : forall x y z:uniset, seq (union x (union y z)) (union z (union x y)). Proof. diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v index 8f583be97..d9e5ad676 100644 --- a/theories/Sorting/Heap.v +++ b/theories/Sorting/Heap.v @@ -136,7 +136,7 @@ Section defs. (munion (list_contents _ eqA_dec l1) (list_contents _ eqA_dec l2)) -> (forall a, HdRel leA a l1 -> HdRel leA a l2 -> HdRel leA a l) -> merge_lem l1 l2. - Require Import Morphisms. + Import Morphisms. Instance: Equivalence (@meq A). Proof. constructor; auto with datatypes. red. apply meq_trans. Defined. diff --git a/theories/Strings/String.v b/theories/Strings/String.v index a302b8329..2be6618ad 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -165,6 +165,18 @@ intros n0 H; apply Rec; simpl; auto. apply Le.le_S_n; auto. Qed. +(** *** Concatenating lists of strings *) + +(** [concat sep sl] concatenates the list of strings [sl], inserting + the separator string [sep] between each. *) + +Fixpoint concat (sep : string) (ls : list string) := + match ls with + | nil => EmptyString + | cons x nil => x + | cons x xs => x ++ sep ++ concat sep xs + end. + (** *** Test functions *) (** Test if [s1] is a prefix of [s2] *) diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 1da46e8ce..a103cfe7f 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -341,6 +341,22 @@ let loop_flush_all () = Format.pp_print_flush !Topfmt.std_ft (); Format.pp_print_flush !Topfmt.err_ft () +let pr_open_cur_subgoals () = + try + let proof = Proof_global.give_me_the_proof () in + Printer.pr_open_subgoals ~proof + with Proof_global.NoCurrentProof -> Pp.str "" + +(* Goal equality heuristic. *) +let pequal cmp1 cmp2 (a1,a2) (b1,b2) = cmp1 a1 b1 && cmp2 a2 b2 +let evleq e1 e2 = CList.equal Evar.equal e1 e2 +let cproof p1 p2 = + let (a1,a2,a3,a4,_),(b1,b2,b3,b4,_) = Proof.proof p1, Proof.proof p2 in + evleq a1 b1 && + CList.equal (pequal evleq evleq) a2 b2 && + CList.equal Evar.equal a3 b3 && + CList.equal Evar.equal a4 b4 + let drop_last_doc = ref None let rec loop ~time ~state = @@ -351,6 +367,10 @@ let rec loop ~time ~state = (* Be careful to keep this loop tail-recursive *) let rec vernac_loop ~state = let nstate = do_vernac ~time ~state in + let proof_changed = not (Option.equal cproof nstate.proof state.proof) in + let print_goals = not !Flags.quiet && + proof_changed && Proof_global.there_are_pending_proofs () in + if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); loop_flush_all (); vernac_loop ~state:nstate (* We recover the current stateid, threading from the caller is diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7c889500a..56bdcc7e5 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -70,12 +70,6 @@ let print_cmd_header ?loc com = Pp.pp_with !Topfmt.std_ft (pp_cmd_header ?loc com); Format.pp_print_flush !Topfmt.std_ft () -let pr_open_cur_subgoals () = - try - let proof = Proof_global.give_me_the_proof () in - Printer.pr_open_subgoals ~proof - with Proof_global.NoCurrentProof -> Pp.str "" - (* Reenable when we get back to feedback printing *) (* let is_end_of_input any = match any with *) (* Stm.End_of_input -> true *) @@ -94,23 +88,8 @@ end let interp_vernac ~time ~check ~interactive ~state (loc,com) = let open State in try - (* XXX: We need to run this before add as the classification is - highly dynamic and depends on the structure of the - document. Hopefully this is fixed when VtMeta can be removed - and Undo etc... are just interpreted regularly. *) - - (* XXX: The classifier can emit warnings so we need to guard - against that... *) - let wflags = CWarnings.get_flags () in - CWarnings.set_flags "none"; - let is_proof_step = match fst (Vernac_classifier.classify_vernac com) with - | VtProofStep _ | VtMeta | VtStartProof _ -> true - | _ -> false - in - CWarnings.set_flags wflags; - - (* The -time option is only supported from console-based - clients due to the way it prints. *) + (* The -time option is only supported from console-based clients + due to the way it prints. *) if time then print_cmd_header ?loc com; let com = if time then VernacTime(time,(CAst.make ?loc com)) else com in let doc, nsid, ntip = Stm.add ~doc:state.doc ~ontop:state.sid (not !Flags.quiet) (loc,com) in @@ -123,14 +102,6 @@ let interp_vernac ~time ~check ~interactive ~state (loc,com) = it otherwise reveals bugs *) (* Stm.observe nsid; *) let ndoc = if check then Stm.finish ~doc else doc in - - (* We could use a more refined criteria that depends on the - vernac. For now we imitate the old approach and rely on the - classification. *) - let print_goals = interactive && not !Flags.quiet && - is_proof_step && Proof_global.there_are_pending_proofs () in - - if print_goals then Feedback.msg_notice (pr_open_cur_subgoals ()); let new_proof = Proof_global.give_me_the_proof_opt () in { doc = ndoc; sid = nsid; proof = new_proof } with reraise -> diff --git a/vernac/classes.ml b/vernac/classes.ml index 25d893bfb..192cc8a55 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -374,16 +374,34 @@ let context poly l = with e when CErrors.noncritical e -> user_err Pp.(str "Anonymous variables not allowed in contexts.") in - let uctx = ref (Evd.universe_context_set sigma) in + let univs = + let uctx = Evd.universe_context_set sigma in + match ctx with + | [] -> assert false + | [_] -> + if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else Monomorphic_const_entry uctx + | _::_::_ -> + if Lib.sections_are_opened () + then + begin + Declare.declare_universe_context poly uctx; + if poly then Polymorphic_const_entry Univ.UContext.empty + else Monomorphic_const_entry Univ.ContextSet.empty + end + else if poly + then Polymorphic_const_entry (Univ.ContextSet.to_context uctx) + else + begin + Declare.declare_universe_context poly uctx; + Monomorphic_const_entry Univ.ContextSet.empty + end + in let fn status (id, b, t) = let b, t = Option.map (to_constr sigma) b, to_constr sigma t in if Lib.is_modtype () && not (Lib.sections_are_opened ()) then (* Declare the universe context once *) - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) - else Monomorphic_const_entry !uctx - in - let () = uctx := Univ.ContextSet.empty in let decl = match b with | None -> (ParameterEntry (None,(t,univs),None), IsAssumption Logical) @@ -405,10 +423,6 @@ let context poly l = in let impl = List.exists test impls in let decl = (Discharge, poly, Definitional) in - let univs = if poly - then Polymorphic_const_entry (Univ.ContextSet.to_context !uctx) - else Monomorphic_const_entry !uctx - in let nstatus = match b with | None -> pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl @@ -422,6 +436,4 @@ let context poly l = in status && nstatus in - if Lib.sections_are_opened () then - Declare.declare_universe_context poly !uctx; List.fold_left fn true (List.rev ctx) diff --git a/vernac/comAssumption.mli b/vernac/comAssumption.mli index f235de350..56e324376 100644 --- a/vernac/comAssumption.mli +++ b/vernac/comAssumption.mli @@ -19,7 +19,7 @@ open Decl_kinds (** {6 Parameters/Assumptions} *) val do_assumptions : locality * polymorphic * assumption_object_kind -> - Vernacexpr.inline -> (Vernacexpr.ident_decl list * constr_expr) with_coercion list -> bool + Vernacexpr.inline -> (ident_decl list * constr_expr) with_coercion list -> bool (************************************************************************) (** Internal API *) diff --git a/vernac/comDefinition.mli b/vernac/comDefinition.mli index 0d6367291..6f81c4575 100644 --- a/vernac/comDefinition.mli +++ b/vernac/comDefinition.mli @@ -17,7 +17,7 @@ open Constrexpr (** {6 Definitions/Let} *) val do_definition : program_mode:bool -> - Id.t -> definition_kind -> Vernacexpr.universe_decl_expr option -> + Id.t -> definition_kind -> universe_decl_expr option -> local_binder_expr list -> red_expr option -> constr_expr -> constr_expr option -> unit Lemmas.declaration_hook -> unit @@ -27,6 +27,6 @@ val do_definition : program_mode:bool -> (** Not used anywhere. *) val interp_definition : - Vernacexpr.universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> + universe_decl_expr option -> local_binder_expr list -> polymorphic -> red_expr option -> constr_expr -> constr_expr option -> Safe_typing.private_constants definition_entry * Evd.evar_map * Univdecls.universe_decl * Impargs.manual_implicits diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index edfe7aa81..a794c2db0 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -14,7 +14,6 @@ open Pretyping open Evarutil open Evarconv open Misctypes -open Vernacexpr module RelDecl = Context.Rel.Declaration diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index b181984e0..36c2993af 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -32,7 +32,7 @@ val do_cofixpoint : type structured_fixpoint_expr = { fix_name : Id.t; - fix_univs : Vernacexpr.universe_decl_expr option; + fix_univs : Constrexpr.universe_decl_expr option; fix_annot : Misctypes.lident option; fix_binders : local_binder_expr list; fix_body : constr_expr option; diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index 457a1da05..c59286d1a 100644 --- a/vernac/comInductive.ml +++ b/vernac/comInductive.ml @@ -57,7 +57,7 @@ let push_types env idl tl = type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli index b8d85c8d9..833935724 100644 --- a/vernac/comInductive.mli +++ b/vernac/comInductive.mli @@ -47,7 +47,7 @@ val declare_mutual_inductive_with_eliminations : type structured_one_inductive_expr = { ind_name : Id.t; - ind_univs : Vernacexpr.universe_decl_expr option; + ind_univs : universe_decl_expr option; ind_arity : constr_expr; ind_lc : (Id.t * constr_expr) list } diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 0ff6d9c17..5779c07ab 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -805,7 +805,14 @@ let vernac_end_segment ({v=id} as lid) = (* Libraries *) +let warn_require_in_section = + let name = "require-in-section" in + let category = "deprecated" in + CWarnings.create ~name ~category + (fun () -> strbrk "Use of “Require” inside a section is deprecated.") + let vernac_require from import qidl = + if Lib.sections_are_opened () then warn_require_in_section (); let qidl = List.map qualid_of_reference qidl in let root = match from with | None -> None |