Commit 6c54a423 authored by Ralf Jung's avatar Ralf Jung

coqdocify some comments

parent 93b4ec70
...@@ -10,8 +10,8 @@ Set Default Proof Using "Type". ...@@ -10,8 +10,8 @@ Set Default Proof Using "Type".
Export ListNotations. Export ListNotations.
From Coq.Program Require Export Basics Syntax. From Coq.Program Require Export Basics Syntax.
(** Enable implicit generalization. *) (** * Enable implicit generalization. *)
(* This option enables implicit generalization in arguments of the form (** This option enables implicit generalization in arguments of the form
`{...} (i.e., anonymous arguments). Unfortunately, it also enables `{...} (i.e., anonymous arguments). Unfortunately, it also enables
implicit generalization in `Instance`. We think that the fact taht both implicit generalization in `Instance`. We think that the fact taht both
behaviors are coupled together is a [bug in behaviors are coupled together is a [bug in
...@@ -63,13 +63,13 @@ Class NoBackTrack (P : Prop) := { no_backtrack : P }. ...@@ -63,13 +63,13 @@ Class NoBackTrack (P : Prop) := { no_backtrack : P }.
Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances. Hint Extern 0 (NoBackTrack _) => constructor; apply _ : typeclass_instances.
(** * Typeclass opaque definitions *) (** * Typeclass opaque definitions *)
(* The constant [tc_opaque] is used to make definitions opaque for just type (** The constant [tc_opaque] is used to make definitions opaque for just type
class search. Note that [simpl] is set up to always unfold [tc_opaque]. *) class search. Note that [simpl] is set up to always unfold [tc_opaque]. *)
Definition tc_opaque {A} (x : A) : A := x. Definition tc_opaque {A} (x : A) : A := x.
Typeclasses Opaque tc_opaque. Typeclasses Opaque tc_opaque.
Arguments tc_opaque {_} _ /. Arguments tc_opaque {_} _ /.
(* Below we define type class versions of the common logical operators. It is (** Below we define type class versions of the common logical operators. It is
important to note that we duplicate the definitions, and do not declare the important to note that we duplicate the definitions, and do not declare the
existing logical operators as type classes. That is, we do not say: existing logical operators as type classes. That is, we do not say:
......
...@@ -35,11 +35,10 @@ is rather efficient when having big hint databases, or expensive [Hint Extern] ...@@ -35,11 +35,10 @@ is rather efficient when having big hint databases, or expensive [Hint Extern]
declarations as the ones above. *) declarations as the ones above. *)
Tactic Notation "intuition" := intuition auto. Tactic Notation "intuition" := intuition auto.
(* [done] can get slow as it calls "trivial". [fast_done] can solve way less (** [done] can get slow as it calls "trivial". [fast_done] can solve way less
goals, but it will also always finish quickly. goals, but it will also always finish quickly. We do 'reflexivity' last because
We do 'reflexivity' last because for goals of the form ?x = y, if for goals of the form ?x = y, if we have x = y in the context, we will typically
we have x = y in the context, we will typically want to use the want to use the assumption and not reflexivity *)
assumption and not reflexivity *)
Ltac fast_done := Ltac fast_done :=
solve solve
[ eassumption [ eassumption
...@@ -321,7 +320,7 @@ Ltac f_equiv := ...@@ -321,7 +320,7 @@ Ltac f_equiv :=
try simple apply reflexivity. try simple apply reflexivity.
Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv. Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
(* The tactic [solve_proper_unfold] unfolds the first head symbol, so that (** The tactic [solve_proper_unfold] unfolds the first head symbol, so that
we proceed by repeatedly using [f_equiv]. *) we proceed by repeatedly using [f_equiv]. *)
Ltac solve_proper_unfold := Ltac solve_proper_unfold :=
(* Try unfolding the head symbol, which is the one we are proving a new property about *) (* Try unfolding the head symbol, which is the one we are proving a new property about *)
...@@ -335,9 +334,9 @@ Ltac solve_proper_unfold := ...@@ -335,9 +334,9 @@ Ltac solve_proper_unfold :=
| |- ?R (?f _ _) (?f _ _) => unfold f | |- ?R (?f _ _) (?f _ _) => unfold f
| |- ?R (?f _) (?f _) => unfold f | |- ?R (?f _) (?f _) => unfold f
end. end.
(* [solve_proper_prepare] does some preparation work before the main (** [solve_proper_prepare] does some preparation work before the main
[solve_proper] loop. Having this as a separate tactic is useful for [solve_proper] loop. Having this as a separate tactic is useful for debugging
debugging [solve_proper] failure. *) [solve_proper] failure. *)
Ltac solve_proper_prepare := Ltac solve_proper_prepare :=
(* Introduce everything *) (* Introduce everything *)
intros; intros;
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment