aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/base_include3
-rw-r--r--dev/bugzilla2github_stripped.csv501
-rw-r--r--dev/ci/ci-basic-overlay.sh8
-rw-r--r--dev/doc/changes.md12
-rw-r--r--dev/doc/versions-history.tex18
-rw-r--r--engine/namegen.ml13
-rw-r--r--engine/namegen.mli7
-rw-r--r--ide/tags.ml25
-rw-r--r--ide/tags.mli1
-rw-r--r--interp/constrextern.ml48
-rw-r--r--plugins/ltac/tacintern.ml23
-rw-r--r--pretyping/evarsolve.ml12
-rw-r--r--pretyping/patternops.ml25
-rw-r--r--pretyping/patternops.mli2
-rw-r--r--test-suite/bugs/closed/2881.v7
-rw-r--r--test-suite/bugs/closed/5401.v21
-rw-r--r--toplevel/coqloop.ml2
-rw-r--r--toplevel/coqloop.mli2
-rw-r--r--toplevel/coqtop.ml10
-rw-r--r--toplevel/coqtop.mli3
20 files changed, 684 insertions, 59 deletions
diff --git a/dev/base_include b/dev/base_include
index 79ecd73e0d..f2912e1127 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -233,8 +233,7 @@ let _ = Flags.in_toplevel := true
let _ = Constrextern.set_extern_reference
(fun ?loc _ r -> Libnames.Qualid (loc,Nametab.shortest_qualid_of_global Idset.empty r));;
-open Coqloop
-let go = loop
+let go () = Coqloop.loop Option.(get !Coqtop.drop_last_doc)
let _ =
print_string
diff --git a/dev/bugzilla2github_stripped.csv b/dev/bugzilla2github_stripped.csv
new file mode 100644
index 0000000000..3f5cbfd71d
--- /dev/null
+++ b/dev/bugzilla2github_stripped.csv
@@ -0,0 +1,501 @@
+2, 1156
+3, 1157
+4, 1158
+7, 1160
+8, 1161
+10, 1163
+12, 1164
+13, 1165
+14, 1169
+16, 1171
+17, 1184
+18, 1190
+19, 1191
+20, 1193
+21, 1200
+23, 1201
+24, 1203
+25, 1208
+26, 1210
+27, 1212
+28, 1216
+30, 1217
+31, 1223
+34, 1227
+35, 1232
+36, 1235
+38, 1238
+39, 1244
+40, 1245
+41, 1246
+42, 1247
+44, 1248
+45, 1249
+46, 1250
+47, 1252
+48, 1253
+49, 1254
+50, 1256
+52, 1262
+54, 1263
+55, 1264
+56, 1265
+59, 1266
+60, 1267
+61, 1268
+63, 1270
+64, 1272
+65, 1274
+66, 1275
+69, 1276
+70, 1279
+71, 1283
+72, 1284
+73, 1285
+74, 1286
+75, 1287
+78, 1288
+79, 1291
+80, 1292
+82, 1293
+83, 1295
+84, 1296
+85, 1297
+86, 1299
+88, 1301
+89, 1303
+90, 1304
+91, 1305
+92, 1307
+93, 1308
+94, 1310
+95, 1312
+96, 1313
+97, 1314
+98, 1316
+99, 1318
+100, 1319
+101, 1320
+102, 1321
+103, 1323
+105, 1324
+106, 1327
+107, 1328
+108, 1330
+109, 1334
+112, 1335
+115, 1336
+119, 1337
+121, 1341
+123, 1342
+124, 1343
+125, 1344
+126, 1345
+127, 1346
+128, 1348
+129, 1349
+134, 1350
+135, 1351
+136, 1352
+137, 1353
+138, 1354
+139, 1355
+140, 1356
+142, 1357
+143, 1358
+144, 1359
+145, 1360
+147, 1361
+148, 1362
+149, 1363
+150, 1365
+152, 1366
+154, 1368
+155, 1369
+160, 1370
+161, 1371
+162, 1372
+164, 1373
+165, 1374
+166, 1376
+167, 1377
+169, 1378
+170, 1380
+178, 1382
+179, 1383
+180, 1384
+181, 1385
+182, 1386
+183, 1387
+184, 1390
+185, 1391
+186, 1392
+187, 1393
+189, 1394
+190, 1398
+191, 1401
+192, 1402
+194, 1403
+195, 1404
+196, 1405
+197, 1407
+198, 1409
+199, 1410
+202, 1412
+204, 1413
+205, 1421
+207, 1422
+209, 1423
+210, 1426
+212, 1427
+213, 1428
+214, 1429
+215, 1433
+216, 1435
+219, 1436
+220, 1437
+221, 1440
+222, 1444
+224, 1445
+225, 1450
+228, 1452
+229, 1453
+235, 1457
+236, 1458
+238, 1459
+239, 1460
+240, 1462
+242, 1465
+243, 1466
+244, 1470
+245, 1471
+248, 1472
+250, 1473
+253, 1474
+254, 1475
+259, 1476
+261, 1478
+262, 1479
+263, 1480
+264, 1481
+265, 1484
+266, 1485
+267, 1486
+268, 1488
+269, 1489
+270, 1490
+271, 1492
+272, 1493
+273, 1494
+274, 1498
+275, 1500
+277, 1503
+278, 1504
+279, 1505
+282, 1506
+283, 1511
+289, 1513
+290, 1514
+291, 1516
+292, 1517
+294, 1520
+295, 1521
+299, 1523
+301, 1524
+302, 1525
+303, 1527
+305, 1529
+311, 1530
+315, 1531
+316, 1532
+317, 1534
+320, 1535
+322, 1539
+324, 1541
+328, 1542
+329, 1543
+330, 1544
+331, 1545
+333, 1546
+335, 1547
+336, 1548
+338, 1549
+343, 1550
+348, 1551
+350, 1552
+351, 1553
+352, 1554
+353, 1555
+356, 1556
+363, 1557
+368, 1558
+371, 1559
+372, 1560
+413, 1561
+418, 1562
+420, 1563
+426, 1564
+431, 1565
+444, 1566
+447, 1567
+452, 1569
+459, 1570
+462, 1571
+463, 1573
+468, 1574
+472, 1575
+473, 1577
+509, 1578
+519, 1579
+529, 1580
+540, 1581
+541, 1583
+545, 1584
+546, 1585
+547, 1589
+550, 1590
+552, 1591
+553, 1592
+554, 1593
+574, 1594
+592, 1595
+602, 1597
+603, 1598
+606, 1599
+607, 1600
+667, 1601
+668, 1602
+686, 1603
+690, 1605
+699, 1606
+705, 1607
+708, 1609
+711, 1610
+728, 1611
+739, 1612
+742, 1613
+743, 1615
+774, 1617
+775, 1619
+776, 1623
+777, 1624
+778, 1625
+779, 1627
+780, 1628
+781, 1629
+782, 1630
+783, 1631
+784, 1632
+785, 1633
+786, 1636
+787, 1637
+788, 1638
+789, 1639
+790, 1640
+793, 1641
+794, 1642
+795, 1644
+797, 1645
+798, 1646
+803, 1647
+804, 1649
+805, 1650
+808, 1652
+813, 1653
+815, 1655
+816, 1656
+818, 1657
+820, 1658
+821, 1659
+822, 1660
+823, 1661
+826, 1662
+828, 1663
+829, 1664
+830, 1665
+831, 1666
+832, 1667
+834, 1668
+835, 1669
+836, 1670
+837, 5689
+839, 5791
+840, 5792
+841, 5793
+842, 5794
+843, 5795
+844, 5796
+846, 5797
+849, 5798
+850, 5799
+854, 5800
+855, 5801
+856, 5802
+857, 5803
+860, 5804
+861, 5805
+862, 5806
+863, 5807
+864, 5808
+865, 5809
+867, 5810
+868, 5811
+869, 5812
+870, 5813
+871, 5814
+872, 5815
+874, 5816
+875, 5817
+878, 5818
+879, 5819
+881, 5820
+883, 5821
+884, 5822
+885, 5823
+886, 5824
+888, 5825
+889, 5826
+890, 5827
+891, 5828
+892, 5829
+893, 5830
+894, 5831
+896, 5832
+898, 5833
+901, 5834
+903, 5835
+905, 5836
+906, 5837
+909, 5838
+914, 5839
+915, 5840
+922, 5841
+923, 5842
+925, 5843
+927, 5844
+931, 5845
+932, 5846
+934, 5847
+935, 5848
+936, 5849
+937, 5850
+938, 5851
+939, 5852
+940, 5853
+941, 5854
+945, 5855
+946, 5856
+947, 5857
+949, 5858
+950, 5859
+951, 5860
+952, 5861
+953, 5862
+954, 5863
+957, 5864
+960, 5865
+963, 5866
+965, 5867
+967, 5868
+968, 5869
+969, 5870
+972, 5871
+973, 5872
+974, 5873
+975, 5874
+976, 5875
+977, 5876
+979, 5877
+983, 5878
+984, 5879
+985, 5880
+986, 5881
+987, 5882
+988, 5883
+990, 5884
+991, 5885
+993, 5886
+996, 5887
+997, 5888
+1000, 5889
+1001, 5890
+1002, 5891
+1003, 5892
+1004, 5893
+1005, 5894
+1006, 5895
+1007, 5896
+1010, 5897
+1012, 5898
+1013, 5899
+1014, 5900
+1015, 5901
+1016, 5902
+1017, 5903
+1018, 5904
+1025, 5905
+1028, 5906
+1029, 5907
+1030, 5908
+1031, 5909
+1033, 5910
+1035, 5911
+1036, 5912
+1037, 5913
+1039, 5914
+1041, 5915
+1042, 5916
+1044, 5917
+1045, 5918
+1052, 5919
+1053, 5920
+1054, 5921
+1055, 5922
+1056, 5923
+1060, 5924
+1064, 5925
+1067, 5926
+1070, 5927
+1072, 5928
+1075, 5929
+1076, 5930
+1085, 5931
+1086, 5932
+1087, 5933
+1089, 5934
+1091, 5935
+1096, 5936
+1097, 5937
+1098, 5938
+1099, 5939
+1100, 5940
+1101, 5941
+1102, 5942
+1104, 5943
+1107, 5944
+1108, 5945
+1111, 5946
+1113, 5947
+1114, 5948
+1115, 5949
+1116, 5950
+1118, 5951
+1119, 5952
+1120, 5953
+1122, 5954
+1123, 5955
+1124, 5956
+1128, 5957
+1129, 5958
+1132, 5959
+1136, 5960
+1137, 5961
+1138, 5962
+1140, 5963
+1141, 5964
+1142, 5965
+1144, 5966
+1145, 5967
+1149, 5968
+1151, 5969
+1153, 5970
diff --git a/dev/ci/ci-basic-overlay.sh b/dev/ci/ci-basic-overlay.sh
index 9be882bb3c..5c37b3133e 100644
--- a/dev/ci/ci-basic-overlay.sh
+++ b/dev/ci/ci-basic-overlay.sh
@@ -28,11 +28,11 @@
########################################################################
# Mathclasses + Corn
########################################################################
-: ${math_classes_CI_BRANCH:=external-bignums}
-: ${math_classes_CI_GITURL:=https://github.com/letouzey/math-classes.git}
+: ${math_classes_CI_BRANCH:=master}
+: ${math_classes_CI_GITURL:=https://github.com/math-classes/math-classes.git}
-: ${Corn_CI_BRANCH:=external-bignums}
-: ${Corn_CI_GITURL:=https://github.com/letouzey/corn.git}
+: ${Corn_CI_BRANCH:=master}
+: ${Corn_CI_GITURL:=https://github.com/c-corn/corn.git}
########################################################################
# Iris
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index b1ebec44ef..5be8257e87 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -1,5 +1,17 @@
## Changes between Coq 8.7 and Coq 8.8
+### Bug tracker
+
+As of 18/10/2017, Coq uses [GitHub issues](https://github.com/coq/coq/issues)
+as bug tracker.
+Old bug reports were migrated from Bugzilla to GitHub issues using
+[this migration script](https://gist.github.com/Zimmi48/d923e52f64fe17c72852d9c148bfcdc6#file-bugzilla2github)
+as detailed in [this blog post](https://www.theozimmermann.net/2017/10/bugzilla-to-github/).
+
+All the bugs with a number below 1154 had to be renumbered, you can find
+a correspondence table [here](/dev/bugzilla2github_stripped.csv).
+All the other bugs kept their number.
+
### Plugin API
Coq 8.8 offers a new module overlay containing a proposed plugin API
diff --git a/dev/doc/versions-history.tex b/dev/doc/versions-history.tex
index 492e75a7bb..3867d4af90 100644
--- a/dev/doc/versions-history.tex
+++ b/dev/doc/versions-history.tex
@@ -376,9 +376,27 @@ Coq V8.5 beta1 & released 21 January 2015 & \feature{computation via compilation
&& \feature{new proof engine deployed} [2-11-2013]\\
&& \feature{universe polymorphism} [6-5-2014]\\
&& \feature{primitive projections} [6-5-2014]\\
+&& \feature{miscellaneous optimizations}\\
Coq V8.5 beta2 & released 22 April 2015 & \feature{MMaps library} [4-3-2015]\\
+Coq V8.5 & released 22 January 2016 & \\
+
+Coq V8.6 beta 1 & released 19 November 2016 & \feature{irrefutable patterns} [15-2-2016]\\
+&& \feature{Ltac profiling} [14-6-2016]\\
+&& \feature{warning system} [29-6-2016]\\
+&& \feature{miscellaneous optimizations}\\
+
+Coq V8.6 & released 14 December 2016 & \\
+
+Coq V8.7 beta 1 & released 6 September 2017 & \feature{bundled with Ssreflect plugin} [6-6-2017]\\
+&& \feature{cumulative polymorphic inductive types} [19-6-2017]\\
+&& \feature{further optimizations}\\
+
+Coq V8.7 beta 2 & released 6 October 2017 & \\
+
+Coq V8.7 & released 18 October 2016 & \\
+
\end{tabular}
\medskip
diff --git a/engine/namegen.ml b/engine/namegen.ml
index 2e62b89011..a38c73ed0b 100644
--- a/engine/namegen.ml
+++ b/engine/namegen.ml
@@ -376,15 +376,22 @@ let next_name_for_display sigma flags =
| RenamingElsewhereFor env_t -> next_name_away_for_default_printing sigma env_t
(* Remark: Anonymous var may be dependent in Evar's contexts *)
-let compute_displayed_name_in sigma flags avoid na c =
+let compute_displayed_name_in_gen_poly noccurn_fun sigma flags avoid na c =
match na with
- | Anonymous when noccurn sigma 1 c ->
+ | Anonymous when noccurn_fun sigma 1 c ->
(Anonymous,avoid)
| _ ->
let fresh_id = next_name_for_display sigma flags na avoid in
- let idopt = if noccurn sigma 1 c then Anonymous else Name fresh_id in
+ let idopt = if noccurn_fun sigma 1 c then Anonymous else Name fresh_id in
(idopt, Id.Set.add fresh_id avoid)
+let compute_displayed_name_in = compute_displayed_name_in_gen_poly noccurn
+
+let compute_displayed_name_in_gen f sigma =
+ (* only flag which does not need a constr, maybe to be refined *)
+ let flag = RenamingForGoal in
+ compute_displayed_name_in_gen_poly f sigma flag
+
let compute_and_force_displayed_name_in sigma flags avoid na c =
match na with
| Anonymous when noccurn sigma 1 c ->
diff --git a/engine/namegen.mli b/engine/namegen.mli
index 6fde90a39c..d29b69259f 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -106,10 +106,15 @@ val compute_displayed_name_in :
val compute_and_force_displayed_name_in :
evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
val compute_displayed_let_name_in :
- evar_map -> renaming_flags -> Id.Set.t -> Name.t -> constr -> Name.t * Id.Set.t
+ evar_map -> renaming_flags -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
val rename_bound_vars_as_displayed :
evar_map -> Id.Set.t -> Name.t list -> types -> types
+(* Generic function expecting a "not occurn" function *)
+val compute_displayed_name_in_gen :
+ (evar_map -> int -> 'a -> bool) ->
+ evar_map -> Id.Set.t -> Name.t -> 'a -> Name.t * Id.Set.t
+
(**********************************************************************)
(* Naming strategy for arguments in Prop when eliminating inductive types *)
diff --git a/ide/tags.ml b/ide/tags.ml
index 08ca47a842..4020271798 100644
--- a/ide/tags.ml
+++ b/ide/tags.ml
@@ -15,33 +15,22 @@ let make_tag (tt:GText.tag_table) ~name prop =
module Script =
struct
+ (* More recently defined tags have highest priority in case of overlapping *)
let table = GText.tag_table ()
- let comment = make_tag table ~name:"comment" []
- let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE]
let warning = make_tag table ~name:"warning" [`UNDERLINE `SINGLE; `FOREGROUND "blue"]
+ let error = make_tag table ~name:"error" [`UNDERLINE `SINGLE]
let error_bg = make_tag table ~name:"error_bg" []
let to_process = make_tag table ~name:"to_process" []
let processed = make_tag table ~name:"processed" []
- let incomplete = make_tag table ~name:"incomplete" [
- `BACKGROUND_STIPPLE_SET true;
- ]
+ let incomplete = make_tag table ~name:"incomplete" [`BACKGROUND_STIPPLE_SET true]
let unjustified = make_tag table ~name:"unjustified" [`BACKGROUND "gold"]
- let found = make_tag table ~name:"found" [`BACKGROUND "blue"; `FOREGROUND "white"]
- let sentence = make_tag table ~name:"sentence" []
let tooltip = make_tag table ~name:"tooltip" [] (* debug:`BACKGROUND "blue" *)
-
let ephemere =
[error; warning; error_bg; tooltip; processed; to_process; incomplete; unjustified]
-
- let all =
- comment :: found :: sentence :: ephemere
-
- let edit_zone =
- let t = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] in
- t#set_priority (List.length all);
- t
- let all = edit_zone :: all
-
+ let comment = make_tag table ~name:"comment" []
+ let sentence = make_tag table ~name:"sentence" []
+ let edit_zone = make_tag table ~name:"edit_zone" [`UNDERLINE `SINGLE] (* for debugging *)
+ let all = edit_zone :: comment :: sentence :: ephemere
end
module Proof =
struct
diff --git a/ide/tags.mli b/ide/tags.mli
index 265dfe46e3..15a35185df 100644
--- a/ide/tags.mli
+++ b/ide/tags.mli
@@ -17,7 +17,6 @@ sig
val processed : GText.tag
val incomplete : GText.tag
val unjustified : GText.tag
- val found : GText.tag
val sentence : GText.tag
val tooltip : GText.tag
val edit_zone : GText.tag (* for debugging *)
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index f1bee65ef8..bb4227b4a7 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -1120,7 +1120,11 @@ let any_any_branch =
(* | _ => _ *)
Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
-let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
+let compute_displayed_name_in_pattern sigma avoid na c =
+ let open Namegen in
+ compute_displayed_name_in_gen (fun _ -> Patternops.noccurn_pattern) sigma avoid na c
+
+let rec glob_of_pat avoid env sigma pat = DAst.make @@ match pat with
| PRef ref -> GRef (ref,None)
| PVar id -> GVar id
| PEvar (evk,l) ->
@@ -1130,7 +1134,7 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
| None -> Id.of_string "__"
| Some id -> id
in
- GEvar (id,List.map (on_snd (glob_of_pat env sigma)) l)
+ GEvar (id,List.map (on_snd (glob_of_pat avoid env sigma)) l)
| PRel n ->
let id = try match lookup_name_of_rel n env with
| Name id -> id
@@ -1141,30 +1145,36 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
| PMeta None -> GHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous,None)
| PMeta (Some n) -> GPatVar (Evar_kinds.FirstOrderPatVar n)
| PProj (p,c) -> GApp (DAst.make @@ GRef (ConstRef (Projection.constant p),None),
- [glob_of_pat env sigma c])
+ [glob_of_pat avoid env sigma c])
| PApp (f,args) ->
- GApp (glob_of_pat env sigma f,Array.map_to_list (glob_of_pat env sigma) args)
+ GApp (glob_of_pat avoid env sigma f,Array.map_to_list (glob_of_pat avoid env sigma) args)
| PSoApp (n,args) ->
GApp (DAst.make @@ GPatVar (Evar_kinds.SecondOrderPatVar n),
- List.map (glob_of_pat env sigma) args)
+ List.map (glob_of_pat avoid env sigma) args)
| PProd (na,t,c) ->
- GProd (na,Explicit,glob_of_pat env sigma t,glob_of_pat (na::env) sigma c)
+ let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in
+ let env' = Termops.add_name na' env in
+ GProd (na',Explicit,glob_of_pat avoid env sigma t,glob_of_pat avoid' env' sigma c)
| PLetIn (na,b,t,c) ->
- GLetIn (na,glob_of_pat env sigma b, Option.map (glob_of_pat env sigma) t,
- glob_of_pat (na::env) sigma c)
+ let na',avoid' = Namegen.compute_displayed_let_name_in sigma Namegen.RenamingForGoal avoid na c in
+ let env' = Termops.add_name na' env in
+ GLetIn (na',glob_of_pat avoid env sigma b, Option.map (glob_of_pat avoid env sigma) t,
+ glob_of_pat avoid' env' sigma c)
| PLambda (na,t,c) ->
- GLambda (na,Explicit,glob_of_pat env sigma t, glob_of_pat (na::env) sigma c)
+ let na',avoid' = compute_displayed_name_in_pattern sigma avoid na c in
+ let env' = Termops.add_name na' env in
+ GLambda (na',Explicit,glob_of_pat avoid env sigma t, glob_of_pat avoid' env' sigma c)
| PIf (c,b1,b2) ->
- GIf (glob_of_pat env sigma c, (Anonymous,None),
- glob_of_pat env sigma b1, glob_of_pat env sigma b2)
+ GIf (glob_of_pat avoid env sigma c, (Anonymous,None),
+ glob_of_pat avoid env sigma b1, glob_of_pat avoid env sigma b2)
| PCase ({cip_style=LetStyle; cip_ind_tags=None},PMeta None,tm,[(0,n,b)]) ->
- let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat env sigma b) in
- GLetTuple (nal,(Anonymous,None),glob_of_pat env sigma tm,b)
+ let nal,b = it_destRLambda_or_LetIn_names n (glob_of_pat avoid env sigma b) in
+ GLetTuple (nal,(Anonymous,None),glob_of_pat avoid env sigma tm,b)
| PCase (info,p,tm,bl) ->
let mat = match bl, info.cip_ind with
| [], _ -> []
| _, Some ind ->
- let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat env sigma c)) bl in
+ let bl' = List.map (fun (i,n,c) -> (i,n,glob_of_pat avoid env sigma c)) bl in
simple_cases_matrix_of_branches ind bl'
| _, None -> anomaly (Pp.str "PCase with some branches but unknown inductive.")
in
@@ -1173,16 +1183,16 @@ let rec glob_of_pat env sigma pat = DAst.make @@ match pat with
let indnames,rtn = match p, info.cip_ind, info.cip_ind_tags with
| PMeta None, _, _ -> (Anonymous,None),None
| _, Some ind, Some nargs ->
- return_type_of_predicate ind nargs (glob_of_pat env sigma p)
+ return_type_of_predicate ind nargs (glob_of_pat avoid env sigma p)
| _ -> anomaly (Pp.str "PCase with non-trivial predicate but unknown inductive.")
in
- GCases (RegularStyle,rtn,[glob_of_pat env sigma tm,indnames],mat)
- | PFix f -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
- | PCoFix c -> DAst.get (Detyping.detype_names false Id.Set.empty env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
+ GCases (RegularStyle,rtn,[glob_of_pat avoid env sigma tm,indnames],mat)
+ | PFix f -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkFix f))) (** FIXME bad env *)
+ | PCoFix c -> DAst.get (Detyping.detype_names false avoid env (Global.env()) sigma (EConstr.of_constr (mkCoFix c)))
| PSort s -> GSort s
let extern_constr_pattern env sigma pat =
- extern true (None,[]) Id.Set.empty (glob_of_pat env sigma pat)
+ extern true (None,[]) Id.Set.empty (glob_of_pat Idset.empty env sigma pat)
let extern_rel_context where env sigma sign =
let a = detype_rel_context Detyping.Later where Id.Set.empty (names_of_rel_context env,env) sigma sign in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 99d7684d36..f171fd07d7 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -322,13 +322,23 @@ let intern_constr_pattern ist ~as_type ~ltacvars pc =
let dummy_pat = PRel 0
-let intern_typed_pattern ist p =
+let intern_typed_pattern ist ~as_type ~ltacvars p =
(* we cannot ensure in non strict mode that the pattern is closed *)
(* keeping a constr_expr copy is too complicated and we want anyway to *)
(* type it, so we remember the pattern as a glob_constr only *)
+ let metas,pat =
+ if !strict_check then
+ let ltacvars = {
+ Constrintern.ltac_vars = ltacvars;
+ ltac_bound = Id.Set.empty;
+ ltac_extra = ist.extra;
+ } in
+ Constrintern.intern_constr_pattern ist.genv ~as_type ~ltacvars p
+ else
+ [], dummy_pat in
let (glob,_ as c) = intern_constr_gen true false ist p in
let bound_names = Glob_ops.bound_glob_vars glob in
- (bound_names,c,dummy_pat)
+ metas,(bound_names,c,pat)
let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
let interp_ref r =
@@ -364,7 +374,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
(* We interpret similarly @ref and ref *)
interp_ref (AN r)
| Inr c ->
- Inr (intern_typed_pattern ist c))
+ Inr (snd (intern_typed_pattern ist ~as_type:false ~ltacvars:ist.ltacvars c)))
(* This seems fairly hacky, but it's the first way I've found to get proper
globalization of [unfold]. --adamc *)
@@ -529,7 +539,12 @@ let rec intern_atomic lf ist x =
then intern_type ist c else intern_constr ist c),
clause_app (intern_hyp_location ist) cl)
| TacChange (Some p,c,cl) ->
- TacChange (Some (intern_typed_pattern ist p),intern_constr ist c,
+ let { ltacvars } = ist in
+ let metas,pat = intern_typed_pattern ist ~as_type:false ~ltacvars p in
+ let fold accu x = Id.Set.add x accu in
+ let ltacvars = List.fold_left fold ltacvars metas in
+ let ist' = { ist with ltacvars } in
+ TacChange (Some pat,intern_constr ist' c,
clause_app (intern_hyp_location ist) cl)
(* Equality and inversion *)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ad1409f5b1..7f81d1aa34 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -842,6 +842,15 @@ let rec find_solution_type evarenv = function
| (id,ProjectEvar _)::l -> find_solution_type evarenv l
| [] -> assert false
+let find_most_recent_projection evi sols =
+ let sign = List.map get_id (evar_filtered_context evi) in
+ match sols with
+ | y::l ->
+ List.fold_right (fun (id,p as x) (id',_ as y) ->
+ if List.index Id.equal id sign < List.index Id.equal id' sign then x else y)
+ l y
+ | _ -> assert false
+
(* In case the solution to a projection problem requires the instantiation of
* subsidiary evars, [do_projection_effects] performs them; it
* also try to instantiate the type of those subsidiary evars if their
@@ -1429,7 +1438,8 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
let c, p = match sols with
| [] -> raise Not_found
| [id,p] -> (mkVar id, p)
- | (id,p)::_::_ ->
+ | _ ->
+ let (id,p) = find_most_recent_projection evi sols in
if choose then (mkVar id, p) else raise (NotUniqueInType sols)
in
let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3b3ad021e4..aaa9467068 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -96,6 +96,31 @@ let rec occur_meta_pattern = function
| PMeta _ | PSoApp _ -> true
| PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
+let rec occurn_pattern n = function
+ | PRel p -> Int.equal n p
+ | PApp (f,args) ->
+ (occurn_pattern n f) || (Array.exists (occurn_pattern n) args)
+ | PProj (_,arg) -> occurn_pattern n arg
+ | PLambda (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+ | PProd (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+ | PLetIn (na,b,t,c) ->
+ Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t ||
+ (occurn_pattern (n+1) c)
+ | PIf (c,c1,c2) ->
+ (occurn_pattern n c) ||
+ (occurn_pattern n c1) || (occurn_pattern n c2)
+ | PCase(_,p,c,br) ->
+ (occurn_pattern n p) ||
+ (occurn_pattern n c) ||
+ (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
+ | PMeta _ | PSoApp _ -> true
+ | PEvar (_,args) -> Array.exists (occurn_pattern n) args
+ | PVar _ | PRef _ | PSort _ -> false
+ | PFix fix -> not (noccurn n (mkFix fix))
+ | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+
+let noccurn_pattern n c = not (occurn_pattern n c)
+
exception BoundPattern;;
let rec head_pattern_bound t =
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index ffe0186af0..2d1ce1dbc9 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -22,6 +22,8 @@ val occur_meta_pattern : constr_pattern -> bool
val subst_pattern : substitution -> constr_pattern -> constr_pattern
+val noccurn_pattern : int -> constr_pattern -> bool
+
exception BoundPattern
(** [head_pattern_bound t] extracts the head variable/constant of the
diff --git a/test-suite/bugs/closed/2881.v b/test-suite/bugs/closed/2881.v
new file mode 100644
index 0000000000..b4f09305b4
--- /dev/null
+++ b/test-suite/bugs/closed/2881.v
@@ -0,0 +1,7 @@
+(* About scoping of pattern variables in strict/non-strict mode *)
+
+Ltac eta_red := change (fun a => ?f0 a) with f0.
+Goal forall T1 T2 (f : T1 -> T2), (fun x => f x) = f.
+intros.
+eta_red.
+Abort.
diff --git a/test-suite/bugs/closed/5401.v b/test-suite/bugs/closed/5401.v
new file mode 100644
index 0000000000..95193b993b
--- /dev/null
+++ b/test-suite/bugs/closed/5401.v
@@ -0,0 +1,21 @@
+(* Testing printing of bound unnamed variables in pattern printer *)
+
+Module A.
+Parameter P : nat -> Type.
+Parameter v : forall m, P m.
+Parameter f : forall (P : nat -> Type), (forall a, P a) -> P 0.
+Class U (R : P 0) (m : forall x, P x) : Prop.
+Instance w : U (f _ (fun _ => v _)) v.
+Print HintDb typeclass_instances.
+End A.
+
+(* #5731 *)
+
+Module B.
+Axiom rel : Type -> Prop.
+Axiom arrow_rel : forall {A1}, A1 -> rel A1.
+Axiom forall_rel : forall E, (forall v1 : Type, E v1 -> rel v1) -> Prop.
+Axiom inl_rel: forall_rel _ (fun _ => arrow_rel).
+Hint Resolve inl_rel : foo.
+Print HintDb foo.
+End B.
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index c16e2751bc..910c81381b 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -350,7 +350,7 @@ let rec loop doc =
not possible due exceptions. *)
in vernac_loop doc (Stm.get_current_state ~doc)
with
- | CErrors.Drop -> ()
+ | CErrors.Drop -> doc
| CErrors.Quit -> exit 0
| any ->
Feedback.msg_error (str "Anomaly: main loop exited with exception: " ++
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 46dabf995d..46934f326a 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -36,4 +36,4 @@ val do_vernac : Stm.doc -> Stateid.t -> Stm.doc * Stateid.t
(** Main entry point of Coq: read and execute vernac commands. *)
-val loop : Stm.doc -> unit
+val loop : Stm.doc -> Stm.doc
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 19fcd99937..f3d5d9b859 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -79,6 +79,7 @@ let toploop_init = ref begin fun x ->
will not be generally be initialized, thus stateid, etc... may be
bogus. For now we just print to the console too *)
let coqtop_init_feed = Coqloop.coqloop_feed
+let drop_last_doc = ref None
(* Default toplevel loop *)
let console_toploop_run doc =
@@ -88,8 +89,9 @@ let console_toploop_run doc =
Flags.if_verbose warning "Dumpglob cannot be used in interactive mode.";
Dumpglob.noglob ()
end;
- Coqloop.loop doc;
+ let doc = Coqloop.loop doc in
(* Initialise and launch the Ocaml toplevel *)
+ drop_last_doc := Some doc;
Coqinit.init_ocaml_path();
Mltop.ocaml_toploop();
(* We let the feeder in place for users of Drop *)
@@ -183,9 +185,9 @@ let load_vernacular doc sid =
(fun (doc,sid) (f_in, verbosely) ->
let s = Loadpath.locate_file f_in in
if !Flags.beautify then
- Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in
+ Flags.with_option Flags.beautify_file (Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid) f_in
else
- Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
+ Vernac.load_vernac ~verbosely ~interactive:false ~check:true doc sid s)
(doc, sid) (List.rev !load_vernacular_list)
let load_init_vernaculars doc sid =
@@ -726,7 +728,7 @@ let parse_args arglist =
|"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true
|"-native-compiler" ->
if Coq_config.no_native_compiler then
- warning "Native compilation was disabled at configure time."
+ warning "Native compilation was disabled at configure time."
else Flags.native_compiler := true
|"-output-context" -> output_context := true
|"-profile-ltac" -> Flags.profile_ltac := true
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 1c7c3f944a..5b9494eaa9 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -15,6 +15,9 @@ val init_toplevel : string list -> (Stm.doc * Stateid.t) option
val start : unit -> unit
+(* Last document seen after `Drop` *)
+val drop_last_doc : Stm.doc option ref
+
(* For other toploops *)
val toploop_init : (string list -> string list) ref
val toploop_run : (Stm.doc -> unit) ref
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 18:16:40 +0000