aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Lists/TheoryList.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Lists/TheoryList.v')
-rw-r--r--theories/Lists/TheoryList.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Lists/TheoryList.v b/theories/Lists/TheoryList.v
index 226d07149..5185f2c53 100644
--- a/theories/Lists/TheoryList.v
+++ b/theories/Lists/TheoryList.v
@@ -349,7 +349,7 @@ destruct (TS_dec a) as [[c H1]| ].
left; exists c.
exists a; auto.
auto.
-(*
+(*
Realizer try_find.
*)
Qed.
@@ -359,7 +359,7 @@ End Find_sec.
Section Assoc_sec.
Variable B : Type.
-Fixpoint assoc (a:A) (l:list (A * B)) {struct l} :
+Fixpoint assoc (a:A) (l:list (A * B)) {struct l} :
Exc B :=
match l with
| nil => error