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.
---
 library/impargs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index bce7a15cbe..a709aedeee 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -494,7 +494,7 @@ let implicits_of_global ref =
       let rename imp name = match imp, name with
        | Some (_, x,y), Name id -> Some (id, x,y)
        | _ -> imp in
-      List.map2 (fun (t, il) rl -> t, List.map2 rename il rl) l rename_l
+      List.map (fun (t, il) -> t, List.map2 rename il rename_l) l
     with Not_found -> l
     | Invalid_argument _ ->
         anomaly (Pp.str "renamings list and implicits list have different lenghts")
-- 
cgit v1.2.3


From 6ecb796d462896a19212bcc5b8c0036833c6c85f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Mon, 24 Oct 2016 17:53:42 +0200
Subject: Proper fix for #3753 (anomaly with implicit arguments and renamings)

Instead of circumventing the problem on the caller's side, as was done
in Arguments, we simply avoid failing as there was no real reason for
this anomaly to be triggered. If the list of renamings is shorter than
the one of implicits, we simply interpret the remaining arguments as not
renamed.
---
 library/impargs.ml | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index a709aedeee..13816edb19 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -491,13 +491,15 @@ let implicits_of_global ref =
     let l = Refmap.find ref !implicits_table in
     try
       let rename_l = Arguments_renaming.arguments_names ref in
-      let rename imp name = match imp, name with
-       | Some (_, x,y), Name id -> Some (id, x,y)
-       | _ -> imp in
-      List.map (fun (t, il) -> t, List.map2 rename il rename_l) l
+      let rec rename implicits names = match implicits, names with
+        | [], _ -> []
+        | _, [] -> implicits
+        | Some (_, x,y) :: implicits, Name id :: names ->
+           Some (id, x,y) :: rename implicits names
+        | imp :: implicits, _ :: names -> imp :: rename implicits names
+      in
+      List.map (fun (t, il) -> t, rename il rename_l) l
     with Not_found -> l
-    | Invalid_argument _ ->
-        anomaly (Pp.str "renamings list and implicits list have different lenghts")
   with Not_found -> [DefaultImpArgs,[]]
 
 let cache_implicits_decl (ref,imps) =
-- 
cgit v1.2.3


From ebb5bd7c2048daa7241bb07d8b53d07e0be27e62 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Tue, 25 Oct 2016 13:47:45 +0200
Subject: Add missing dot to impargs error message.

---
 library/impargs.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 13816edb19..828d652c83 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -659,7 +659,7 @@ let check_inclusion l =
   let rec aux = function
     | n1::(n2::_ as nl) ->
 	if n1 <= n2 then
-	  error "Sequences of implicit arguments must be of different lengths";
+	  error "Sequences of implicit arguments must be of different lengths.";
 	aux nl
     | _ -> () in
   aux (List.map (fun (imps,_) -> List.length imps) l)
-- 
cgit v1.2.3