diff options
| -rw-r--r-- | CHANGES | 117 | ||||
| -rw-r--r-- | CREDITS | 39 | ||||
| -rwxr-xr-x | doc/common/macros.tex | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-ext.tex | 36 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 29 | ||||
| -rw-r--r-- | library/impargs.ml | 20 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 9 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | test-suite/success/unification.v | 8 |
9 files changed, 168 insertions, 93 deletions
@@ -5,86 +5,85 @@ Language - If a fixpoint is not written with an explicit { struct ... }, then all arguments are tried successively (from left to right) until one is - found that satisfies the structural decreasing condition. + found that satisfies the structural decreasing condition. (DOC TODO?) - Improved inference of implicit arguments. - New experimental typeclass system giving ad-hoc polymorphism and overloading based on dependent records and implicit arguments. -- New syntax "let| pat := b in c" for let-binding using irrefutable patterns. +- New syntax "let 'pat := b in c" for let-binding using irrefutable patterns. - New syntax "forall {A}, T" for specifying maximally inserted implicit arguments in terms. +- Sort of Record/Structure, Inductive and CoInductive defaults to Type + if omitted. (DOC TODO?) +- Record/Structure now usable for defining coinductive types + (e.g. "Record stream := { hd : nat; tl : stream }.") Commands -- Added option Global to "Implicit Arguments" and "Arguments Scope" for - section surviving. -- Added option "Unset Elimination Schemes" to deactivated the automatic - generation of elimination schemes. +- Added option Global to "Arguments Scope" for section surviving. (DOC TODO) +- Added option "Unset Elimination Schemes" to deactivate the automatic + generation of elimination schemes. (DOC TODO) - Modification of the Scheme command so you can ask for the name to be - automatically computed (e.g. Scheme Induction for nat Sort Set). + automatically computed (e.g. Scheme Induction for nat Sort Set). (DOC TODO?) - New command "Combined Scheme" to build combined mutual induction - principles from existing mutual induction principles. -- New commad "Scheme Equality" tries to build a decidable (boolean) equality - for simple inductive datatypes and a decision property over this equality. - e.g. Scheme Equality for nat. + principles from existing mutual induction principles. +- New command "Scheme Equality" to build a decidable (boolean) equality + for simple inductive datatypes and a decision property over this equality + (e.g. Scheme Equality for nat). - Added option "Set Equality Scheme" to make automatic the declaration - of the boolean equality when possible. + of the boolean equality when possible. (DOC TODO?) - Source of universe inconsistencies now printed when option "Set Printing Universes" is activated, -- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the "compute" - reduction strategy, respectively meaning reduce only, or everything - but, the constants id1 ... idn. "lazy" alone or followed by +- Support for option "[id1 ... idn]", and "-[id1 ... idn]", for the + "compute"/"cbv" reduction strategy, respectively meaning reduce only, or + everything but, the constants id1 ... idn. "lazy" alone or followed by "[id1 ... idn]", and "-[id1 ... idn]" also supported, meaning apply all of beta-iota-zeta-delta, possibly restricting delta. -Libraries +Libraries (DOC TO CHECK) -- library IntMap, subsumed by FSets/FMaps, has been removed from +- New arithmetical libraries: + - Numbers contains an abstract modular development of natural and integer + arithmetics. + - Ints contains a library of efficient computational bounded and + unbounded integers that can be mapped to processor native arithmetics. +- Library IntMap, subsumed by FSets/FMaps, has been removed from Coq Standard Library and moved into a user contribution Cachan/IntMap - Better computational behavior of some constants (eq_nat_dec and le_lt_dec more efficient, Z_lt_le_dec and Positive_as_OT.compare - transparent, ...) [exceptional source of incompatibilities]. + transparent, ...) (exceptional source of incompatibilities). - Boolean operators moved from module Bool to module Datatypes. - Improvements to NArith (Nminus, Nmin, Nmax), and to QArith (in particular a better power function). -- In SetoidList, eqlistA now express that two lists have similar elements +- In SetoidList, eqlistA now expresses that two lists have similar elements at the same position, while the predicate previously called eqlistA - is now equivlistA (this one only states that the lists contains the same + is now equivlistA (this one only states that the lists contain the same elements, nothing more). -- In ListSet, a few definitions are now in Type (may induce possible - incompatibilities) -- Changes in FSets/FMaps. +- In ListSet, a few definitions are now in Type (may induce a few + incompatibilities). +- Changes in FSets/FMaps: - Improvements: in particular FMap now provides an induction principle - on maps, and some properties about FSets and fold need less hypothesis. + on maps, and some properties about FSets and fold needs less hypotheses. The polymorphic parameter for the fold function is now in Type. - Loading FSets/FMap used to open unwanted scopes of integer datatypes (see bug #1347). These scopes may need to be opened manually now. - - Hints in FSetInterface.v have been transfered from the core database + - Hints in FSetInterface.v have been transfered from the "core" database to a "set" database, and some expensive hints have been downgraded as "Immediate". A compatibility "oldset" database retains these expensive hints, so using "(e)auto with set oldset" should help porting scripts. Same for FSetWeakInterface and FMap(Weak)Interface. - Changes in Reals: - - most statement in "sigT" (including the + - Most statement in "sigT" (including the completeness axiom) are now in "sig" (in case of incompatibility, - use proj1_sig instead of projT1, sig instead of sigT, etc), - - more uniform naming scheme (identifiers in French moved to English, - consistent use of 0 -- zero -- instead of O -- letter O --, etc) - - lemma on prod_f_SO is now on prod_f_R0, - - useless hypothesis of ln_exists1 dropped, - - new Rlogic.v states a few logical properties about R axioms, - - RIneq.v extended and made cleaner, - - slightly more powerful "real" hints database (Rle_ge now fully usable as - a hint, occasionally leading to a few more subgoals automatically proved) + use proj1_sig instead of projT1, sig instead of sigT, etc). + - More uniform naming scheme (identifiers in French moved to English, + consistent use of 0 -- zero -- instead of O -- letter O --, etc). + - Lemma on prod_f_SO is now on prod_f_R0. + - Useless hypothesis of ln_exists1 dropped. + - New Rlogic.v states a few logical properties about R axioms. + - RIneq.v extended and made cleaner. - Slight restructuration of the Logic library regarding choice and classical logic. Addition of files providing intuitionistic axiomatizations of - descriptions: Epsilon.v, Description.v and IndefiniteDescription.v - -Language - -- Sort of Record/Structure, Inductive and CoInductive defaults to Type - if omitted -- Record/Structure now usable for defining coinductive types - (e.g. "Record stream := { hd : nat; tl : stream }.") + descriptions: Epsilon.v, Description.v and IndefiniteDescription.v. Notations and implicit arguments @@ -94,7 +93,10 @@ Notations and implicit arguments - New modifiers in "Implicit Arguments" to force an implicit argument to be maximally inserted and/or forced if it is not seen as inferable. - New modifier of "Implicit Arguments" to enrich the set of implicit arguments. -- Level "constr" moved from 9 to 8. + (DOC TODO?) +- New options Global and Local to "Implicit Arguments" for section + surviving or non export outside module. +- Level "constr" moved from 9 to 8. (DOC TODO?) - Structure/Record now printed as Record (unless option Printing All is set). - Support for parametric notations defining constants (i.e. abbreviations). @@ -102,13 +104,13 @@ Tactic Language - Second-order pattern-matching now working in Ltac "match" clauses (syntax for second-order unification variable is "@?X"). -- Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer) +- Ltac accepts integer arguments (syntax is "ltac:nnn" for nnn an integer). - The general sequence tactical "expr_0 ; [ expr_1 | ... | expr_n ]" is extended so that at most one expr_i may have the form "expr .." or just "..". Also, n can be different from the number of subgoals generated by expr_0. In this case, the value of expr (or idtac in case of just "..") is applied to the intermediate subgoals to make - the number of tactics equal to the number of subgoals. + the number of tactics equal to the number of subgoals. (DOC TODO) - A name used as the name of the parameter of a lemma (like f in "apply f_equal with (f:=t)") is now interpreted as a ltac variable if such a variable exists (this is a possible source of @@ -116,18 +118,20 @@ Tactic Language ltac function into names that do not clash with the lemmas parameter names used in the tactic). - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression. -- "let rec ... in ... " now supports for expressions without explicit + (DOC TODO?) +- "let rec ... in ... " now supported for expressions without explicit parameters; interpretation is lazy to the contrary of "let ... in ..."; hence, the "rec" keyword can be used to turn the argument of a "let ... in ..." into a lazy one. +- Patterns for hypotheses types in "match goal" are now interpreted in + type_scope. Tactics - New tactics [apply -> term], [apply <- term], [apply -> term in - ident], [apply <- term in ident] for applying equivalences (iff). + ident], [apply <- term in ident] for applying equivalences (iff). (DOC TODO) - Slight improvement of the hnf and simpl tactics when applied on expressions with explicit occurrences of match or fix. -- Better heuristic of lemma unfolding for apply/eapply. - New tactics "eapply in", "erewrite", "erewrite in". - Unfoldable references can be given by notation's string rather than by name in unfold. @@ -147,15 +151,14 @@ Tactics - New syntax "rename a into b, c into d" for "rename a into b; rename c into d" - New tactic "dependent induction H [ generalizing id_1 .. id_n ]" to do induction-inversion on instantiated inductive families à la BasicElim. -- Tactic apply now able to reason modulo unfolding of constants +- Tactic "apply" now able to reason modulo unfolding of constants (possible source of incompatibility in situations where apply may fail, e.g. as argument of a try or a repeat and in a ltac function); version of apply that does not unfold is renamed into "simple apply" (usable for compatibility or for automation). -- Tactic apply now able to traverse conjunctions and to select the first +- Tactic "apply" now able to traverse conjunctions and to select the first matching lemma among the components of the conjunction; tactic apply also able to apply lemmas of conclusion an empty type. -- Pattern for hypotheses types in match goal are now interpreted in type_scope. Type Classes @@ -187,13 +190,13 @@ Program "let" in Programs). - Program CoFixpoint is accepted, Program Fixpoint uses the new way to infer which argument decreases structurally. -- Program Lemma, Axiom etc... now permit to have obligations in the statement iff - they can be automatically solved by the default tactic. +- Program Lemma, Axiom etc... now permit to have obligations in the statement + iff they can be automatically solved by the default tactic. - New command "Preterm [ of id ]" to see the actual term fed to Coq for debugging purposes. -- Changed the notations "left" and "right" to "in_left" and "in_right" to hide the - proofs in standard disjunctions, to avoid breaking existing scripts when importing - Program. Also, put them in program_scope. +- Changed the notations "left" and "right" to "in_left" and "in_right" to hide + the proofs in standard disjunctions, to avoid breaking existing scripts when + importing Program. Also, put them in program_scope. Tools @@ -1,6 +1,6 @@ The "Coq proof assistant" was jointly developed by -- INRIA Formel, Coq, LogiCal, ProVal projects (since 1985), +- INRIA Formel, Coq, LogiCal, ProVal, TypiCal projects (since 1985), - Laboratoire de l'Informatique du Parallelisme (LIP) associated to CNRS and ENS Lyon (Sep. 1989 to Aug. 1997), - Laboratoire de Recherche en Informatique (LRI) @@ -14,7 +14,7 @@ All files of the "Coq proof assistant" in directories or sub-directories of scripts states tactics test-suite theories tools toplevel are distributed under the terms of the GNU Lesser General Public License -Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2006, +Version 2.1 (see file LICENSE). These files are COPYRIGHT 1999-2008, The Coq development team, CNRS, INRIA and Université Paris Sud. Files from the directory doc are distributed as indicated in file doc/LICENCE. @@ -24,26 +24,30 @@ by the Coq development team. All of them are released under the terms of the GNU Lesser General Public License Version 2.1. contrib/cc - developed by Pierre Corbineau (ENS Cachan, 2001 and LRI, 2001-2005) + developed by Pierre Corbineau (ENS Cachan, 2001, LRI, 2001-2005, Radboud + University at Nijmegen, 2005-2008) contrib/correctness developed by Jean-Christophe Filliâtre (LRI, 1999-2001) contrib/dp - developed by Nicolas Ayache and Jean-Christophe Filliâtre (LRI, 2005-2006) + developed by Nicolas Ayache (LRI, 2005-2006) and Jean-Christophe Filliâtre + (LRI, 2005-2008) contrib/extraction - developed by Pierre Letouzey (LRI, 2000-2006) + developed by Pierre Letouzey (LRI, 2000-2008) contrib/field developed by David Delahaye and Micaela Mayero (INRIA-LogiCal, 2001) contrib/first-order - developed by Pierre Corbineau (LRI, 2003-2005) + developed by Pierre Corbineau (LRI, 2003-2008) contrib/fourier developed by Loïc Pottier (INRIA-Lemme, 2001) contrib/funind - developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2006), - Julien Forest (INRIA-Everest, 2006) - and Yves Bertot (INRIA-Marelle, 2005-2006). + developed by Pierre Courtieu (INRIA-Lemme, 2003-2004, CNAM, 2004-2008), + Julien Forest (INRIA-Everest, 2006, CNAM, 2007-2008) + and Yves Bertot (INRIA-Marelle, 2005-2006) contrib/interface developed by Yves Bertot with contributions from Loïc Pottier and - Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006) + Laurence Rideau as part of the Pcoq project (INRIA-Lemme, 1997-2006); + extended by Lionel Mamane as part of the TeXMacs project (Radboud university + at Nijmegen, 2007-2008) contrib/omega developed by Pierre Crégut (France Telecom R&D, 1996) contrib/recdef @@ -60,11 +64,11 @@ contrib/setoid_ring Assia Mahboubi, Laurent Théry (INRIA-Marelle, 2006) and Bruno Barras (INRIA LogiCal, 2005-2006), contrib/subtac - developed by Matthieu Sozeau (LRI, 2005-2006) + developed by Matthieu Sozeau (LRI, 2005-2008) contrib/xml developed by Claudio Sacerdoti (Univ. Bologna, 2000-2005) - as part of the HELM and MoWGLI projects - + as part of the HELM and MoWGLI projects; extension by Cezary Kaliszyk as + part of the ProofWeb project (Radbout University at Nijmegen, 2008) parsing/search.ml mainly developed by Yves Bertot (INRIA-Lemme, 2000-2004) theories/ZArith @@ -84,11 +88,12 @@ influenced significantly the design of Coq especially with Intensive users suggested improvements of the system : - Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme projects), + Y. Bertot, L. Pottier, L. Théry (INRIA-Lemme/Marelle projects), C. Alvarado, P. Crégut, J.-F. Monin (France Telecom R&D), P. Castéran (University Bordeaux 1), The Foundations Group (Radboud University, Nijmegen, The Netherlands), - Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis). + Laboratoire J.-A. Dieudonné (University of Nice-Sophia Antipolis), + G. Gonthier (INRIA-MSR joint lab), A. Charguéraud (INRIA-Gallium project). The following people have contributed to the development of different versions of the Coq Proof assistant during the indicated time : @@ -117,13 +122,15 @@ of the Coq Proof assistant during the indicated time : César Muñoz (INRIA, 1994-1995) Chetan Murthy (INRIA, 1992-1994) Julien Narboux (INRIA, 2005-2006) - Jean-Marc Notin (CNRS, 2006) + Jean-Marc Notin (CNRS, 2006-now) Catherine Parent-Vigouroux (ENS Lyon, 1992-1995) Patrick Loiseleur (Paris Sud, 1997-1999) Christine Paulin-Mohring (INRIA, 1985-1989, ENS Lyon, 1989-1997, LRI, 1997-now) Clément Renard (INRIA, 2001-2004) Claudio Sacerdoti Coen (INRIA, 2004-2005) + Matthieu Sozeau (INRIA, 2005-now) + Arnaud Spiwack (INRIA, 2006-now) Amokrane Saïbi (INRIA, 1993-1998) Benjamin Werner (INRIA, 1989-1994) diff --git a/doc/common/macros.tex b/doc/common/macros.tex index 47409b984..3bfe09c16 100755 --- a/doc/common/macros.tex +++ b/doc/common/macros.tex @@ -213,6 +213,7 @@ \newcommand{\onemodbinding}{\textrm{\textsl{module\_binding}}} \newcommand{\modbindings}{\textrm{\textsl{module\_bindings}}} \newcommand{\qualid}{\textrm{\textsl{qualid}}} +\newcommand{\qualidorstring}{\textrm{\textsl{qualid\_or\_string}}} \newcommand{\class}{\textrm{\textsl{class}}} \newcommand{\dirpath}{\textrm{\textsl{dirpath}}} \newcommand{\typedidents}{\textrm{\textsl{typed\_idents}}} diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex index de6b93b42..c19e01538 100644 --- a/doc/refman/RefMan-ext.tex +++ b/doc/refman/RefMan-ext.tex @@ -1183,6 +1183,23 @@ After the above declaration is issued, implicit arguments can just (and have to) be skipped in any expression involving an application of {\qualid}. +\begin{Variants} +\item {\tt Implicit Arguments Global {\qualid} [ \nelist{\possiblybracketedident}{} ] +\comindex{Implicit Arguments Global}} + +Tells to recompute the implicit arguments of {\qualid} after ending of +the current section if any, enforcing the implicit arguments known +from inside the section to be the ones declared by the command. + +\item {\tt Implicit Arguments Local {\qualid} [ \nelist{\possiblybracketedident}{} ] +\comindex{Implicit Arguments Local}} + +When in a module, tells not to activate the implicit arguments of +{\qualid} declared by this commands to contexts that requires the +module. + +\end{Variants} + \Example \begin{coq_eval} Reset Initial. @@ -1217,7 +1234,8 @@ implicit arguments of {\qualid}. {\Coq} can also automatically detect what are the implicit arguments of a defined object. The command is just \begin{quote} -\tt Implicit Arguments {\qualid}. +{\tt Implicit Arguments {\qualid} +\comindex{Implicit Arguments}} \end{quote} The auto-detection is governed by options telling if strict, contextual, or reversible-pattern implicit arguments must be @@ -1225,6 +1243,22 @@ considered or not (see Sections~\ref{SetStrictImplicit},~\ref{SetContextualImplicit},~\ref{SetReversiblePatternImplicit} and also~\ref{SetMaximalImplicitInsertion}). +\begin{Variants} +\item {\tt Implicit Arguments Global {\qualid} +\comindex{Implicit Arguments Global}} + +Tells to recompute the implicit arguments of {\qualid} after ending of +the current section if any. + +\item {\tt Implicit Arguments Local {\qualid} +\comindex{Implicit Arguments Local}} + +When in a module, tells not to activate the implicit arguments of +{\qualid} computed by this declaration to contexts that requires the +module. + +\end{Variants} + \Example \begin{coq_eval} Reset Initial. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index f5bef115f..a51e97d95 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -642,6 +642,12 @@ This does the same but uses the bindings in each {\bindinglist} to instantiate the parameters of the corresponding type of {\term} (see syntax of bindings in Section~\ref{Binding-list}). +\item {\tt eapply \nelist{{\term} {\bindinglist}}{,} in {\ident}} + +This works as {\tt apply \nelist{{\term} {\bindinglist}}{,} in +{\ident}} but turns unresolved bindings into existential variables, if +any, instead of failing. + \end{Variants} \subsection{\tt generalize \term @@ -1086,6 +1092,19 @@ with its $\beta\iota$-normal form. \ErrMsg {\qualid}$_i$ {\tt does not occur} +\item {\tt unfold {\qstring}} + + If {\qstring} denotes the discriminating symbol of a notation (e.g. {\tt + "+"}) or an expression defining a notation (e.g. \verb!"_ + _"!), and + this notation refers to an unfoldable constant, then the tactic + unfolds it. + +\item {\tt unfold \qualidorstring$_1$ at \num$_1^1$, \dots, \num$_i^1$, +\dots,\ \qualidorstring$_n$ at \num$_1^n$ \dots\ \num$_j^n$} + + This is the most general form, where {\qualidorstring} is either a + {\qualid} or a {\qstring} referring to a notation. + \end{Variants} \subsection{{\tt fold} \term @@ -1980,6 +1999,11 @@ This happens if \term$_1$ does not occur in the goal. of $\term$ will be done, leading to failure if these $n$ rewrites are not possible. \end{itemize} +\item {\tt erewrite {\term}\tacindex{erewrite}} + +This tactic works as {\tt rewrite {\term}} but turning unresolved +bindings into existential variables, if any, instead of failing. It has +the same variants as {\tt rewrite} has. \end{Variants} @@ -3596,6 +3620,7 @@ The tactic {\tt exists (n // m)} did not fail. The hole was solved by \section{Generation of induction principles with {\tt Scheme} \label{Scheme} +\index{Schemes} \comindex{Scheme}} The {\tt Scheme} command is a high-level tool for generating @@ -3624,7 +3649,7 @@ general principle of mutual induction for objects in type {\term$_i$}. Same as before but defines a non-dependent elimination principle more natural in case of inductively defined relations. -\item {\tt Scheme Equality for \ident$_1$} +\item {\tt Scheme Equality for \ident$_1$\comindex{Scheme Equality}} Tries to generate a boolean equality and a proof of the decidability of the usual equality. @@ -3658,8 +3683,6 @@ generates {\ident$_0$} to be the conjunction of the principles: it is built from the common premises of the principles and concluded by the conjunction of their conclusions. -\SeeAlso \ref{CombinedScheme-examples} - \SeeAlso Section~\ref{CombinedScheme-examples} \section{Generation of induction principles with {\tt Functional Scheme} diff --git a/library/impargs.ml b/library/impargs.ml index fc2d63ca8..79abdb4c9 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -428,7 +428,7 @@ type implicit_interactive_request = | ImplManual of implicit_status list type implicit_discharge_request = - | ImplNoDischarge + | ImplLocal | ImplConstant of constant * implicits_flags | ImplMutualInductive of kernel_name * implicits_flags | ImplInteractive of global_reference * implicits_flags * @@ -451,11 +451,11 @@ let subst_implicits_decl subst (r,imps as o) = let r' = fst (subst_global subst r) in if r==r' then o else (r',imps) let subst_implicits (_,subst,(req,l)) = - (ImplNoDischarge,list_smartmap (subst_implicits_decl subst) l) + (ImplLocal,list_smartmap (subst_implicits_decl subst) l) let discharge_implicits (_,(req,l)) = match req with - | ImplNoDischarge -> None + | ImplLocal -> None | ImplInteractive (ref,flags,exp) -> Some (ImplInteractive (pop_global_reference ref,flags,exp),l) | ImplConstant (con,flags) -> @@ -469,7 +469,7 @@ let rebuild_implicits (info,(req,l)) = [] info in let l' = match req with - | ImplNoDischarge -> assert false + | ImplLocal -> assert false | ImplConstant (con,flags) -> [ConstRef con, compute_constant_implicits flags manual con] | ImplMutualInductive (kn,flags) -> @@ -482,7 +482,9 @@ let rebuild_implicits (info,(req,l)) = (* let auto = if flags.main then auto else List.map (fun _ -> None) auto in *) let l' = merge_impls auto l in [ref,l'] in (req,l') - + +let export_implicits (req,_ as x) = + if req = ImplLocal then None else Some x let (inImplicits, _) = declare_object {(default_object "IMPLICITS") with @@ -492,7 +494,7 @@ let (inImplicits, _) = classify_function = (fun (_,x) -> Substitute x); discharge_function = discharge_implicits; rebuild_function = rebuild_implicits; - export_function = (fun x -> Some x) } + export_function = export_implicits } let declare_implicits_gen req flags ref = let imps = compute_global_implicits flags [] ref in @@ -501,12 +503,12 @@ let declare_implicits_gen req flags ref = let declare_implicits local ref = let flags = { !implicit_args with main = true } in let req = - if local then ImplNoDischarge else ImplInteractive(ref,flags,ImplAuto) in + if local then ImplLocal else ImplInteractive(ref,flags,ImplAuto) in declare_implicits_gen req flags ref let declare_var_implicits id = if !implicit_args.main then - declare_implicits_gen ImplNoDischarge !implicit_args (VarRef id) + declare_implicits_gen ImplLocal !implicit_args (VarRef id) let declare_constant_implicits con = if !implicit_args.main then @@ -534,7 +536,7 @@ let declare_manual_implicits local ref enriching l = let t = Global.type_of_global ref in let l' = compute_manual_implicits env flags t enriching l in let req = - if local or isVarRef ref then ImplNoDischarge + if local or isVarRef ref then ImplLocal else ImplInteractive(ref,flags,ImplManual l') in add_anonymous_leaf (inImplicits (req,[ref,l'])) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index ae860d978..45c16a133 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -503,13 +503,10 @@ GEXTEND Gram (* Implicit *) | IDENT "Implicit"; IDENT "Arguments"; enrich = [ IDENT "Enriching" -> true | -> false ]; - (local,qid,pos) = - [ local = [ IDENT "Global" -> false | IDENT "Local" -> true ]; - qid = global -> (local,qid,None) - | qid = global; - l = OPT [ "["; l = LIST0 implicit_name; "]" -> + local = [ IDENT "Global" -> false | IDENT "Local" -> true | -> Lib.sections_are_opened () ]; + qid = global; + pos = OPT [ "["; l = LIST0 implicit_name; "]" -> List.map (fun (id,b,f) -> (ExplByName id,b,f)) l ] -> - (true,qid,l) ] -> VernacDeclareImplicits (local,qid,enrich,pos) | IDENT "Implicit"; ["Type" | IDENT "Types"]; diff --git a/tactics/inv.ml b/tactics/inv.ml index 03eaf2d4d..a77a97906 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -450,7 +450,7 @@ let raw_inversion inv_kind id status names gl = let env = pf_env gl and sigma = project gl in let c = mkVar id in let (ind,t) = - try pf_reduce_to_quantified_ind gl (pf_type_of gl c) + try pf_reduce_to_atomic_ind gl (pf_type_of gl c) with UserError _ -> errorlabstrm "raw_inversion" (str ("The type of "^(string_of_id id)^" is not inductive")) in diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v index e31d67d8c..51b0e06e5 100644 --- a/test-suite/success/unification.v +++ b/test-suite/success/unification.v @@ -109,3 +109,11 @@ intros. apply H0. (* Check that equation ?n[H] = ?n[H] is correctly considered true *) reflexivity. Qed. + +(* Check treatment of metas erased by K-redexes at the time of turning + them to evas *) + +Inductive nonemptyT (t : Type) : Prop := nonemptyT_intro : t -> nonemptyT t. +Goal True. +try case nonemptyT_intro. (* check that it fails w/o anomaly *) +Abort. |