coq/test-suite/output-coqtop, branch master The formal proof system Avoid using "subgoals" in the UI, it means the same as "goals" 2021-01-13T23:24:23+00:00 Jim Fehrle 2020-12-17T23:04:36+00:00 3da2dbe9728ae7f5b1860a8e3a6c458e6d976f84 






Slight improvement in naming existential variables.
2020-06-01T17:56:12+00:00

Hugo Herbelin

2020-05-31T16:38:34+00:00

f12b5b295afcd387624a8404a1385f5a1a66e2a9

In a Meta := Evar unification problem and the Meta is bound to a
(named) binder, and the Evar is a GoalEvar, we set the source of the
evar to be the one of the Meta.





In a Meta := Evar unification problem and the Meta is bound to a
(named) binder, and the Evar is a GoalEvar, we set the source of the
evar to be the one of the Meta.







Use implicit arguments in notations for eq.
2020-02-25T12:43:23+00:00

Gaëtan Gilbert

2020-02-20T15:50:24+00:00

0dab087b10598f79ffa4f907c6d93fb7932e1c5b

This gives IMO slightly nicer errors when the type cannot be inferred,
ie
~~~coq
Type (forall x, x = x).
~~~
says "cannot infer the implicit parameter A of eq" instead of "cannot
infer this placeholder".





This gives IMO slightly nicer errors when the type cannot be inferred,
ie
~~~coq
Type (forall x, x = x).
~~~
says "cannot infer the implicit parameter A of eq" instead of "cannot
infer this placeholder".







Show diffs in "Show Proof."
2019-10-29T18:25:01+00:00

Jim Fehrle

2019-07-07T02:25:39+00:00

5ec7eca640a6ee495eb2c0fb8d8a4076256ff96d

Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output





Add experimental "Show Proof" command to the toplevel that shadows
the current command in the parser (in coqtop and PG only).
Apply existing code to highlight diffs in the output







Fix #10420 Add dependent evar mapping info to output
2019-09-19T19:56:42+00:00

Jim Fehrle

2019-07-05T06:19:10+00:00

04105f0430cad4e8d018ab47efccf79bf8511a32












Re-add the "Show Goal" command for Prooftree in PG.
2019-06-25T19:45:03+00:00

Jim Fehrle

2019-06-08T12:04:41+00:00

403917b7d9ecb2ddfaaac2185c355d415d5fa5bc

It prints a goal given its internal goal id and the Stm state id.





It prints a goal given its internal goal id and the Stm state id.