coq/pretyping, branch master The formal proof system Merge PR #14041: Enable canonical fun _ => _ projections. 2021-04-23T14:48:49+00:00 coqbot-app[bot] 2021-04-23T14:48:49+00:00 d332bbc3c1118631eb8c935ba61a8d071a90428e Reviewed-by: gares Ack-by: Janno Ack-by: CohenCyril Ack-by: Zimmi48 Ack-by: jfehrle Ack-by: SkySkimmer 
Reviewed-by: gares
Ack-by: Janno
Ack-by: CohenCyril
Ack-by: Zimmi48
Ack-by: jfehrle
Ack-by: SkySkimmer
Enable canonical `fun _ => _` projections. 2021-04-22T07:16:22+00:00 Jan-Oliver Kaiser 2020-05-14T15:08:20+00:00 2cbc36c6ae4ca22e000dbb045c865f54a454aca3 






Merge PR #13911: Remove the :> type cast?
2021-04-21T14:58:51+00:00

coqbot-app[bot]

2021-04-21T14:58:51+00:00

f9996cdaf0b6aee12c5b71432b1edb90dffb569a

Reviewed-by: mattam82
Ack-by: Zimmi48





Reviewed-by: mattam82
Ack-by: Zimmi48







Remove the :> type cast
2021-03-30T16:51:56+00:00

Jim Fehrle

2021-03-07T18:15:11+00:00

eeb142f3c69d2467fbadd7dd1470ac1606b2e5bf












[flags] [profile] Remove bit-rotten CProfile code.
2021-03-30T13:37:00+00:00

Emilio Jesus Gallego Arias

2020-03-10T05:06:34+00:00

5d3c0a0326af68e85f1f1cfc6bfa2214b0052de8

As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.

It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.

We thus remove all bitrotten dead code.





As of today Coq has the `CProfile` infrastructure disabled by default,
untested, and not easily accessible.

It was decided that `CProfile` should remain not user-accessible, and
only available thus by manual editing of Coq code to switch the flag
and manually instrument functions.

We thus remove all bitrotten dead code.







[doc] cleanup pretyping/structures.mli
2021-03-26T19:21:46+00:00

Enrico Tassi

2021-03-26T19:21:46+00:00

d9c80dadd353bd8b0eb90ce290048a2538f1a41a












[recordops] complete API rewrite; the module is now called [structures]
2021-03-26T14:19:19+00:00

Enrico Tassi

2021-03-18T18:15:39+00:00

34ece1ae3e6696bdc9556e5019c3b8ec3fd23f8a












Merge PR #13909: Minimize the set of multiple inheritance (coercion) paths to check for conversion
2021-03-25T18:40:29+00:00

coqbot-app[bot]

2021-03-25T18:40:29+00:00

d1194d6458a433e34c3b4eecf13c18b084f4a9a5

Reviewed-by: gares
Ack-by: SkySkimmer





Reviewed-by: gares
Ack-by: SkySkimmer







Expose less interface in coercionops.mli
2021-03-25T15:24:37+00:00

Kazuhiko Sakaguchi

2021-03-25T15:24:37+00:00

f71129454d2c4ecde10e2a2e4284d6a576ee39ca












Move the responsibility of type-checking to the caller for tactic-in-terms.
2021-03-12T18:16:55+00:00

Pierre-Marie Pédrot

2021-03-12T17:30:09+00:00

5645beeab5801e86704c97b2cc8687b01c14acb8

Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.

This should be 1:1 equivalent to the previous code, we are just moving code
around.





Instead of taking a type and checking that the inferred type for the expression
is correct, we simply pick an optional constraint and return the type directly
in the callback. This prevents having to compute type conversion twice in the
special case of Ltac2 variable quotations.

This should be 1:1 equivalent to the previous code, we are just moving code
around.