Skip to content
Snippets Groups Projects
Commit 394c8d20 authored by Paolo G. Giarrusso's avatar Paolo G. Giarrusso Committed by Ralf Jung
Browse files

fix typo

parent 35705c3c
Branches
Tags
1 merge request!299alternative implementation of mk_evar that keeps naive_solver working
Pipeline #50596 passed
......@@ -227,7 +227,7 @@ Note that the obvious alternative [open_constr (_:T)] has subtly different
behavior, see std++ issue 115.
Usually, Ltacs cannot return a value and have a side-effect, but we use the
trickd escribed at
trick described at
<https://stackoverflow.com/questions/45949064/check-for-evars-in-a-tactic-that-returns-a-value/46178884#46178884>
to work around that: wrap the side-effect in a [match goal]. *)
Ltac mk_evar T :=
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment