- Mar 07, 2022
-
-
Allan Blanchard authored
-
Allan Blanchard authored
-
Allan Blanchard authored
-
Allan Blanchard authored
- insert place holders for Dune tests
-
- Mar 01, 2022
-
-
Patrick Baudin authored
-
- Feb 25, 2022
-
-
Patrick Baudin authored
-
- Feb 24, 2022
-
-
-
Allan Blanchard authored
- it works only when the function is unique currently - only used for tests
-
Allan Blanchard authored
-
Allan Blanchard authored
-
- Feb 23, 2022
-
-
Patrick Baudin authored
-
- Feb 22, 2022
-
-
Patrick Baudin authored
-
Patrick Baudin authored
-
Patrick Baudin authored
-
- Feb 18, 2022
-
-
Allan Blanchard authored
-
- Feb 16, 2022
-
-
Patrick Baudin authored
-
- 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
-
Patrick Baudin 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
-