diff options
-rw-r--r-- | checker/check.ml | 2 | ||||
-rw-r--r-- | checker/checker.ml | 5 | ||||
-rw-r--r-- | configure.ml | 55 | ||||
-rwxr-xr-x | dev/nsis/coq.nsi | 1 | ||||
-rw-r--r-- | ide/ide_slave.ml | 2 | ||||
-rw-r--r-- | interp/constrextern.ml | 44 | ||||
-rw-r--r-- | library/library.ml | 14 | ||||
-rw-r--r-- | ltac/tacintern.ml | 18 | ||||
-rw-r--r-- | pretyping/evarconv.ml | 49 | ||||
-rw-r--r-- | pretyping/find_subterm.ml | 1 | ||||
-rw-r--r-- | printing/pptactic.ml | 3 | ||||
-rw-r--r-- | printing/pptacticsig.mli | 2 | ||||
-rw-r--r-- | test-suite/bugs/closed/4644.v | 52 | ||||
-rw-r--r-- | tools/coq_makefile.ml | 53 |
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"; |