Skip to content

Commit

Permalink
fix compute
Browse files Browse the repository at this point in the history
  • Loading branch information
thery committed Oct 29, 2023
1 parent 64bfde1 commit cf031a5
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion Ssreflect15min/quesako.v
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ already require thinking a bit about data-structures and complexity. *)
Close Scope Z_scope.

(* E.g. unary numbes are not an option. *)
Time Eval compute in (1000 * 1000 : nat).
(* Time Eval compute in (1000 * 1000 : nat). *)

(* A reflection-based tactic replace explicit deduction steps,
logged in proof terms, with computational steps, checked by the kernel's
Expand Down

0 comments on commit cf031a5

Please sign in to comment.