diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/Coercion.tex | 7 | ||||
| -rw-r--r-- | test-suite/success/coercions.v | 57 | ||||
| -rw-r--r-- | vernac/class.ml | 2 |
4 files changed, 61 insertions, 6 deletions
@@ -80,6 +80,7 @@ Vernacular Commands - Using “Require” inside a section is deprecated. - An experimental command "Show Extraction" allows to extract the content of the current ongoing proof (grant wish #4129). +- Coercion now accepts the type of its argument to be "Prop" or "Type". Universes diff --git a/doc/refman/Coercion.tex b/doc/refman/Coercion.tex index ec46e1eb5..53b6b7827 100644 --- a/doc/refman/Coercion.tex +++ b/doc/refman/Coercion.tex @@ -33,7 +33,7 @@ classes: \begin{itemize} \item {\tt Sortclass}, the class of sorts; - its objects are the terms whose type is a sort. + its objects are the terms whose type is a sort (e.g., \ssrC{Prop} or \ssrC{Type}). \item {\tt Funclass}, the class of functions; its objects are all the terms with a functional type, i.e. of form $forall~ x:A, B$. @@ -73,8 +73,8 @@ conditions holds: We then write $f:C \mbox{\texttt{>->}} D$. The restriction on the type of coercions is called {\em the uniform inheritance condition}. -Remark that the abstract classes {\tt Funclass} and {\tt Sortclass} -cannot be source classes. +Remark: the abstract class {\tt Sortclass} can be used as source class, +but the abstract class {\tt Funclass} cannot. To coerce an object $t:C~t_1..t_n$ of $C$ towards $D$, we have to apply the coercion $f$ to it; the obtained term $f~t_1..t_n~t$ is @@ -160,7 +160,6 @@ Declares the construction denoted by {\qualid} as a coercion between \item {\qualid} \errindex{not declared} \item {\qualid} \errindex{is already a coercion} \item \errindex{Funclass cannot be a source class} -\item \errindex{Sortclass cannot be a source class} \item {\qualid} \errindex{is not a function} \item \errindex{Cannot find the source class of {\qualid}} \item \errindex{Cannot recognize {\class$_1$} as a source class of {\qualid}} diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v index 9b11bc011..9389c9d32 100644 --- a/test-suite/success/coercions.v +++ b/test-suite/success/coercions.v @@ -130,4 +130,59 @@ Local Coercion l2v2 : list >-> vect. of coercions *) Fail Check (fun l : list (T1 * T1) => (l : vect _ _)). Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)). -Section what_we_could_do. +End what_we_could_do. + + +(** Unit test for Prop as source class *) + +Module TestPropAsSourceCoercion. + + Parameter heap : Prop. + + Parameter heap_empty : heap. + + Definition hprop := heap -> Prop. + + Coercion hpure (P:Prop) : hprop := fun h => h = heap_empty /\ P. + + Parameter heap_single : nat -> nat -> hprop. + + Parameter hstar : hprop -> hprop -> hprop. + + Notation "H1 \* H2" := (hstar H1 H2) (at level 69). + + Definition test := heap_single 4 5 \* (5 <> 4) \* heap_single 2 4 \* (True). + + (* Print test. -- reveals [hpure] coercions *) + +End TestPropAsSourceCoercion. + + +(** Unit test for Type as source class *) + +Module TestTypeAsSourceCoercion. + + Require Import Coq.Setoids.Setoid. + + Record setoid := { A : Type ; R : relation A ; eqv : Equivalence R }. + + Definition default_setoid (T : Type) : setoid + := {| A := T ; R := eq ; eqv := _ |}. + + Coercion default_setoid : Sortclass >-> setoid. + + Definition foo := Type : setoid. + + Inductive type := U | Nat. + Inductive term : type -> Type := + | ty (_ : Type) : term U + | nv (_ : nat) : term Nat. + + Coercion ty : Sortclass >-> term. + + Definition ty1 := Type : term _. + Definition ty2 := Prop : term _. + Definition ty3 := Set : term _. + Definition ty4 := (Type : Type) : term _. + +End TestTypeAsSourceCoercion. diff --git a/vernac/class.ml b/vernac/class.ml index cc676af1b..59d933108 100644 --- a/vernac/class.ml +++ b/vernac/class.ml @@ -225,7 +225,7 @@ let build_id_coercion idf_opt source poly = ConstRef kn let check_source = function -| Some (CL_FUN|CL_SORT as s) -> raise (CoercionError (ForbiddenSourceClass s)) +| Some (CL_FUN as s) -> raise (CoercionError (ForbiddenSourceClass s)) | _ -> () (* |