diff options
| author | Hugo Herbelin | 2016-04-10 18:30:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-06-16 17:30:17 +0200 |
| commit | 53e8a445177501846c75147680da03a95d5e9b5c (patch) | |
| tree | 217550bb8e12bd6028e3c68d0cda46fa0decdc0d | |
| parent | 8ee9906d70e0181a0e247b3ec0adbe889f3fdbce (diff) | |
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}.
| -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 |