diff options
-rw-r--r-- | CHANGES | 30 | ||||
-rw-r--r-- | interp/constrintern.ml | 29 | ||||
-rw-r--r-- | ltac/extratactics.ml4 | 35 | ||||
-rw-r--r-- | ltac/tacintern.ml | 18 | ||||
-rw-r--r-- | pretyping/evarsolve.ml | 31 | ||||
-rw-r--r-- | proofs/pfedit.ml | 6 | ||||
-rw-r--r-- | test-suite/Makefile | 22 | ||||
-rw-r--r-- | test-suite/bugs/closed/3825.v | 8 | ||||
-rw-r--r-- | test-suite/bugs/closed/4375.v | 9 | ||||
-rw-r--r-- | test-suite/bugs/closed/4882.v | 50 | ||||
-rw-r--r-- | test-suite/misc/deps/A/A.v | 1 | ||||
-rw-r--r-- | test-suite/misc/deps/B/A.v | 1 | ||||
-rw-r--r-- | test-suite/misc/deps/B/B.v | 7 | ||||
-rw-r--r-- | test-suite/misc/deps/checksum.v | 2 | ||||
-rw-r--r-- | test-suite/success/vm_univ_poly.v | 12 |
15 files changed, 205 insertions, 56 deletions
@@ -82,14 +82,38 @@ Tools Changes from V8.5pl1 to V8.5pl2 =============================== -Bugfixes +Critical bugfix +- Checksums of .vo files dependencies were not correctly checked. + +Other bugfixes +- #4097: more efficient occur-check in presence of primitive projections +- #4398: type_scope used consistently in "match goal". +- #4450: eauto does not work with polymorphic lemmas - #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 +- #4725: Function (Error: Conversion test raised an anomaly) and Program + (Error: Cannot infer this placeholder of type) +- #4747: Problem building Coq 8.5pl1 with OCaml 4.03.0: Fatal warnings - #4752: CoqIDE crash on files not ended by ".v". -- #4398: type_scope used consistently in "match goal". +- #4777: printing inefficiency with implicit arguments +- #4818: "Admitted" fails due to undefined universe anomaly after calling + "destruct" +- #4823: remote counter: avoid thread race on sockets +- #4881: synchronizing "Declare Implicit Tactic" with backtrack. +- #4882: anomaly with Declare Implicit Tactic on hole of type with evars +- Fix use of "Declare Implicit Tactic" in refine. + triggered by CoqIDE + +Universes +- Disallow silently dropping universe instances applied to variables + (forward compatible) +- Allow explicit universe instances on notations, when they can apply + to the head reference of their expansion. + +Build infrastructure +- New update on how to find camlp5 binary and library at configure time. Changes from V8.5 to V8.5pl1 ============================ diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 470eb8324..1c50253d9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -741,7 +741,13 @@ let string_of_ty = function | Method -> "meth" | Variable -> "var" -let intern_var genv (ltacvars,ntnvars) namedctx loc id = +let gvar (loc, id) us = match us with +| None -> GVar (loc, id) +| Some _ -> + user_err_loc (loc, "", str "Variable " ++ pr_id id ++ + str " cannot have a universe instance") + +let intern_var genv (ltacvars,ntnvars) namedctx loc id us = (* Is [id] an inductive type potentially with implicit *) try let ty,expl_impls,impls,argsc = Id.Map.find id genv.impls in @@ -749,21 +755,21 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = (fun id -> CRef (Ident (loc,id),None), Some (loc,ExplByName id)) expl_impls in let tys = string_of_ty ty in Dumpglob.dump_reference loc "<>" (Id.to_string id) tys; - GVar (loc,id), make_implicits_list impls, argsc, expl_impls + gvar (loc,id) us, make_implicits_list impls, argsc, expl_impls with Not_found -> (* Is [id] bound in current term or is an ltac var bound to constr *) if Id.Set.mem id genv.ids || Id.Set.mem id ltacvars.ltac_vars then - GVar (loc,id), [], [], [] + gvar (loc,id) us, [], [], [] (* Is [id] a notation variable *) else if Id.Map.mem id ntnvars then - (set_var_scope loc id true genv ntnvars; GVar (loc,id), [], [], []) + (set_var_scope loc id true genv ntnvars; gvar (loc,id) us, [], [], []) (* Is [id] the special variable for recursive notations *) else if Id.equal id ldots_var then if Id.Map.is_empty ntnvars then error_ldots_var loc - else GVar (loc,id), [], [], [] + else gvar (loc,id) us, [], [], [] else if Id.Set.mem id ltacvars.ltac_bound then (* Is [id] bound to a free name in ltac (this is an ltac error message) *) user_err_loc (loc,"intern_var", @@ -778,10 +784,10 @@ let intern_var genv (ltacvars,ntnvars) namedctx loc id = let impls = implicits_of_global ref in let scopes = find_arguments_scope ref in Dumpglob.dump_reference loc "<>" (string_of_qualid (Decls.variable_secpath id)) "var"; - GRef (loc, ref, None), impls, scopes, [] + GRef (loc, ref, us), impls, scopes, [] with e when CErrors.noncritical e -> (* [id] a goal variable *) - GVar (loc,id), [], [], [] + gvar (loc,id) us, [], [], [] let find_appl_head_data c = match c with @@ -843,9 +849,12 @@ let intern_qualid loc qid intern env lvar us args = let c = match us, c with | None, _ -> c | Some _, GRef (loc, ref, None) -> GRef (loc, ref, us) + | Some _, GApp (loc, GRef (loc', ref, None), arg) -> + GApp (loc, GRef (loc', ref, us), arg) | Some _, _ -> user_err_loc (loc, "", str "Notation " ++ pr_qualid qid ++ - str " cannot have a universe instance") + str " cannot have a universe instance, its expanded head + does not start with a reference") in c, projapp, args2 @@ -864,7 +873,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = let x, imp, scopes, l = find_appl_head_data r in (x,imp,scopes,l), args2 | Ident (loc, id) -> - try intern_var env lvar namedctx loc id, args + try intern_var env lvar namedctx loc id us, args with Not_found -> let qid = qualid_of_ident id in try @@ -874,7 +883,7 @@ let intern_applied_reference intern env namedctx (_, ntnvars as lvar) us args = with Not_found -> (* Extra allowance for non globalizing functions *) if !interning_grammar || env.unb then - (GVar (loc,id), [], [], []), args + (gvar (loc,id) us, [], [], []), args else error_global_not_found_loc loc qid let interp_reference vars r = diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4 index 2ee9a6c98..be47293fc 100644 --- a/ltac/extratactics.ml4 +++ b/ltac/extratactics.ml4 @@ -337,11 +337,18 @@ END (**********************************************************************) (* Refine *) +let constr_flags = { + Pretyping.use_typeclasses = true; + Pretyping.use_unif_heuristics = true; + Pretyping.use_hook = Some Pfedit.solve_by_implicit_tactic; + Pretyping.fail_evar = false; + Pretyping.expand_evars = true } + let refine_tac ist simple c = Proofview.Goal.nf_enter { enter = begin fun gl -> let concl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in - let flags = Pretyping.all_no_fail_flags in + let flags = constr_flags in let expected_type = Pretyping.OfType concl in let c = Pretyping.type_uconstr ~flags ~expected_type ist c in let update = { run = fun sigma -> c.delayed env sigma } in @@ -517,11 +524,29 @@ VERNAC COMMAND EXTEND AddStepr CLASSIFIED AS SIDEFF [ add_transitivity_lemma false t ] END +let cache_implicit_tactic (_,tac) = match tac with + | Some tac -> Pfedit.declare_implicit_tactic (Tacinterp.eval_tactic tac) + | None -> Pfedit.clear_implicit_tactic () + +let subst_implicit_tactic (subst,tac) = + Option.map (Tacsubst.subst_tactic subst) tac + +let inImplicitTactic : glob_tactic_expr option -> obj = + declare_object {(default_object "IMPLICIT-TACTIC") with + open_function = (fun i o -> if Int.equal i 1 then cache_implicit_tactic o); + cache_function = cache_implicit_tactic; + subst_function = subst_implicit_tactic; + classify_function = (fun o -> Dispose)} + +let declare_implicit_tactic tac = + Lib.add_anonymous_leaf (inImplicitTactic (Some (Tacintern.glob_tactic tac))) + +let clear_implicit_tactic () = + Lib.add_anonymous_leaf (inImplicitTactic None) + VERNAC COMMAND EXTEND ImplicitTactic CLASSIFIED AS SIDEFF -| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> - [ Pfedit.declare_implicit_tactic (Tacinterp.interp tac) ] -| [ "Clear" "Implicit" "Tactic" ] -> - [ Pfedit.clear_implicit_tactic () ] +| [ "Declare" "Implicit" "Tactic" tactic(tac) ] -> [ declare_implicit_tactic tac ] +| [ "Clear" "Implicit" "Tactic" ] -> [ clear_implicit_tactic () ] END diff --git a/ltac/tacintern.ml b/ltac/tacintern.ml index 00722ac28..455b871c8 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:false ~ltacvars pc in + let (metas,pc) = intern_constr_pattern ist ~as_type ~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 ?(as_type=false) lfun = function +let rec intern_match_goal_hyps ist 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 ?(as_type=false) 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 ~as_type lfun tl in + let lfun, metas3, hyps = intern_match_goal_hyps ist 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 ~as_type:true lmr)) + ist.ltacvars, TacMatchGoal(lz,lr, intern_match_rule onlytac ist lmr) | TacMatch (lz,c,lmr) -> ist.ltacvars, TacMatch (lz,intern_tactic_or_tacarg ist c,intern_match_rule onlytac ist lmr) @@ -668,18 +668,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 ?(as_type=false) = function +and intern_match_rule onlytac ist = function | (All tc)::tl -> - All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist ~as_type tl) + All (intern_tactic onlytac ist tc) :: (intern_match_rule onlytac ist tl) | (Pat (rl,mp,tc))::tl -> let {ltacvars=lfun; genv=env} = ist 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 lfun',metas1,hyps = intern_match_goal_hyps ist lfun rl in + let ido,metas2,pat = intern_pattern ist 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 ~as_type tl) + Pat (hyps,pat,intern_tactic onlytac ist' tc) :: (intern_match_rule onlytac ist tl) | [] -> [] and intern_genarg ist (GenArg (Rawwit wit, x)) = diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 62700aef3..338ac4300 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -212,30 +212,29 @@ let restrict_instance evd evk filter argsv = open Context.Rel.Declaration let noccur_evar env evd evk c = let cache = ref Int.Set.empty (* cache for let-ins *) in - let rec occur_rec (k, env as acc) c = + let rec occur_rec check_types (k, env as acc) c = match kind_of_term c with | Evar (evk',args' as ev') -> (match safe_evar_value evd ev' with - | Some c -> occur_rec acc c + | Some c -> occur_rec check_types acc c | None -> if Evar.equal evk evk' then raise Occur - else Array.iter (occur_rec acc) args') + else (if check_types then + occur_rec false acc (existential_type evd ev'); + Array.iter (occur_rec check_types acc) args')) | Rel i when i > k -> - if not (Int.Set.mem (i-k) !cache) then - (match Environ.lookup_rel i env with - | LocalAssum _ -> () - | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec acc (lift i b)) - | Proj (p,c) -> - let c = - try Retyping.expand_projection env evd p c [] - with Retyping.RetypeError _ -> - (* Can happen when called from w_unify which doesn't assign evars/metas - eagerly enough *) c - in occur_rec acc c + if not (Int.Set.mem (i-k) !cache) then + let decl = Environ.lookup_rel i env in + if check_types then + (cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i (get_type decl))); + (match decl with + | LocalAssum _ -> () + | LocalDef (_,b,_) -> cache := Int.Set.add (i-k) !cache; occur_rec false acc (lift i b)) + | Proj (p,c) -> occur_rec true acc c | _ -> iter_constr_with_full_binders (fun rd (k,env) -> (succ k, push_rel rd env)) - occur_rec acc c + (occur_rec check_types) acc c in - try occur_rec (0,env) c; true with Occur -> false + try occur_rec false (0,env) c; true with Occur -> false (***************************************) (* Managing chains of local definitons *) diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index 30b031a60..e4bae2012 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -215,7 +215,7 @@ let refine_by_tactic env sigma ty tac = (* Support for resolution of evars in tactic interpretation, including resolution by application of tactics *) -let implicit_tactic = ref None +let implicit_tactic = Summary.ref None ~name:"implicit-tactic" let declare_implicit_tactic tac = implicit_tactic := Some tac @@ -230,8 +230,10 @@ let solve_by_implicit_tactic env sigma evk = (Environ.named_context env) -> let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError ("",Pp.str"Proof is not complete."))) []) in (try + let c = Evarutil.nf_evars_universes sigma evi.evar_concl in + if Evarutil.has_undefined_evars sigma c then raise Exit; let (ans, _, _) = - build_by_tactic env (Evd.evar_universe_context sigma) evi.evar_concl tac in + build_by_tactic env (Evd.evar_universe_context sigma) c tac in ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/test-suite/Makefile b/test-suite/Makefile index d779d1f9a..81321729d 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -360,7 +360,7 @@ modules/%.vo: modules/%.v # Miscellaneous tests ####################################################################### -misc: misc/deps-order.log misc/universes.log +misc: misc/deps-order.log misc/universes.log misc/deps-checksum.log # Check that both coqdep and coqtop/coqc supports -R # Check that both coqdep and coqtop/coqc takes the later -R @@ -389,6 +389,26 @@ misc/deps-order.log: rm $$tmpoutput; \ } > "$@" +deps-checksum: misc/deps-checksum.log +misc/deps-checksum.log: + @echo "TEST misc/deps-checksum" + $(HIDE){ \ + echo $(call log_intro,deps-checksum); \ + rm -f misc/deps/*/*.vo; \ + $(bincoqc) -R misc/deps/A A misc/deps/A/A.v; \ + $(bincoqc) -R misc/deps/B A misc/deps/B/A.v; \ + $(bincoqc) -R misc/deps/B A misc/deps/B/B.v; \ + $(coqtop) -R misc/deps/B A -R misc/deps/A A -load-vernac-source misc/deps/checksum.v 2>&1; \ + if [ $$? = 0 ]; then \ + echo $(log_success); \ + echo " misc/deps-checksum...Ok"; \ + else \ + echo $(log_failure); \ + echo " misc/deps-checksum...Error!"; \ + fi; \ + } > "$@" + + # Sort universes for the whole standard library EXPECTED_UNIVERSES := 4 # Prop is not counted universes: misc/universes.log diff --git a/test-suite/bugs/closed/3825.v b/test-suite/bugs/closed/3825.v index e594b74b6..666c64631 100644 --- a/test-suite/bugs/closed/3825.v +++ b/test-suite/bugs/closed/3825.v @@ -14,3 +14,11 @@ Notation qux := (nat -> nat). Fail Check qux@{i}. +Axiom TruncType@{i} : nat -> Type@{i}. + +Notation "n -Type" := (TruncType n) (at level 1) : type_scope. +Notation hProp := (0)-Type. + +Check hProp. +Check hProp@{i}. + diff --git a/test-suite/bugs/closed/4375.v b/test-suite/bugs/closed/4375.v index 03af16535..71e3a7518 100644 --- a/test-suite/bugs/closed/4375.v +++ b/test-suite/bugs/closed/4375.v @@ -93,14 +93,15 @@ Polymorphic CoInductive foo@{i} (T : Type@{i}) : Type@{i} := | A : foo T -> foo T. Polymorphic CoFixpoint cg@{i} (t : Type@{i}) : foo@{i} t := - @A@{i} t (cg@{i} t). + @A@{i} t (cg t). Print cg. Polymorphic CoFixpoint ca@{i} (t : Type@{i}) : foo@{i} t := - @A@{i} t (@cb@{i} t) + @A@{i} t (cb t) with cb@{i} (t : Type@{i}) : foo@{i} t := - @A@{i} t (@ca@{i} t). + @A@{i} t (ca t). Print ca. -Print cb.
\ No newline at end of file +Print cb. +
\ No newline at end of file diff --git a/test-suite/bugs/closed/4882.v b/test-suite/bugs/closed/4882.v new file mode 100644 index 000000000..8c26af708 --- /dev/null +++ b/test-suite/bugs/closed/4882.v @@ -0,0 +1,50 @@ + +Definition Foo {T}{a : T} : T := a. + +Module A. + + Declare Implicit Tactic eauto. + + Goal forall A (x : A), A. + intros. + apply Foo. (* Check defined evars are normalized *) + (* Qed. *) + Abort. + +End A. + +Module B. + + Definition Foo {T}{a : T} : T := a. + + Declare Implicit Tactic eassumption. + + Goal forall A (x : A), A. + intros. + apply Foo. + (* Qed. *) + Abort. + +End B. + +Module C. + + Declare Implicit Tactic first [exact True|assumption]. + + Goal forall (x : True), True. + intros. + apply (@Foo _ _). + Qed. + +End C. + +Module D. + + Declare Implicit Tactic assumption. + + Goal forall A (x : A), A. + intros. + exact _. + Qed. + +End D. diff --git a/test-suite/misc/deps/A/A.v b/test-suite/misc/deps/A/A.v new file mode 100644 index 000000000..49aaf4a79 --- /dev/null +++ b/test-suite/misc/deps/A/A.v @@ -0,0 +1 @@ +Definition b := true. diff --git a/test-suite/misc/deps/B/A.v b/test-suite/misc/deps/B/A.v new file mode 100644 index 000000000..c01a30dca --- /dev/null +++ b/test-suite/misc/deps/B/A.v @@ -0,0 +1 @@ +Definition b := false. diff --git a/test-suite/misc/deps/B/B.v b/test-suite/misc/deps/B/B.v new file mode 100644 index 000000000..f3cda70a9 --- /dev/null +++ b/test-suite/misc/deps/B/B.v @@ -0,0 +1,7 @@ +Require A. + +Definition c := A.b. +Lemma foo : c = false. +Proof. +reflexivity. +Qed. diff --git a/test-suite/misc/deps/checksum.v b/test-suite/misc/deps/checksum.v new file mode 100644 index 000000000..450045e4b --- /dev/null +++ b/test-suite/misc/deps/checksum.v @@ -0,0 +1,2 @@ +Require Import A. +Fail Require Import B. diff --git a/test-suite/success/vm_univ_poly.v b/test-suite/success/vm_univ_poly.v index 58fa39743..62df96c0b 100644 --- a/test-suite/success/vm_univ_poly.v +++ b/test-suite/success/vm_univ_poly.v @@ -38,8 +38,8 @@ Definition _4 : sumbool_copy x = x := (* Polymorphic Inductive Types *) Polymorphic Inductive poption@{i} (T : Type@{i}) : Type@{i} := -| PSome : T -> poption@{i} T -| PNone : poption@{i} T. +| PSome : T -> poption T +| PNone : poption T. Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x : T) : T := match p with @@ -49,7 +49,7 @@ Polymorphic Definition poption_default@{i} {T : Type@{i}} (p : poption@{i} T) (x Polymorphic Inductive plist@{i} (T : Type@{i}) : Type@{i} := | pnil -| pcons : T -> plist@{i} T -> plist@{i} T. +| pcons : T -> plist T -> plist T. Arguments pnil {_}. Arguments pcons {_} _ _. @@ -59,7 +59,7 @@ Polymorphic Definition pmap@{i j} fix pmap (ls : plist@{i} T) : plist@{j} U := match ls with | @pnil _ => @pnil _ - | @pcons _ l ls => @pcons@{j} U (f l) (pmap@{i j} ls) + | @pcons _ l ls => @pcons@{j} U (f l) (pmap ls) end. Universe Ubool. @@ -75,7 +75,7 @@ Eval vm_compute in pmap (fun x => x -> Type) (pcons tbool (pcons (plist tbool) p Polymorphic Inductive Tree@{i} (T : Type@{i}) : Type@{i} := | Empty -| Branch : plist@{i} (Tree@{i} T) -> Tree@{i} T. +| Branch : plist@{i} (Tree T) -> Tree T. Polymorphic Definition pfold@{i u} {T : Type@{i}} {U : Type@{u}} (f : T -> U -> U) := @@ -111,7 +111,7 @@ Polymorphic Fixpoint repeat@{i} {T : Type@{i}} (n : nat@{i}) (v : T) : plist@{i} Polymorphic Fixpoint big_tree@{i} (n : nat@{i}) : Tree@{i} nat@{i} := match n with | O => @Empty nat@{i} - | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree@{i} n')) + | S n' => Branch@{i} nat@{i} (repeat@{i} n' (big_tree n')) end. Eval compute in height (big_tree (S (S (S O)))). |