aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/subtac/subtac_classes.ml14
-rw-r--r--doc/refman/Classes.tex66
-rw-r--r--doc/refman/Program.tex11
-rw-r--r--doc/refman/RefMan-ext.tex2
-rw-r--r--doc/refman/Setoid.tex24
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--theories/Classes/EquivDec.v27
-rw-r--r--theories/Classes/RelationClasses.v8
-rw-r--r--theories/Classes/SetoidClass.v6
-rw-r--r--theories/Classes/SetoidDec.v14
-rw-r--r--toplevel/classes.ml14
11 files changed, 103 insertions, 87 deletions
diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml
index cbfec12df4..15729b6266 100644
--- a/contrib/subtac/subtac_classes.ml
+++ b/contrib/subtac/subtac_classes.ml
@@ -137,11 +137,17 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
let sigma = Evd.evars_of !isevars in
let subst = List.map (Evarutil.nf_evar sigma) subst in
let subst =
- let props = match props with CRecord (loc, _, fs) -> fs
- | _ -> errorlabstrm "new_instance" (Pp.str "Expected a record declaration for the instance body")
+ let props =
+ match props with
+ | CRecord (loc, _, fs) ->
+ if List.length fs > List.length k.cl_props then
+ Classes.mismatched_props env' (List.map snd fs) k.cl_props;
+ fs
+ | _ ->
+ if List.length k.cl_props <> 1 then
+ errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body")
+ else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props]
in
- if List.length props > List.length k.cl_props then
- Classes.mismatched_props env' (List.map snd props) k.cl_props;
match k.cl_props with
| [(na,b,ty)] ->
let term = match props with [] -> CHole (Util.dummy_loc, None) | [(_,f)] -> f | _ -> assert false in
diff --git a/doc/refman/Classes.tex b/doc/refman/Classes.tex
index ecfe48e602..9bcca85895 100644
--- a/doc/refman/Classes.tex
+++ b/doc/refman/Classes.tex
@@ -2,7 +2,7 @@
\def\eol{\setlength\parskip{0pt}\par}
\def\indent#1{\noindent\kern#1}
\def\cst#1{\textsf{#1}}
-\def\tele#1{\overrightarrow{#1}}
+\def\tele#1{\ensuremath{\overrightarrow{#1}}}
\achapter{\protect{Type Classes}}
\aauthor{Matthieu Sozeau}
@@ -20,15 +20,15 @@ classes in \Haskell which also applies.
\asection{Class and Instance declarations}
\label{ClassesInstances}
-The syntax for class and instance declarations is a mix between the
-record syntax of \Coq~and the type classes syntax of \Haskell:
+The syntax for class and instance declarations is the same as
+record syntax of \Coq:
\def\kw{\texttt}
\def\classid{\texttt}
\begin{center}
\[\begin{array}{l}
-\kw{Class}~\classid{Id}~(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n)
-:= \{\\
+\kw{Class}~\classid{Id}~(\alpha_1 : \tau_1) \cdots (\alpha_n : \tau_n)
+[: \sort] := \{\\
\begin{array}{p{0em}lcl}
& \cst{f}_1 & : & \type_1 ; \\
& \vdots & & \\
@@ -37,11 +37,11 @@ record syntax of \Coq~and the type classes syntax of \Haskell:
\end{center}
\begin{center}
\[\begin{array}{l}
-\kw{Instance}~\ident~:~\classid{Id}~\term_1 \cdots \term_n :=\\
+\kw{Instance}~\ident~:~\classid{Id}~\term_1 \cdots \term_n := \{\\
\begin{array}{p{0em}lcl}
& \cst{f}_1 & := & \term_{f_1} ; \\
& \vdots & & \\
- & \cst{f}_m & := & \term_{f_m}.
+ & \cst{f}_m & := & \term_{f_m} \}.
\end{array}\end{array}\]
\end{center}
\begin{coq_eval}
@@ -67,9 +67,9 @@ leibniz equality on some type. An example implementation is:
\begin{coq_example*}
Instance unit_EqDec : EqDec unit :=
- eqb x y := true ;
+{ eqb x y := true ;
eqb_leibniz x y H :=
- match x, y return x = y with tt, tt => refl_equal tt end.
+ match x, y return x = y with tt, tt => refl_equal tt end }.
\end{coq_example*}
If one does not give all the members in the \texttt{Instance}
@@ -78,9 +78,8 @@ inhabitants of the remaining fields, e.g.:
\begin{coq_example*}
Instance eq_bool : EqDec bool :=
- eqb x y := if x then y else negb y.
+{ eqb x y := if x then y else negb y }.
\end{coq_example*}
-
\begin{coq_example}
Proof. intros x y H.
destruct x ; destruct y ; (discriminate || reflexivity).
@@ -96,7 +95,7 @@ richer facilities for dealing with obligations.
Once a type class is declared, one can use it in class binders:
\begin{coq_example}
- Definition neqb {A : Type} {eqa : EqDec A} (x y : A) := negb (eqb x y).
+Definition neqb {A} {eqa : EqDec A} (x y : A) := negb (eqb x y).
\end{coq_example}
When one calls a class method, a constraint is generated that is
@@ -106,7 +105,7 @@ satisfied by \texttt{{eqa : EqDec A}}. In case no satisfying constraint can be
found, an error is raised:
\begin{coq_example}
- Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
+Definition neqb' (A : Type) (x y : A) := negb (eqb x y).
\end{coq_example}
The algorithm used to solve constraints is a variant of the eauto tactic
@@ -116,7 +115,7 @@ local hypotheses as well as declared lemmas in the
written:
\begin{coq_example}
- Definition neqb' (A : Type) (eqa : EqDec A) (x y : A) := negb (eqb x y).
+Definition neqb' A (eqa : EqDec A) (x y : A) := negb (eqb x y).
\end{coq_example}
However, the generalizing binders should be used instead as they have
@@ -142,7 +141,7 @@ binders begining with a backquote \texttt{`} and the codomain of
Following the previous example, one can write:
\begin{coq_example}
- Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
+Definition neqb_impl `{eqa : EqDec A} (x y : A) := negb (eqb x y).
\end{coq_example}
Here \texttt{A} is implicitely generalized, and the resulting function
@@ -164,9 +163,9 @@ the constraints as a binding context before the instance, e.g.:
\begin{coq_example}
Instance prod_eqb `(EA : EqDec A, EB : EqDec B) : EqDec (A * B) :=
- eqb x y := match x, y with
+{ eqb x y := match x, y with
| (la, ra), (lb, rb) => andb (eqb la lb) (eqb ra rb)
- end.
+ end }.
\end{coq_example}
\begin{coq_eval}
Admitted.
@@ -182,10 +181,10 @@ One can also parameterize classes by other classes, generating a
hierarchy of classes and superclasses. In the same way, we give the
superclasses as a binding context:
-\begin{coq_example}
+\begin{coq_example*}
Class Ord `(E : EqDec A) :=
{ le : A -> A -> bool }.
-\end{coq_example}
+\end{coq_example*}
Contrary to \Haskell, we have no special syntax for superclasses, but
this declaration is morally equivalent to:
@@ -202,20 +201,18 @@ As we have seen, \texttt{Ord} is encoded as a record type with two parameters:
a type \texttt{A} and an \texttt{E} of type \texttt{EqDec A}. However, one can
still use it as if it had a single parameter inside generalizing binders: the
generalization of superclasses will be done automatically.
-\begin{coq_example}
-Definition le_eqb `{Ord A} (x y : A) :=
- andb (le x y) (le y x).
-\end{coq_example}
+\begin{coq_example*}
+Definition le_eqb `{Ord A} (x y : A) := andb (le x y) (le y x).
+\end{coq_example*}
In some cases, to be able to specify sharing of structures, one may want to give
explicitely the superclasses. It is is possible to do it directly in regular
binders, and using the \texttt{!} modifier in class binders. For
example:
-
-\begin{coq_example}
-Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) :=
+\begin{coq_example*}
+Definition lt `{eqa : EqDec A, ! Ord eqa} (x y : A) :=
andb (le x y) (neqb x y).
-\end{coq_example}
+\end{coq_example*}
The \texttt{!} modifier switches the way a binder is parsed back to the
regular interpretation of Coq. In particular, it uses the implicit
@@ -237,7 +234,8 @@ Class Transitive (A : Type) (R : relation A) :=
transitivity : forall x y z, R x y -> R y z -> R x z.
\end{coq_example*}
-This declares singleton classes for reflexive and transitive relations.
+This declares singleton classes for reflexive and transitive relations,
+(see \ref{SingletonClass} for an explanation).
These may be used as part of other classes:
\begin{coq_example*}
@@ -259,7 +257,7 @@ same effect.
\section{Summary of the commands
\label{TypeClassCommands}}
-\subsection{\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$}
+\subsection{\tt Class {\ident} {\binder$_1$ \ldots~\binder$_n$}
: \sort := \{ field$_1$ ; \ldots ; field$_k$ \}.}
\comindex{Class}
\label{Class}
@@ -269,7 +267,7 @@ parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
{\tt field$_k$}.
\begin{Variants}
-\item {\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$}
+\item \label{SingletonClass} {\tt Class {\ident} {\binder$_1$ \ldots \binder$_n$}
: \sort := \ident$_1$ : \type$_1$.}
This variant declares a \emph{singleton} class whose only method is
{\tt \ident$_1$}. This singleton class is a so-called definitional
@@ -286,7 +284,7 @@ parameters {\binder$_1$} to {\binder$_n$} and fields {\tt field$_1$} to
\subsection{\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
{Class} {t$_1$ \ldots t$_n$} [| \textit{priority}]
- := field$_1$ := b$_1$ ; \ldots ; field$_i$ := b$_i$}
+ := \{ field$_1$ := b$_1$ ; \ldots ; field$_i$ := b$_i$ \}}
\comindex{Instance}
\label{Instance}
@@ -302,6 +300,12 @@ An optional \textit{priority} can be declared, 0 being the highest
priority as for auto hints.
\begin{Variants}
+\item {\tt Instance {\ident} {\binder$_1$ \ldots \binder$_n$} :
+ {Class} {t$_1$ \ldots t$_n$} [| \textit{priority}] := \term}
+ This syntax is used for declaration of singleton class instances.
+ It does not include curly braces and one need not even mention
+ the unique field name.
+
\item {\tt Instance Global} One can use the \texttt{Global} modifier on
instances declared in a section so that their generalization is automatically
redeclared after the section is closed.
diff --git a/doc/refman/Program.tex b/doc/refman/Program.tex
index dfcebf1860..20444dc0a1 100644
--- a/doc/refman/Program.tex
+++ b/doc/refman/Program.tex
@@ -137,18 +137,18 @@ Program Fixpoint div2 (n : nat) : { x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
\end{coq_example}
Here we have one obligation for each branch (branches for \verb:0: and \verb:(S 0): are
-automatically generated by the pattern-matching compilation algorithm):
+automatically generated by the pattern-matching compilation algorithm).
\begin{coq_example}
- Obligations.
+ Obligation 1.
\end{coq_example}
-You can use a well-founded order or a measure as termination orders using the syntax:
+One can use a well-founded order or a measure as termination orders using the syntax:
\begin{coq_eval}
Reset Initial.
Require Import Arith.
Require Import Program.
\end{coq_eval}
-\begin{coq_example}
+\begin{coq_example*}
Definition id (n : nat) := n.
Program Fixpoint div2 (n : nat) {measure id n} :
{ x : nat | n = 2 * x \/ n = 2 * x + 1 } :=
@@ -156,7 +156,7 @@ Program Fixpoint div2 (n : nat) {measure id n} :
| S (S p) => S (div2 p)
| _ => O
end.
-\end{coq_example}
+\end{coq_example*}
The \verb|measure| keyword expects a measure function into the naturals, whereas
\verb|wf| expects a relation.
@@ -270,4 +270,5 @@ Program Fixpoint f (x : A | P) { measure size } :=
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
+%%% compile-command: "BIBINPUTS=\".\" make -C ../.. -f Makefile.stage3 doc/refman/Reference-Manual.pdf"
%%% End:
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 502b42b837..8b404f4efa 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -24,7 +24,7 @@ construction allows to define ``signatures''.
&& ~~~~\zeroone{\ident}
\verb!{! \zeroone{\nelist{\field}{;}} \verb!}! \verb:.:\\
& & \\
-{\field} & ::= & {\name} : {\type} \\
+{\field} & ::= & {\name} : {\type} [ {\tt where} {\it notation} ] \\
& $|$ & {\name} {\typecstr} := {\term}
\end{tabular}
\end{centerframe}
diff --git a/doc/refman/Setoid.tex b/doc/refman/Setoid.tex
index c2d20b4905..6a80be633d 100644
--- a/doc/refman/Setoid.tex
+++ b/doc/refman/Setoid.tex
@@ -482,8 +482,7 @@ can be registered as parametric relations and morphisms.
\begin{cscexample}[First class setoids]
\begin{coq_example*}
-Require Export Relation_Definitions.
-Require Import Setoid.
+Require Import Relation_Definitions Setoid.
Record Setoid: Type :=
{ car:Type;
eq:car->car->Prop;
@@ -494,8 +493,7 @@ Record Setoid: Type :=
Add Parametric Relation (s : Setoid) : (@car s) (@eq s)
reflexivity proved by (refl s)
symmetry proved by (sym s)
- transitivity proved by (trans s)
-as eq_rel.
+ transitivity proved by (trans s) as eq_rel.
Record Morphism (S1 S2:Setoid): Type :=
{ f:car S1 ->car S2;
compat: forall (x1 x2: car S1), eq S1 x1 x2 -> eq S2 (f x1) (f x2) }.
@@ -636,13 +634,15 @@ Admitted.
One then has to show that if two predicates are equivalent at every
point, their universal quantifications are equivalent. Once we have
declared such a morphism, it will be used by the setoid rewriting tactic
-each time we try to rewrite under a binder. Indeed, when rewriting under
-a lambda, binding variable $x$, say from $P~x$ to $Q~x$ using the
-relation \texttt{iff}, the tactic will generate a proof of
-\texttt{pointwise\_relation A iff (fun x => P x) (fun x => Q x)}
-from the proof of \texttt{iff (P x) (Q x)} and a
-constraint of the form \texttt{Morphism (pointwise\_relation A iff ==> ?) m}
-will be generated for the surrounding morphism \texttt{m}.
+each time we try to rewrite under an \texttt{all} application (products
+in \Prop{} are implicitely translated to such applications).
+
+Indeed, when rewriting under a lambda, binding variable $x$, say from
+$P~x$ to $Q~x$ using the relation \texttt{iff}, the tactic will generate
+a proof of \texttt{pointwise\_relation A iff (fun x => P x) (fun x => Q
+x)} from the proof of \texttt{iff (P x) (Q x)} and a constraint of the
+form \texttt{Morphism (pointwise\_relation A iff ==> ?) m} will be
+generated for the surrounding morphism \texttt{m}.
Hence, one can add higher-order combinators as morphisms by providing
signatures using pointwise extension for the relations on the functional
@@ -694,7 +694,7 @@ any rewriting constraints arising from a rewrite using \texttt{iff},
\texttt{impl} or \texttt{inverse impl} through \texttt{and}.
Sub-relations are implemented in \texttt{Classes.Morphisms} and are a
-prime example of a completely user-space extension of the algorithm.
+prime example of a mostly user-space extension of the algorithm.
\asection{Constant unfolding}
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3a88a09f81..2b99fee979 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -505,7 +505,8 @@ GEXTEND Gram
| IDENT "Instance"; name = identref; sup = OPT binders_let; ":";
expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200";
pri = OPT [ "|"; i = natural -> i ] ;
- props = [ ":="; decl = record_declaration -> decl | -> CRecord (loc, None, []) ] ->
+ props = [ ":="; "{"; r = record_declaration; "}" -> r |
+ ":="; c = lconstr -> c | -> CRecord (loc, None, []) ] ->
let sup =
match sup with
None -> []
@@ -695,7 +696,6 @@ GEXTEND Gram
| IDENT "Hint"; "*" -> PrintHintDb
| IDENT "HintDb"; s = IDENT -> PrintHintDbName s
| "Rewrite"; IDENT "HintDb"; s = IDENT -> PrintRewriteHintDbName s
- | IDENT "Setoids" -> PrintSetoids
| IDENT "Scopes" -> PrintScopes
| IDENT "Scope"; s = IDENT -> PrintScope s
| IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v
index b85d5d7d24..ff407182df 100644
--- a/theories/Classes/EquivDec.v
+++ b/theories/Classes/EquivDec.v
@@ -9,7 +9,7 @@
(* Decidable equivalences.
*
* Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
* 91405 Orsay, France *)
(* $Id$ *)
@@ -75,16 +75,13 @@ Require Import Coq.Arith.Peano_dec.
(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
-Program Instance nat_eq_eqdec : EqDec nat eq :=
- equiv_dec := eq_nat_dec.
+Program Instance nat_eq_eqdec : EqDec nat eq := eq_nat_dec.
Require Import Coq.Bool.Bool.
-Program Instance bool_eqdec : EqDec bool eq :=
- equiv_dec := bool_dec.
+Program Instance bool_eqdec : EqDec bool eq := bool_dec.
-Program Instance unit_eqdec : EqDec unit eq :=
- equiv_dec x y := in_left.
+Program Instance unit_eqdec : EqDec unit eq := λ x y, in_left.
Next Obligation.
Proof.
@@ -94,24 +91,24 @@ Program Instance unit_eqdec : EqDec unit eq :=
Program Instance prod_eqdec `(EqDec A eq, EqDec B eq) :
! EqDec (prod A B) eq :=
- equiv_dec x y :=
+ { equiv_dec x y :=
let '(x1, x2) := x in
let '(y1, y2) := y in
if x1 == y1 then
if x2 == y2 then in_left
else in_right
- else in_right.
+ else in_right }.
Solve Obligations using unfold complement, equiv ; program_simpl.
Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
- EqDec (sum A B) eq :=
+ EqDec (sum A B) eq := {
equiv_dec x y :=
match x, y with
| inl a, inl b => if a == b then in_left else in_right
| inr a, inr b => if a == b then in_left else in_right
| inl _, inr _ | inr _, inl _ => in_right
- end.
+ end }.
Solve Obligations using unfold complement, equiv ; program_simpl.
@@ -119,11 +116,11 @@ Program Instance sum_eqdec `(EqDec A eq, EqDec B eq) :
Proving the reflection requires functional extensionality though. *)
Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
- equiv_dec f g :=
+ { equiv_dec f g :=
if f true == g true then
if f false == g false then in_left
else in_right
- else in_right.
+ else in_right }.
Solve Obligations using try red ; unfold equiv, complement ; program_simpl.
@@ -136,7 +133,7 @@ Program Instance bool_function_eqdec `(EqDec A eq) : ! EqDec (bool -> A) eq :=
Require Import List.
Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
- equiv_dec :=
+ { equiv_dec :=
fix aux (x : list A) y { struct x } :=
match x, y with
| nil, nil => in_left
@@ -145,7 +142,7 @@ Program Instance list_eqdec `(eqa : EqDec A eq) : ! EqDec (list A) eq :=
if aux tl tl' then in_left else in_right
else in_right
| _, _ => in_right
- end.
+ end }.
Solve Obligations using unfold equiv, complement in * ; program_simpl ; intuition (discriminate || eauto).
diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v
index b9256bdbc0..659289f889 100644
--- a/theories/Classes/RelationClasses.v
+++ b/theories/Classes/RelationClasses.v
@@ -71,10 +71,10 @@ Hint Extern 4 => solve_relation : relations.
(** We can already dualize all these properties. *)
Program Instance flip_Reflexive `(Reflexive A R) : Reflexive (flip R) :=
- reflexivity := reflexivity (R:=R).
+ reflexivity (R:=R).
Program Instance flip_Irreflexive `(Irreflexive A R) : Irreflexive (flip R) :=
- irreflexivity := irreflexivity (R:=R).
+ irreflexivity (R:=R).
Program Instance flip_Symmetric `(Symmetric A R) : Symmetric (flip R).
@@ -168,8 +168,8 @@ Class Equivalence {A} (R : relation A) : Prop := {
(** An Equivalence is a PER plus reflexivity. *)
Instance Equivalence_PER `(Equivalence A R) : PER R | 10 :=
- PER_Symmetric := Equivalence_Symmetric ;
- PER_Transitive := Equivalence_Transitive.
+ { PER_Symmetric := Equivalence_Symmetric ;
+ PER_Transitive := Equivalence_Transitive }.
(** We can now define antisymmetry w.r.t. an equivalence relation on the carrier. *)
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index 78616a9a42..ae03e28e56 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -56,7 +56,7 @@ Existing Instance setoid_trans.
(* equiv := eq ; setoid_equiv := eq_equivalence. *)
Program Instance iff_setoid : Setoid Prop :=
- equiv := iff ; setoid_equiv := iff_equivalence.
+ { equiv := iff ; setoid_equiv := iff_equivalence }.
(** Overloaded notations for setoid equivalence and inequivalence. Not to be confused with [eq] and [=]. *)
@@ -120,10 +120,10 @@ Ltac setoidify := repeat setoidify_tac.
(** Every setoid relation gives rise to a morphism, in fact every partial setoid does. *)
Program Instance setoid_morphism `(sa : Setoid A) : Morphism (equiv ++> equiv ++> iff) equiv :=
- respect := respect.
+ respect.
Program Instance setoid_partial_app_morphism `(sa : Setoid A) (x : A) : Morphism (equiv ++> iff) (equiv x) :=
- respect := respect.
+ respect.
Ltac morphism_tac := try red ; unfold arrow ; intros ; program_simpl ; try tauto.
diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v
index 8504a06f43..d68e3fd22b 100644
--- a/theories/Classes/SetoidDec.v
+++ b/theories/Classes/SetoidDec.v
@@ -9,7 +9,7 @@
(* Decidable setoid equality theory.
*
* Author: Matthieu Sozeau
- * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud
+ * Institution: LRI, CNRS UMR 8623 - UniversitÃcopyright Paris Sud
* 91405 Orsay, France *)
(* $Id$ *)
@@ -75,18 +75,18 @@ Require Import Coq.Arith.Arith.
(** The equiv is burried inside the setoid, but we can recover it by specifying which setoid we're talking about. *)
Program Instance eq_setoid A : Setoid A | 10 :=
- equiv := eq ; setoid_equiv := eq_equivalence.
+ { equiv := eq ; setoid_equiv := eq_equivalence }.
Program Instance nat_eq_eqdec : EqDec (eq_setoid nat) :=
- equiv_dec := eq_nat_dec.
+ eq_nat_dec.
Require Import Coq.Bool.Bool.
Program Instance bool_eqdec : EqDec (eq_setoid bool) :=
- equiv_dec := bool_dec.
+ bool_dec.
Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
- equiv_dec x y := in_left.
+ λ x y, in_left.
Next Obligation.
Proof.
@@ -95,7 +95,7 @@ Program Instance unit_eqdec : EqDec (eq_setoid unit) :=
Qed.
Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : EqDec (eq_setoid (prod A B)) :=
- equiv_dec x y :=
+ λ x y,
let '(x1, x2) := x in
let '(y1, y2) := y in
if x1 == y1 then
@@ -108,7 +108,7 @@ Program Instance prod_eqdec `(! EqDec (eq_setoid A), ! EqDec (eq_setoid B)) : Eq
(** Objects of function spaces with countable domains like bool have decidable equality. *)
Program Instance bool_function_eqdec `(! EqDec (eq_setoid A)) : EqDec (eq_setoid (bool -> A)) :=
- equiv_dec f g :=
+ λ f g,
if f true == g true then
if f false == g false then in_left
else in_right
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 7ff942253a..081d182921 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -185,9 +185,17 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true)
end
else
begin
- let props = match props with CRecord (loc, _, fs) -> fs | _ -> assert false in
- if List.length props > List.length k.cl_props then
- mismatched_props env' (List.map snd props) k.cl_props;
+ let props =
+ match props with
+ | CRecord (loc, _, fs) ->
+ if List.length fs > List.length k.cl_props then
+ mismatched_props env' (List.map snd fs) k.cl_props;
+ fs
+ | _ ->
+ if List.length k.cl_props <> 1 then
+ errorlabstrm "new_instance" (Pp.str "Expected a definition for the instance body")
+ else [(dummy_loc, Nameops.out_name (pi1 (List.hd k.cl_props))), props]
+ in
let subst =
match k.cl_props with
| [(na,b,ty)] ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 06:13:03 +0000