diff options
| -rw-r--r-- | CHANGES | 5 | ||||
| -rw-r--r-- | pretyping/namegen.ml | 2 | ||||
| -rw-r--r-- | test-suite/output/Naming.out | 21 | ||||
| -rw-r--r-- | test-suite/output/Naming.v | 9 |
4 files changed, 26 insertions, 11 deletions
@@ -45,9 +45,8 @@ Tactics - Binders given before ":" in lemmas are now automatically introduced in the context (possible source of incompatibility that can be avoided by unsetting option "Automatic Introduction"). -- Made choice of introduction names compliant with printed names and - in particular with "intros until" names (possible source of exceptional - incompatibilities). +- Made quantified hypotheses get the name they would have if introduced in + the context (possible but rare source of incompatibilities). Tactic Language diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index c4349624fe..7d141faf1e 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -225,7 +225,7 @@ let make_all_name_different env = let visibly_occur_id id c = let rec occur c = match kind_of_term c with - | Const _ | Ind _ | Construct _ + | Const _ | Ind _ | Construct _ | Var _ when shortest_qualid_of_global Idset.empty (global_of_constr c) = qualid_of_ident id -> raise Occur | _ -> iter_constr occur c diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index 86055c3baf..105940a45d 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -1,11 +1,11 @@ 1 subgoal - + x3 : nat ============================ forall x x1 x4 x0 : nat, (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 1 subgoal - + x3 : nat x : nat x1 : nat @@ -15,14 +15,14 @@ ============================ x + x1 = x4 + x0 1 subgoal - + x3 : nat ============================ forall x x1 x4 x0 : nat, (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> x + x1 = x4 + x0 -> foo (S x) 1 subgoal - + x3 : nat ============================ forall x x1 x4 x0 : nat, @@ -32,7 +32,7 @@ x + x1 = x4 + x0 -> forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - + x3 : nat x : nat x1 : nat @@ -45,7 +45,7 @@ x + x1 = x4 + x0 -> forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - + x3 : nat x : nat x1 : nat @@ -58,7 +58,7 @@ ============================ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x 1 subgoal - + x3 : nat x : nat x1 : nat @@ -74,3 +74,10 @@ S : nat ============================ x5 + S = x6 + x7 + Datatypes.S x +1 subgoal + + x3 : nat + a : nat + H : a = 0 -> forall a : nat, a = 0 + ============================ + a = 0 diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 89e641ac99..327643dc57 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -80,3 +80,12 @@ before the intros and after (note the x5/x0 and the S0/S) *) Abort. + +(* Check naming in hypotheses *) + +Goal forall a, (a = 0 -> forall a, a = 0) -> a = 0. +intros. +Show. +apply H with (a:=a). (* test compliance with printing *) +Abort. + |