diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | interp/constrintern.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/Arguments_renaming.out | 6 |
3 files changed, 11 insertions, 3 deletions
@@ -1,6 +1,12 @@ Changes beyond V8.5 =================== +Specification language + +- Giving implicit arguments explicitly to a constant with multiple + choices of implicit arguments does not break any more insertion of + further maximal implicit arguments. + Tactics - Flag "Bracketing Last Introduction Pattern" is now on by default. diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 50252a368f..0c02c5dab2 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1731,7 +1731,7 @@ let internalize globalenv env allow_patvar lvar c = in aux 1 l subscopes eargs rargs and apply_impargs c env imp subscopes l loc = - let imp = select_impargs_size (List.length l) imp in + let imp = select_impargs_size (List.length (List.filter (fun (_,x) -> x == None) l)) imp in let l = intern_impargs c env imp subscopes l in smart_gapp c loc l 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 |