diff options
70 files changed, 348 insertions, 719 deletions
@@ -148,6 +148,7 @@ of the Coq Proof assistant during the indicated time: Pierre-Marie Pédrot (INRIA-PPS, 2011-2015, INRIA-Ascola, 2015-2016, University of Ljubljana, 2016-2017, MPI-SWS, 2017-2018) + Clément Pit-Claudel (MIT, 2015-2018) Matthias Puech (INRIA-Bologna, 2008-2011) Yann Régis-Gianas (INRIA-PPS then IRIF, 2009-now) Clément Renard (INRIA, 2001-2004) diff --git a/checker/cic.mli b/checker/cic.mli index 42629ced2..c4b00d0dc 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -104,7 +104,7 @@ type constr = | Case of case_info * constr * constr * constr array | Fix of constr pfixpoint | CoFix of constr pcofixpoint - | Proj of projection * constr + | Proj of Projection.t * constr type existential = constr pexistential type rec_declaration = constr prec_declaration diff --git a/checker/closure.ml b/checker/closure.ml index 184af0e13..bfba6c161 100644 --- a/checker/closure.ml +++ b/checker/closure.ml @@ -251,7 +251,7 @@ and fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) @@ -281,7 +281,7 @@ let update v1 (no,t) = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * projection + | Zproj of int * int * Projection.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr diff --git a/checker/closure.mli b/checker/closure.mli index f68c0468a..4cf02ae2b 100644 --- a/checker/closure.mli +++ b/checker/closure.mli @@ -87,7 +87,7 @@ type fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) @@ -107,7 +107,7 @@ type fterm = type stack_member = | Zapp of fconstr array | ZcaseT of case_info * constr * constr array * fconstr subs - | Zproj of int * int * projection + | Zproj of int * int * Projection.t | Zfix of fconstr * stack | Zshift of int | Zupdate of fconstr diff --git a/checker/environ.mli b/checker/environ.mli index 36e0ea027..81da83875 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -58,7 +58,7 @@ val constant_value : env -> Constant.t puniverses -> constr val evaluable_constant : Constant.t -> env -> bool val is_projection : Constant.t -> env -> bool -val lookup_projection : projection -> env -> projection_body +val lookup_projection : Projection.t -> env -> projection_body (* Inductives *) val mind_equiv : env -> inductive -> inductive -> bool diff --git a/checker/reduction.ml b/checker/reduction.ml index 97255dd49..072dec63f 100644 --- a/checker/reduction.ml +++ b/checker/reduction.ml @@ -54,7 +54,7 @@ let compare_stack_shape stk1 stk2 = type lft_constr_stack_elt = Zlapp of (lift * fconstr) array - | Zlproj of Names.projection * lift + | Zlproj of Names.Projection.t * lift | Zlfix of (lift * fconstr) * lft_constr_stack | Zlcase of case_info * lift * fconstr * fconstr array and lft_constr_stack = lft_constr_stack_elt list @@ -142,7 +142,7 @@ let compare_stacks f fmind lft1 stk1 lft2 stk2 = | (Zlfix(fx1,a1),Zlfix(fx2,a2)) -> f fx1 fx2; cmp_rec a1 a2 | (Zlproj (c1,l1),Zlproj (c2,l2)) -> - if not (Names.eq_con_chk + if not (Names.Constant.UserOrd.equal (Names.Projection.constant c1) (Names.Projection.constant c2)) then raise NotConvertible diff --git a/checker/subtyping.ml b/checker/subtyping.ml index ee73eb1ab..5cb38cb81 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -224,7 +224,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= | Some None, Some None -> true | Some (Some (id1,p1,pb1)), Some (Some (id2,p2,pb2)) -> Id.equal id1 id2 && - Array.for_all2 eq_con_chk p1 p2 && + Array.for_all2 Constant.UserOrd.equal p1 p2 && Array.for_all2 eq_projection_body pb1 pb2 | _, _ -> false in diff --git a/checker/term.ml b/checker/term.ml index 19034a57d..0236f7867 100644 --- a/checker/term.ml +++ b/checker/term.ml @@ -390,7 +390,7 @@ let compare_constr f t1 t2 = f h1 h2 && List.for_all2 f l1 l2 else false | Evar (e1,l1), Evar (e2,l2) -> Int.equal e1 e2 && Array.equal f l1 l2 - | Const c1, Const c2 -> eq_puniverses eq_con_chk c1 c2 + | Const c1, Const c2 -> eq_puniverses Constant.UserOrd.equal c1 c2 | Ind c1, Ind c2 -> eq_puniverses eq_ind_chk c1 c2 | Construct ((c1,i1),u1), Construct ((c2,i2),u2) -> Int.equal i1 i2 && eq_ind_chk c1 c2 && Univ.Instance.equal u1 u2 diff --git a/checker/values.ml b/checker/values.ml index 160653d9b..1ac8d7cef 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -15,7 +15,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 2c3436106636784886f122c8ab578098 checker/cic.mli +MD5 c4fdf8a846aed45c27b5acb1add7d1c6 checker/cic.mli *) diff --git a/clib/cArray.ml b/clib/cArray.ml index 5eb20bc16..071f4689b 100644 --- a/clib/cArray.ml +++ b/clib/cArray.ml @@ -62,9 +62,12 @@ sig val fold_left2_map : ('a -> 'b -> 'c -> 'a * 'd) -> 'a -> 'b array -> 'c array -> 'a * 'd array val fold_right2_map : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array + [@@ocaml.deprecated "Same as [fold_left_map]"] val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c + [@@ocaml.deprecated "Same as [fold_right_map]"] val fold_map2' : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c + [@@ocaml.deprecated "Same as [fold_right2_map]"] val distinct : 'a array -> bool val rev_of_list : 'a list -> 'a array val rev_to_list : 'a array -> 'a list diff --git a/clib/cArray.mli b/clib/cArray.mli index f4f60f8aa..9c2f521f4 100644 --- a/clib/cArray.mli +++ b/clib/cArray.mli @@ -114,14 +114,14 @@ sig (** Same with two arrays, folding on the left *) val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b array -> 'a * 'c array - (** @deprecated Same as [fold_left_map] *) + [@@ocaml.deprecated "Same as [fold_left_map]"] val fold_map' : ('a -> 'c -> 'b * 'c) -> 'a array -> 'c -> 'b array * 'c - (** @deprecated Same as [fold_right_map] *) + [@@ocaml.deprecated "Same as [fold_right_map]"] val fold_map2' : ('a -> 'b -> 'c -> 'd * 'c) -> 'a array -> 'b array -> 'c -> 'd array * 'c - (** @deprecated Same as [fold_right2_map] *) + [@@ocaml.deprecated "Same as [fold_right2_map]"] val distinct : 'a array -> bool (** Return [true] if every element of the array is unique (for default diff --git a/clib/cList.ml b/clib/cList.ml index 80bb18477..8727f4696 100644 --- a/clib/cList.ml +++ b/clib/cList.ml @@ -102,7 +102,9 @@ sig val fold_left3_map : ('a -> 'b -> 'c -> 'd -> 'a * 'e) -> 'a -> 'b list -> 'c list -> 'd list -> 'a * 'e list val fold_left4_map : ('a -> 'b -> 'c -> 'd -> 'e -> 'a * 'r) -> 'a -> 'b list -> 'c list -> 'd list -> 'e list -> 'a * 'r list val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list + [@@ocaml.deprecated "Same as [fold_left_map]"] val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a + [@@ocaml.deprecated "Same as [fold_right_map]"] val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b val remove_assoc_f : 'a eq -> 'a -> ('a * 'b) list -> ('a * 'b) list diff --git a/clib/cList.mli b/clib/cList.mli index db37050aa..fd6d6a158 100644 --- a/clib/cList.mli +++ b/clib/cList.mli @@ -228,11 +228,10 @@ sig (** Same with four lists, folding on the left *) val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b list -> 'a * 'c list - (* [@@ocaml.deprecated "Same as [fold_left_map]"] *) - (** @deprecated Same as [fold_left_map] *) + [@@ocaml.deprecated "Same as [fold_left_map]"] val fold_map' : ('b -> 'a -> 'c * 'a) -> 'b list -> 'a -> 'c list * 'a - (** @deprecated Same as [fold_right_map] *) + [@@ocaml.deprecated "Same as [fold_right_map]"] val map_assoc : ('a -> 'b) -> ('c * 'a) list -> ('c * 'b) list val assoc_f : 'a eq -> 'a -> ('a * 'b) list -> 'b diff --git a/clib/option.mli b/clib/option.mli index 67b42268a..14fa9da38 100644 --- a/clib/option.mli +++ b/clib/option.mli @@ -98,6 +98,7 @@ val fold_right_map : ('b -> 'a -> 'c * 'a) -> 'b option -> 'a -> 'c option * 'a (** @deprecated Same as [fold_left_map] *) val fold_map : ('a -> 'b -> 'a * 'c) -> 'a -> 'b option -> 'a * 'c option +[@@ocaml.deprecated "Same as [fold_left_map]"] (** [cata f e x] is [e] if [x] is [None] and [f a] if [x] is [Some a] *) val cata : ('a -> 'b) -> 'b -> 'a option -> 'b diff --git a/doc/sphinx/addendum/miscellaneous-extensions.rst b/doc/sphinx/addendum/miscellaneous-extensions.rst index b0343a8f0..3ed4ce762 100644 --- a/doc/sphinx/addendum/miscellaneous-extensions.rst +++ b/doc/sphinx/addendum/miscellaneous-extensions.rst @@ -5,9 +5,6 @@ Miscellaneous extensions ======================= -:Source: https://coq.inria.fr/distrib/current/refman/miscellaneous.html -:Converted by: Paul Steckler - .. contents:: :local: :depth: 1 diff --git a/doc/sphinx/addendum/type-classes.rst b/doc/sphinx/addendum/type-classes.rst index becebb421..5518da9ac 100644 --- a/doc/sphinx/addendum/type-classes.rst +++ b/doc/sphinx/addendum/type-classes.rst @@ -5,9 +5,6 @@ Type Classes ============ -:Source: https://coq.inria.fr/distrib/current/refman/type-classes.html -:Author: Matthieu Sozeau - This chapter presents a quick reference of the commands related to type classes. For an actual introduction to type classes, there is a description of the system :cite:`sozeau08` and the literature on type diff --git a/doc/sphinx/credits.rst b/doc/sphinx/credits.rst index fac0d0a4f..f3d9f57b4 100644 --- a/doc/sphinx/credits.rst +++ b/doc/sphinx/credits.rst @@ -1307,9 +1307,9 @@ features and deprecations, cleanups of the internals of the system along with a few new features. The main user visible changes are: - Kernel: fix a subject reduction failure due to allowing fixpoints - on non-recursive values, which allows to recover full parametricity - for CIC, by Matthieu Sozeau. Handling of evars in the VM (the kernel - still does not accept evars) by Pierre-Marie Pédrot. + on non-recursive values, by Matthieu Sozeau. + Handling of evars in the VM (the kernel still does not accept evars) + by Pierre-Marie Pédrot. - Notations: many improvements on recursive notations and support for destructuring patterns in the syntax of notations by Hugo Herbelin. @@ -1338,7 +1338,14 @@ with a few new features. The main user visible changes are: - Documentation: a large community effort resulted in the migration of the reference manual to the Sphinx documentation tool. The result - is this manual. + is this manual. The new documentation infrastructure (based on Sphinx) + is by Clément Pit-Claudel. The migration was coordinated by Maxime Dénès + and Paul Steckler, with some help of Théo Zimmermann during the + final integration phase. The 14 people who ported the manual are + Calvin Beck, Heiko Becker, Yves Bertot, Maxime Dénès, Richard Ford, + Pierre Letouzey, Assia Mahboubi, Clément Pit-Claudel, + Laurence Rideau, Matthieu Sozeau, Paul Steckler, Enrico Tassi, + Laurent Théry, Nikita Zyuzin. - Tools: experimental ``-mangle-names`` option to coqtop/coqc for linting proof scripts, by Jasper Hugunin. diff --git a/doc/sphinx/introduction.rst b/doc/sphinx/introduction.rst index 514745c1b..67de2ae68 100644 --- a/doc/sphinx/introduction.rst +++ b/doc/sphinx/introduction.rst @@ -2,7 +2,7 @@ Introduction ------------------------ -This document is the Reference Manual of version of the |Coq| proof +This document is the Reference Manual of the |Coq| proof assistant. A companion volume, the |Coq| Tutorial, is provided for the beginners. It is advised to read the Tutorial first. A book :cite:`CoqArt` on practical uses of the |Coq| system was diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 7ed652409..13d20d7cf 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -373,19 +373,22 @@ following rules. -**Remark**: **Prod-Prop** and **Prod-Set** typing-rules make sense if we consider the -semantic difference between :math:`\Prop` and :math:`\Set`: +.. note:: + **Prod-Prop** and **Prod-Set** typing-rules make sense if we consider the + semantic difference between :math:`\Prop` and :math:`\Set`: -+ All values of a type that has a sort :math:`\Set` are extractable. -+ No values of a type that has a sort :math:`\Prop` are extractable. + + All values of a type that has a sort :math:`\Set` are extractable. + + No values of a type that has a sort :math:`\Prop` are extractable. -**Remark**: We may have :math:`\letin{x}{t:T}{u}` well-typed without having -:math:`((λ x:T.u) t)` well-typed (where :math:`T` is a type of -:math:`t`). This is because the value :math:`t` associated to -:math:`x` may be used in a conversion rule (see Section :ref:`Conversion-rules`). +.. note:: + We may have :math:`\letin{x}{t:T}{u}` well-typed without having + :math:`((λ x:T.u) t)` well-typed (where :math:`T` is a type of + :math:`t`). This is because the value :math:`t` associated to + :math:`x` may be used in a conversion rule + (see Section :ref:`Conversion-rules`). .. _Conversion-rules: @@ -487,29 +490,31 @@ term :math:`t` of functional type :math:`∀ x:T, U` with its so-called η-expan for :math:`x` an arbitrary variable name fresh in :math:`t`. -**Remark**: We deliberately do not define η-reduction: +.. note:: -.. math:: - λ x:T. (t~x) \not\triangleright_η t + We deliberately do not define η-reduction: -This is because, in general, the type of :math:`t` need not to be convertible -to the type of :math:`λ x:T. (t~x)`. E.g., if we take :math:`f` such that: + .. math:: + λ x:T. (t~x) \not\triangleright_η t -.. math:: - f : ∀ x:\Type(2),\Type(1) + This is because, in general, the type of :math:`t` need not to be convertible + to the type of :math:`λ x:T. (t~x)`. E.g., if we take :math:`f` such that: + + .. math:: + f : ∀ x:\Type(2),\Type(1) -then + then -.. math:: - λ x:\Type(1),(f~x) : ∀ x:\Type(1),\Type(1) + .. math:: + λ x:\Type(1),(f~x) : ∀ x:\Type(1),\Type(1) -We could not allow + We could not allow -.. math:: - λ x:Type(1),(f x) \triangleright_η f + .. math:: + λ x:Type(1),(f x) \triangleright_η f -because the type of the reduced term :math:`∀ x:\Type(2),\Type(1)` would not be -convertible to the type of the original term :math:`∀ x:\Type(1),\Type(1).` + because the type of the reduced term :math:`∀ x:\Type(2),\Type(1)` would not be + convertible to the type of the original term :math:`∀ x:\Type(1),\Type(1).` .. _Convertibility: @@ -794,18 +799,18 @@ contains an inductive declaration. --------------------- E[Γ] ⊢ c : C -**Example.** -Provided that our environment :math:`E` contains inductive definitions we showed before, -these two inference rules above enable us to conclude that: +.. example:: + Provided that our environment :math:`E` contains inductive definitions we showed before, + these two inference rules above enable us to conclude that: -.. math:: - \begin{array}{l} + .. math:: + \begin{array}{l} E[Γ] ⊢ \even : \nat→\Prop\\ E[Γ] ⊢ \odd : \nat→\Prop\\ E[Γ] ⊢ \even\_O : \even~O\\ E[Γ] ⊢ \even\_S : \forall~n:\nat, \odd~n → \even~(S~n)\\ E[Γ] ⊢ \odd\_S : \forall~n:\nat, \even~n → \odd~(S~n) - \end{array} + \end{array} @@ -1135,9 +1140,10 @@ eliminations schemes are allowed. Check (fun (A:Prop) (B:Set) => prod A B). Check (fun (A:Type) (B:Prop) => prod A B). -Remark: Template polymorphism used to be called “sort-polymorphism of -inductive types” before universe polymorphism (see Chapter :ref:`polymorphicuniverses`) was -introduced. +.. note:: + Template polymorphism used to be called “sort-polymorphism of + inductive types” before universe polymorphism + (see Chapter :ref:`polymorphicuniverses`) was introduced. .. _Destructors: @@ -1473,20 +1479,20 @@ definition :math:`\ind{r}{Γ_I}{Γ_C}` with :math:`Γ_C = [c_1 :C_1 ;…;c_n :C_ -**Example.** -Below is a typing rule for the term shown in the previous example: - -.. inference:: list example - - \begin{array}{l} - E[Γ] ⊢ t : (\List ~\nat) \\ - E[Γ] ⊢ P : B \\ - [(\List ~\nat)|B] \\ - E[Γ] ⊢ f_1 : {(\kw{nil} ~\nat)}^P \\ - E[Γ] ⊢ f_2 : {(\kw{cons} ~\nat)}^P - \end{array} - ------------------------------------------------ - E[Γ] ⊢ \case(t,P,f_1 |f_2 ) : (P~t) +.. example:: + Below is a typing rule for the term shown in the previous example: + + .. inference:: list example + + \begin{array}{l} + E[Γ] ⊢ t : (\List ~\nat) \\ + E[Γ] ⊢ P : B \\ + [(\List ~\nat)|B] \\ + E[Γ] ⊢ f_1 : {(\kw{nil} ~\nat)}^P \\ + E[Γ] ⊢ f_2 : {(\kw{cons} ~\nat)}^P + \end{array} + ------------------------------------------------ + E[Γ] ⊢ \case(t,P,f_1 |f_2 ) : (P~t) .. _Definition-of-ι-reduction: diff --git a/doc/sphinx/language/coq-library.rst b/doc/sphinx/language/coq-library.rst index 29053d6a5..82ced65b4 100644 --- a/doc/sphinx/language/coq-library.rst +++ b/doc/sphinx/language/coq-library.rst @@ -5,9 +5,6 @@ The |Coq| library ================= -:Source: https://coq.inria.fr/distrib/current/refman/stdlib.html -:Converted by: Pierre Letouzey - .. index:: single: Theories diff --git a/doc/sphinx/language/gallina-extensions.rst b/doc/sphinx/language/gallina-extensions.rst index 1d6c11b38..687775980 100644 --- a/doc/sphinx/language/gallina-extensions.rst +++ b/doc/sphinx/language/gallina-extensions.rst @@ -41,7 +41,9 @@ Remark that the type of a particular identifier may depend on a previously-given order of the fields is important. Finally, each `param` is a parameter of the record. More generally, a record may have explicitly defined (a.k.a. manifest) -fields. For instance, we might have:: +fields. For instance, we might have: + +.. coqtop:: in Record ident param : sort := { ident₁ : type₁ ; ident₂ := term₂ ; ident₃ : type₃ }. @@ -50,6 +52,8 @@ may depend on |ident_1|. .. example:: + The set of rational numbers may be defined as: + .. coqtop:: reset all Record Rat : Set := mkRat @@ -169,7 +173,7 @@ and the syntax `term.(@qualid` |term_1| |term_n| `)` to `@qualid` |term_1| `…` In each case, `term` is the object projected and the other arguments are the parameters of the inductive type. -.. note::. Records defined with the ``Record`` keyword are not allowed to be +.. note:: Records defined with the ``Record`` keyword are not allowed to be recursive (references to the record's name in the type of its field raises an error). To define recursive records, one can use the ``Inductive`` and ``CoInductive`` keywords, resulting in an inductive or co-inductive record. @@ -181,7 +185,7 @@ other arguments are the parameters of the inductive type. defined with the ``Record`` keyword can be activated with the ``Nonrecursive Elimination Schemes`` option (see :ref:`TODO-13.1.1-nonrecursive-elimination-schemes`). -.. note::``Structure`` is a synonym of the keyword ``Record``. +.. note:: ``Structure`` is a synonym of the keyword ``Record``. .. warn:: @ident cannot be defined. @@ -217,7 +221,9 @@ the errors of inductive definitions, as described in Section Primitive Projections ~~~~~~~~~~~~~~~~~~~~~ -The option ``Set Primitive Projections`` turns on the use of primitive +.. opt:: Primitive Projections + +Turns on the use of primitive projections when defining subsequent records (even through the ``Inductive`` and ``CoInductive`` commands). Primitive projections extended the Calculus of Inductive Constructions with a new binary @@ -229,11 +235,15 @@ terms when manipulating parameterized records and typechecking time. On the user level, primitive projections can be used as a replacement for the usual defined ones, although there are a few notable differences. -The internally omitted parameters can be reconstructed at printing time -even though they are absent in the actual AST manipulated by the kernel. This -can be obtained by setting the ``Printing Primitive Projection Parameters`` -flag. Another compatibility printing can be activated thanks to the -``Printing Primitive Projection Compatibility`` option which governs the +.. opt:: Printing Primitive Projection Parameters + +This compatibility option reconstructs internally omitted parameters at +printing time (even though they are absent in the actual AST manipulated +by the kernel). + +.. opt:: Printing Primitive Projection Compatibility + +This compatibility option (on by default) governs the printing of pattern-matching over primitive records. Primitive Record Types @@ -244,6 +254,8 @@ record types change meaning. When a type is declared with primitive projections, its :g:`match` construct is disabled (see :ref:`primitive_projections` though). To eliminate the (co-)inductive type, one must use its defined primitive projections. +.. The following paragraph is quite redundant with what is above + For compatibility, the parameters still appear to the user when printing terms even though they are absent in the actual AST manipulated by the kernel. This can be changed by unsetting the @@ -462,116 +474,63 @@ of :g:`match` expressions. Printing nested patterns +++++++++++++++++++++++++ +.. opt:: Printing Matching. + The Calculus of Inductive Constructions knows pattern-matching only over simple patterns. It is however convenient to re-factorize nested pattern-matching into a single pattern-matching over a nested -pattern. |Coq|’s printer tries to do such limited re-factorization. - -.. cmd:: Set Printing Matching. +pattern. -This tells |Coq| to try to use nested patterns. This is the default -behavior. +When this option is on (default), |Coq|’s printer tries to do such +limited re-factorization. +Turning it off tells |Coq| to print only simple pattern-matching problems +in the same way as the |Coq| kernel handles them. -.. cmd:: Unset Printing Matching. - -This tells |Coq| to print only simple pattern-matching problems in the -same way as the |Coq| kernel handles them. - -.. cmd:: Test Printing Matching. - -This tells if the printing matching mode is on or off. The default is -on. Factorization of clauses with same right-hand side ++++++++++++++++++++++++++++++++++++++++++++++++++ +.. opt:: Printing Factorizable Match Patterns. + When several patterns share the same right-hand side, it is additionally possible to share the clauses using disjunctive patterns. Assuming that the -printing matching mode is on, whether |Coq|'s printer shall try to do this kind -of factorization is governed by the following commands: - -.. cmd:: Set Printing Factorizable Match Patterns. - -This tells |Coq|'s printer to try to use disjunctive patterns. This is the -default behavior. - -.. cmd:: Unset Printing Factorizable Match Patterns. - -This tells |Coq|'s printer not to try to use disjunctive patterns. - -.. cmd:: Test Printing Factorizable Match Patterns. - -This tells if the factorization of clauses with same right-hand side is on or -off. +printing matching mode is on, this option (on by default) tells |Coq|'s +printer to try to do this kind of factorization. Use of a default clause +++++++++++++++++++++++ +.. opt:: Printing Allow Default Clause. + When several patterns share the same right-hand side which do not depend on the arguments of the patterns, yet an extra factorization is possible: the disjunction of patterns can be replaced with a `_` default clause. Assuming that -the printing matching mode and the factorization mode are on, whether |Coq|'s -printer shall try to use a default clause is governed by the following commands: - -.. cmd:: Set Printing Allow Default Clause. - -This tells |Coq|'s printer to use a default clause when relevant. This is the -default behavior. - -.. cmd:: Unset Printing Allow Default Clause. - -This tells |Coq|'s printer not to use a default clause. - -.. cmd:: Test Printing Allow Default Clause. - -This tells if the use of a default clause is allowed. +the printing matching mode and the factorization mode are on, this option (on by +default) tells |Coq|'s printer to use a default clause when relevant. Printing of wildcard patterns ++++++++++++++++++++++++++++++ -Some variables in a pattern may not occur in the right-hand side of -the pattern-matching clause. There are options to control the display -of these variables. - -.. cmd:: Set Printing Wildcard. +.. opt:: Printing Wildcard. -The variables having no occurrences in the right-hand side of the +Some variables in a pattern may not occur in the right-hand side of +the pattern-matching clause. When this option is on (default), the +variables having no occurrences in the right-hand side of the pattern-matching clause are just printed using the wildcard symbol “_”. -.. cmd:: Unset Printing Wildcard. - -The variables, even useless, are printed using their usual name. But -some non-dependent variables have no name. These ones are still -printed using a “_”. - -.. cmd:: Test Printing Wildcard. - -This tells if the wildcard printing mode is on or off. The default is -to print wildcard for useless variables. - Printing of the elimination predicate +++++++++++++++++++++++++++++++++++++ +.. opt:: Printing Synth. + In most of the cases, the type of the result of a matched term is mechanically synthesizable. Especially, if the result type does not -depend of the matched term. - -.. cmd:: Set Printing Synth. - -The result type is not printed when |Coq| knows that it can re- +depend of the matched term. When this option is on (default), +the result type is not printed when |Coq| knows that it can re- synthesize it. -.. cmd:: Unset Printing Synth. - -This forces the result type to be always printed. - -.. cmd:: Test Printing Synth. - -This tells if the non-printing of synthesizable types is on or off. -The default is to not print synthesizable types. - Printing matching on irrefutable patterns ++++++++++++++++++++++++++++++++++++++++++ @@ -1188,24 +1147,24 @@ some of the fields and give one of its possible implementations: Notice that ``M`` is a correct body for the component ``M2`` since its ``T`` component is equal ``nat`` and hence ``M1.T`` as specified. -**Remarks:** +.. note:: -#. Modules and module types can be nested components of each other. -#. One can have sections inside a module or a module type, but not a - module or a module type inside a section. -#. Commands like ``Hint`` or ``Notation`` can also appear inside modules and - module types. Note that in case of a module definition like: + #. Modules and module types can be nested components of each other. + #. One can have sections inside a module or a module type, but not a + module or a module type inside a section. + #. Commands like ``Hint`` or ``Notation`` can also appear inside modules and + module types. Note that in case of a module definition like: -:: + :: - Module N : SIG := M. + Module N : SIG := M. -or:: + or:: - Module N : SIG. … End N. + Module N : SIG. … End N. -hints and the like valid for ``N`` are not those defined in ``M`` (or the module body) but the ones defined -in ``SIG``. + hints and the like valid for ``N`` are not those defined in ``M`` + (or the module body) but the ones defined in ``SIG``. .. _import_qualid: @@ -1780,14 +1739,10 @@ appear strictly in the body of the type, they are implicit. Mode for automatic declaration of implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -In case one wants to systematically declare implicit the arguments -detectable as such, one may switch to the automatic declaration of -implicit arguments mode by using the command: +.. opt:: Implicit Arguments. -.. cmd:: Set Implicit Arguments. - -Conversely, one may unset the mode by using ``Unset Implicit Arguments``. -The mode is off by default. Auto-detection of implicit arguments is +This option (off by default) allows to systematically declare implicit +the arguments detectable as such. Auto-detection of implicit arguments is governed by options controlling whether strict and contextual implicit arguments have to be considered or not. @@ -1796,76 +1751,53 @@ arguments have to be considered or not. Controlling strict implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +.. opt:: Strict Implicit. + When the mode for automatic declaration of implicit arguments is on, the default is to automatically set implicit only the strict implicit arguments plus, for historical reasons, a small subset of the non-strict implicit arguments. To relax this constraint and to set -implicit all non strict implicit arguments by default, use the command: - -.. cmd:: Unset Strict Implicit. - -Conversely, use the command ``Set Strict Implicit`` to restore the -original mode that declares implicit only the strict implicit -arguments plus a small subset of the non strict implicit arguments. +implicit all non strict implicit arguments by default, you can turn this +option off. -In the other way round, to capture exactly the strict implicit -arguments and no more than the strict implicit arguments, use the -command +.. opt:: Strongly Strict Implicit. -.. cmd:: Set Strongly Strict Implicit. - -Conversely, use the command ``Unset Strongly Strict Implicit`` to let the -option “Strict Implicit” decide what to do. - -Remark: In versions of |Coq| prior to version 8.0, the default was to -declare the strict implicit arguments as implicit. +Use this option (off by default) to capture exactly the strict implicit +arguments and no more than the strict implicit arguments. .. _controlling-contextual-implicit-args: Controlling contextual implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -By default, |Coq| does not automatically set implicit the contextual -implicit arguments. To tell |Coq| to infer also contextual implicit -argument, use command +.. opt:: Contextual Implicit. -.. cmd:: Set Contextual Implicit. - -Conversely, use command ``Unset Contextual Implicit`` to unset the -contextual implicit mode. +By default, |Coq| does not automatically set implicit the contextual +implicit arguments. You can turn this option on to tell |Coq| to also +infer contextual implicit argument. .. _controlling-rev-pattern-implicit-args: Controlling reversible-pattern implicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -By default, |Coq| does not automatically set implicit the reversible-pattern -implicit arguments. To tell |Coq| to infer also reversible- -pattern implicit argument, use command - -.. cmd:: Set Reversible Pattern Implicit. +.. opt:: Reversible Pattern Implicit. -Conversely, use command ``Unset Reversible Pattern Implicit`` to unset the -reversible-pattern implicit mode. +By default, |Coq| does not automatically set implicit the reversible-pattern +implicit arguments. You can turn this option on to tell |Coq| to also infer +reversible-pattern implicit argument. .. _controlling-insertion-implicit-args: Controlling the insertion of implicit arguments not followed by explicit arguments ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Implicit arguments can be declared to be automatically inserted when a -function is partially applied and the next argument of the function is -an implicit one. In case the implicit arguments are automatically -declared (with the command ``Set Implicit Arguments``), the command +.. opt:: Maximal Implicit Insertion. -.. cmd:: Set Maximal Implicit Insertion. - -is used to tell to declare the implicit arguments with a maximal -insertion status. By default, automatically declared implicit -arguments are not declared to be insertable maximally. To restore the -default mode for maximal insertion, use the command - -.. cmd:: Unset Maximal Implicit Insertion. +Assuming the implicit argument mode is on, this option (off by default) +declares implicit arguments to be automatically inserted when a +function is partially applied and the next argument of the function is +an implicit one. Explicit applications ~~~~~~~~~~~~~~~~~~~~~ @@ -1935,26 +1867,18 @@ if each of them is to be used maximally or not, use the command Explicit displaying of implicit arguments for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -By default the basic pretty-printing rules hide the inferable implicit -arguments of an application. To force printing all implicit arguments, -use command +.. opt:: Printing Implicit. -.. cmd:: Set Printing Implicit. - -Conversely, to restore the hiding of implicit arguments, use command +By default, the basic pretty-printing rules hide the inferable implicit +arguments of an application. Turn this option on to force printing all +implicit arguments. -.. cmd:: Unset Printing Implicit. +.. opt:: Printing Implicit Defensive. -By default the basic pretty-printing rules display the implicit +By default, the basic pretty-printing rules display the implicit arguments that are not detected as strict implicit arguments. This “defensive” mode can quickly make the display cumbersome so this can -be deactivated by using the command - -.. cmd:: Unset Printing Implicit Defensive. - -Conversely, to force the display of non strict arguments, use command - -.. cmd:: Set Printing Implicit Defensive. +be deactivated by turning this option off. See also: ``Set Printing All`` in :ref:`printing_constructions_full`. @@ -1981,17 +1905,14 @@ but succeeds in Deactivation of implicit arguments for parsing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -Use of implicit arguments can be deactivated by issuing the command: +.. opt:: Parsing Explicit. -.. cmd:: Set Parsing Explicit. +Turning this option on, deactivates the use of implicit arguments. In this case, all arguments of constants, inductive types, constructors, etc, including the arguments declared as implicit, have -to be given as if none arguments were implicit. By symmetry, this also -affects printing. To restore parsing and normal printing of implicit -arguments, use: - -.. cmd:: Unset Parsing Explicit. +to be given as if no arguments were implicit. By symmetry, this also +affects printing. Canonical structures ~~~~~~~~~~~~~~~~~~~~ @@ -2201,38 +2122,30 @@ to coercions are provided in :ref:`implicitcoercions`. Printing constructions in full ------------------------------ +.. opt:: Printing All. + Coercions, implicit arguments, the type of pattern-matching, but also notations (see :ref:`syntaxextensionsandinterpretationscopes`) can obfuscate the behavior of some tactics (typically the tactics applying to occurrences of subterms are -sensitive to the implicit arguments). The command - -.. cmd:: Set Printing All. - +sensitive to the implicit arguments). Turning this option on deactivates all high-level printing features such as coercions, implicit arguments, returned type of pattern-matching, notations and various syntactic sugar for pattern-matching or record projections. Otherwise said, ``Set Printing All`` includes the effects of the commands ``Set Printing Implicit``, ``Set Printing Coercions``, ``Set Printing Synth``, ``Unset Printing Projections``, and ``Unset Printing Notations``. To reactivate -the high-level printing features, use the command - -.. cmd:: Unset Printing All. +the high-level printing features, use the command ``Unset Printing All``. Printing universes ------------------ -The following command: +.. opt:: Printing Universes. -.. cmd:: Set Printing Universes. - -activates the display of the actual level of each occurrence of ``Type``. +Turn this option on to activate the display of the actual level of each occurrence of ``Type``. See :ref:`TODO-4.1.1-sorts` for details. This wizard option, in combination with ``Set Printing All`` (see :ref:`printing_constructions_full`) can help to diagnose failures to unify terms apparently identical but internally different in the -Calculus of Inductive Constructions. To reactivate the display of the -actual level of the occurrences of Type, use - -.. cmd:: Unset Printing Universes. +Calculus of Inductive Constructions. The constraints on the internal level of the occurrences of Type (see :ref:`TODO-4.1.1-sorts`) can be printed using the command @@ -2314,18 +2227,12 @@ with a named-goal selector, see :ref:`TODO-9.2-goal-selectors`). Explicit displaying of existential instances for pretty-printing ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -The command: - -.. cmd:: Set Printing Existential Instances. - -activates the full display of how the context of an existential -variable is instantiated at each of the occurrences of the existential -variable. +.. opt:: Printing Existential Instances. -To deactivate the full display of the instances of existential -variables, use +This option (off by default) activates the full display of how the +context of an existential variable is instantiated at each of the +occurrences of the existential variable. -.. cmd:: Unset Printing Existential Instances. Solving existential variables using tactics ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ diff --git a/doc/sphinx/practical-tools/coqide.rst b/doc/sphinx/practical-tools/coqide.rst index 1fcfc665b..a3b942628 100644 --- a/doc/sphinx/practical-tools/coqide.rst +++ b/doc/sphinx/practical-tools/coqide.rst @@ -10,7 +10,7 @@ used as a user-friendly replacement to `coqtop`. Its main purpose is to allow the user to navigate forward and backward into a Coq vernacular file, executing corresponding commands or undoing them respectively. -CoqIDE is run by typing the command `coqide` on the command line. +|CoqIDE| is run by typing the command `coqide` on the command line. Without argument, the main screen is displayed with an “unnamed buffer”, and with a file name as argument, another buffer displaying the contents of that file. Additionally, `coqide` accepts the same @@ -43,7 +43,7 @@ is the one where Coq commands are currently executed. Buffers may be edited as in any text editor, and classical basic editing commands (Copy/Paste, …) are available in the *Edit* menu. -CoqIDE offers only basic editing commands, so if you need more complex +|CoqIDE| offers only basic editing commands, so if you need more complex editing commands, you may launch your favorite text editor on the current buffer, using the *Edit/External Editor* menu. @@ -86,7 +86,7 @@ If you ever try to execute a command which happens to run during a long time, and would like to abort it before its termination, you may use the interrupt button (the white cross on a red circle). -There are other buttons on the CoqIDE toolbar: a button to save the running +There are other buttons on the |CoqIDE| toolbar: a button to save the running buffer; a button to close the current buffer (an "X"); buttons to switch among buffers (left and right arrows); an "information" button; and a "gears" button. @@ -157,7 +157,7 @@ Queries We call *query* any vernacular command that does not change the current state, such as ``Check``, ``Search``, etc. To run such commands interactively, without -writing them in scripts, CoqIDE offers a *query pane*. The query pane can be +writing them in scripts, |CoqIDE| offers a *query pane*. The query pane can be displayed on demand by using the ``View`` menu, or using the shortcut ``F1``. Queries can also be performed by selecting a particular phrase, then choosing an item from the ``Queries`` menu. The response then appears in the message window. @@ -221,7 +221,7 @@ still edit this configuration file by hand, but this is more involved. Using Unicode symbols -------------------------- -CoqIDE is based on GTK+ and inherits from it support for Unicode in +|CoqIDE| is based on GTK+ and inherits from it support for Unicode in its text windows. Consequently a large set of symbols is available for notations. diff --git a/doc/sphinx/proof-engine/ssreflect-proof-language.rst b/doc/sphinx/proof-engine/ssreflect-proof-language.rst index bd71e5ed8..df5b36297 100644 --- a/doc/sphinx/proof-engine/ssreflect-proof-language.rst +++ b/doc/sphinx/proof-engine/ssreflect-proof-language.rst @@ -6,10 +6,7 @@ The |SSR| proof language ------------------------------ -:Source: https://coq.inria.fr/distrib/current/refman/ssreflect.html -:Converted by: Enrico Tassi - -Author: Georges Gonthier, Assia Mahboubi, Enrico Tassi +:Authors: Georges Gonthier, Assia Mahboubi, Enrico Tassi Introduction diff --git a/doc/sphinx/user-extensions/syntax-extensions.rst b/doc/sphinx/user-extensions/syntax-extensions.rst index 6e6d66447..531295b63 100644 --- a/doc/sphinx/user-extensions/syntax-extensions.rst +++ b/doc/sphinx/user-extensions/syntax-extensions.rst @@ -10,12 +10,12 @@ parses and prints objects, i.e. the translations between the concrete and internal representations of terms and commands. The main commands to provide custom symbolic notations for terms are -``Notation`` and ``Infix``. They are described in section 12.1. There is also a +``Notation`` and ``Infix``. They are described in section :ref:`Notations`. There is also a variant of ``Notation`` which does not modify the parser. This provides with a form of abbreviation and it is described in Section :ref:`Abbreviations`. It is sometimes expected that the same symbolic notation has different meanings in different contexts. To achieve this form of overloading, |Coq| offers a notion -of interpretation scope. This is described in Section :ref:`scopes`. +of interpretation scope. This is described in Section :ref:`Scopes`. The main command to provide custom notations for tactics is ``Tactic Notation``. It is described in Section :ref:`TacticNotation`. @@ -24,6 +24,8 @@ It is described in Section :ref:`TacticNotation`. Set Printing Depth 50. +.. _Notations: + Notations --------- @@ -68,7 +70,7 @@ have to be given. .. note:: The right-hand side of a notation is interpreted at the time the notation is - given. In particular, disambiguiation of constants, implicit arguments (see + given. In particular, disambiguation of constants, implicit arguments (see Section :ref:`ImplicitArguments`), coercions (see Section :ref:`Coercions`), etc. are resolved at the time of the declaration of the notation. @@ -689,8 +691,7 @@ side. E.g.: Summary ~~~~~~~ -Syntax of notations -~~~~~~~~~~~~~~~~~~~ +**Syntax of notations** The different syntactic variants of the command Notation are given on the following figure. The optional :token:`scope` is described in the Section 12.2. @@ -743,8 +744,7 @@ following figure. The optional :token:`scope` is described in the Section 12.2. given to some notation, say ``"{ y } & { z }"`` in fact applies to the underlying ``"{ x }"``\-free rule which is ``"y & z"``). -Persistence of notations -~~~~~~~~~~~~~~~~~~~~~~~~ +**Persistence of notations** Notations do not survive the end of sections. @@ -753,6 +753,8 @@ Notations do not survive the end of sections. Notations survive modules unless the command ``Local Notation`` is used instead of ``Notation``. +.. _Scopes: + Interpretation scopes ---------------------- @@ -1125,6 +1127,8 @@ Displaying informations about scopes class of all the existing interpretation scopes. It also displays the lonely notations. +.. _Abbreviations: + Abbreviations -------------- @@ -1187,6 +1191,8 @@ Abbreviations denoted expression is performed at definition time. Type-checking is done only at the time of use of the abbreviation. +.. _TacticNotation: + Tactic Notations ----------------- diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 28c9dd3c2..8ee3b9050 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -108,7 +108,7 @@ val mkLetIn : Name.t * t * t * t -> t val mkApp : t * t array -> t val mkConst : Constant.t -> t val mkConstU : Constant.t * EInstance.t -> t -val mkProj : (projection * t) -> t +val mkProj : (Projection.t * t) -> t val mkInd : inductive -> t val mkIndU : inductive * EInstance.t -> t val mkConstruct : constructor -> t @@ -173,7 +173,7 @@ val destEvar : Evd.evar_map -> t -> t pexistential val destInd : Evd.evar_map -> t -> inductive * EInstance.t val destConstruct : Evd.evar_map -> t -> constructor * EInstance.t val destCase : Evd.evar_map -> t -> case_info * t * t * t array -val destProj : Evd.evar_map -> t -> projection * t +val destProj : Evd.evar_map -> t -> Projection.t * t val destFix : Evd.evar_map -> t -> (t, t) pfixpoint val destCoFix : Evd.evar_map -> t -> (t, t) pcofixpoint diff --git a/ide/coqOps.ml b/ide/coqOps.ml index 78fbce5c8..6c3438a4b 100644 --- a/ide/coqOps.ml +++ b/ide/coqOps.ml @@ -362,7 +362,12 @@ object(self) let query = Coq.query (route_id,(phrase,sid)) in Coq.bind (Coq.seq action query) next + method private still_valid { edit_id = id } = + try ignore(Doc.find_id document (fun _ { edit_id = id1 } -> id = id1)); true + with Not_found -> false + method private mark_as_needed sentence = + if self#still_valid sentence then begin Minilib.log_pp Pp.(str "Marking " ++ dbg_to_string buffer false None sentence); let start = buffer#get_iter_at_mark sentence.start in let stop = buffer#get_iter_at_mark sentence.stop in @@ -383,6 +388,7 @@ object(self) in List.iter (fun t -> buffer#remove_tag t ~start ~stop) all_tags; List.iter (fun t -> buffer#apply_tag t ~start ~stop) tags + end method private attach_tooltip ?loc sentence text = let start_sentence, stop_sentence, phrase = self#get_sentence sentence in diff --git a/interp/impargs.mli b/interp/impargs.mli index 1eeb8e41a..103a4f9e9 100644 --- a/interp/impargs.mli +++ b/interp/impargs.mli @@ -130,7 +130,7 @@ val make_implicits_list : implicit_status list -> implicits_list list val drop_first_implicits : int -> implicits_list -> implicits_list -val projection_implicits : env -> projection -> implicit_status list -> +val projection_implicits : env -> Projection.t -> implicit_status list -> implicit_status list val select_impargs_size : int -> implicits_list list -> implicit_status list diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index aa9a6ed0d..a76f82094 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -210,7 +210,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',na = protect g e na in GIf (f e c,(na,Option.map (f e') po),f e b1,f e b2) | NRec (fk,idl,dll,tl,bl) -> - let e,dll = Array.fold_left_map (List.fold_map (fun e (na,oc,b) -> + let e,dll = Array.fold_left_map (List.fold_left_map (fun e (na,oc,b) -> let e,na = protect g e na in (e,(na,Explicit,Option.map (f e) oc,f e b)))) e dll in let e',idl = Array.fold_left_map (to_id (protect g)) e idl in diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 5f683790c..08114abc4 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -96,7 +96,7 @@ module type RedFlagsSig = sig val red_transparent : reds -> transparent_state val mkflags : red_kind list -> reds val red_set : reds -> red_kind -> bool - val red_projection : reds -> projection -> bool + val red_projection : reds -> Projection.t -> bool end module RedFlags = (struct @@ -364,7 +364,7 @@ and fterm = | FInd of pinductive | FConstruct of pconstructor | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 3a7f77d52..e2f5a3b82 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -74,7 +74,7 @@ module type RedFlagsSig = sig (** This tests if the projection is in unfolded state already or is unfodable due to delta. *) - val red_projection : reds -> projection -> bool + val red_projection : reds -> Projection.t -> bool end module RedFlags : RedFlagsSig @@ -132,7 +132,7 @@ type fterm = | FInd of inductive Univ.puniverses | FConstruct of constructor Univ.puniverses | FApp of fconstr * fconstr array - | FProj of projection * fconstr + | FProj of Projection.t * fconstr | FFix of fixpoint * fconstr subs | FCoFix of cofixpoint * fconstr subs | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *) diff --git a/kernel/constr.ml b/kernel/constr.ml index ba7fecadf..4f062d72f 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -100,7 +100,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr (* constr is the fixpoint of the previous type. Requires option -rectypes of the Caml compiler to be set *) type t = (t, t, Sorts.t, Instance.t) kind_of_term diff --git a/kernel/constr.mli b/kernel/constr.mli index 98c0eaa28..0d464840c 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -122,7 +122,7 @@ val mkConst : Constant.t -> constr val mkConstU : pconstant -> constr (** Constructs a projection application *) -val mkProj : (projection * constr) -> constr +val mkProj : (Projection.t * constr) -> constr (** Inductive types *) @@ -220,7 +220,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr (** User view of [constr]. For [App], it is ensured there is at least one argument and the function is not itself an applicative @@ -318,7 +318,7 @@ where [info] is pretty-printing information *) val destCase : constr -> case_info * constr * constr * constr array (** Destructs a projection *) -val destProj : constr -> projection * constr +val destProj : constr -> Projection.t * constr (** Destructs the {% $ %}i{% $ %}th function of the block [Fixpoint f{_ 1} ctx{_ 1} = b{_ 1} diff --git a/kernel/environ.mli b/kernel/environ.mli index 4e6ac1e72..fdd84b25b 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -168,7 +168,7 @@ val constant_opt_value_in : env -> Constant.t puniverses -> constr option (** {6 Primitive projections} *) -val lookup_projection : Names.projection -> env -> projection_body +val lookup_projection : Names.Projection.t -> env -> projection_body val is_projection : Constant.t -> env -> bool (** {5 Inductive types } *) diff --git a/kernel/names.mli b/kernel/names.mli index ffd96781b..96e020aed 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -547,6 +547,8 @@ val eq_constant_key : Constant.t -> Constant.t -> bool (** equalities on constant and inductive names (for the checker) *) val eq_con_chk : Constant.t -> Constant.t -> bool +[@@ocaml.deprecated "Same as [Constant.UserOrd.equal]."] + val eq_ind_chk : inductive -> inductive -> bool (** {6 Deprecated functions. For backward compatibility.} *) @@ -633,27 +635,27 @@ val eq_label : Label.t -> Label.t -> bool (** {5 Unique bound module names} *) type mod_bound_id = MBId.t -(** Alias type. *) +[@@ocaml.deprecated "Same as [MBId.t]."] -val mod_bound_id_ord : mod_bound_id -> mod_bound_id -> int +val mod_bound_id_ord : MBId.t -> MBId.t -> int [@@ocaml.deprecated "Same as [MBId.compare]."] -val mod_bound_id_eq : mod_bound_id -> mod_bound_id -> bool +val mod_bound_id_eq : MBId.t -> MBId.t -> bool [@@ocaml.deprecated "Same as [MBId.equal]."] -val make_mbid : DirPath.t -> Id.t -> mod_bound_id +val make_mbid : DirPath.t -> Id.t -> MBId.t [@@ocaml.deprecated "Same as [MBId.make]."] -val repr_mbid : mod_bound_id -> int * Id.t * DirPath.t +val repr_mbid : MBId.t -> int * Id.t * DirPath.t [@@ocaml.deprecated "Same as [MBId.repr]."] -val id_of_mbid : mod_bound_id -> Id.t +val id_of_mbid : MBId.t -> Id.t [@@ocaml.deprecated "Same as [MBId.to_id]."] -val string_of_mbid : mod_bound_id -> string +val string_of_mbid : MBId.t -> string [@@ocaml.deprecated "Same as [MBId.to_string]."] -val debug_string_of_mbid : mod_bound_id -> string +val debug_string_of_mbid : MBId.t -> string [@@ocaml.deprecated "Same as [MBId.debug_to_string]."] (** {5 Names} *) @@ -745,6 +747,7 @@ module Projection : sig end type projection = Projection.t +[@@ocaml.deprecated "Alias for [Projection.t]"] val constant_of_kn_equiv : KerName.t -> KerName.t -> Constant.t [@@ocaml.deprecated "Same as [Constant.make]"] diff --git a/kernel/term.ml b/kernel/term.ml index 403ed881c..e1affb1c0 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -92,7 +92,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) pfixpoint | CoFix of ('constr, 'types) pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr type values = Vmvalues.values diff --git a/kernel/term.mli b/kernel/term.mli index 7cb3b662d..ee84dcb2b 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -155,7 +155,7 @@ val destCase : constr -> case_info * constr * constr * constr array [@@ocaml.deprecated "Alias for [Constr.destCase]"] (** Destructs a projection *) -val destProj : constr -> projection * constr +val destProj : constr -> Projection.t * constr [@@ocaml.deprecated "Alias for [Constr.destProj]"] (** Destructs the {% $ %}i{% $ %}th function of the block @@ -403,7 +403,7 @@ val mkApp : constr * constr array -> constr [@@ocaml.deprecated "Alias for Constr"] val mkConst : Constant.t -> constr [@@ocaml.deprecated "Alias for Constr"] -val mkProj : projection * constr -> constr +val mkProj : Projection.t * constr -> constr [@@ocaml.deprecated "Alias for Constr"] val mkInd : inductive -> constr [@@ocaml.deprecated "Alias for Constr"] @@ -571,7 +571,7 @@ type ('constr, 'types, 'sort, 'univs) kind_of_term = | Case of Constr.case_info * 'constr * 'constr * 'constr array | Fix of ('constr, 'types) Constr.pfixpoint | CoFix of ('constr, 'types) Constr.pcofixpoint - | Proj of projection * 'constr + | Proj of Projection.t * 'constr [@@ocaml.deprecated "Alias for Constr.kind_of_term"] type values = Vmvalues.values diff --git a/kernel/typeops.mli b/kernel/typeops.mli index bff40b017..85b2cfffd 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -60,7 +60,7 @@ val judge_of_constant : env -> pconstant -> unsafe_judgment (** {6 type of an applied projection } *) -val judge_of_projection : env -> Names.projection -> unsafe_judgment -> unsafe_judgment +val judge_of_projection : env -> Projection.t -> unsafe_judgment -> unsafe_judgment (** {6 Type of application. } *) val judge_of_apply : @@ -100,7 +100,7 @@ val judge_of_case : env -> case_info -> unsafe_judgment -> unsafe_judgment -> unsafe_judgment array -> unsafe_judgment -val type_of_projection_constant : env -> Names.projection puniverses -> types +val type_of_projection_constant : env -> Projection.t puniverses -> types val type_of_constant_in : env -> pconstant -> types diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 92c86eaea..fda25a0a6 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -22,11 +22,8 @@ type t = { let warnings : (string, t) Hashtbl.t = Hashtbl.create 97 let categories : (string, string list) Hashtbl.t = Hashtbl.create 97 -let current_loc = ref None let flags = ref "" -let set_current_loc loc = current_loc := loc - let get_flags () = !flags let add_warning_in_category ~name ~category = @@ -170,7 +167,6 @@ let create ~name ~category ?(default=Enabled) pp = set_flags !flags; fun ?loc x -> let w = Hashtbl.find warnings name in - let loc = Option.append loc !current_loc in match w.status with | Disabled -> () | AsError -> CErrors.user_err ?loc (pp x) diff --git a/lib/cWarnings.mli b/lib/cWarnings.mli index fa96b18c8..f97a53c4d 100644 --- a/lib/cWarnings.mli +++ b/lib/cWarnings.mli @@ -10,8 +10,6 @@ type status = Disabled | Enabled | AsError -val set_current_loc : Loc.t option -> unit - val create : name:string -> category:string -> ?default:status -> ('a -> Pp.t) -> ?loc:Loc.t -> 'a -> unit diff --git a/lib/loc.ml b/lib/loc.ml index 6f5283aab..1a09091bf 100644 --- a/lib/loc.ml +++ b/lib/loc.ml @@ -62,6 +62,11 @@ let merge_opt l1 l2 = match l1, l2 with | None, Some l -> Some l | Some l1, Some l2 -> Some (merge l1 l2) +let finer l1 l2 = match l1, l2 with + | None, _ -> false + | Some l , None -> true + | Some l1, Some l2 -> l1.fname = l2.fname && merge l1 l2 = l2 + let unloc loc = (loc.bp, loc.ep) let shift_loc kb kp loc = { loc with bp = loc.bp + kb ; ep = loc.ep + kp } diff --git a/lib/loc.mli b/lib/loc.mli index 813c45fbb..23df1ebd9 100644 --- a/lib/loc.mli +++ b/lib/loc.mli @@ -42,6 +42,10 @@ val merge : t -> t -> t val merge_opt : t option -> t option -> t option (** Merge locations, usually generating the largest possible span *) +val finer : t option -> t option -> bool +(** Answers [true] when the first location is more defined, or, when + both defined, included in the second one *) + val shift_loc : int -> int -> t -> t (** [shift_loc loc n p] shifts the beginning of location by [n] and the end by [p]; it is assumed that the shifts do not change the diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 5a4818926..8e53a044d 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -9,7 +9,7 @@ (************************************************************************) (* This file implements the basic congruence-closure algorithm by *) -(* Downey,Sethi and Tarjan. *) +(* Downey, Sethi and Tarjan. *) (* Plus some e-matching and constructor handling by P. Corbineau *) open CErrors @@ -18,7 +18,6 @@ open Names open Sorts open Constr open Vars -open Evd open Goptions open Tacmach open Util @@ -272,7 +271,8 @@ type state = mutable rew_depth:int; mutable changed:bool; by_type: Int.Set.t Typehash.t; - mutable gls:Goal.goal Evd.sigma} + mutable env:Environ.env; + sigma:Evd.evar_map} let dummy_node = { @@ -307,7 +307,8 @@ let empty depth gls:state = rew_depth=depth; by_type=Constrhash.create init_size; changed=false; - gls=gls + env=pf_env gls; + sigma=project gls } let forest state = state.uf @@ -426,7 +427,7 @@ let cc_product s1 s2 = mkLambda(_B_,mkSort(s2),_body_)) let rec constr_of_term = function - Symb s-> applist_projection s [] + Symb s-> s | Product(s1,s2) -> cc_product s1 s2 | Eps id -> mkVar id | Constructor cinfo -> mkConstructU cinfo.ci_constr @@ -434,25 +435,7 @@ let rec constr_of_term = function make_app [(constr_of_term s2)] s1 and make_app l=function Appli (s1,s2)->make_app ((constr_of_term s2)::l) s1 - | other -> - applist_proj other l -and applist_proj c l = - match c with - | Symb s -> applist_projection s l - | _ -> Term.applistc (constr_of_term c) l -and applist_projection c l = - match Constr.kind c with - | Const c when Environ.is_projection (fst c) (Global.env()) -> - let p = Projection.make (fst c) false in - (match l with - | [] -> (* Expand the projection *) - let ty = Typeops.type_of_constant_in (Global.env ()) c in (* FIXME constraints *) - let pb = Environ.lookup_projection p (Global.env()) in - let ctx,_ = Term.decompose_prod_n_assum (pb.Declarations.proj_npars + 1) ty in - Term.it_mkLambda_or_LetIn (mkProj(p,mkRel 1)) ctx - | hd :: tl -> - Term.applistc (mkProj (p, hd)) tl) - | _ -> Term.applistc c l + | other -> Term.applist (constr_of_term other,l) let rec canonize_name sigma c = let c = EConstr.Unsafe.to_constr c in @@ -511,8 +494,8 @@ let rec add_term state t= Not_found -> let b=next uf in let trm = constr_of_term t in - let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in - let typ = canonize_name (project state.gls) typ in + let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in + let typ = canonize_name state.sigma typ in let new_node= match t with Symb _ | Product (_,_) -> @@ -820,11 +803,10 @@ let one_step state = let __eps__ = Id.of_string "_eps_" let new_state_var typ state = - let id = pf_get_new_id __eps__ state.gls in - let {it=gl ; sigma=sigma} = state.gls in - let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in - state.gls<- gls; - id + let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in + let id = Namegen.next_ident_away __eps__ ids in + state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env; + id let complete_one_class state i= match (get_representative state.uf i).inductive_status with @@ -832,9 +814,9 @@ let complete_one_class state i= let rec app t typ n = if n<=0 then t else let _,etyp,rest= destProd typ in - let id = new_state_var etyp state in + let id = new_state_var (EConstr.of_constr etyp) state in app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in - let _c = pf_unsafe_type_of state.gls + let _c = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in let _c = EConstr.Unsafe.to_constr _c in let _args = diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9c350483b..d395e3601 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -91,10 +91,19 @@ let functional_induction with_clean c princl pat = if princ_infos.Tactics.farg_in_concl then [c] else [] in + if List.length args + List.length c_list = 0 + then user_err Pp.(str "Cannot recognize a valid functional scheme" ); let encoded_pat_as_patlist = - List.make (List.length args + List.length c_list - 1) None @ [pat] in - List.map2 (fun c pat -> ((None,Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)) )),(None,pat),None)) - (args@c_list) encoded_pat_as_patlist + List.make (List.length args + List.length c_list - 1) None @ [pat] + in + List.map2 + (fun c pat -> + ((None, + Ltac_plugin.Tacexpr.ElimOnConstr (fun env sigma -> (sigma,(c,NoBindings)))), + (None,pat), + None)) + (args@c_list) + encoded_pat_as_patlist in let princ' = Some (princ,bindings) in let princ_vars = diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml index 57a11d947..105b5c59a 100644 --- a/plugins/ltac/tactic_debug.ml +++ b/plugins/ltac/tactic_debug.ml @@ -399,8 +399,6 @@ let skip_extensions trace = | [] -> [] in List.rev (aux (List.rev trace)) -let finer_loc loc1 loc2 = Loc.merge_opt loc1 loc2 = loc2 - let extract_ltac_trace ?loc trace = let trace = skip_extensions trace in let (tloc,c),tail = List.sep_last trace in @@ -408,7 +406,7 @@ let extract_ltac_trace ?loc trace = (* We entered a user-defined tactic, we display the trace with location of the call *) let msg = hov 0 (explain_ltac_call_trace c tail loc ++ fnl()) in - (if finer_loc loc tloc then loc else tloc), Some msg + (if Loc.finer loc tloc then loc else tloc), Some msg else (* We entered a primitive tactic, we don't display trace but report on the finest location *) @@ -417,7 +415,7 @@ let extract_ltac_trace ?loc trace = let rec aux best_loc = function | (loc,_)::tail -> if Option.is_empty best_loc || - not (Option.is_empty loc) && finer_loc loc best_loc + not (Option.is_empty loc) && Loc.finer loc best_loc then aux loc tail else diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index a2155697e..cb0fc3257 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -71,7 +71,7 @@ and cbv_stack = | TOP | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - | PROJ of projection * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * Declarations.projection_body * cbv_stack (* les vars pourraient etre des constr, cela permet de retarder les lift: utile ?? *) diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 2ac59911c..cdaa39c53 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -41,7 +41,7 @@ and cbv_stack = | TOP | APP of cbv_value array * cbv_stack | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack - | PROJ of projection * Declarations.projection_body * cbv_stack + | PROJ of Projection.t * Declarations.projection_body * cbv_stack val shift_value : int -> cbv_value -> cbv_value diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 627430708..9270d6e3a 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -38,7 +38,7 @@ val e_cumul : env -> ?ts:transparent_state -> evar_map ref -> constr -> constr - val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map val consider_remaining_unif_problems : env -> ?ts:transparent_state -> evar_map -> evar_map -(** @deprecated Alias for [solve_unif_constraints_with_heuristics] *) +[@@ocaml.deprecated "Alias for [solve_unif_constraints_with_heuristics]"] (** Check all pending unification problems are solved and raise an error otherwise *) diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 9b21599b6..3f05c58c4 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -63,7 +63,7 @@ val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map -> val reconsider_unif_constraints : conv_fun -> evar_map -> unification_result val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result -(** @deprecated Alias for [reconsider_unif_constraints] *) +[@@ocaml.deprecated "Alias for [reconsider_unif_constraints]"] val is_unification_pattern_evar : env -> evar_map -> existential -> constr list -> constr -> alias list option diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 296f25d3f..b0d714b03 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -129,8 +129,8 @@ val allowed_sorts : env -> inductive -> Sorts.family list val has_dependent_elim : mutual_inductive_body -> bool (** Primitive projections *) -val projection_nparams : projection -> int -val projection_nparams_env : env -> projection -> int +val projection_nparams : Projection.t -> int +val projection_nparams_env : env -> Projection.t -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> EConstr.t -> EConstr.types -> types diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 9e3e68f05..360c6e86e 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -275,12 +275,12 @@ sig type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list @@ -332,12 +332,12 @@ struct type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int * int list * 'a t * Cst_stack.t and 'a t = 'a member list diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 29dc3ed0f..b8ac085a7 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -70,12 +70,12 @@ module Stack : sig type cst_member = | Cst_const of pconstant - | Cst_proj of projection + | Cst_proj of Projection.t type 'a member = | App of 'a app_node | Case of case_info * 'a * 'a array * Cst_stack.t - | Proj of int * int * projection * Cst_stack.t + | Proj of int * int * Projection.t * Cst_stack.t | Fix of ('a, 'a) pfixpoint * 'a t * Cst_stack.t | Cst of cst_member * int (** current foccussed arg *) * int list (** remaining args *) * 'a t * Cst_stack.t diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 40424ead4..2aff0c777 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -50,6 +50,6 @@ val type_of_global_reference_knowing_conclusion : val sorts_of_context : env -> evar_map -> rel_context -> Sorts.t list -val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr +val expand_projection : env -> evar_map -> Names.Projection.t -> constr -> constr list -> constr val print_retype_error : retype_error -> Pp.t diff --git a/pretyping/typing.mli b/pretyping/typing.mli index fe83a2cc8..4905adf1f 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -55,4 +55,4 @@ val judge_of_abstraction : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_judgment -> unsafe_judgment val judge_of_product : Environ.env -> Name.t -> unsafe_type_judgment -> unsafe_type_judgment -> unsafe_judgment -val judge_of_projection : env -> evar_map -> projection -> unsafe_judgment -> unsafe_judgment +val judge_of_projection : env -> evar_map -> Projection.t -> unsafe_judgment -> unsafe_judgment diff --git a/pretyping/unification.ml b/pretyping/unification.ml index f2f922fd5..ca03b96ab 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -466,7 +466,7 @@ let use_metas_pattern_unification sigma flags nb l = type key = | IsKey of CClosure.table_key - | IsProj of projection * EConstr.constr + | IsProj of Projection.t * EConstr.constr let expand_table_key env = function | ConstKey cst -> constant_opt_value_in env cst diff --git a/proofs/goal.ml b/proofs/goal.ml index ba7e458f3..6912db364 100644 --- a/proofs/goal.ml +++ b/proofs/goal.ml @@ -117,20 +117,6 @@ module V82 = struct with a good implementation of them. *) - (* Used for congruence closure *) - let new_goal_with sigma gl extra_hyps = - let evi = Evd.find sigma gl in - let hyps = evi.Evd.evar_hyps in - let new_hyps = - List.fold_right Environ.push_named_context_val extra_hyps hyps in - let filter = evi.Evd.evar_filter in - let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in - let new_evi = - { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in - let new_evi = Typeclasses.mark_unresolvable new_evi in - let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in - { Evd.it = evk ; sigma = sigma; } - (* Used by the compatibility layer and typeclasses *) let nf_evar sigma gl = let evi = Evd.find sigma gl in diff --git a/proofs/goal.mli b/proofs/goal.mli index dc9863156..b8c979ad7 100644 --- a/proofs/goal.mli +++ b/proofs/goal.mli @@ -64,9 +64,6 @@ module V82 : sig (* Principal part of tclNOTSAMEGOAL *) val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool - (* Used for congruence closure *) - val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma - (* Used by the compatibility layer and typeclasses *) val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map diff --git a/stm/stm.ml b/stm/stm.ml index ba0a2017a..30aa9ea06 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -3013,7 +3013,6 @@ let add ~doc ~ontop ?newtip verb { CAst.loc; v=ast } = str ") than the tip: " ++ str (Stateid.to_string cur_tip) ++ str "." ++ fnl () ++ str "This is not supported yet, sorry."); let indentation, strlen = compute_indentation ?loc ontop in - CWarnings.set_current_loc loc; (* XXX: Classifiy vernac should be moved inside process transaction *) let clas = Vernac_classifier.classify_vernac ast in let aast = { verbose = verb; indentation; strlen; loc; expr = ast } in @@ -3037,7 +3036,6 @@ let query ~doc ~at ~route s = while true do let { CAst.loc; v=ast } = parse_sentence ~doc at s in let indentation, strlen = compute_indentation ?loc at in - CWarnings.set_current_loc loc; let st = State.get_cached at in let aast = { verbose = true; indentation; strlen; loc; expr = ast } in ignore(stm_vernac_interp ~route at st aast) diff --git a/test-suite/bugs/opened/1501.v b/test-suite/bugs/closed/1501.v index b36f21da1..e771e192d 100644 --- a/test-suite/bugs/opened/1501.v +++ b/test-suite/bugs/closed/1501.v @@ -3,6 +3,7 @@ Set Implicit Arguments. Require Export Relation_Definitions. Require Export Setoid. +Require Import Morphisms. Section Essais. @@ -40,57 +41,27 @@ Parameter Hint Resolve equiv_refl equiv_sym equiv_trans: monad. -Instance equiv_rel A: Equivalence (@equiv A). -Proof. - constructor. - intros xa; apply equiv_refl. - intros xa xb; apply equiv_sym. - intros xa xb xc; apply equiv_trans. -Defined. - -Definition fequiv (A B: Type) (f g: A -> K B) := forall (x:A), (equiv (f x) (g -x)). - -Lemma fequiv_refl : forall (A B: Type) (f : A -> K B), fequiv f f. -Proof. - unfold fequiv; auto with monad. -Qed. - -Lemma fequiv_sym : forall (A B: Type) (x y : A -> K B), fequiv x y -> fequiv y -x. -Proof. - unfold fequiv; auto with monad. -Qed. +Add Parametric Relation A : (K A) (@equiv A) + reflexivity proved by (@equiv_refl A) + symmetry proved by (@equiv_sym A) + transitivity proved by (@equiv_trans A) + as equiv_rel. -Lemma fequiv_trans : forall (A B: Type) (x y z : A -> K B), fequiv x y -> -fequiv -y z -> fequiv x z. +Add Parametric Morphism A B : (@bind A B) + with signature (@equiv A) ==> (pointwise_relation A (@equiv B)) ==> (@equiv B) + as bind_mor. Proof. - unfold fequiv; intros; eapply equiv_trans; auto with monad. -Qed. - -Instance fequiv_re A B: Equivalence (@fequiv A B). -Proof. - constructor. - intros f; apply fequiv_refl. - intros f g; apply fequiv_sym. - intros f g h; apply fequiv_trans. -Defined. - -Instance bind_mor A B: Morphisms.Proper (@equiv _ ==> @fequiv _ _ ==> @equiv _) (@bind A B). -Proof. - unfold fequiv; intros x y xy_equiv f g fg_equiv; apply bind_compat; auto. + unfold pointwise_relation; intros; apply bind_compat; auto. Qed. Lemma test: forall (A B: Type) (m1 m2 m3: K A) (f: A -> A -> K B), - (equiv m1 m2) -> (equiv m2 m3) -> - equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) - (bind m2 (fun a => bind m3 (fun a' => f a a'))). + (equiv m1 m2) -> (equiv m2 m3) -> + equiv (bind m1 (fun a => bind m2 (fun a' => f a a'))) + (bind m2 (fun a => bind m3 (fun a' => f a a'))). Proof. intros A B m1 m2 m3 f H1 H2. setoid_rewrite H1. (* this works *) - Fail setoid_rewrite H2. -Abort. -(* trivial by equiv_refl. -Qed.*) + setoid_rewrite H2. + reflexivity. +Qed. diff --git a/test-suite/bugs/opened/2456.v b/test-suite/bugs/closed/2456.v index 5294adefd..e5a392c4d 100644 --- a/test-suite/bugs/opened/2456.v +++ b/test-suite/bugs/closed/2456.v @@ -50,4 +50,9 @@ Fail dependent destruction commute1; dependent destruction catchCommuteDetails; dependent destruction commute2; dependent destruction catchCommuteDetails generalizing X. -Admitted. +revert X. +dependent destruction commute1; +dependent destruction catchCommuteDetails; +dependent destruction commute2; +dependent destruction catchCommuteDetails. +Abort. diff --git a/test-suite/bugs/opened/2814.v b/test-suite/bugs/closed/2814.v index a740b4384..99da1e3e4 100644 --- a/test-suite/bugs/opened/2814.v +++ b/test-suite/bugs/closed/2814.v @@ -3,3 +3,4 @@ Require Import Program. Goal forall (x : Type) (f g : Type -> Type) (H : f x ~= g x), False. intros. Fail induction H. +Abort. diff --git a/test-suite/bugs/opened/3100.v b/test-suite/bugs/closed/3100.v index 6f35a74dc..6f35a74dc 100644 --- a/test-suite/bugs/opened/3100.v +++ b/test-suite/bugs/closed/3100.v diff --git a/test-suite/bugs/opened/3230.v b/test-suite/bugs/closed/3230.v index 265310b1a..265310b1a 100644 --- a/test-suite/bugs/opened/3230.v +++ b/test-suite/bugs/closed/3230.v diff --git a/test-suite/bugs/opened/3320.v b/test-suite/bugs/closed/3320.v index 05cf73281..0aac3c1b0 100644 --- a/test-suite/bugs/opened/3320.v +++ b/test-suite/bugs/closed/3320.v @@ -2,3 +2,4 @@ Goal forall x : nat, True. fix 1. assumption. Fail Qed. +Undo. diff --git a/test-suite/bugs/opened/3209.v b/test-suite/bugs/opened/3209.v deleted file mode 100644 index 3203afa13..000000000 --- a/test-suite/bugs/opened/3209.v +++ /dev/null @@ -1,17 +0,0 @@ -Inductive eqT {A} (x : A) : A -> Type := - reflT : eqT x x. -Definition Bi_inv (A B : Type) (f : (A -> B)) := - sigT (fun (g : B -> A) => - sigT (fun (h : B -> A) => - sigT (fun (α : forall b : B, eqT (f (g b)) b) => - forall a : A, eqT (h (f a)) a))). -Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f). - -Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B). -Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B := - sigT_rect (fun _ => TEquiv A B) - (fun (f : TEquiv A B -> eqT A B) H => - sigT_rect (fun _ => TEquiv A B) - (fun g _ => g e) - H) - (UA A B). diff --git a/test-suite/bugs/opened/3263.v b/test-suite/bugs/opened/3263.v deleted file mode 100644 index f0c707bd1..000000000 --- a/test-suite/bugs/opened/3263.v +++ /dev/null @@ -1,232 +0,0 @@ -Require Import TestSuite.admit. -(* File reduced by coq-bug-finder from originally 10918 lines, then 3649 lines to 3177 lines, then from 3189 lines to 3164 lines, then from 2653 lines to 2496 lines, 2653 lines, then from 1642 lines to 651 lines, then from 736 lines to 473 lines, then from 433 lines to 275 lines, then from 258 lines to 235 lines. *) -Generalizable All Variables. -Set Implicit Arguments. - -Arguments fst {_ _} _. -Arguments snd {_ _} _. - -Axiom cheat : forall {T}, T. - -Reserved Notation "g 'o' f" (at level 40, left associativity). - -Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a. -Arguments idpath {A a} , [A] a. -Notation "x = y" := (paths x y) : type_scope. - -Definition symmetry {A : Type} {x y : A} (p : x = y) : y = x - := match p with idpath => idpath end. - -Delimit Scope morphism_scope with morphism. -Delimit Scope category_scope with category. -Delimit Scope object_scope with object. -Record PreCategory (object : Type) := - Build_PreCategory' { - object :> Type := object; - morphism : object -> object -> Type; - identity : forall x, morphism x x; - compose : forall s d d', - morphism d d' - -> morphism s d - -> morphism s d' - where "f 'o' g" := (compose f g); - associativity : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - (m3 o m2) o m1 = m3 o (m2 o m1); - associativity_sym : forall x1 x2 x3 x4 - (m1 : morphism x1 x2) - (m2 : morphism x2 x3) - (m3 : morphism x3 x4), - m3 o (m2 o m1) = (m3 o m2) o m1; - left_identity : forall a b (f : morphism a b), identity b o f = f; - right_identity : forall a b (f : morphism a b), f o identity a = f; - identity_identity : forall x, identity x o identity x = identity x - }. -Bind Scope category_scope with PreCategory. -Arguments PreCategory {_}. -Arguments identity {_} [!C%category] x%object : rename. - -Arguments compose {_} [!C%category s%object d%object d'%object] m1%morphism m2%morphism : rename. - -Infix "o" := compose : morphism_scope. - -Delimit Scope functor_scope with functor. -Local Open Scope morphism_scope. -Record Functor `(C : @PreCategory objC, D : @PreCategory objD) := - { - object_of :> C -> D; - morphism_of : forall s d, morphism C s d - -> morphism D (object_of s) (object_of d); - composition_of : forall s d d' - (m1 : morphism C s d) (m2: morphism C d d'), - morphism_of _ _ (m2 o m1) - = (morphism_of _ _ m2) o (morphism_of _ _ m1); - identity_of : forall x, morphism_of _ _ (identity x) - = identity (object_of x) - }. -Bind Scope functor_scope with Functor. - -Arguments morphism_of {_} [C%category] {_} [D%category] F%functor [s%object d%object] m%morphism : rename, simpl nomatch. - -Notation "F '_1' m" := (morphism_of F m) (at level 10, no associativity) : morphism_scope. - -Class IsIsomorphism `{C : @PreCategory objC} {s d} (m : morphism C s d) := - { - morphism_inverse : morphism C d s; - left_inverse : morphism_inverse o m = identity _; - right_inverse : m o morphism_inverse = identity _ - }. - -Definition opposite `(C : @PreCategory objC) : PreCategory - := @Build_PreCategory' - C - (fun s d => morphism C d s) - (identity (C := C)) - (fun _ _ _ m1 m2 => m2 o m1) - (fun _ _ _ _ _ _ _ => @associativity_sym _ _ _ _ _ _ _ _ _) - (fun _ _ _ _ _ _ _ => @associativity _ _ _ _ _ _ _ _ _) - (fun _ _ => @right_identity _ _ _ _) - (fun _ _ => @left_identity _ _ _ _) - (@identity_identity _ C). - -Notation "C ^op" := (opposite C) (at level 3) : category_scope. - -Definition prod `(C : @PreCategory objC, D : @PreCategory objD) : @PreCategory (objC * objD). - refine (@Build_PreCategory' - (C * D)%type - (fun s d => (morphism C (fst s) (fst d) - * morphism D (snd s) (snd d))%type) - (fun x => (identity (fst x), identity (snd x))) - (fun s d d' m2 m1 => (fst m2 o fst m1, snd m2 o snd m1)) - _ - _ - _ - _ - _); admit. -Defined. -Infix "*" := prod : category_scope. - -Definition compose_functor `(C : @PreCategory objC, D : @PreCategory objD, E : @PreCategory objE) (G : Functor D E) (F : Functor C D) : Functor C E - := Build_Functor - C E - (fun c => G (F c)) - (fun _ _ m => morphism_of G (morphism_of F m)) - cheat - cheat. - -Infix "o" := compose_functor : functor_scope. - -Record NaturalTransformation `(C : @PreCategory objC, D : @PreCategory objD) (F G : Functor C D) := - Build_NaturalTransformation' { - components_of :> forall c, morphism D (F c) (G c); - commutes : forall s d (m : morphism C s d), - components_of d o F _1 m = G _1 m o components_of s; - - commutes_sym : forall s d (m : C.(morphism) s d), - G _1 m o components_of s = components_of d o F _1 m - }. -Definition functor_category `(C : @PreCategory objC, D : @PreCategory objD) : PreCategory - := @Build_PreCategory' (Functor C D) - (@NaturalTransformation _ C _ D) - cheat - cheat - cheat - cheat - cheat - cheat - cheat. - -Definition opposite_functor `(F : @Functor objC C objD D) : Functor C^op D^op - := Build_Functor (C^op) (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). - -Definition opposite_invL `(F : @Functor objC C^op objD D) : Functor C D^op - := Build_Functor C (D^op) - (object_of F) - (fun s d => morphism_of F (s := d) (d := s)) - (fun d' d s m1 m2 => composition_of F s d d' m2 m1) - (identity_of F). -Notation "F ^op" := (opposite_functor F) : functor_scope. - -Notation "F ^op'L" := (opposite_invL F) (at level 3) : functor_scope. -Definition fst `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) C - := Build_Functor (C * D) C - (@fst _ _) - (fun _ _ => @fst _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). - -Definition snd `{C : @PreCategory objC, D : @PreCategory objD} : Functor (C * D) D - := Build_Functor (C * D) D - (@snd _ _) - (fun _ _ => @snd _ _) - (fun _ _ _ _ _ => idpath) - (fun _ => idpath). -Definition prod_functor `(F : @Functor objC C objD D, F' : @Functor objC C objD' D') -: Functor C (D * D') - := Build_Functor - C (D * D') - (fun c => (F c, F' c)) - (fun s d m => (F _1 m, F' _1 m))%morphism - cheat - cheat. -Definition pair `(F : @Functor objC C objD D, F' : @Functor objC' C' objD' D') : Functor (C * C') (D * D') - := (prod_functor (F o fst) (F' o snd))%functor. -Notation cat_of obj := - (@Build_PreCategory' obj - (fun x y => forall _ : x, y) - (fun _ x => x) - (fun _ _ _ f g x => f (g x))%core - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ _ _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ _ _ => idpath) - (fun _ => idpath)). - -Definition hom_functor `(C : @PreCategory objC) : Functor (C^op * C) (cat_of Type) - := Build_Functor _ _ cheat cheat cheat cheat. - -Definition induced_hom_natural_transformation `(F : @Functor objC C objD D) -: NaturalTransformation (hom_functor C) (hom_functor D o pair F^op F) - := Build_NaturalTransformation' _ _ cheat cheat cheat. - -Class IsFullyFaithful `(F : @Functor objC C objD D) - := is_fully_faithful - : forall x y : C, - IsIsomorphism (induced_hom_natural_transformation F (x, y)). - -Definition coyoneda `(A : @PreCategory objA) : Functor A^op (@functor_category _ A _ (cat_of Type)) - := cheat. - -Definition yoneda `(A : @PreCategory objA) : Functor A (@functor_category _ A^op _ (cat_of Type)) - := (((coyoneda A^op)^op'L)^op'L)%functor. -Definition coyoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@coyoneda _ A). -Admitted. - -Definition yoneda_embedding_fast `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda. - Time let t := (type of CYE) in - let t' := (eval simpl in t) in pose proof ((fun (x : t) => (x : t')) CYE) as CYE'. (* Finished transaction in 0. secs (0.216013u,0.004s) *) - Fail Timeout 1 let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). - Time let t := match goal with |- ?G => constr:(G) end in - let t' := (eval simpl in t) in exact ((fun (x : t') => (x : t)) CYE'). (* Finished transaction in 0. secs (0.248016u,0.s) *) -Fail Timeout 2 Defined. -Time Defined. (* Finished transaction in 1. secs (0.432027u,0.s) *) - -Definition yoneda_embedding `(A : @PreCategory objA) : @IsFullyFaithful _ _ _ _ (@yoneda _ A). -Proof. - intros a b. - pose proof (coyoneda_embedding A^op a b) as CYE. - unfold yoneda; simpl in *. - Fail Timeout 1 exact CYE. - Time exact CYE. (* Finished transaction in 0. secs (0.012001u,0.s) *) -Fail Timeout 60 Defined. (* Timeout! *) diff --git a/test-suite/bugs/opened/3916.v b/test-suite/bugs/opened/3916.v deleted file mode 100644 index fd95503e6..000000000 --- a/test-suite/bugs/opened/3916.v +++ /dev/null @@ -1,3 +0,0 @@ -Require Import List. - -Fail Hint Resolve -> in_map. (* Also happens when using <- instead of -> *) diff --git a/test-suite/bugs/opened/3948.v b/test-suite/bugs/opened/3948.v deleted file mode 100644 index 5c4b4277b..000000000 --- a/test-suite/bugs/opened/3948.v +++ /dev/null @@ -1,25 +0,0 @@ -Module Type S. -Parameter t : Type. -End S. - -Module Bar(X : S). -Proof. - Definition elt := X.t. - Axiom fold : elt. -End Bar. - -Module Make (X: S) := Bar(X). - -Declare Module X : S. - -Module Type Interface. - Parameter constant : unit. -End Interface. - -Module DepMap : Interface. - Module Dom := Make(X). - Definition constant : unit := - let _ := @Dom.fold in tt. -End DepMap. - -Print Assumptions DepMap.constant. diff --git a/test-suite/bugs/opened/4813.v b/test-suite/bugs/opened/4813.v index b75170179..2ac553593 100644 --- a/test-suite/bugs/opened/4813.v +++ b/test-suite/bugs/opened/4813.v @@ -1,5 +1,5 @@ -(* An example one would like to see succeeding *) +Require Import Program.Tactics. Record T := BT { t : Set }. Record U (x : T) := BU { u : t x -> Prop }. -Fail Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. +Program Definition A (H : unit -> Prop) : U (BT unit) := BU _ H. diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index bbfe5ec42..49a8b9cf4 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -151,3 +151,17 @@ Section JLeivant. congruence. Qed. End JLeivant. + +(* An example with primitive projections *) + +Module PrimitiveProjections. +Set Primitive Projections. +Record t (A:Type) := { f : A }. +Goal forall g (a:t nat), @f nat = g -> f a = 0 -> g a = 0. +congruence. +Undo. +intros. +unfold f in H0. (* internally turn the projection to unfolded form *) +congruence. +Qed. +End PrimitiveProjections. diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index d0989cfcc..63b8b538a 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -272,6 +272,15 @@ let read_sentence ~state input = (* TopErr.print_toplevel_parse_error reraise top_buffer; *) Exninfo.iraise reraise +let extract_default_loc loc doc_id sid : Loc.t option = + match loc with + | Some _ -> loc + | None -> + try + let doc = Stm.get_doc doc_id in + Option.cata fst None Stm.(get_ast ~doc sid) + with _ -> loc + (** Coqloop Console feedback handler *) let coqloop_feed (fb : Feedback.feedback) = let open Feedback in match fb.contents with @@ -290,6 +299,9 @@ let coqloop_feed (fb : Feedback.feedback) = let open Feedback in (* Re-enable when we switch back to feedback-based error printing *) | Message (Error,loc,msg) -> () (* TopErr.print_error_for_buffer ?loc lvl msg top_buffer *) + | Message (Warning,loc,msg) -> + let loc = extract_default_loc loc fb.doc_id fb.span_id in + TopErr.print_error_for_buffer ?loc Warning msg top_buffer | Message (lvl,loc,msg) -> TopErr.print_error_for_buffer ?loc lvl msg top_buffer |