diff options
72 files changed, 240 insertions, 753 deletions
diff --git a/.travis.yml b/.travis.yml index 9ec936b0c..481a63558 100644 --- a/.travis.yml +++ b/.travis.yml @@ -243,7 +243,8 @@ matrix: - EXTRA_OPAM="${LABLGTK}" before_install: - brew update - - brew install opam gnu-time gtk+ expat gtksourceview libxml2 gdk-pixbuf python3 + - brew install opam gnu-time gtk+ expat gtksourceview gdk-pixbuf + - brew upgrade python - pip3 install macpack before_deploy: - dev/build/osx/make-macos-dmg.sh @@ -86,6 +86,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 +112,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/Classes.tex b/doc/refman/Classes.tex index 6e76d04e7..da798a238 100644 --- a/doc/refman/Classes.tex +++ b/doc/refman/Classes.tex @@ -492,26 +492,6 @@ control on the triggering of instances. For example, forcing a constant to explicitely appear in the pattern will make it never apply on a goal where there is a hole in that place. -\subsection{\tt Set Typeclasses Legacy Resolution} -\optindex{Typeclasses Legacy Resolution} -\emph{Deprecated since 8.7} - -This option (off by default) uses the 8.5 implementation of resolution. -Use for compatibility purposes only (porting and debugging). - -\subsection{\tt Set Typeclasses Module Eta} -\optindex{Typeclasses Modulo Eta} -\emph{Deprecated since 8.7} - -This option allows eta-conversion for functions and records during -unification of type-classes. This option is unsupported since 8.6 with -{\tt Typeclasses Filtered Unification} set, but still affects the -default unification strategy, and the one used in {\tt Legacy - Resolution} mode. It is \emph{unset} by default. If {\tt Typeclasses - Filtered Unification} is set, this has no effect and unification will -find solutions up-to eta conversion. Note however that syntactic -pattern-matching is not up-to eta. - \subsection{\tt Set Typeclasses Limit Intros} \optindex{Typeclasses Limit Intros} @@ -525,13 +505,6 @@ invertibility status of the product introduction rule, resulting in potentially more expensive proof-search (i.e. more useless backtracking). -\subsection{\tt Set Typeclass Resolution After Apply} -\optindex{Typeclass Resolution After Apply} -\emph{Deprecated since 8.6} - -This option (off by default in Coq 8.6 and 8.5) controls the resolution -of typeclass subgoals generated by the {\tt apply} tactic. - \subsection{\tt Set Typeclass Resolution For Conversion} \optindex{Typeclass Resolution For Conversion} diff --git a/doc/refman/RefMan-sch.tex b/doc/refman/RefMan-sch.tex index 30724759d..600471123 100644 --- a/doc/refman/RefMan-sch.tex +++ b/doc/refman/RefMan-sch.tex @@ -127,7 +127,6 @@ conclusion is {\tt (n:nat)(even n)->(Q n)}. \optindex{Boolean Equality Schemes} \optindex{Elimination Schemes} \optindex{Nonrecursive Elimination Schemes} -\optindex{Record Elimination Schemes} \optindex{Case Analysis Schemes} \optindex{Decidable Equality Schemes} \optindex{Rewriting Schemes} @@ -144,7 +143,6 @@ and {\tt Record} (see~\ref{Record}) do not have an automatic declaration of the induction principles. It can be activated with the command {\tt Set Nonrecursive Elimination Schemes}. It can be deactivated again with {\tt Unset Nonrecursive Elimination Schemes}. -{\tt Record Elimination Schemes} is a deprecated alias of {\tt Nonrecursive Elimination Schemes}. In addition, the {\tt Case Analysis Schemes} flag governs the generation of case analysis lemmas for inductive types, i.e. corresponding to the diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 6dca314b4..40ba43b6c 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4589,7 +4589,6 @@ incompatibilities. \end{Variants} \optindex{Intuition Negation Unfolding} -\optindex{Intuition Iff Unfolding} Some aspects of the tactic {\tt intuition} can be controlled using options. To avoid that inner negations which do not @@ -4609,17 +4608,6 @@ To do that all negations of the goal are unfolded even inner ones To avoid that inner occurrence of {\tt iff} which do not need to be unfolded are unfolded (this is the default), use: -\begin{quote} -{\tt Unset Intuition Iff Unfolding} -\end{quote} - -To do that all negations of the goal are unfolded even inner ones -(this is the default), use: - -\begin{quote} -{\tt Set Intuition Iff Unfolding} -\end{quote} - % En attente d'un moyen de valoriser les fichiers de demos %\SeeAlso file \texttt{contrib/Rocq/DEMOS/Demo\_tauto.v} 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/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/ltac/tauto.ml b/plugins/ltac/tauto.ml index d0f31cd42..a51c09ca4 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -65,11 +65,6 @@ let assoc_flags ist : tauto_flags = (* Whether inner not are unfolded *) let negation_unfolding = ref true -(* Whether inner iff are unfolded *) -let iff_unfolding = ref false - -let unfold_iff () = !iff_unfolding - open Goptions let _ = declare_bool_option @@ -79,14 +74,6 @@ let _ = optread = (fun () -> !negation_unfolding); optwrite = (:=) negation_unfolding } -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "unfolding of iff in intuition"; - optkey = ["Intuition";"Iff";"Unfolding"]; - optread = (fun () -> !iff_unfolding); - optwrite = (:=) iff_unfolding } - (** Base tactics *) let idtac = Proofview.tclUNIT () @@ -202,16 +189,13 @@ let make_unfold name = let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in (Locus.AllOccurrences, ArgArg (EvalConstRef const, None)) -let u_iff = make_unfold "iff" let u_not = make_unfold "not" let reduction_not_iff _ ist = let make_reduce c = TacAtom (Loc.tag @@ TacReduce (Genredexpr.Unfold c, Locusops.allHypsAndConcl)) in - let tac = match !negation_unfolding, unfold_iff () with - | true, true -> make_reduce [u_not; u_iff] - | true, false -> make_reduce [u_not] - | false, true -> make_reduce [u_iff] - | false, false -> TacId [] + let tac = match !negation_unfolding with + | true -> make_reduce [u_not] + | false -> TacId [] in eval_tactic_ist ist tac diff --git a/plugins/ssr/ssrast.mli b/plugins/ssr/ssrast.mli index 9783bc61d..7f5f2f63d 100644 --- a/plugins/ssr/ssrast.mli +++ b/plugins/ssr/ssrast.mli @@ -138,7 +138,7 @@ type ssrclseq = InGoal | InHyps type 'tac ssrhint = bool * 'tac option list type 'tac fwdbinders = - bool * (ssrhpats * ((ssrfwdfmt * ssrterm) * 'tac ssrhint)) + bool * (ssrhpats * ((ssrfwdfmt * ast_closure_term) * 'tac ssrhint)) type clause = (ssrclear * ((ssrhyp_or_id * string) * @@ -157,13 +157,15 @@ type 'a ssrseqarg = ssrindex * ('a ssrhint * 'a option) open Ssrmatching_plugin open Ssrmatching + +type 'a ssrcasearg = ssripat option * ('a * ssripats) +type 'a ssrmovearg = ssrview * 'a ssrcasearg + type ssrdgens = { dgens : (ssrdocc * cpattern) list; gens : (ssrdocc * cpattern) list; clr : ssrclear } -type ssrcasearg = ssripat option * (ssrdgens * ssripats) -type ssrmovearg = ssrview * ssrcasearg -type ssragens = ((ssrhyps option * occ) * ssrterm) list list * ssrclear -type ssrapplyarg = ssrterm list * (ssragens * ssripats) +type 'a ssragens = (ssrdocc * 'a) list list * ssrclear +type ssrapplyarg = ssrterm list * (ssrterm ssragens * ssripats) (* OOP : these are general shortcuts *) type gist = Tacintern.glob_sign diff --git a/plugins/ssr/ssrbwd.mli b/plugins/ssr/ssrbwd.mli index 6243e5e68..694ecfa37 100644 --- a/plugins/ssr/ssrbwd.mli +++ b/plugins/ssr/ssrbwd.mli @@ -13,4 +13,4 @@ open Proofview val apply_top_tac : unit tactic -val inner_ssrapplytac : ssrterm list -> ssragens -> ist -> unit tactic +val inner_ssrapplytac : ssrterm list -> ssrterm ssragens -> ist -> unit tactic diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 511c83269..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 *) @@ -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 *) diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml index f45a191b7..859513d5c 100644 --- a/plugins/ssr/ssrequality.ml +++ b/plugins/ssr/ssrequality.ml @@ -143,18 +143,6 @@ let newssrcongrtac arg ist gl = (** 7. Rewriting tactics (rewrite, unlock) *) -(** Coq rewrite compatibility flag *) - - -let _ = - let ssr_strict_match = ref false in - Goptions.declare_bool_option - { Goptions.optname = "strict redex matching"; - Goptions.optkey = ["Match"; "Strict"]; - Goptions.optread = (fun () -> !ssr_strict_match); - Goptions.optdepr = true; (* noop *) - Goptions.optwrite = (fun b -> ssr_strict_match := b) } - (** Rewrite rules *) type ssrwkind = RWred of ssrsimpl | RWdef | RWeq 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/ssripats.mli b/plugins/ssr/ssripats.mli index b8716c0c4..89cba4be7 100644 --- a/plugins/ssr/ssripats.mli +++ b/plugins/ssr/ssripats.mli @@ -29,11 +29,11 @@ val tclIPATssr : ssripats -> unit Proofview.tactic [tac E: gens => ipats] where [E] is injected into [ipats] (at the right place) and [gens] are generalized before calling [tac] *) -val ssrmovetac : ssrmovearg -> unit Proofview.tactic +val ssrmovetac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrsmovetac : unit Proofview.tactic -val ssrelimtac : ssrmovearg -> unit Proofview.tactic +val ssrelimtac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrselimtoptac : unit Proofview.tactic -val ssrcasetac : ssrmovearg -> unit Proofview.tactic +val ssrcasetac : ssrdgens ssrmovearg -> unit Proofview.tactic val ssrscasetoptac : unit Proofview.tactic (* The implementation of abstract: is half here, for the [[: var ]] 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/ssrparser.mli b/plugins/ssr/ssrparser.mli index a52248614..130550388 100644 --- a/plugins/ssr/ssrparser.mli +++ b/plugins/ssr/ssrparser.mli @@ -20,3 +20,16 @@ val pr_ssrtclarg : 'a -> 'b -> (Notation_term.tolerability -> 'c -> 'd) -> 'c -> val add_genarg : string -> ('a -> Pp.t) -> 'a Genarg.uniform_genarg_type +(* Parsing witnesses, needed to serialize ssreflect syntax *) +open Ssrmatching_plugin +open Ssrmatching +open Ssrast +open Ssrequality + +val wit_ssrrwargs : ssrrwarg list Genarg.uniform_genarg_type +val wit_ssrclauses : clauses Genarg.uniform_genarg_type +val wit_ssrcasearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type +val wit_ssrmovearg : (cpattern ssragens) ssrmovearg Genarg.uniform_genarg_type +val wit_ssrapplyarg : ssrapplyarg Genarg.uniform_genarg_type +val wit_ssrhavefwdwbinders : + (Tacexpr.raw_tactic_expr fwdbinders, Tacexpr.glob_tactic_expr fwdbinders, Tacinterp.Value.t fwdbinders) Genarg.genarg_type diff --git a/plugins/ssr/ssrtacticals.ml b/plugins/ssr/ssrtacticals.ml index b29c83eff..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" 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/unification.ml b/pretyping/unification.ml index 5bc93f1fa..f4269a2c5 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -250,20 +250,6 @@ let unify_r2l x = x let sort_eqns = unify_r2l *) -let global_pattern_unification_flag = ref true - -open Goptions - -(* Compatibility option introduced and activated in Coq 8.4 *) - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "pattern-unification for existential variables in tactics"; - optkey = ["Tactic";"Pattern";"Unification"]; - optread = (fun () -> !global_pattern_unification_flag); - optwrite = (:=) global_pattern_unification_flag } - type core_unify_flags = { modulo_conv_on_closed_terms : Names.transparent_state option; (* What this flag controls was activated with all constants transparent, *) @@ -287,12 +273,10 @@ type core_unify_flags = { use_pattern_unification : bool; (* This solves pattern "?n x1 ... xn = t" when the xi are distinct rels *) - (* This says if pattern unification is tried; can be overwritten with *) - (* option "Set Tactic Pattern Unification" *) + (* This says if pattern unification is tried *) use_meta_bound_pattern_unification : bool; - (* This is implied by use_pattern_unification (though deactivated *) - (* by unsetting Tactic Pattern Unification); has no particular *) + (* This is implied by use_pattern_unification; has no particular *) (* reasons to be set differently than use_pattern_unification *) (* except for compatibility of "auto". *) (* This was on for all tactics, including auto, since Sep 2006 for 8.1 *) @@ -473,10 +457,10 @@ let set_flags_for_type flags = { flags with } let use_evars_pattern_unification flags = - !global_pattern_unification_flag && flags.use_pattern_unification + flags.use_pattern_unification let use_metas_pattern_unification sigma flags nb l = - !global_pattern_unification_flag && flags.use_pattern_unification + flags.use_pattern_unification || flags.use_meta_bound_pattern_unification && Array.for_all (fun c -> isRel sigma c && destRel sigma c <= nb) l 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/class_tactics.ml b/tactics/class_tactics.ml index 4c91f3f61..9f6624889 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -20,7 +20,6 @@ open Names open Term open Termops open EConstr -open Proof_type open Tacmach open Tactics open Clenv @@ -28,7 +27,6 @@ open Typeclasses open Globnames open Evd open Locus -open Misctypes open Proofview.Notations open Hints @@ -41,10 +39,6 @@ module NamedDecl = Context.Named.Declaration let typeclasses_debug = ref 0 let typeclasses_depth = ref None -let typeclasses_modulo_eta = ref false -let set_typeclasses_modulo_eta d = (:=) typeclasses_modulo_eta d -let get_typeclasses_modulo_eta () = !typeclasses_modulo_eta - (** When this flag is enabled, the resolution of type classes tries to avoid useless introductions. This is no longer useful since we have eta, but is here for compatibility purposes. Another compatibility issues is that the @@ -71,13 +65,6 @@ let set_typeclasses_filtered_unification d = let get_typeclasses_filtered_unification () = !typeclasses_filtered_unification -(** [typeclasses_legacy_resolution] falls back to the 8.5 resolution algorithm, - instead of the 8.6 one which uses the native backtracking facilities of the - proof engine. *) -let typeclasses_legacy_resolution = ref false -let set_typeclasses_legacy_resolution d = (:=) typeclasses_legacy_resolution d -let get_typeclasses_legacy_resolution () = !typeclasses_legacy_resolution - let set_typeclasses_debug d = (:=) typeclasses_debug (if d then 1 else 0) let get_typeclasses_debug () = if !typeclasses_debug > 0 then true else false @@ -94,14 +81,6 @@ open Goptions let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "do typeclass search modulo eta conversion"; - optkey = ["Typeclasses";"Modulo";"Eta"]; - optread = get_typeclasses_modulo_eta; - optwrite = set_typeclasses_modulo_eta; } - -let _ = - declare_bool_option { optdepr = false; optname = "do typeclass search avoiding eta-expansions " ^ " in proof terms (expensive)"; @@ -127,14 +106,6 @@ let _ = let _ = declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "compat"; - optkey = ["Typeclasses";"Legacy";"Resolution"]; - optread = get_typeclasses_legacy_resolution; - optwrite = set_typeclasses_legacy_resolution; } - -let _ = - declare_bool_option { optdepr = false; optname = "compat"; optkey = ["Typeclasses";"Filtered";"Unification"]; @@ -199,7 +170,7 @@ let auto_core_unif_flags st freeze = { frozen_evars = freeze; restrict_conv_on_strict_subterms = false; (* ? *) modulo_betaiota = true; - modulo_eta = !typeclasses_modulo_eta; + modulo_eta = false; } let auto_unif_flags freeze st = @@ -426,9 +397,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm else let tac = with_prods nprods poly (term,cl) (unify_resolve poly flags) in - if get_typeclasses_legacy_resolution () then - Tacticals.New.tclTHEN tac Proofview.shelve_unifiable - else Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) | ERes_pf (term,cl) -> @@ -441,9 +409,6 @@ and e_my_find_search db_list local_db secvars hdc complete only_classes env sigm else let tac = with_prods nprods poly (term,cl) (unify_e_resolve poly flags) in - if get_typeclasses_legacy_resolution () then - Tacticals.New.tclTHEN tac Proofview.shelve_unifiable - else Proofview.tclBIND (Proofview.with_shelf tac) (fun (gls, ()) -> shelve_dependencies gls) | Give_exact (c,clenv) -> @@ -618,359 +583,6 @@ let make_hints g st only_classes sign = ([]) sign in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true) -(** <= 8.5 resolution *) -module V85 = struct - - type autoinfo = { hints : hint_db; is_evar: existential_key option; - only_classes: bool; unique : bool; - auto_depth: int list; auto_last_tac: Pp.t Lazy.t; - auto_path : global_reference option list; - auto_cut : hints_path } - type autogoal = goal * autoinfo - type failure = NotApplicable | ReachedLimit - type 'ans fk = failure -> 'ans - type ('a,'ans) sk = 'a -> 'ans fk -> 'ans - type 'a tac = { skft : 'ans. ('a,'ans) sk -> 'ans fk -> autogoal sigma -> 'ans } - - type auto_result = autogoal list sigma - - type atac = auto_result tac - - (* Some utility types to avoid the need of -rectypes *) - - type 'a optionk = - | Nonek - | Somek of 'a * 'a optionk fk - - type ('a,'b) optionk2 = - | Nonek2 of failure - | Somek2 of 'a * 'b * ('a,'b) optionk2 fk - - let pf_filtered_hyps gls = - Goal.V82.hyps gls.Evd.sigma (sig_it gls) - - let make_autogoal_hints = - let cache = Summary.ref ~name:"make_autogoal_hints_cache" - (true, Environ.empty_named_context_val, - Hint_db.empty full_transparent_state true) - in - fun only_classes ?(st=full_transparent_state) g -> - let sign = pf_filtered_hyps g in - let (onlyc, sign', cached_hints) = !cache in - if onlyc == only_classes && - (sign == sign' || Environ.eq_named_context_val sign sign') - && Hint_db.transparent_state cached_hints == st - then - cached_hints - else - let hints = make_hints g st only_classes (EConstr.named_context_of_val sign) - in - cache := (only_classes, sign, hints); hints - - let lift_tactic tac (f : goal list sigma -> autoinfo -> autogoal list sigma) : 'a tac = - { skft = fun sk fk {it = gl,hints; sigma=s;} -> - let res = try Some (tac {it=gl; sigma=s;}) - with e when catchable e -> None in - match res with - | Some gls -> sk (f gls hints) fk - | None -> fk NotApplicable } - - let intro_tac : atac = - let tac {it = gls; sigma = s} info = - let gls' = - List.map (fun g' -> - let env = Goal.V82.env s g' in - let context = EConstr.named_context_of_val (Goal.V82.hyps s g') in - let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) - (true,false,false) info.only_classes empty_hint_info (List.hd context) in - let ldb = Hint_db.add_list env s hint info.hints in - (g', { info with is_evar = None; hints = ldb; - auto_last_tac = lazy (str"intro") })) gls - in {it = gls'; sigma = s;} - in - lift_tactic (Proofview.V82.of_tactic Tactics.intro) tac - - let normevars_tac : atac = - { skft = fun sk fk {it = (gl, info); sigma = s;} -> - let gl', sigma' = Goal.V82.nf_evar s gl in - let info' = { info with auto_last_tac = lazy (str"normevars") } in - sk {it = [gl', info']; sigma = sigma';} fk } - - let merge_failures x y = - match x, y with - | _, ReachedLimit - | ReachedLimit, _ -> ReachedLimit - | NotApplicable, NotApplicable -> NotApplicable - - let or_tac (x : 'a tac) (y : 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft sk - (fun f -> y.skft sk (fun f' -> fk (merge_failures f f')) gls) gls } - - let or_else_tac (x : 'a tac) (y : failure -> 'a tac) : 'a tac = - { skft = fun sk fk gls -> x.skft sk - (fun f -> (y f).skft sk fk gls) gls } - - let needs_backtrack env evd oev concl = - if Option.is_empty oev || is_Prop env evd concl then - occur_existential evd concl - else true - - let hints_tac hints sk fk {it = gl,info; sigma = s} = - let env = Goal.V82.env s gl in - let concl = Goal.V82.concl s gl in - let tacgl = {it = gl; sigma = s;} in - let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in - let poss = e_possible_resolve hints info.hints secvars info.only_classes env s concl in - let unique = is_unique env s concl in - let rec aux i foundone = function - | (tac, _, extern, name, pp) :: tl -> - let derivs = path_derivate info.auto_cut name in - let res = - try - if path_matches derivs [] then None - else Some (Proofview.V82.of_tactic tac tacgl) - with e when catchable e -> None - in - (match res with - | None -> aux i foundone tl - | Some {it = gls; sigma = s';} -> - if !typeclasses_debug > 0 then - Feedback.msg_debug - (pr_depth (i :: info.auto_depth) ++ str": " ++ Lazy.force pp - ++ str" on" ++ spc () ++ pr_ev s gl); - let sgls = - evars_to_goals - (fun evm ev evi -> - if Typeclasses.is_resolvable evi && not (Evd.is_undefined s ev) && - (not info.only_classes || Typeclasses.is_class_evar evm evi) - then Typeclasses.mark_unresolvable evi, true - else evi, false) s' - in - let newgls, s' = - let gls' = List.map (fun g -> (None, g)) gls in - match sgls with - | None -> gls', s' - | Some (evgls, s') -> - if not !typeclasses_dependency_order then - (gls' @ List.map (fun (ev,_) -> (Some ev, ev)) (Evar.Map.bindings evgls), s') - else - (* Reorder with dependent subgoals. *) - let evm = List.fold_left - (fun acc g -> Evar.Map.add g (Evd.find_undefined s' g) acc) evgls gls in - let gls = top_sort s' evm in - (List.map (fun ev -> Some ev, ev) gls, s') - in - let reindex g = - let open Goal.V82 in - extern && not (Environ.eq_named_context_val - (hyps s' g) (hyps s' gl)) - in - let gl' j (evar, g) = - let hints' = - if reindex g then - make_autogoal_hints - info.only_classes - ~st:(Hint_db.transparent_state info.hints) - {it = g; sigma = s';} - else info.hints - in - { info with - auto_depth = j :: i :: info.auto_depth; - auto_last_tac = pp; - is_evar = evar; - hints = hints'; - auto_cut = derivs } - in - let gls' = List.map_i (fun i g -> snd g, gl' i g) 1 newgls in - let glsv = {it = gls'; sigma = s';} in - let fk' = - (fun e -> - let do_backtrack = - if unique then occur_existential tacgl.sigma concl - else if info.unique then true - else if List.is_empty gls' then - needs_backtrack env tacgl.sigma info.is_evar concl - else true - in - let e' = match foundone with None -> e - | Some e' -> merge_failures e e' in - if !typeclasses_debug > 0 then - Feedback.msg_debug - ((if do_backtrack then str"Backtracking after " - else str "Not backtracking after ") - ++ Lazy.force pp); - if do_backtrack then aux (succ i) (Some e') tl - else fk e') - in - sk glsv fk') - | [] -> - if foundone == None && !typeclasses_debug > 0 then - Feedback.msg_debug - (pr_depth info.auto_depth ++ str": no match for " ++ - Printer.pr_econstr_env (Goal.V82.env s gl) s concl ++ - spc () ++ str ", " ++ int (List.length poss) ++ - str" possibilities"); - match foundone with - | Some e -> fk e - | None -> fk NotApplicable - in aux 1 None poss - - let hints_tac hints = - { skft = fun sk fk gls -> hints_tac hints sk fk gls } - - let then_list (second : atac) (sk : (auto_result, 'a) sk) : (auto_result, 'a) sk = - let rec aux s (acc : autogoal list list) fk = function - | (gl,info) :: gls -> - Control.check_for_interrupt (); - (match info.is_evar with - | Some ev when Evd.is_defined s ev -> aux s acc fk gls - | _ -> - second.skft - (fun {it=gls';sigma=s'} fk' -> - let fk'' = - if not info.unique && List.is_empty gls' && - not (needs_backtrack (Goal.V82.env s gl) s - info.is_evar (Goal.V82.concl s gl)) - then fk - else fk' - in - aux s' (gls'::acc) fk'' gls) - fk {it = (gl,info); sigma = s; }) - | [] -> Somek2 (List.rev acc, s, fk) - in fun {it = gls; sigma = s; } fk -> - let rec aux' = function - | Nonek2 e -> fk e - | Somek2 (res, s', fk') -> - let goals' = List.concat res in - sk {it = goals'; sigma = s'; } (fun e -> aux' (fk' e)) - in aux' (aux s [] (fun e -> Nonek2 e) gls) - - let then_tac (first : atac) (second : atac) : atac = - { skft = fun sk fk -> first.skft (then_list second sk) fk } - - let run_tac (t : 'a tac) (gl : autogoal sigma) : auto_result option = - t.skft (fun x _ -> Some x) (fun _ -> None) gl - - type run_list_res = auto_result optionk - - let run_list_tac (t : 'a tac) p goals (gl : autogoal list sigma) : run_list_res = - (then_list t (fun x fk -> Somek (x, fk))) - gl - (fun _ -> Nonek) - - let fail_tac reason : atac = - { skft = fun sk fk _ -> fk reason } - - let rec fix (t : 'a tac) : 'a tac = - then_tac t { skft = fun sk fk -> (fix t).skft sk fk } - - let rec fix_limit limit (t : 'a tac) : 'a tac = - if Int.equal limit 0 then fail_tac ReachedLimit - else then_tac t { skft = fun sk fk -> (fix_limit (pred limit) t).skft sk fk } - - let fix_iterative t = - let rec aux depth = - or_else_tac (fix_limit depth t) - (function - | NotApplicable as e -> fail_tac e - | ReachedLimit -> aux (succ depth)) - in aux 1 - - let fix_iterative_limit limit (t : 'a tac) : 'a tac = - let rec aux depth = - if Int.equal limit depth then fail_tac ReachedLimit - else or_tac (fix_limit depth t) - { skft = fun sk fk -> (aux (succ depth)).skft sk fk } - in aux 1 - - let make_autogoal ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) - cut ev g = - let hints = make_autogoal_hints only_classes ~st g in - (g.it, { hints = hints ; is_evar = ev; unique = unique; - only_classes = only_classes; auto_depth = []; - auto_last_tac = lazy (str"none"); - auto_path = []; auto_cut = cut }) - - - let make_autogoals ?(only_classes=true) ?(unique=false) - ?(st=full_transparent_state) hints gs evm' = - let cut = cut_of_hints hints in - let gl i g = - let (gl, auto) = make_autogoal ~only_classes ~unique - ~st cut (Some g) {it = g; sigma = evm'; } in - (gl, { auto with auto_depth = [i]}) - in { it = List.map_i gl 1 gs; sigma = evm' } - - let get_result r = - match r with - | Nonek -> None - | Somek (gls, fk) -> Some (gls.sigma,fk) - - let run_on_evars ?(only_classes=true) ?(unique=false) ?(st=full_transparent_state) - p evm hints tac = - match evars_to_goals p evm with - | None -> None (* This happens only because there's no evar having p *) - | Some (goals, evm') -> - let goals = - if !typeclasses_dependency_order then - top_sort evm' goals - else List.map (fun (ev, _) -> ev) (Evar.Map.bindings goals) - in - let res = run_list_tac tac p goals - (make_autogoals ~only_classes ~unique ~st hints goals evm') in - match get_result res with - | None -> raise Not_found - | Some (evm', fk) -> - Some (evars_reset_evd ~with_conv_pbs:true ~with_univs:false evm' evm, fk) - - let eauto_tac hints = - then_tac normevars_tac (or_tac (hints_tac hints) intro_tac) - - let eauto_tac strategy depth hints = - match strategy with - | Bfs -> - begin match depth with - | None -> fix_iterative (eauto_tac hints) - | Some depth -> fix_iterative_limit depth (eauto_tac hints) end - | Dfs -> - match depth with - | None -> fix (eauto_tac hints) - | Some depth -> fix_limit depth (eauto_tac hints) - - let real_eauto ?depth strategy unique st hints p evd = - let res = - run_on_evars ~st ~unique p evd hints (eauto_tac strategy depth hints) - in - match res with - | None -> evd - | Some (evd', fk) -> - if unique then - (match get_result (fk NotApplicable) with - | Some (evd'', fk') -> user_err Pp.(str "Typeclass resolution gives multiple solutions") - | None -> evd') - else evd' - - let resolve_all_evars_once debug depth unique p evd = - let db = searchtable_map typeclasses_db in - let strategy = if get_typeclasses_iterative_deepening () then Bfs else Dfs in - real_eauto ?depth strategy unique (Hint_db.transparent_state db) [db] p evd - - let eauto85 ?(only_classes=true) ?st ?strategy depth hints g = - let strategy = - match strategy with - | None -> if get_typeclasses_iterative_deepening () then Bfs else Dfs - | Some s -> s - in - let gl = { it = make_autogoal ~only_classes ?st - (cut_of_hints hints) None g; sigma = project g; } in - match run_tac (eauto_tac strategy depth hints) gl with - | None -> raise Not_found - | Some {it = goals; sigma = s; } -> - {it = List.map fst goals; sigma = s;} - -end - -(** 8.6 resolution *) module Search = struct type autoinfo = { search_depth : int list; @@ -1406,13 +1018,7 @@ let typeclasses_eauto ?(only_classes=false) ?(st=full_transparent_state) in let st = match dbs with x :: _ -> Hint_db.transparent_state x | _ -> st in let depth = match depth with None -> get_typeclasses_depth () | Some l -> Some l in - if get_typeclasses_legacy_resolution () then - Proofview.V82.tactic - (fun gl -> - try V85.eauto85 depth ~only_classes ~st ?strategy dbs gl - with Not_found -> - Refiner.tclFAIL 0 (str"Proof search failed") gl) - else Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs + Search.eauto_tac ~st ~only_classes ?strategy ~depth ~dep:true dbs (** We compute dependencies via a union-find algorithm. Beware of the imperative effects on the partition structure, @@ -1531,12 +1137,7 @@ let resolve_all_evars debug depth unique env p oevd do_split fail = | comp :: comps -> let p = select_and_update_evars p oevd (in_comp comp) in try - let evd' = - if get_typeclasses_legacy_resolution () then - V85.resolve_all_evars_once debug depth unique p evd - else - Search.typeclasses_resolve env evd debug depth unique p - in + let evd' = Search.typeclasses_resolve env evd debug depth unique p in if has_undefined p oevd evd' then raise Unresolved; docomp evd' comps with Unresolved | Not_found -> @@ -1581,9 +1182,6 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique = let st = Hint_db.transparent_state hints in let depth = get_typeclasses_depth () in let gls' = - if get_typeclasses_legacy_resolution () then - V85.eauto85 depth ~st [hints] gls - else try Proofview.V82.of_tactic (Search.eauto_tac ~st ~only_classes:true ~depth [hints] ~dep:true) gls diff --git a/tactics/equality.ml b/tactics/equality.ml index f15a64fc8..236db1dcc 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -69,20 +69,10 @@ let _ = optread = (fun () -> !discriminate_introduction); optwrite = (:=) discriminate_introduction } -let injection_pattern_l2r_order = ref true - let use_injection_pattern_l2r_order = function - | None -> !injection_pattern_l2r_order + | None -> true | Some flags -> flags.injection_pattern_l2r_order -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "injection left-to-right pattern order and clear by default when with introduction pattern"; - optkey = ["Injection";"L2R";"Pattern";"Order"]; - optread = (fun () -> !injection_pattern_l2r_order) ; - optwrite = (fun b -> injection_pattern_l2r_order := b) } - let injection_in_context = ref false let use_injection_in_context = function 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 20519dd98..b99a45103 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -61,16 +61,6 @@ let typ_of env sigma c = open Goptions -let apply_solve_class_goals = ref false - -let _ = - declare_bool_option - { optdepr = true; (* remove in 8.8 *) - optname = "Perform typeclass resolution on apply-generated subgoals."; - optkey = ["Typeclass";"Resolution";"After";"Apply"]; - optread = (fun () -> !apply_solve_class_goals); - optwrite = (fun a -> apply_solve_class_goals := a); } - let clear_hyp_by_default = ref false let use_clear_hyp_by_default () = !clear_hyp_by_default @@ -1689,22 +1679,6 @@ let descend_in_conjunctions avoid tac (err, info) c = (* Resolution tactics *) (****************************************************) -let solve_remaining_apply_goals = - Proofview.Goal.enter begin fun gl -> - let evd = Proofview.Goal.sigma gl in - if !apply_solve_class_goals then - try - let env = Proofview.Goal.env gl in - let concl = Proofview.Goal.concl gl in - if Typeclasses.is_class_type evd concl then - let evd', c' = Typeclasses.resolve_one_typeclass env evd concl in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS evd') - (Refine.refine ~typecheck:false (fun h -> (h,c'))) - else Proofview.tclUNIT () - with Not_found -> Proofview.tclUNIT () - else Proofview.tclUNIT () - end - let tclORELSEOPT t k = Proofview.tclORELSE t (fun e -> match k e with @@ -1780,11 +1754,9 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind : | _ -> None) end in - Tacticals.New.tclTHENLIST [ - try_main_apply with_destruct c; - solve_remaining_apply_goals; - apply_clear_request clear_flag (use_clear_hyp_by_default ()) c - ] + Tacticals.New.tclTHEN + (try_main_apply with_destruct c) + (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c) end let rec apply_with_bindings_gen b e = function 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/3481.v b/test-suite/bugs/closed/3481.v index 89d476dcb..38f03b166 100644 --- a/test-suite/bugs/closed/3481.v +++ b/test-suite/bugs/closed/3481.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Module NonPrim. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Record prodwithlet (A B : Type) : Type := pair' { fst : A; fst' := fst; snd : B }. @@ -21,7 +21,7 @@ End NonPrim. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/3513.v b/test-suite/bugs/closed/3513.v index 5adc48215..1f0f3b0da 100644 --- a/test-suite/bugs/closed/3513.v +++ b/test-suite/bugs/closed/3513.v @@ -69,26 +69,6 @@ Goal forall (T : Type) (O0 : T -> OPred) (O1 : T -> PointedOPred) refine (P _ _) end; unfold Basics.flip. Focus 2. - Set Typeclasses Debug. - Set Typeclasses Legacy Resolution. - apply reflexivity. - (* Debug: 1.1: apply @IsPointed_catOP on -(IsPointed (exists x0 : Actions, (catOP ?Goal O2 : OPred) x0)) -Debug: 1.1.1.1: apply OPred_inhabited on (IsPointed (exists x0 : Actions, ?Goal x0)) -Debug: 1.1.2.1: apply OPred_inhabited on (IsPointed (exists x : Actions, O2 x)) -Debug: 2.1: apply @Equivalence_Reflexive on (Reflexive lentails) -Debug: 2.1.1: no match for (Equivalence lentails) , 5 possibilities -Debug: Backtracking after apply @Equivalence_Reflexive -Debug: 2.2: apply @PreOrder_Reflexive on (Reflexive lentails) -Debug: 2.2.1.1: apply @lentailsPre on (PreOrder lentails) -Debug: 2.2.1.1.1.1: apply ILFun_ILogic on (ILogic OPred) -*) - Undo. Unset Typeclasses Legacy Resolution. - Test Typeclasses Unique Solutions. - Test Typeclasses Unique Instances. - Show Existentials. - Set Typeclasses Debug Verbosity 2. - Set Printing All. (* As in 8.5, allow a shelved subgoal to remain *) apply reflexivity. diff --git a/test-suite/bugs/closed/3520.v b/test-suite/bugs/closed/3520.v index c981207e6..ea122e521 100644 --- a/test-suite/bugs/closed/3520.v +++ b/test-suite/bugs/closed/3520.v @@ -3,7 +3,7 @@ Set Primitive Projections. Record foo (A : Type) := { bar : Type ; baz := Set; bad : baz = bar }. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record notprim : Prop := { irrel : True; relevant : nat }. diff --git a/test-suite/bugs/closed/3662.v b/test-suite/bugs/closed/3662.v index bd53389b4..b8754bce9 100644 --- a/test-suite/bugs/closed/3662.v +++ b/test-suite/bugs/closed/3662.v @@ -1,6 +1,6 @@ Set Primitive Projections. Set Implicit Arguments. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record prod A B := pair { fst : A ; snd : B }. Definition f : Set -> Type := fun x => x. 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/bugs/closed/HoTT_coq_077.v b/test-suite/bugs/closed/HoTT_coq_077.v index 017780c1f..f69c71a02 100644 --- a/test-suite/bugs/closed/HoTT_coq_077.v +++ b/test-suite/bugs/closed/HoTT_coq_077.v @@ -3,7 +3,7 @@ Set Implicit Arguments. Require Import Logic. Set Asymmetric Patterns. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/closed/HoTT_coq_104.v b/test-suite/bugs/closed/HoTT_coq_104.v index 5bb7fa8c1..a6ff78d12 100644 --- a/test-suite/bugs/closed/HoTT_coq_104.v +++ b/test-suite/bugs/closed/HoTT_coq_104.v @@ -4,7 +4,7 @@ Require Import Logic. Global Set Universe Polymorphism. Global Set Asymmetric Patterns. -Local Set Record Elimination Schemes. +Local Set Nonrecursive Elimination Schemes. Local Set Primitive Projections. Record prod (A B : Type) : Type := diff --git a/test-suite/bugs/opened/3926.v b/test-suite/bugs/opened/3926.v deleted file mode 100644 index cfad76357..000000000 --- a/test-suite/bugs/opened/3926.v +++ /dev/null @@ -1,30 +0,0 @@ -Notation compose := (fun g f x => g (f x)). -Notation "g 'o' f" := (compose g f) (at level 40, left associativity) : function_scope. -Open Scope function_scope. -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y) : type_scope. -Arguments idpath {A a} , [A] a. -Definition ap {A B:Type} (f:A -> B) {x y:A} (p:x = y) : f x = f y := match p with idpath => idpath end. -Class IsEquiv {A B : Type} (f : A -> B) := { equiv_inv : B -> A }. -Notation "f ^-1" := (@equiv_inv _ _ f _) (at level 3, format "f '^-1'") : equiv_scope. -Local Open Scope equiv_scope. -Axiom eisretr : forall {A B} (f : A -> B) `{IsEquiv A B f} x, f (f^-1 x) = x. -Generalizable Variables A B C f g. -Global Instance isequiv_compose `{IsEquiv A B f} `{IsEquiv B C g} : IsEquiv (compose g f) | 1000 - := Build_IsEquiv A C (compose g f) (compose f^-1 g^-1). -Definition isequiv_homotopic {A B} (f : A -> B) {g : A -> B} `{IsEquiv A B f} (h : forall x, f x = g x) : IsEquiv g - := Build_IsEquiv _ _ g (f ^-1). -Global Instance isequiv_inverse {A B} (f : A -> B) `{IsEquiv A B f} : IsEquiv f^-1 | 10000 - := Build_IsEquiv B A f^-1 f. -Definition cancelR_isequiv {A B C} (f : A -> B) {g : B -> C} - `{IsEquiv A B f} `{IsEquiv A C (g o f)} - : IsEquiv g. -Proof. - Unset Typeclasses Modulo Eta. - exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))) || fail "too early". - Undo. - Set Typeclasses Modulo Eta. - Set Typeclasses Dependency Order. - Set Typeclasses Debug. - Fail exact (isequiv_homotopic (compose (compose g f) f^-1) - (fun b => ap g (eisretr f b))). 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/Inductive.v b/test-suite/success/Inductive.v index 893d75b77..5b1482fd5 100644 --- a/test-suite/success/Inductive.v +++ b/test-suite/success/Inductive.v @@ -200,3 +200,9 @@ Module NonRecLetIn. (fun n b c => f_equal (Rec n) eq_refl) 0 (Rec 0 (Base 1)). End NonRecLetIn. + +(* Test treatment of let-in in the definition of Records *) +(* Should fail with "Sort expected" *) + +Fail Inductive foo (T : Type) : let T := Type in T := + { r : forall x : T, x = x }. diff --git a/test-suite/success/letproj.v b/test-suite/success/letproj.v index a183be622..de2857b43 100644 --- a/test-suite/success/letproj.v +++ b/test-suite/success/letproj.v @@ -1,5 +1,5 @@ Set Primitive Projections. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Record Foo (A : Type) := { bar : A -> A; baz : A }. Definition test (A : Type) (f : Foo A) := diff --git a/test-suite/success/old_typeclass.v b/test-suite/success/old_typeclass.v deleted file mode 100644 index 01e35810b..000000000 --- a/test-suite/success/old_typeclass.v +++ /dev/null @@ -1,13 +0,0 @@ -Require Import Setoid Coq.Classes.Morphisms. -Set Typeclasses Legacy Resolution. - -Declare Instance and_Proper_eq: Proper (Logic.eq ==> Logic.eq ==> Logic.eq) and. - -Axiom In : Prop. -Axiom union_spec : In <-> True. - -Lemma foo : In /\ True. -Proof. -progress rewrite union_spec. -repeat constructor. -Qed. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 576bdbf71..31a1608c4 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -1,5 +1,5 @@ Set Primitive Projections. -Set Record Elimination Schemes. +Set Nonrecursive Elimination Schemes. Module Prim. Record F := { a : nat; b : a = a }. 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/indschemes.ml b/vernac/indschemes.ml index 779926a7d..41c44b126 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -61,13 +61,6 @@ let _ = optkey = ["Nonrecursive";"Elimination";"Schemes"]; optread = (fun () -> !bifinite_elim_flag) ; optwrite = (fun b -> bifinite_elim_flag := b) } -let _ = - declare_bool_option - { optdepr = true; (* compatibility 2014-09-03*) - optname = "automatic declaration of induction schemes for non-recursive types"; - optkey = ["Record";"Elimination";"Schemes"]; - optread = (fun () -> !bifinite_elim_flag) ; - optwrite = (fun b -> bifinite_elim_flag := b) } let case_flag = ref false let _ = diff --git a/vernac/record.ml b/vernac/record.ml index 1991a8640..e21f53f55 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -124,7 +124,7 @@ let typecheck_params_and_fields finite def id poly pl t ps nots fs = match t with | { CAst.v = CSort (Misctypes.GType []) } -> true | _ -> false in let sigma, s = interp_type_evars env sigma ~impls:empty_internalization_env t in - let sred = Reductionops.whd_all env sigma s in + let sred = Reductionops.whd_allnolet env sigma s in (match EConstr.kind sigma sred with | Sort s' -> let s' = EConstr.ESorts.kind sigma s' in |