coq
coq copied to clipboard
coq
Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive developme...
When printing Exn1 raises Exn2, it used to say ~~~ : backtrace of Exn2
#### Description of the problem CoqIDE does not check which version of Coq it runs and does not report this version to the user (it reports the version of CoqIDE...
With @Alizter, we noticed that the refman and stdlib-doc jobs take about 10 minutes longer in master compared to the equivalent Dune jobs in v8.16.
```coq Goal forall n m:nat, m > 0 -> True /\ False. intros. split. 2: refine ?[Goal]. Show Existentials. (* Existential 1 = ?Goal : [n : nat m :...
Neither of these does the trick: 
It seems to me we should show the name of named goals such as "foo" in the context even if `Printing Goal Names` isn't enabled. Maybe like this: ```coq ______________________________________(?foo)...
Windows doesn't support signals, so another mechanism was used to support "Interrupt computations" in CoqIDE. On Windows, every process that shares a console (i.e. coqide and all the coqidetop's and...
This is a prototype implementation for CEP https://github.com/coq/ceps/pull/65 We add a common metadata object to atomic libobjects, so we can store documentation, location, and other interesting attributes that are needed...
