aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml2
-rw-r--r--checker/checker.ml5
-rw-r--r--configure.ml55
-rwxr-xr-xdev/nsis/coq.nsi1
-rw-r--r--ide/ide_slave.ml2
-rw-r--r--interp/constrextern.ml44
-rw-r--r--library/library.ml14
-rw-r--r--ltac/tacintern.ml18
-rw-r--r--pretyping/evarconv.ml49
-rw-r--r--pretyping/find_subterm.ml1
-rw-r--r--printing/pptactic.ml3
-rw-r--r--printing/pptacticsig.mli2
-rw-r--r--test-suite/bugs/closed/4644.v52
-rw-r--r--tools/coq_makefile.ml53
14 files changed, 194 insertions, 107 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 93eb2a0d2..da3cd0316 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -303,7 +303,7 @@ let intern_from_file (dir, f) =
try
let ch = System.with_magic_number_check raw_intern_library f in
let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in
- let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in
+ let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in
let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in
let (discharging:'a option), _, _ = System.marshal_in_segment f ch in
let (tasks:'a option), _, _ = System.marshal_in_segment f ch in
diff --git a/checker/checker.ml b/checker/checker.ml
index 61b13c60b..9d76fb09e 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -179,10 +179,7 @@ let print_usage_channel co command =
output_string co command;
output_string co "coqchk options are:\n";
output_string co
-" -I dir -as coqdir map physical dir to logical coqdir\
-\n -I dir map directory dir to the empty logical path\
-\n -include dir (idem)\
-\n -R dir coqdir recursively map physical dir to logical coqdir\
+" -R dir coqdir map physical dir to logical coqdir\
\n\
\n -admit module load module and dependencies without checking\
\n -norec module check module but admit dependencies without checking\
diff --git a/configure.ml b/configure.ml
index 1ea56d3ce..f2f239075 100644
--- a/configure.ml
+++ b/configure.ml
@@ -513,43 +513,32 @@ exception NoCamlp5
let check_camlp5 testcma = match !Prefs.camlp5dir with
| Some dir ->
- if Sys.file_exists (dir/testcma) then dir
+ if Sys.file_exists (dir/testcma) then
+ let camlp5o =
+ try which_camlpX "camlp5o"
+ with Not_found -> die "Error: cannot find Camlp5 binaries in path.\n" in
+ dir, camlp5o
else
let msg =
sprintf "Cannot find camlp5 libraries in '%s' (%s not found)."
dir testcma
in die msg
| None ->
- let dir,_ = tryrun "camlp5" ["-where"] in
- let dir2 =
- if Sys.file_exists (camllib/"camlp5"/testcma) then
- camllib/"camlp5"
- else if Sys.file_exists (camllib/"site-lib"/"camlp5"/testcma) then
- camllib/"site-lib"/"camlp5"
- else ""
- in
- (* if the two values are different then camlp5 has been relocated
- * and will not be able to find its own files, so we prefer the
- * path where the files actually do exist *)
- if dir2 = "" then
- if dir = "" then
- let () = printf "No Camlp5 installation found." in
- let () = printf "Looking for Camlp4 instead...\n" in
- raise NoCamlp5
- else dir
- else dir2
-
-let check_camlp5_version () =
- try
- let camlp5o = which_camlpX "camlp5o" in
- let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
- let version = List.nth (string_split ' ' version_line) 2 in
- match string_split '.' version with
- | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) ->
- printf "You have Camlp5 %s. Good!\n" version; camlp5o, version
- | _ -> failwith "bad version"
- with
- | Not_found -> die "Error: cannot find Camlp5 binaries in path.\n"
+ try
+ let camlp5o = which_camlpX "camlp5o" in
+ let dir,_ = tryrun camlp5o ["-where"] in
+ dir, camlp5o
+ with Not_found ->
+ let () = printf "No Camlp5 installation found." in
+ let () = printf "Looking for Camlp4 instead...\n" in
+ raise NoCamlp5
+
+let check_camlp5_version camlp5o =
+ let version_line, _ = run ~err:StdOut camlp5o ["-v"] in
+ let version = List.nth (string_split ' ' version_line) 2 in
+ match string_split '.' version with
+ | major::minor::_ when s2i major > 5 || (s2i major, s2i minor) >= (5,1) ->
+ printf "You have Camlp5 %s. Good!\n" version; version
| _ -> die "Error: unsupported Camlp5 (version < 5.01 or unrecognized).\n"
let check_caml_version_for_camlp4 () =
@@ -563,8 +552,8 @@ let config_camlpX () =
try
if not !Prefs.usecamlp5 then raise NoCamlp5;
let camlp5mod = "gramlib" in
- let camlp5libdir = check_camlp5 (camlp5mod^".cma") in
- let camlp5o, camlp5_version = check_camlp5_version () in
+ let camlp5libdir, camlp5o = check_camlp5 (camlp5mod^".cma") in
+ let camlp5_version = check_camlp5_version camlp5o in
"camlp5", camlp5o, Filename.dirname camlp5o, camlp5libdir, camlp5mod, camlp5_version
with NoCamlp5 ->
(* We now try to use Camlp4, either by explicit choice or
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index e1052b1e1..80da84517 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -83,6 +83,7 @@ FunctionEnd
Section "Coq" Sec1
SetOutPath "$INSTDIR\"
+ File ${COQ_SRC_PATH}\LICENSE
SetOutPath "$INSTDIR\bin"
File ${COQ_SRC_PATH}\bin\*.exe
diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 6a386e050..79affb36f 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -383,8 +383,6 @@ let init =
match file with
| None -> Stm.get_current_state ()
| Some file ->
- if not (Filename.check_suffix file ".v") then
- error "A file with suffix .v is expected.";
let dir = Filename.dirname file in
let open Loadpath in let open CUnix in
let initial_id, _ =
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index e5ccb76b4..57091ca89 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -481,15 +481,15 @@ let explicitize loc inctx impl (cf,f) args =
(!print_implicits && !print_implicits_explicit_args) ||
(is_needed_for_correct_partial_application tail imp) ||
(!print_implicits_defensive &&
- is_significant_implicit a &&
- not (is_inferable_implicit inctx n imp))
+ not (is_inferable_implicit inctx n imp) &&
+ is_significant_implicit (Lazy.force a))
in
if visible then
- (a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
+ (Lazy.force a,Some (Loc.ghost, ExplByName (name_of_implicit imp))) :: tail
else
tail
- | a::args, _::impl -> (a,None) :: exprec (q+1) (args,impl)
- | args, [] -> List.map (fun a -> (a,None)) args (*In case of polymorphism*)
+ | a::args, _::impl -> (Lazy.force a,None) :: exprec (q+1) (args,impl)
+ | args, [] -> List.map (fun a -> (Lazy.force a,None)) args (*In case of polymorphism*)
| [], (imp :: _) when is_status_implicit imp && maximal_insertion_of imp ->
(* The non-explicit application cannot be parsed back with the same type *)
raise Expl
@@ -516,7 +516,7 @@ let explicitize loc inctx impl (cf,f) args =
with Expl ->
let f',us = match f with CRef (f,us) -> f,us | _ -> assert false in
let ip = if !print_projections then ip else None in
- CAppExpl (loc, (ip, f', us), args)
+ CAppExpl (loc, (ip, f', us), List.map Lazy.force args)
let is_start_implicit = function
| imp :: _ -> is_status_implicit imp && maximal_insertion_of imp
@@ -538,19 +538,21 @@ let extern_app loc inctx impl (cf,f) us args =
(!print_implicits && not !print_implicits_explicit_args)) &&
List.exists is_status_implicit impl)
then
+ let args = List.map Lazy.force args in
CAppExpl (loc, (is_projection (List.length args) cf,f,us), args)
else
explicitize loc inctx impl (cf,CRef (f,us)) args
-let rec extern_args extern scopes env args subscopes =
- match args with
- | [] -> []
- | a::args ->
- let argscopes, subscopes = match subscopes with
- | [] -> (None,scopes), []
- | scopt::subscopes -> (scopt,scopes), subscopes in
- extern argscopes env a :: extern_args extern scopes env args subscopes
+let rec fill_arg_scopes args subscopes scopes = match args, subscopes with
+| [], _ -> []
+| a :: args, scopt :: subscopes ->
+ (a, (scopt, scopes)) :: fill_arg_scopes args subscopes scopes
+| a :: args, [] ->
+ (a, (None, scopes)) :: fill_arg_scopes args [] scopes
+let extern_args extern env args =
+ let map (arg, argscopes) = lazy (extern argscopes env arg) in
+ List.map map args
let match_coercion_app = function
| GApp (loc,GRef (_,r,_),args) -> Some (loc, r, 0, args)
@@ -647,8 +649,7 @@ let rec extern inctx scopes vars r =
(match f with
| GRef (rloc,ref,us) ->
let subscopes = find_arguments_scope ref in
- let args =
- extern_args (extern true) (snd scopes) vars args subscopes in
+ let args = fill_arg_scopes args subscopes (snd scopes) in
begin
try
if !Flags.raw_print then raise Exit;
@@ -683,12 +684,14 @@ let rec extern inctx scopes vars r =
match args with
| [] -> raise No_match
(* we give up since the constructor is not complete *)
- | head :: tail -> ip q locs' tail
- ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
+ | (arg, scopes) :: tail ->
+ let head = extern true scopes vars arg in
+ ip q locs' tail ((extern_reference loc Id.Set.empty (ConstRef c), head) :: acc)
in
CRecord (loc, List.rev (ip projs locals args []))
with
| Not_found | No_match | Exit ->
+ let args = extern_args (extern true) vars args in
extern_app loc inctx
(select_stronger_impargs (implicits_of_global ref))
(Some ref,extern_reference rloc vars ref) (extern_universes us) args
@@ -696,7 +699,7 @@ let rec extern inctx scopes vars r =
| _ ->
explicitize loc inctx [] (None,sub_extern false scopes vars f)
- (List.map (sub_extern true scopes vars) args))
+ (List.map (fun c -> lazy (sub_extern true scopes vars c)) args))
| GLetIn (loc,na,t,c) ->
CLetIn (loc,(loc,na),sub_extern false scopes vars t,
@@ -916,7 +919,8 @@ and extern_notation (tmp_scope,scopes as allscopes) vars t = function
if List.is_empty l then a else CApp (loc,(None,a),l) in
if List.is_empty args then e
else
- let args = extern_args (extern true) scopes vars args argsscopes in
+ let args = fill_arg_scopes args argsscopes scopes in
+ let args = extern_args (extern true) vars args in
explicitize loc false argsimpls (None,e) args
with
No_match -> extern_notation allscopes vars t rules
diff --git a/library/library.ml b/library/library.ml
index 192700be7..4d0082850 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -35,7 +35,7 @@ module Delayed :
sig
type 'a delayed
-val in_delayed : string -> in_channel -> 'a delayed
+val in_delayed : string -> in_channel -> 'a delayed * Digest.t
val fetch_delayed : 'a delayed -> 'a
end =
@@ -50,7 +50,7 @@ type 'a delayed = {
let in_delayed f ch =
let pos = pos_in ch in
let _, digest = System.skip_in_segment f ch in
- { del_file = f; del_digest = digest; del_off = pos; }
+ ({ del_file = f; del_digest = digest; del_off = pos; }, digest)
(** Fetching a table of opaque terms at position [pos] in file [f],
expecting to find first a copy of [digest]. *)
@@ -427,23 +427,23 @@ let mk_summary m = {
let intern_from_file f =
let ch = raw_intern_library f in
let (lsd : seg_sum), _, digest_lsd = System.marshal_in_segment f ch in
- let (lmd : seg_lib delayed) = in_delayed f ch in
+ let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in
let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in
let _ = System.skip_in_segment f ch in
let _ = System.skip_in_segment f ch in
- let (del_opaque : seg_proofs delayed) = in_delayed f ch in
+ let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in
close_in ch;
register_library_filename lsd.md_name f;
add_opaque_table lsd.md_name (ToFetch del_opaque);
let open Safe_typing in
match univs with
- | None -> mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
+ | None -> mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
| Some (utab,uall,true) ->
add_univ_table lsd.md_name (Fetched utab);
- mk_library lsd lmd (Dvivo (digest_lsd,digest_u)) uall
+ mk_library lsd lmd (Dvivo (digest_lmd,digest_u)) uall
| Some (utab,_,false) ->
add_univ_table lsd.md_name (Fetched utab);
- mk_library lsd lmd (Dvo_or_vi digest_lsd) Univ.ContextSet.empty
+ mk_library lsd lmd (Dvo_or_vi digest_lmd) Univ.ContextSet.empty
module DPMap = Map.Make(DirPath)
diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml
index d39f83552..7cda7d137 100644
--- a/ltac/tacintern.ml
+++ b/ltac/tacintern.ml
@@ -424,7 +424,7 @@ let intern_hyp_location ist ((occs,id),hl) =
(* Reads a pattern *)
let intern_pattern ist ?(as_type=false) ltacvars = function
| Subterm (b,ido,pc) ->
- let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
+ let (metas,pc) = intern_constr_pattern ist ~as_type:false ~ltacvars pc in
ido, metas, Subterm (b,ido,pc)
| Term pc ->
let (metas,pc) = intern_constr_pattern ist ~as_type ~ltacvars pc in
@@ -446,7 +446,7 @@ let opt_cons accu = function
| Some id -> Id.Set.add id accu
(* Reads the hypotheses of a "match goal" rule *)
-let rec intern_match_goal_hyps ist lfun = function
+let rec intern_match_goal_hyps ist ?(as_type=false) lfun = function
| (Hyp ((_,na) as locna,mp))::tl ->
let ido, metas1, pat = intern_pattern ist ~as_type:true lfun mp in
let lfun, metas2, hyps = intern_match_goal_hyps ist lfun tl in
@@ -455,7 +455,7 @@ let rec intern_match_goal_hyps ist lfun = function
| (Def ((_,na) as locna,mv,mp))::tl ->
let ido, metas1, patv = intern_pattern ist ~as_type:false lfun mv in
let ido', metas2, patt = intern_pattern ist ~as_type:true lfun mp in
- let lfun, metas3, hyps = intern_match_goal_hyps ist lfun tl in
+ let lfun, metas3, hyps = intern_match_goal_hyps ist ~as_type lfun tl in
let lfun' = name_cons (opt_cons (opt_cons lfun ido) ido') na in
lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
| [] -> lfun, [], []
@@ -564,7 +564,7 @@ and intern_tactic_seq onlytac ist = function
ist.ltacvars, TacLetIn (isrec,l,intern_tactic onlytac ist' u)
| TacMatchGoal (lz,lr,lmr) ->
- ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr))
+ ist.ltacvars, (TacMatchGoal(lz,lr, intern_match_rule onlytac ist ~as_type:true lmr))
| TacMatch (lz,c,lmr) ->
ist.ltacvars,
TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr)
@@ -666,18 +666,18 @@ and intern_tacarg strict onlytac ist = function
TacGeneric arg
(* Reads the rules of a Match Context or a Match *)
-and intern_match_rule onlytac ist = function
+and intern_match_rule onlytac ist ?(as_type=false) = function
| (All tc)::tl ->
- All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl)
+ All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist ~as_type tl)
| (Pat (rl,mp,tc))::tl ->
let {ltacvars=lfun; genv=env} = ist in
- let lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in
- let ido,metas2,pat = intern_pattern ist lfun mp in
+ let lfun',metas1,hyps = intern_match_goal_hyps ist ~as_type lfun rl in
+ let ido,metas2,pat = intern_pattern ist ~as_type lfun mp in
let fold accu x = Id.Set.add x accu in
let ltacvars = List.fold_left fold (opt_cons lfun' ido) metas1 in
let ltacvars = List.fold_left fold ltacvars metas2 in
let ist' = { ist with ltacvars } in
- Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl)
+ Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist ~as_type tl)
| [] -> []
and intern_genarg ist (GenArg (Rawwit wit, x)) =
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 89cb723bc..7ec7d21c0 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -506,10 +506,13 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
match (flex_kind_of_term (fst ts) env evd term1 sk1,
flex_kind_of_term (fst ts) env evd term2 sk2) with
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
+ (* sk1[?ev1] =? sk2[?ev2] *)
let f1 i =
+ (* Try first-order unification *)
match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
- |None, Success i' ->
- (* Evar can be defined in i' *)
+ | None, Success i' ->
+ (* We do have sk1[] = sk2[]: we now unify ?ev1 and ?ev2 *)
+ (* Note that ?ev1 and ?ev2, may have been instantiated in the meantime *)
let ev1' = whd_evar i' (mkEvar ev1) in
if isEvar ev1' then
solve_simple_eqn (evar_conv_x ts) env i'
@@ -517,7 +520,9 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else
evar_eqappr_x ts env evd pbty
((ev1', sk1), csts1) ((term2, sk2), csts2)
- |Some (r,[]), Success i' ->
+ | Some (r,[]), Success i' ->
+ (* We have sk1'[] = sk2[] for some sk1' s.t. sk1[]=sk1'[r[]] *)
+ (* we now unify r[?ev1] and ?ev2 *)
let ev2' = whd_evar i' (mkEvar ev2) in
if isEvar ev2' then
solve_simple_eqn (evar_conv_x ts) env i'
@@ -525,16 +530,46 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
else
evar_eqappr_x ts env evd pbty
((ev2', sk1), csts1) ((term2, sk2), csts2)
-
- |Some ([],r), Success i' ->
+ | Some ([],r), Success i' ->
+ (* Symmetrically *)
+ (* We have sk1[] = sk2'[] for some sk2' s.t. sk2[]=sk2'[r[]] *)
+ (* we now unify ?ev1 and r[?ev2] *)
let ev1' = whd_evar i' (mkEvar ev1) in
if isEvar ev1' then
solve_simple_eqn (evar_conv_x ts) env i'
(position_problem true pbty,destEvar ev1',Stack.zip(term2,r))
else evar_eqappr_x ts env evd pbty
((ev1', sk1), csts1) ((term2, sk2), csts2)
- |_, (UnifFailure _ as x) -> x
- |Some _, _ -> UnifFailure (i,NotSameArgSize)
+ | None, (UnifFailure _ as x) ->
+ (* sk1 and sk2 have no common outer part *)
+ if Stack.not_purely_applicative sk2 then
+ (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+ flex_rigid true ev1 appr1 appr2
+ else
+ if Stack.not_purely_applicative sk1 then
+ (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+ flex_rigid false ev2 appr2 appr1
+ else
+ (* We could instead try Miller unification, then
+ postpone to see if other equations help, as in:
+ [Check fun a b : unit => (eqᵣefl : _ a = _ a b)] *)
+ x
+ | Some _, Success _ ->
+ (* sk1 and sk2 have a common outer part *)
+ if Stack.not_purely_applicative sk2 then
+ (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+ flex_rigid true ev1 appr1 appr2
+ else
+ if Stack.not_purely_applicative sk1 then
+ (* Ad hoc compatibility with 8.4 which treated non-app as rigid *)
+ flex_rigid false ev2 appr2 appr1
+ else
+ (* We could instead try Miller unification, then
+ postpone to see if other equations help, as in:
+ [Check fun a b c : unit => (eqᵣefl : _ a b = _ c a b)] *)
+ UnifFailure (i,NotSameArgSize)
+ | _, _ -> anomaly (Pp.str "Unexpected result from ise_stack2.")
+
and f2 i =
if Evar.equal sp1 sp2 then
match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index ae8b91c34..df1fc20f1 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -108,7 +108,6 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t =
raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
let rec substrec k t =
if nowhere_except_in && !pos > maxocc then t else
- if not (Vars.closed0 t) then subst_below k t else
try
let subst = test.match_fun test.testing_state t in
if Locusops.is_selected !pos occs then
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 3d1e3e054..5356cdee8 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -366,7 +366,6 @@ module Make
in
str "<" ++ name ++ str ">" ++ args
-
let pr_alias_key key =
try
let prods = (KNmap.find key !prnotation_tab).pptac_prods in
@@ -383,7 +382,7 @@ module Make
str (String.concat " " (pr prods))
with Not_found ->
KerName.print key
-
+
let pr_alias_gen pr_gen lev key l =
try
let pp = KNmap.find key !prnotation_tab in
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index f02785a55..c08d6044d 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -50,6 +50,8 @@ module type Pp = sig
val pr_alias : (Val.t -> std_ppcmds) ->
int -> Names.KerName.t -> Val.t list -> std_ppcmds
+ val pr_alias_key : Names.KerName.t -> std_ppcmds
+
val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
val pr_raw_tactic : raw_tactic_expr -> std_ppcmds
diff --git a/test-suite/bugs/closed/4644.v b/test-suite/bugs/closed/4644.v
new file mode 100644
index 000000000..f09b27c2b
--- /dev/null
+++ b/test-suite/bugs/closed/4644.v
@@ -0,0 +1,52 @@
+(* Testing a regression of unification in 8.5 in problems of the form
+ "match ?y with ... end = ?x args" *)
+
+Lemma foo : exists b, forall a, match a with tt => tt end = b a.
+Proof.
+eexists. intro.
+refine (_ : _ = match _ with tt => _ end).
+refine eq_refl.
+Qed.
+
+(**********************************************************************)
+
+Axiom proof_admitted : False.
+Tactic Notation "admit" := case proof_admitted.
+Require Export Coq.Classes.Morphisms.
+Require Import Coq.Lists.List.
+
+Global Set Implicit Arguments.
+
+Definition list_caset A (P : list A -> Type) (N : P nil) (C : forall x xs, P (x::xs))
+ ls
+ : P ls
+ := match ls with
+ | nil => N
+ | x::xs => C x xs
+ end.
+
+Axiom list_caset_Proper'
+ : forall {A P},
+ Proper (eq
+ ==> pointwise_relation _ (pointwise_relation _ eq)
+ ==> eq
+ ==> eq)
+ (@list_caset A (fun _ => P)).
+Goal forall (T T' : Set) (a3 : list T), exists y2, forall (a4 : T' -> bool),
+ match a3 with
+ | nil => 0
+ | (_ :: _)%list => 1
+ end = y2 a4.
+ clear; eexists; intros.
+ reflexivity. Undo.
+ Local Ltac t :=
+ lazymatch goal with
+ | [ |- match ?v with nil => ?N | cons x xs => @?C x xs end = _ :> ?P ]
+ => let T := type of v in
+ let A := match (eval hnf in T) with list ?A => A end in
+ refine (@list_caset_Proper' A P _ _ _ _ _ _ _ _ _
+ : @list_caset A (fun _ => P) N C v = match _ with nil => _ | cons x xs => _ end)
+ end.
+ (etransitivity; [ t | reflexivity ]) || fail 0 "too early".
+ Undo.
+ t.
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index c8dc4a8de..4264ff1d9 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -27,6 +27,10 @@ let rec print_list sep = function
| x :: l -> print x; print sep; print_list sep l
| [] -> ()
+let rec print_prefix_list sep = function
+ | x :: l -> print sep; print x; print_prefix_list sep l
+ | [] -> ()
+
let section s =
let l = String.length s in
let print_com s =
@@ -580,28 +584,35 @@ let parameters () =
print " $(filter-out Warning: Error:,\\\n";
print " $(shell $(COQBIN)coqtop -q -noinit -batch -quiet -print-mod-uid $(1))))\n\n"
-let include_dirs (inc_ml,inc_i,inc_r) =
+let include_dirs (inc_ml,inc_q,inc_r) =
let parse_ml_includes l = List.map (fun (x,_) -> "-I \"" ^ x ^ "\"") l in
- let parse_includes l = List.map (fun (x,l,_) ->
- let l' = if l = "" then "\"\"" else l in
- "-Q \"" ^ x ^ "\" " ^ l' ^"") l in
- let parse_rec_includes l = List.map (fun (p,l,_) ->
- let l' = if l = "" then "\"\"" else l in
- "-R \"" ^ p ^ "\" " ^ l' ^"") l in
+ let includes =
+ List.map (fun (p,l,_) ->
+ let l' = if l = "" then "\"\"" else l in
+ " \"" ^ p ^ "\" " ^ l' ^"") in
let str_ml = parse_ml_includes inc_ml in
- let str_i = parse_includes inc_i in
- let str_r = parse_rec_includes inc_r in
- section "Libraries definitions.";
- if !some_ml4file || !some_mlfile || !some_mlifile then begin
- print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n";
- end;
- if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
- print "COQLIBS?="; print_list "\\\n " str_i;
- List.iter (fun x -> print "\\\n "; print x) str_r;
- List.iter (fun x -> print "\\\n "; print x) str_ml; print "\n";
- print "COQDOCLIBS?="; print_list "\\\n " str_i;
- List.iter (fun x -> print "\\\n "; print x) str_r; print "\n\n";
- end
+ section "Libraries definitions.";
+ if !some_ml4file || !some_mlfile || !some_mlifile then begin
+ print "OCAMLLIBS?="; print_list "\\\n " str_ml; print "\n";
+ end;
+ if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
+ print "COQLIBS?=";
+ print_prefix_list "\\\n -Q" (includes inc_q);
+ print_prefix_list "\\\n -R" (includes inc_r);
+ print_prefix_list "\\\n " str_ml;
+ print "\n";
+ end;
+ if !some_vfile then begin
+ print "COQCHKLIBS?=";
+ print_prefix_list "\\\n -R" (includes inc_q);
+ print_prefix_list "\\\n -R" (includes inc_r);
+ print "\n";
+ print "COQDOCLIBS?=";
+ print_prefix_list "\\\n -R" (includes inc_q);
+ print_prefix_list "\\\n -R" (includes inc_r);
+ print "\n";
+ end;
+ print "\n"
let double_colon = ["clean"; "cleanall"; "archclean"]
@@ -777,7 +788,7 @@ let main_targets vfiles (mlifiles,ml4files,mlfiles,mllibfiles,mlpackfiles) other
print "all-gal.pdf: $(VFILES)\n";
print "\t$(COQDOC) -toc $(COQDOCFLAGS) -pdf -g $(COQDOCLIBS) -o $@ `$(COQDEP) -sort -suffix .v $^`\n\n";
print "validate: $(VOFILES)\n";
- print "\t$(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $(notdir $(^:.vo=))\n\n";
+ print "\t$(COQCHK) $(COQCHKFLAGS) $(COQCHKLIBS) $(notdir $(^:.vo=))\n\n";
print "beautify: $(VFILES:=.beautified)\n";
print "\tfor file in $^; do mv $${file%.beautified} $${file%beautified}old && mv $${file} $${file%.beautified}; done\n";
print "\t@echo \'Do not do \"make clean\" until you are sure that everything went well!\'\n";
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 10:34:01 +0000