diff options
| -rw-r--r-- | doc/sphinx/language/cic.rst | 2 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 35 | ||||
| -rw-r--r-- | doc/sphinx/proof-engine/tactics.rst | 25 | ||||
| -rw-r--r-- | plugins/ssrmatching/g_ssrmatching.mlg | 2 | ||||
| -rw-r--r-- | plugins/ssrmatching/g_ssrmatching.mli | 13 | ||||
| -rw-r--r-- | pretyping/recordops.ml | 37 |
6 files changed, 82 insertions, 32 deletions
diff --git a/doc/sphinx/language/cic.rst b/doc/sphinx/language/cic.rst index 67683902cd..962d2a94e3 100644 --- a/doc/sphinx/language/cic.rst +++ b/doc/sphinx/language/cic.rst @@ -51,7 +51,7 @@ function types over these data types. Consequently they also have a type. Because assuming simply that :math:`\Set` has type :math:`\Set` leads to an inconsistent theory :cite:`Coq86`, the language of |Cic| has infinitely many sorts. There are, in addition to :math:`\Set` and :math:`\Prop` -a hierarchy of universes :math:`\Type(i)` for any integer :math:`i`. +a hierarchy of universes :math:`\Type(i)` for any integer :math:`i ≥ 1`. Like :math:`\Set`, all of the sorts :math:`\Type(i)` contain small sets such as booleans, natural numbers, as well as products, subsets and function diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 590d71b5f3..24645a8cc3 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -346,11 +346,46 @@ Navigation in the proof tree Goals are just existential variables and existential variables do not get a name by default. You can give a name to a goal by using :n:`refine ?[@ident]`. + You may also wrap this in an Ltac-definition like: + + .. coqtop:: in + + Ltac name_goal name := refine ?[name]. .. seealso:: :ref:`existential-variables` .. example:: + This first example uses the Ltac definition above, and the named goals + only serve for documentation. + + .. coqtop:: all + + Goal forall n, n + 0 = n. + Proof. + induction n; [ name_goal base | name_goal step ]. + [base]: { + + .. coqtop:: all + + reflexivity. + + .. coqtop:: in + + } + + .. coqtop:: all + + [step]: { + + .. coqtop:: all + + simpl. + f_equal. + assumption. + } + Qed. + This can also be a way of focusing on a shelved goal, for instance: .. coqtop:: all diff --git a/doc/sphinx/proof-engine/tactics.rst b/doc/sphinx/proof-engine/tactics.rst index 7eef504ea9..081fef07b9 100644 --- a/doc/sphinx/proof-engine/tactics.rst +++ b/doc/sphinx/proof-engine/tactics.rst @@ -3307,12 +3307,29 @@ the conversion in hypotheses :n:`{+ @ident}`. :name: fold This tactic applies to any goal. The term :n:`@term` is reduced using the - ``red`` tactic. Every occurrence of the resulting :n:`@term` in the goal is - then replaced by :n:`@term`. + :tacn:`red` tactic. Every occurrence of the resulting :n:`@term` in the goal is + then replaced by :n:`@term`. This tactic is particularly useful when a fixpoint + definition has been wrongfully unfolded, making the goal very hard to read. + On the other hand, when an unfolded function applied to its argument has been + reduced, the :tacn:`fold` tactic won't do anything. -.. tacv:: fold {+ @term} + .. example:: + + .. coqtop:: all + + Goal ~0=0. + unfold not. + Fail progress fold not. + pattern (0 = 0). + fold not. + + .. coqtop:: none + + Abort. + + .. tacv:: fold {+ @term} - Equivalent to :n:`fold @term ; ... ; fold @term`. + Equivalent to :n:`fold @term ; ... ; fold @term`. .. tacn:: pattern @term :name: pattern diff --git a/plugins/ssrmatching/g_ssrmatching.mlg b/plugins/ssrmatching/g_ssrmatching.mlg index 4ddaeb49fd..d1c7a23e99 100644 --- a/plugins/ssrmatching/g_ssrmatching.mlg +++ b/plugins/ssrmatching/g_ssrmatching.mlg @@ -8,6 +8,8 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) + { open Ltac_plugin diff --git a/plugins/ssrmatching/g_ssrmatching.mli b/plugins/ssrmatching/g_ssrmatching.mli index 588a1a3eac..65ea3f79c8 100644 --- a/plugins/ssrmatching/g_ssrmatching.mli +++ b/plugins/ssrmatching/g_ssrmatching.mli @@ -1,5 +1,14 @@ -(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) -(* Distributed under the terms of CeCILL-B. *) +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* (c) Copyright 2006-2015 Microsoft Corporation and Inria. *) open Genarg open Ssrmatching diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index f58cce41cc..6d9e3230a4 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -197,32 +197,19 @@ let keep_true_projections projs kinds = let filter (p, (_, b)) = if b then Some p else None in List.map_filter filter (List.combine projs kinds) -let cs_pattern_of_constr env t = +let rec cs_pattern_of_constr env t = match kind t with - App (f,vargs) -> - begin - try Const_cs (global_of_constr f) , None, Array.to_list vargs - with - | Not_found when isProj f -> - let p, c = destProj f in - let { Environ.uj_type = ty } = Typeops.infer env c in - let _, params = Inductive.find_rectype env ty in - Const_cs (ConstRef (Projection.constant p)), None, - params @ [c] @ Array.to_list vargs - | e when CErrors.noncritical e -> raise Not_found - end - | Rel n -> Default_cs, Some n, [] - | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] - | Proj (p, c) -> - let { Environ.uj_type = ty } = Typeops.infer env c in - let _, params = Inductive.find_rectype env ty in - Const_cs (ConstRef (Projection.constant p)), None, params @ [c] - | Sort s -> Sort_cs (Sorts.family s), None, [] - | _ -> - begin - try Const_cs (global_of_constr t) , None, [] - with e when CErrors.noncritical e -> raise Not_found - end + | App (f,vargs) -> + let patt, n, args = cs_pattern_of_constr env f in + patt, n, args @ Array.to_list vargs + | Rel n -> Default_cs, Some n, [] + | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b] + | Proj (p, c) -> + let { Environ.uj_type = ty } = Typeops.infer env c in + let _, params = Inductive.find_rectype env ty in + Const_cs (ConstRef (Projection.constant p)), None, params @ [c] + | Sort s -> Sort_cs (Sorts.family s), None, [] + | _ -> Const_cs (global_of_constr t) , None, [] let warn_projection_no_head_constant = CWarnings.create ~name:"projection-no-head-constant" ~category:"typechecker" |