diff options
| -rw-r--r-- | CHANGES | 6 | ||||
| -rw-r--r-- | configure.ml | 55 | ||||
| -rw-r--r-- | library/lib.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 10 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 111 | ||||
| -rw-r--r-- | pretyping/find_subterm.ml | 1 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 5 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 1 | ||||
| -rw-r--r-- | proofs/clenv.ml | 3 | ||||
| -rw-r--r-- | stm/lemmas.ml | 7 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 18 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4644.v | 52 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4725.v | 38 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4782.v | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4813.v | 9 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4816.v | 11 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4818.v | 24 | ||||
| -rw-r--r-- | toplevel/command.ml | 1 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 10 | ||||
| -rw-r--r-- | toplevel/metasyntax.ml | 2 | ||||
| -rw-r--r-- | toplevel/obligations.ml | 6 |
22 files changed, 277 insertions, 106 deletions
@@ -3,8 +3,12 @@ Changes from V8.5pl1 to V8.5pl2 Bugfixes -- #4677: fix alpha-conversion in notations needing eta-expansion +- #4677: fix alpha-conversion in notations needing eta-expansion. - Fully preserve initial order of hypotheses in "Regular Subst Tactic" mode. +- #4644: a regression in unification. +- #4777: printing inefficiency with implicit arguments +- #4752: CoqIDE crash on files not ended by ".v". +- #4398: type_scope used consistently in "match goal". Changes from V8.5 to V8.5pl1 ============================ diff --git a/configure.ml b/configure.ml index 3fcc24d05d..aa26075b74 100644 --- a/configure.ml +++ b/configure.ml @@ -545,43 +545,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 () = @@ -595,8 +584,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/library/lib.ml b/library/lib.ml index e4617cafb6..f6b4a2458b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -417,7 +417,7 @@ let add_section_variable id impl poly ctx = match !sectab with | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *) | (vars,repl,abs)::sl -> - check_same_poly poly vars; + List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab; sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl let add_section_context ctx = diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 065d0fe537..bc8e721edc 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1510,13 +1510,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + (* Refresh the global universes, now including those of _F *) + let evm = Evd.from_env (Global.env ()) in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in - let relation = - fst (*FIXME*)(interp_constr - env_with_pre_rec_args - (Evd.from_env env_with_pre_rec_args) - r) + let relation, evuctx = + interp_constr env_with_pre_rec_args evm r in + let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref None in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b8d92b9be7..aead1cb35f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -97,8 +97,7 @@ let position_problem l2r = function | CUMUL -> Some l2r let occur_rigidly ev evd t = - let (l, app) = decompose_app_vect t in - let rec aux t = + let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true @@ -110,7 +109,7 @@ let occur_rigidly ev evd t = | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false | Case _ -> false - in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app + in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem @@ -318,25 +317,22 @@ let rec evar_conv_x ts env evd pbty term1 term2 = Note: incomplete heuristic... *) let ground_test = if is_ground_term evd term1 && is_ground_term evd term2 then ( - let evd, e = + let e = try let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 in - if b then evd, None - else evd, Some (ConversionFailed (env,term1,term2)) - with Univ.UniverseInconsistency e -> evd, Some (UnifUnivInconsistency e) + if b then Success evd + else UnifFailure (evd, ConversionFailed (env,term1,term2)) + with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e) in match e with - | None -> Some (evd, e) - | Some e -> - if is_ground_env evd env then Some (evd, Some e) - else None) + | UnifFailure (evd, e) when not (is_ground_env evd env) -> None + | _ -> Some e) else None in match ground_test with - | Some (evd, None) -> Success evd - | Some (evd, Some e) -> UnifFailure (evd,e) + | Some result -> result | None -> (* Until pattern-unification is used consistently, use nohdbeta to not destroy beta-redexes that can be used for 1st-order unification *) @@ -365,8 +361,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = - let default_fail i = (* costly *) - UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in @@ -418,7 +412,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> default_fail evd + | None -> quick_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left @@ -465,10 +459,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in let eta evd = - match kind_of_term termR with - | Lambda _ -> eta env evd false skR termR skF termF - | Construct u -> eta_constructor ts env evd skR u skF termF - | _ -> UnifFailure (evd,NotSameHead) + match kind_of_term termR with + | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> + eta env evd false skR termR skF termF + | Construct u -> eta_constructor ts env evd skR u skF termF + | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> @@ -503,10 +498,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' @@ -514,7 +512,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' @@ -522,16 +522,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 @@ -709,10 +739,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid, _ when isLambda term1 -> + | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 -> eta env evd true sk1 term1 sk2 term2 - | _, Rigid when isLambda term2 -> + | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 -> eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin @@ -1062,7 +1092,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = abstract_free_holes evd subst, true with TypingFailed evd -> evd, false -let second_order_matching_with_args ts env evd ev l t = +let second_order_matching_with_args ts env evd pbty ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in @@ -1070,8 +1100,9 @@ let second_order_matching_with_args ts env evd ev l t = if b then Success evd else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) if b then Success evd else -*) - UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + *) + let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in @@ -1087,7 +1118,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk1 evd term2 args1 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a) (remove_instance_local_defs evd evk2 args2) -> @@ -1095,7 +1128,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk2 evd term1 args2 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in Success (solve_refl ~can_drop:true f env evd @@ -1110,20 +1145,20 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = ise_try evd [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2); (fun evd -> - second_order_matching_with_args ts env evd ev1 l1 t2)] + second_order_matching_with_args ts env evd pbty ev1 l1 t2)] | _,Evar ev2 when Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1); (fun evd -> - second_order_matching_with_args ts env evd ev2 l2 t1)] + second_order_matching_with_args ts env evd pbty ev2 l2 t1)] | Evar ev1,_ -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev1 l1 t2 + second_order_matching_with_args ts env evd pbty ev1 l1 t2 | _,Evar ev2 -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev2 l2 t1 + second_order_matching_with_args ts env evd pbty ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 6733b7fca0..1f5435b6bd 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -105,7 +105,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/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cf5b08c58f..b0715af734 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,15 +14,16 @@ open Type_errors type unification_error = | OccurCheck of existential_key * constr - | NotClean of existential * env * constr + | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr + | ConversionFailed of env * constr * constr (* Non convertible closed terms *) | MetaOccurInBody of existential_key | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f617df9ee7..880f48e5f9 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,6 +24,7 @@ type unification_error = | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 88e1bce95a..79b331a273 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -459,7 +459,8 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e -> + | PretypeError (_,_,ActualTypeNotCoercible (_,_, + (NotClean _ | ConversionFailed _))) as e -> raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 5b205e79ef..1ab695a5f2 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -476,9 +476,11 @@ let save_proof ?proof = function let ctx = Evd.evar_context_universe_context (fst universes) in Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes) | None -> + let pftree = Pfedit.get_pftreestate () in let id, k, typ = Pfedit.current_proof_statement () in + let universes = Proof.initial_euctx pftree in (* This will warn if the proof is complete *) - let pproofs, universes = + let pproofs, _univs = Proof_global.return_proof ~allow_partial:true () in let sec_vars = match Pfedit.get_used_variables(), pproofs with @@ -490,7 +492,8 @@ let save_proof ?proof = function Some (Environ.keep_hyps env (Idset.union ids_typ ids_def)) | _ -> None in let names = Pfedit.get_universe_binders () in - let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in + let evd = Evd.from_ctx universes in + let binders, ctx = Evd.universe_context ?names evd in Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None), (universes, Some binders)) in diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 11f2c5943d..e60bc459b8 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -423,7 +423,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 @@ -445,7 +445,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 @@ -454,7 +454,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, [], [] @@ -600,7 +600,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) @@ -718,18 +718,18 @@ and intern_tacarg strict onlytac ist = function anomaly ~loc (str "Unknown dynamic: <" ++ str tag ++ str ">") (* 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 x = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 4562e25184..b1df1f5aa4 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1501,7 +1501,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) if n<0 then error "Applied theorem has not enough premisses."; let clause = make_clenv_binding_apply env sigma (Some n) (c,thm_ty) lbind in Clenvtac.res_pf clause ~with_evars ~flags - with UserError _ as exn -> + with exn when catchable_exception exn -> Proofview.tclZERO exn in let rec try_red_apply thm_ty (exn0, info) = diff --git a/test-suite/bugs/closed/4644.v b/test-suite/bugs/closed/4644.v new file mode 100644 index 0000000000..f09b27c2b1 --- /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/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v new file mode 100644 index 0000000000..fd5e0fb60d --- /dev/null +++ b/test-suite/bugs/closed/4725.v @@ -0,0 +1,38 @@ +Require Import EquivDec Equivalence List Program. +Require Import Relation_Definitions. +Import ListNotations. +Generalizable All Variables. + +Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V +:= + match l with + | nil => nil + | y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl) + end. + +Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (xs : list V) (x : V) : + length (removeV x xs) < length (x :: xs). + Proof. Admitted. + +(* Function version *) +Set Printing Universes. + +Require Import Recdef. + +Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (l : list V) { measure length l} := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) + end. +Proof. intros. apply remove_le. Qed. + +(* Program version *) + +Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V) + { measure (@length V l) lt } := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _ + end. diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v new file mode 100644 index 0000000000..ed44437861 --- /dev/null +++ b/test-suite/bugs/closed/4782.v @@ -0,0 +1,9 @@ +(* About typing of with bindings *) + +Record r : Type := mk_r { type : Type; cond : type -> Prop }. + +Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p. + +Goal p. +Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil. + diff --git a/test-suite/bugs/closed/4813.v b/test-suite/bugs/closed/4813.v new file mode 100644 index 0000000000..5f8ea74c1a --- /dev/null +++ b/test-suite/bugs/closed/4813.v @@ -0,0 +1,9 @@ +(* On the strength of "apply with" (see also #4782) *) + +Record ProverT := { Facts : Type }. +Record ProverT_correct (P : ProverT) := { Valid : Facts P -> Prop ; + Valid_weaken : Valid = Valid }. +Definition reflexivityValid (_ : unit) := True. +Definition reflexivityProver_correct : ProverT_correct {| Facts := unit |}. +Proof. + eapply Build_ProverT_correct with (Valid := reflexivityValid). diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v new file mode 100644 index 0000000000..5ba0787ee7 --- /dev/null +++ b/test-suite/bugs/closed/4816.v @@ -0,0 +1,11 @@ +Require Coq.Classes.RelationClasses. + +Class PreOrder (A : Type) (r : A -> A -> Type) : Type := +{ refl : forall x, r x x }. + +Section foo. + Polymorphic Universes A. + Section bar. + Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}. + End bar. +End foo.
\ No newline at end of file diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v new file mode 100644 index 0000000000..904abb2287 --- /dev/null +++ b/test-suite/bugs/closed/4818.v @@ -0,0 +1,24 @@ +(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *) +(* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *) +(* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3 + coqtop version 8.5pl1 (June 2016) *) +Set Universe Polymorphism. + +Inductive GCov (I : Type) : Type := | Foo : I -> GCov I. + +Section Product. + +Variables S IS : Type. +Variable locS : IS -> True. + +Goal GCov (IS * S) -> GCov IS. +intros X0. induction X0; intros. +destruct i. +specialize (locS i). +clear -locS. +destruct locS. Show Universes. +Admitted. + +(* +Anomaly: Universe Product.5189 undefined. Please report. +*) diff --git a/toplevel/command.ml b/toplevel/command.ml index 8f7c389975..8eb2232eda 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -923,7 +923,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in - let () = check_evars_are_solved env !evdref (Evd.empty,!evdref) in let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 3ff2d3fb18..244174f651 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -65,12 +65,12 @@ let rec contract3' env a b c = function let (env',t1,t2) = contract2 env' t1 t2 in contract3 env a b c, ConversionFailed (env',t1,t2) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | MetaOccurInBody _ | InstanceNotSameType _ + | MetaOccurInBody _ | InstanceNotSameType _ | ProblemBeyondCapabilities | UnifUnivInconsistency _ as x -> contract3 env a b c, x - | CannotSolveConstraint ((pb,env,t,u),x) -> - let env,t,u = contract2 env t u in + | CannotSolveConstraint ((pb,env',t,u),x) -> + let env',t,u = contract2 env' t u in let y,x = contract3' env a b c x in - y,CannotSolveConstraint ((pb,env,t,u),x) + y,CannotSolveConstraint ((pb,env',t,u),x) (** Printers *) @@ -310,6 +310,8 @@ let rec explain_unification_error env sigma p1 p2 = function (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e + | ProblemBeyondCapabilities -> + [] in match aux p1 p2 e with | [] -> mt () diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 2ccd27acb9..92208e3046 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -982,7 +982,7 @@ let make_interpretation_type isrec = function | NtnInternTypeConstr when isrec -> NtnTypeConstrList | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> error "Type not allowed in recursive notation." + | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders." let make_interpretation_vars recvars allvars = let eq_subscope (sc1, l1) (sc2, l2) = diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index a18552c5ec..6f7a5f684a 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -24,10 +24,6 @@ open Util let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) -let trace s = - if !Flags.debug then msg_debug s - else () - let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -871,8 +867,6 @@ let rec solve_obligation prg num tac = let auto n tac oblset = auto_solve_obligations n ~oblset tac in let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type hook in - let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in let _ = Pfedit.by (snd (get_default_tactic ())) in Option.iter (fun tac -> Pfedit.set_end_tac tac) tac |