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.

1 files changed, 4 insertions, 4 deletions

diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index ca1d0b7fb..e18aece09 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -16,12 +16,12 @@ open Libobject
 (*i*)
 
 let name_table =
-  Summary.ref (Refmap.empty : Name.t list list Refmap.t)
+  Summary.ref (Refmap.empty : Name.t list Refmap.t)
     ~name:"rename-arguments"
 
 type req =
   | ReqLocal
-  | ReqGlobal of global_reference * Name.t list list
+  | ReqGlobal of global_reference * Name.t list
 
 let load_rename_args _ (_, (_, (r, names))) =
   name_table := Refmap.add r names !name_table
@@ -49,7 +49,7 @@ let discharge_rename_args = function
        let vars,_,_ = section_segment_of_reference c in
        let c' = pop_global_reference c in
        let var_names = List.map (fun (id, _,_,_) -> Name id) vars in
-       let names' = List.map (fun l -> var_names @ l) names in
+       let names' = var_names @ names in
        Some (ReqGlobal (c', names), (c', names'))
      with Not_found -> Some req)
   | _ -> None
@@ -83,7 +83,7 @@ let rec rename_prod c = function
       | _ -> c
         
 let rename_type ty ref =
-  try rename_prod ty (List.hd (arguments_names ref))
+  try rename_prod ty (arguments_names ref)
   with Not_found -> ty
 
 let rename_type_of_constant env c =