From 53e8a445177501846c75147680da03a95d5e9b5c Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 10 Apr 2016 18:30:38 +0200
Subject: Not taking arguments given by name or position into account when
 computing the arguments which allows to decide which list of implicit
 arguments to consider when several such lists are available.

For instance, "eq_refl (A:=nat)" is  now interpreted as "@eq_refl nat _",
the same way as if we had said:

Arguments eq_refl {A} {x}.
---
 test-suite/output/Arguments_renaming.out | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'test-suite')

diff --git a/test-suite/output/Arguments_renaming.out b/test-suite/output/Arguments_renaming.out
index 1e3cc37df4..3488cb3056 100644
--- a/test-suite/output/Arguments_renaming.out
+++ b/test-suite/output/Arguments_renaming.out
@@ -6,8 +6,10 @@ Error: To rename arguments the "rename" flag must be specified.
 Argument A renamed to T.
 @eq_refl
      : forall (B : Type) (y : B), y = y
-@eq_refl nat
-     : forall x : nat, x = x
+eq_refl
+     : ?y = ?y
+where
+?y : [ |- nat] 
 Inductive eq (A : Type) (x : A) : A -> Prop :=  eq_refl : x = x
 
 For eq_refl: Arguments are renamed to B, y
-- 
cgit v1.2.3