- Feb 15, 2022
-
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
-
-
-
-
- Feb 11, 2022
-
-
Patrick Baudin authored
-
- Feb 10, 2022
-
-
Thibaut Benjamin authored
-
Thibaut Benjamin authored
-
- Feb 08, 2022
-
-
Andre Maroneze authored
-
Andre Maroneze authored
-
Andre Maroneze authored
-
Andre Maroneze authored
-
Andre Maroneze authored
-
- Feb 07, 2022
-
-
Valentin Perrelle authored
-
- Feb 02, 2022
-
-
Allan Blanchard authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Allan Blanchard authored
- annots order for multiple emitters is unspecified, - use the order used in the Printer
-
Patrick Baudin authored
[Wp] generic sequent simplifier: applies simplify+assume succesively on each terms of a the disjonctive goal
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
[Wp] generic sequent simplifier: applies simplify+assume succesively on eacterms of a the conjective hypothesis
-
Allan Blanchard authored
-
- Feb 01, 2022
-
-
Allan Blanchard authored
-
Allan Blanchard authored
- not available from GUI for now - TacClear and TacUnfold adapted
-
Allan Blanchard authored
-
Allan Blanchard authored
- Rationale: detect RTE fail sooner
-
Allan Blanchard authored
- A1 A2 ... : prove A1 -> hyp A1 -> prove A2 -> hyp A2 ... - Move smoke tests to the end of code assertions
-
Patrick Baudin authored
-
- Jan 31, 2022
-
-
Andre Maroneze authored
-
-
- Jan 28, 2022
-
-
Basile Desloges authored
-
Basile Desloges authored
The term corresponding to the logic var introduced is translated without the logic var in the logic scope.
-