diff options
-rw-r--r-- | CHANGES | 3 | ||||
-rw-r--r-- | plugins/funind/recdef.ml | 3 | ||||
-rw-r--r-- | pretyping/clenv.ml | 3 | ||||
-rw-r--r-- | pretyping/termops.ml | 11 | ||||
-rw-r--r-- | pretyping/termops.mli | 1 | ||||
-rwxr-xr-x | test-suite/check | 1 | ||||
-rw-r--r-- | test-suite/output/Naming.out | 36 | ||||
-rw-r--r-- | test-suite/output/Naming.v | 9 |
8 files changed, 23 insertions, 44 deletions
@@ -45,6 +45,9 @@ 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). Tactic Language diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5c910c424..e153bebf4 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -51,8 +51,7 @@ open Genarg let compute_renamed_type gls c = - let ids = collect_visible_vars c in - rename_bound_vars_as_displayed ids (pf_type_of gls c) + rename_bound_vars_as_displayed [] (pf_type_of gls c) let qed () = Lemmas.save_named true let defined () = Lemmas.save_named false diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml index aa58a0808..a65cc24ff 100644 --- a/pretyping/clenv.ml +++ b/pretyping/clenv.ml @@ -147,8 +147,7 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None let mk_clenv_rename_from_n gls n (c,t) = - let ids = collect_visible_vars t in - mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed ids t) + mk_clenv_from_n gls n (c,rename_bound_vars_as_displayed [] t) let mk_clenv_type_of gls t = mk_clenv_from gls (t,pf_type_of gls t) diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 07ac5df21..4de4bde2c 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -523,17 +523,6 @@ let collect_metas c = in List.rev (collrec [] c) -(* collects all visible var occurences (does not include indirect - dependencies of section variables via global references) *) - -let collect_visible_vars c = - let rec collrec acc c = - match kind_of_term c with - | Var id -> list_add_set id acc - | _ -> fold_constr collrec acc c - in - List.rev (collrec [] c) - (* Tests whether [m] is a subterm of [t]: [m] is appropriately lifted through abstractions of [t] *) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 44a96b613..59f7750d3 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -109,7 +109,6 @@ val free_rels : constr -> Intset.t val dependent : constr -> constr -> bool val dependent_no_evar : constr -> constr -> bool val collect_metas : constr -> int list -val collect_visible_vars : constr -> identifier list val occur_term : constr -> constr -> bool (* Synonymous of dependent *) (* Substitution of metavariables *) diff --git a/test-suite/check b/test-suite/check index c5636a820..06df1a12c 100755 --- a/test-suite/check +++ b/test-suite/check @@ -232,6 +232,7 @@ test_misc () { # Non-standard features # Test xml compilation + nbtests=`expr $nbtests + 1` printf " xml..." COQ_XML_LIBRARY_ROOT=misc/xml $bincoqc -xml misc/berardi_test > /dev/null 2>&1 if [ ! -d misc/xml ]; then diff --git a/test-suite/output/Naming.out b/test-suite/output/Naming.out index 211a16714..86055c3ba 100644 --- a/test-suite/output/Naming.out +++ b/test-suite/output/Naming.out @@ -1,20 +1,9 @@ -Welcome to Coq localhost:/home/herbelin/coq/git,namegen (cd25d05cf1d1aa17f9c4f90d999559c2e7570b56) -Parameter x2:nat. -x2 is assumed -Definition foo y := forall x x3 x4 S, x + S = x3 + x4 + y. -foo is defined -Section A. -Variable x3:nat. -x3 is assumed -Goal forall x x1 x2 x3:nat, - (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3. 1 subgoal x3 : nat ============================ forall x x1 x4 x0 : nat, - (forall x5 x6 : nat, x5 + x1 = x4 + x6) -> x + x1 = x4 + x0 -intros. + (forall x2 x5 : nat, x2 + x1 = x4 + x5) -> x + x1 = x4 + x0 1 subgoal x3 : nat @@ -25,30 +14,23 @@ intros. H : forall x x3 : nat, x + x1 = x4 + x3 ============================ x + x1 = x4 + x0 -Abort. -Current goal aborted -Goal forall x x1 x2 x3:nat, - (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) -> - x+x1 = x2+x3 -> foo (S x). 1 subgoal x3 : nat ============================ forall x x1 x4 x0 : nat, - (forall x5 x6 : nat, x5 + x1 = x4 + x6 -> foo (S x5 + x1)) -> + (forall x2 x5 : nat, x2 + x1 = x4 + x5 -> foo (S x2 + x1)) -> x + x1 = x4 + x0 -> foo (S x) -unfold foo. 1 subgoal x3 : nat ============================ forall x x1 x4 x0 : nat, - (forall x5 x6 : nat, - x5 + x1 = x4 + x6 -> - forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)) -> + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> x + x1 = x4 + x0 -> forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x -do 4 intro. 1 subgoal x3 : nat @@ -57,12 +39,11 @@ do 4 intro. x4 : nat x0 : nat ============================ - (forall x5 x6 : nat, - x5 + x1 = x4 + x6 -> - forall x7 x8 x9 S : nat, x7 + S = x8 + x9 + (Datatypes.S x5 + x1)) -> + (forall x2 x5 : nat, + x2 + x1 = x4 + x5 -> + forall x6 x7 x8 S0 : nat, x6 + S0 = x7 + x8 + (S x2 + x1)) -> x + x1 = x4 + x0 -> forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x -do 2 intro. 1 subgoal x3 : nat @@ -76,7 +57,6 @@ do 2 intro. H0 : x + x1 = x4 + x0 ============================ forall x5 x6 x7 S : nat, x5 + S = x6 + x7 + Datatypes.S x -do 4 intro. 1 subgoal x3 : nat diff --git a/test-suite/output/Naming.v b/test-suite/output/Naming.v index 71587e2ee..89e641ac9 100644 --- a/test-suite/output/Naming.v +++ b/test-suite/output/Naming.v @@ -7,7 +7,9 @@ Section A. Variable x3:nat. Goal forall x x1 x2 x3:nat, (forall x x3:nat, x+x1 = x2+x3) -> x+x1 = x2+x3. +Show. intros. +Show. (* Remark: in V8.2, this used to be printed @@ -37,10 +39,15 @@ Abort. Goal forall x x1 x2 x3:nat, (forall x x3:nat, x+x1 = x2+x3 -> foo (S x + x1)) -> x+x1 = x2+x3 -> foo (S x). +Show. unfold foo. +Show. do 4 intro. (* --> x, x1, x4, x0, ... *) +Show. do 2 intro. +Show. do 4 intro. +Show. (* Remark: in V8.2, this used to be printed @@ -71,3 +78,5 @@ before the intros and x5 + S = x6 + x7 + Datatypes.S x after (note the x5/x0 and the S0/S) *) + +Abort. |