diff options
| -rw-r--r-- | pretyping/evd.ml | 5 | ||||
| -rw-r--r-- | tactics/auto.ml | 7 | ||||
| -rw-r--r-- | tactics/class_tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/eauto.ml4 | 5 | ||||
| -rw-r--r-- | tactics/hints.ml | 23 | ||||
| -rw-r--r-- | tactics/hints.mli | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4354.v | 10 |
7 files changed, 39 insertions, 21 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 842b87c57e..4e0b6f75e7 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -312,7 +312,10 @@ let union_evar_universe_context ctx ctx' = let names = UNameMap.union (fst ctx.uctx_names) (fst ctx'.uctx_names) in let newus = Univ.LSet.diff (Univ.ContextSet.levels ctx'.uctx_local) (Univ.ContextSet.levels ctx.uctx_local) in - let declarenew g = Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g in + let newus = Univ.LSet.diff newus (Univ.LMap.domain ctx.uctx_univ_variables) in + let declarenew g = + Univ.LSet.fold (fun u g -> Univ.add_universe u false g) newus g + in let names_rev = Univ.LMap.union (snd ctx.uctx_names) (snd ctx'.uctx_names) in { uctx_names = (names, names_rev); uctx_local = local; diff --git a/tactics/auto.ml b/tactics/auto.ml index 72ba9e0bd9..e5fdf6a7c2 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -309,7 +309,8 @@ let rec trivial_fail_db dbg mod_delta db_list local_db = let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in let hyp = Context.map_named_declaration nf decl in let hintl = make_resolve_hyp env sigma hyp - in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db) + in trivial_fail_db dbg mod_delta db_list + (Hint_db.add_list env sigma hintl local_db) end) in Proofview.Goal.enter begin fun gl -> @@ -438,7 +439,9 @@ let possible_resolve dbg mod_delta db_list local_db cl = with Not_found -> [] let extend_local_db decl db gl = - Hint_db.add_list (make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) decl) db + let env = Tacmach.New.pf_env gl in + let sigma = Proofview.Goal.sigma gl in + Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db (* Introduce an hypothesis, then call the continuation tactic [kont] with the hint db extended with the so-obtained hypothesis *) diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index 80f47c680f..ed5b783f6c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -190,7 +190,7 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (Hint_db.add_list hintl local_db) g'))) :: + (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: (List.map (fun (x,_,_,_,_) -> x) (e_trivial_resolve db_list local_db (project goal) (pf_concl goal))) in @@ -339,7 +339,7 @@ let make_hints g st only_classes sign = (PathOr (paths, path), hint @ hints) else (paths, hints)) (PathEmpty, []) sign - in Hint_db.add_list hintlist (Hint_db.empty st true) + in Hint_db.add_list (pf_env g) (project g) hintlist (Hint_db.empty st true) let make_autogoal_hints = let cache = ref (true, Environ.empty_named_context_val, @@ -374,7 +374,7 @@ let intro_tac : atac = let context = Environ.named_context_of_val (Goal.V82.hyps s g') in let hint = make_resolve_hyp env s (Hint_db.transparent_state info.hints) (true,false,false) info.only_classes None (List.hd context) in - let ldb = Hint_db.add_list hint info.hints in + let ldb = Hint_db.add_list env s hint info.hints in (g', { info with is_evar = None; hints = ldb; auto_last_tac = lazy (str"intro") })) gls in {it = gls'; sigma = s;}) diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index 34f87c6cf0..83498cabd8 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -147,7 +147,7 @@ let rec e_trivial_fail_db db_list local_db goal = let d = pf_last_hyp g' in let hintl = make_resolve_hyp (pf_env g') (project g') d in (e_trivial_fail_db db_list - (Hint_db.add_list hintl local_db) g'))) :: + (Hint_db.add_list (pf_env g') (project g') hintl local_db) g'))) :: (List.map fst (e_trivial_resolve db_list local_db (pf_concl goal)) ) in tclFIRST (List.map tclCOMPLETE tacl) goal @@ -269,7 +269,8 @@ module SearchProblem = struct let hintl = make_resolve_hyp (pf_env g') (project g') (pf_last_hyp g') in - let ldb = Hint_db.add_list hintl (List.hd s.localdb) in + let ldb = Hint_db.add_list (pf_env g') (project g') + hintl (List.hd s.localdb) in { depth = s.depth; priority = cost; tacres = lgls; last_tactic = pp; dblist = s.dblist; localdb = ldb :: List.tl s.localdb; prev = ps }) diff --git a/tactics/hints.ml b/tactics/hints.ml index a7eae667d0..dbb2340364 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -266,11 +266,10 @@ let strip_params env c = | _ -> c) | _ -> c -let instantiate_hint p = +let instantiate_hint env sigma p = let mk_clenv c cty ctx = - let env = Global.env () in - let sigma = Evd.merge_context_set univ_flexible (Evd.from_env env) ctx in - let cl = mk_clenv_from_env (Global.env()) sigma None (c,cty) in + let sigma = Evd.merge_context_set univ_flexible sigma ctx in + let cl = mk_clenv_from_env env sigma None (c,cty) in {cl with templval = { cl.templval with rebus = strip_params env cl.templval.rebus }; env = empty_env} @@ -524,8 +523,8 @@ module Hint_db = struct in List.fold_left (fun db (gr,(id,v)) -> addkv gr id v db) db' db.hintdb_nopat - let add_one (k, v) db = - let v = instantiate_hint v in + let add_one env sigma (k, v) db = + let v = instantiate_hint env sigma v in let st',db,rebuild = match v.code.obj with | Unfold_nth egr -> @@ -542,7 +541,7 @@ module Hint_db = struct let db, id = next_hint_id db in addkv k id v db - let add_list l db = List.fold_left (fun db k -> add_one k db) db l + let add_list env sigma l db = List.fold_left (fun db k -> add_one env sigma k db) db l let remove_sdl p sdl = List.smartfilter p sdl @@ -812,7 +811,9 @@ let add_hint dbname hintlist = in let () = List.iter check hintlist in let db = get_db dbname in - let db' = Hint_db.add_list hintlist db in + let env = Global.env () in + let sigma = Evd.from_env env in + let db' = Hint_db.add_list env sigma hintlist db in searchtable_add (dbname,db') let add_transparency dbname grs b = @@ -1166,8 +1167,8 @@ let expand_constructor_hints env sigma lems = let add_hint_lemmas env sigma eapply lems hint_db = let lems = expand_constructor_hints env sigma lems in let hintlist' = - List.map_append (make_resolves env sigma (eapply,true,false) None true) lems in - Hint_db.add_list hintlist' hint_db + List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in + Hint_db.add_list env sigma hintlist' hint_db let make_local_hint_db env sigma ts eapply lems = let sign = Environ.named_context env in @@ -1177,7 +1178,7 @@ let make_local_hint_db env sigma ts eapply lems = in let hintlist = List.map_append (make_resolve_hyp env sigma) sign in add_hint_lemmas env sigma eapply lems - (Hint_db.add_list hintlist (Hint_db.empty ts false)) + (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false)) let make_local_hint_db = if Flags.profile then diff --git a/tactics/hints.mli b/tactics/hints.mli index 687bc78c76..5a4fb77091 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -93,8 +93,8 @@ module Hint_db : arguments. *) val map_auto : (global_reference * constr array) -> constr -> t -> full_hint list - val add_one : hint_entry -> t -> t - val add_list : (hint_entry) list -> t -> t + val add_one : env -> evar_map -> hint_entry -> t -> t + val add_list : env -> evar_map -> hint_entry list -> t -> t val remove_one : global_reference -> t -> t val remove_list : global_reference list -> t -> t val iter : (global_reference option -> bool array list -> full_hint list -> unit) -> t -> unit diff --git a/test-suite/bugs/closed/4354.v b/test-suite/bugs/closed/4354.v new file mode 100644 index 0000000000..6a2f9672d3 --- /dev/null +++ b/test-suite/bugs/closed/4354.v @@ -0,0 +1,10 @@ +Inductive True : Prop := I. +Class Lift (T : Type). +Axiom closed_increment : forall {T} {H : Lift T}, True. +Create HintDb core. +Lemma closed_monotonic T (H : Lift T) : True. + auto using closed_increment. Show Universes. +Qed. + +(* also fails with -nois, so the content of the hint database does not matter +*)
\ No newline at end of file |