From 5da679d276e106a62cc3368ceb7358da289ea10a Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 24 Oct 2016 01:25:40 +0200 Subject: Complete overhaul of the Arguments vernacular. The main point of this change is to fix #3035: Avoiding trailing arguments in the Arguments command, and related issues occurring in HoTT for instance. When the "assert" flag is not specified, we now accept prefixes of the list of arguments. The semantics of _ w.r.t. to renaming has changed. Previously, it meant "restore the original name inferred from the type". Now it means "don't change the current name". The syntax of arguments is now restricted. Modifiers like /, ! and scopes are allowed only in the first arguments list. We also add *a lot* of missing checks on input values and fix various bugs. Note that this code is still way too complex for what it does, due to the complexity of the implicit arguments, reduction behaviors and renaming APIs. --- test-suite/.csdp.cache | Bin 89077 -> 89077 bytes 1 file changed, 0 insertions(+), 0 deletions(-) (limited to 'test-suite/.csdp.cache') diff --git a/test-suite/.csdp.cache b/test-suite/.csdp.cache index b8c07512f..b99d80e95 100644 Binary files a/test-suite/.csdp.cache and b/test-suite/.csdp.cache differ -- cgit v1.2.3