diff options
| -rw-r--r-- | CHANGES | 29 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 18 |
2 files changed, 32 insertions, 15 deletions
@@ -1,22 +1,39 @@ 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". -- #4097: more efficient occur-check in presence of primitive projections - -Universes: +- #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/tactics/tacintern.ml b/tactics/tacintern.ml index e60bc459b8..11f2c5943d 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: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 @@ -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 ?(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 @@ -454,7 +454,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, [], [] @@ -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 ~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) @@ -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 ?(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 x = |