Skip to content

Commit

Permalink
[TC] rebasing adding tc. prefix to test
Browse files Browse the repository at this point in the history
  • Loading branch information
FissoreD committed Jul 31, 2024
1 parent a00dae5 commit 9d8cdf7
Showing 1 changed file with 1 addition and 2 deletions.
3 changes: 1 addition & 2 deletions apps/tc/tests/hyp_in_conl.v
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,6 @@ Module M3.
Local Instance AX : A := {}.
Local Instance BX : A -> (B AX) := {}.

Elpi Accumulate TC.Solver lp:{{ print-goal. print-solution. }}.
Definition d : C AX (BX _) := _.
Definition d' : C _ (BX _) := _.
Definition d'' : C AX _ := _.
Expand All @@ -74,7 +73,7 @@ Module M3.
*)
Elpi Query TC.Solver lp:{{
S = {{c AX (BX _)}},
solve-aux1 [] {{C _ _}} S.
tc.solve-aux1 [] {{C _ _}} S.
}}.

End s.
Expand Down

0 comments on commit 9d8cdf7

Please sign in to comment.