fixup attribute parsing

LPCIC · Nov 8, 2023 · 77136d0 · 77136d0
1 parent 13c3290
commit 77136d0
Show file tree

Hide file tree

Showing 2 changed files with 16 additions and 1 deletion.
diff --git a/apps/tc/elpi/create_tc_predicate.elpi b/apps/tc/elpi/create_tc_predicate.elpi
@@ -55,7 +55,9 @@ attr->modes CoqModes :-
 attr->modes [].
 
 pred get-key-from-option i:prop, o:string. 
-get-key-from-option (get-option A _) A :- !.
+get-key-from-option (get-option A tt) A :- !.
+get-key-from-option (get-option "i" ff) "o" :- !.
+get-key-from-option (get-option "o" ff) "i" :- !.
 get-key-from-option A _ :- coq.error A "should be an option".
 
 pred declare-class-in-coq i:gref.

diff --git a/apps/tc/tests/classes_declare.v b/apps/tc/tests/classes_declare.v
@@ -59,4 +59,17 @@ Section S3.
 
 End S3.
 
+Section S31.
+  #[mode(o=ff)] TC.Declare Class class31 (n : nat).
+  Instance inst31 : class31 0. Proof. apply Build_class31. Qed.
+
+  Goal exists x, class31 x. 
+  Proof.
+    eexists.
+    Succeed apply inst31.
+    Fail apply _.
+  Abort.
+
+End S31.
+