diff options
Diffstat (limited to 'tactics')
-rw-r--r-- | tactics/auto.ml | 2 | ||||
-rw-r--r-- | tactics/autorewrite.ml | 4 | ||||
-rw-r--r-- | tactics/btermdn.ml | 2 | ||||
-rw-r--r-- | tactics/class_tactics.ml | 6 | ||||
-rw-r--r-- | tactics/eauto.ml | 9 | ||||
-rw-r--r-- | tactics/elimschemes.ml | 4 | ||||
-rw-r--r-- | tactics/eqschemes.ml | 24 | ||||
-rw-r--r-- | tactics/equality.ml | 40 | ||||
-rw-r--r-- | tactics/hints.ml | 64 | ||||
-rw-r--r-- | tactics/hints.mli | 39 | ||||
-rw-r--r-- | tactics/hipattern.ml | 6 | ||||
-rw-r--r-- | tactics/hipattern.mli | 2 | ||||
-rw-r--r-- | tactics/ind_tables.ml | 4 | ||||
-rw-r--r-- | tactics/tacticals.ml | 12 | ||||
-rw-r--r-- | tactics/tacticals.mli | 6 | ||||
-rw-r--r-- | tactics/tactics.ml | 129 | ||||
-rw-r--r-- | tactics/tactics.mli | 9 | ||||
-rw-r--r-- | tactics/term_dnet.ml | 2 |
18 files changed, 186 insertions, 178 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 15a24fb37..77fe31415 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -79,7 +79,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = let clenv, c = if poly then (** Refresh the instance of the hint *) - let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let emap c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in (** Only metas are mentioning the old universes. *) diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index c3857e6b8..0b0e629ab 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -30,7 +30,7 @@ let subst_hint subst hint = let cst' = subst_mps subst hint.rew_lemma in let typ' = subst_mps subst hint.rew_type in let pat' = subst_mps subst hint.rew_pat in - let t' = Option.smartmap (Genintern.generic_substitute subst) hint.rew_tac in + let t' = Option.Smart.map (Genintern.generic_substitute subst) hint.rew_tac in if hint.rew_lemma == cst' && hint.rew_type == typ' && hint.rew_tac == t' then hint else { hint with rew_lemma = cst'; rew_type = typ'; @@ -93,7 +93,7 @@ let one_base general_rewrite_maybe_in tac_main bas = let try_rewrite dir ctx c tc = Proofview.Goal.enter begin fun gl -> let sigma = Proofview.Goal.sigma gl in - let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in + let subst, ctx' = UnivGen.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index 8e50c977e..8f50b0aa2 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -22,7 +22,7 @@ open Globnames let dnet_depth = ref 8 type term_label = -| GRLabel of global_reference +| GRLabel of GlobRef.t | ProdLabel | LambdaLabel | SortLabel diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml index b11e36bce..ea5d4719c 100644 --- a/tactics/class_tactics.ml +++ b/tactics/class_tactics.ml @@ -226,7 +226,7 @@ let unify_resolve_refine poly flags gls ((c, t, ctx),n,clenv) = Refine.refine ~typecheck:false begin fun sigma -> let sigma, term, ty = if poly then - let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in + let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in let map c = Vars.subst_univs_level_constr subst c in let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in sigma, map c, map t @@ -547,9 +547,9 @@ let make_resolve_hyp env sigma st flags only_classes pri decl = (List.map_append (fun (path,info,c) -> let info = - { info with Vernacexpr.hint_pattern = + { info with hint_pattern = Option.map (Constrintern.intern_constr_pattern env sigma) - info.Vernacexpr.hint_pattern } + info.hint_pattern } in make_resolves env sigma ~name:(PathHints path) (true,false,not !Flags.quiet) info false diff --git a/tactics/eauto.ml b/tactics/eauto.ml index dc310c542..3df9e3f82 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -70,11 +70,10 @@ let first_goal gls = (* tactic -> tactic_list : Apply a tactic to the first goal in the list *) let apply_tac_list tac glls = - let (sigr,lg) = unpackage glls in - match lg with + match glls.it with | (g1::rest) -> - let gl = apply_sig_tac sigr tac g1 in - repackage sigr (gl@rest) + let pack = tac (re_sig g1 glls.sigma) in + re_sig (pack.it @ rest) pack.sigma | _ -> user_err Pp.(str "apply_tac_list") let one_step l gl = @@ -90,7 +89,7 @@ let rec prolog l n gl = let out_term env = function | IsConstr (c, _) -> c - | IsGlobRef gr -> EConstr.of_constr (fst (Universes.fresh_global_instance env gr)) + | IsGlobRef gr -> EConstr.of_constr (fst (UnivGen.fresh_global_instance env gr)) let prolog_tac l n = Proofview.V82.tactic begin fun gl -> diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 6bd4866c6..70f73df5c 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -46,8 +46,8 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = mib.mind_nparams in let sigma, sort = Evd.fresh_sort_in_family env sigma sort in let sigma, t', c' = weaken_sort_scheme env sigma false sort npars c t in - let sigma, nf = Evarutil.nf_evars_and_universes sigma in - (nf c', Evd.evar_universe_context sigma), eff + let sigma = Evd.minimize_universes sigma in + (Evarutil.nf_evars_universes sigma c', Evd.evar_universe_context sigma), eff else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 477de6452..715686ad0 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -102,7 +102,7 @@ let get_coq_eq ctx = let eq = Globnames.destIndRef Coqlib.glob_eq in (* Do not force the lazy if they are not defined *) let eq, ctx = with_context_set ctx - (Universes.fresh_inductive_instance (Global.env ()) eq) in + (UnivGen.fresh_inductive_instance (Global.env ()) eq) in mkIndU eq, mkConstructUi (eq,1), ctx with Not_found -> user_err Pp.(str "eq not found.") @@ -192,7 +192,7 @@ let get_non_sym_eq_data env (ind,u) = (**********************************************************************) let build_sym_scheme env ind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n = @@ -241,11 +241,11 @@ let sym_scheme_kind = let const_of_scheme kind env ind ctx = let sym_scheme, eff = (find_scheme kind ind) in let sym, ctx = with_context_set ctx - (Universes.fresh_constant_instance (Global.env()) sym_scheme) in + (UnivGen.fresh_constant_instance (Global.env()) sym_scheme) in mkConstU sym, ctx, eff let build_sym_involutive_scheme env ind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let eq,eqrefl,ctx = get_coq_eq ctx in @@ -353,7 +353,7 @@ let sym_involutive_scheme_kind = (**********************************************************************) let build_l2r_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in @@ -392,7 +392,7 @@ let build_l2r_rew_scheme dep env ind kind = rel_vect (nrealargs+4) nrealargs; rel_vect 1 nrealargs; [|mkRel 1|]]) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -469,7 +469,7 @@ let build_l2r_rew_scheme dep env ind kind = (**********************************************************************) let build_l2r_forward_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 = get_sym_eq_data env indu in let cstr n p = @@ -495,7 +495,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in let realsign_ind_P n aP = name_context env ((LocalAssum (Name varH,aP))::realsign_P n) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -561,7 +561,7 @@ let build_l2r_forward_rew_scheme dep env ind kind = (**********************************************************************) let build_r2l_forward_rew_scheme dep env ind kind = - let (ind,u as indu), ctx = Universes.fresh_inductive_instance env ind in + let (ind,u as indu), ctx = UnivGen.fresh_inductive_instance env ind in let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) = get_non_sym_eq_data env indu in let cstr n = @@ -573,7 +573,7 @@ let build_r2l_forward_rew_scheme dep env ind kind = let applied_ind = build_dependent_inductive indu specif in let realsign_ind = name_context env ((LocalAssum (Name varH,applied_ind))::realsign) in - let s, ctx' = Universes.fresh_sort_in_family (Global.env ()) kind in + let s, ctx' = UnivGen.fresh_sort_in_family (Global.env ()) kind in let ctx = Univ.ContextSet.union ctx ctx' in let s = mkSort s in let ci = make_case_info (Global.env()) ind RegularStyle in @@ -755,7 +755,7 @@ let rew_r2l_scheme_kind = let build_congr env (eq,refl,ctx) ind = let (ind,u as indu), ctx = with_context_set ctx - (Universes.fresh_inductive_instance env ind) in + (UnivGen.fresh_inductive_instance env ind) in let (mib,mip) = lookup_mind_specif env ind in if not (Int.equal (Array.length mib.mind_packets) 1) || not (Int.equal (Array.length mip.mind_nf_lc) 1) then error "Not an inductive type with a single constructor."; @@ -778,7 +778,7 @@ let build_congr env (eq,refl,ctx) ind = let varH = fresh env (Id.of_string "H") in let varf = fresh env (Id.of_string "f") in let ci = make_case_info (Global.env()) ind RegularStyle in - let uni, ctx = Universes.extend_context (Universes.new_global_univ ()) ctx in + let uni, ctx = UnivGen.extend_context (UnivGen.new_global_univ ()) ctx in let ctx = (fst ctx, Univ.enforce_leq uni (univ_of_eq env eq) (snd ctx)) in let c = my_it_mkLambda_or_LetIn paramsctxt diff --git a/tactics/equality.ml b/tactics/equality.ml index b6bbd0be4..8904cd170 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1176,34 +1176,35 @@ let minimal_free_rels_rec env sigma = let sig_clausal_form env sigma sort_of_ty siglen ty dflt = let sigdata = find_sigma_data env sort_of_ty in - let evdref = ref (Evd.clear_metas sigma) in - let rec sigrec_clausal_form siglen p_i = + let rec sigrec_clausal_form sigma siglen p_i = if Int.equal siglen 0 then (* is the default value typable with the expected type *) let dflt_typ = unsafe_type_of env sigma dflt in try - let () = evdref := Evarconv.the_conv_x_leq env dflt_typ p_i !evdref in - let () = - evdref := Evarconv.solve_unif_constraints_with_heuristics env !evdref in - dflt + let sigma = Evarconv.the_conv_x_leq env dflt_typ p_i sigma in + let sigma = + Evarconv.solve_unif_constraints_with_heuristics env sigma in + sigma, dflt with Evarconv.UnableToUnify _ -> user_err Pp.(str "Cannot solve a unification problem.") else - let (a,p_i_minus_1) = match whd_beta_stack !evdref p_i with + let (a,p_i_minus_1) = match whd_beta_stack sigma p_i with | (_sigS,[a;p]) -> (a, p) | _ -> anomaly ~label:"sig_clausal_form" (Pp.str "should be a sigma type.") in - let ev = Evarutil.e_new_evar env evdref a in + let sigma, ev = Evarutil.new_evar env sigma a in let rty = beta_applist sigma (p_i_minus_1,[ev]) in - let tuple_tail = sigrec_clausal_form (siglen-1) rty in - let evopt = match EConstr.kind !evdref ev with Evar _ -> None | _ -> Some ev in + let sigma, tuple_tail = sigrec_clausal_form sigma (siglen-1) rty in + let evopt = match EConstr.kind sigma ev with Evar _ -> None | _ -> Some ev in match evopt with | Some w -> - let w_type = unsafe_type_of env !evdref w in - if Evarconv.e_cumul env evdref w_type a then - let exist_term = Evarutil.evd_comb1 (Evd.fresh_global env) evdref sigdata.intro in - applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) - else + let w_type = unsafe_type_of env sigma w in + begin match Evarconv.cumul env sigma w_type a with + | Some sigma -> + let sigma, exist_term = Evd.fresh_global env sigma sigdata.intro in + sigma, applist(exist_term,[a;p_i_minus_1;w;tuple_tail]) + | None -> user_err Pp.(str "Cannot solve a unification problem.") + end | None -> (* This at least happens if what has been detected as a dependency is not one; use an evasive error message; @@ -1213,8 +1214,9 @@ let sig_clausal_form env sigma sort_of_ty siglen ty dflt = unsolved evars would mean not binding rel *) user_err Pp.(str "Cannot solve a unification problem.") in - let scf = sigrec_clausal_form siglen ty in - !evdref, Evarutil.nf_evar !evdref scf + let sigma = Evd.clear_metas sigma in + let sigma, scf = sigrec_clausal_form sigma siglen ty in + sigma, Evarutil.nf_evar sigma scf (* The problem is to build a destructor (a generalization of the predecessor) which, when applied to a term made of constructors @@ -1779,7 +1781,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in let u = EInstance.kind sigma u in - let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match EConstr.kind sigma x, EConstr.kind sigma y with | Var z, _ when not (is_evaluable env (EvalVarRef z)) -> @@ -1830,7 +1832,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in let u = EInstance.kind sigma u in - let eq = Universes.constr_of_global_univ (lbeq.eq,u) in + let eq = UnivGen.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then failwith "caught"; diff --git a/tactics/hints.ml b/tactics/hints.ml index 46d162911..3ade5314b 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -28,12 +28,13 @@ open Termops open Inductiveops open Typing open Decl_kinds +open Vernacexpr +open Typeclasses open Pattern open Patternops open Clenv open Tacred open Printer -open Vernacexpr module NamedDecl = Context.Named.Declaration @@ -94,7 +95,6 @@ let secvars_of_hyps hyps = else pred let empty_hint_info = - let open Vernacexpr in { hint_priority = None; hint_pattern = None } (************************************************************************) @@ -115,7 +115,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen @@ -126,10 +126,10 @@ type 'a hints_path_gen = | PathEpsilon type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type hints_path = GlobRef.t hints_path_gen type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type 'a with_uid = { @@ -153,7 +153,7 @@ type 'a with_metadata = { type full_hint = hint with_metadata -type hint_entry = global_reference option * +type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata type import_level = [ `LAX | `WARN | `STRICT ] @@ -308,7 +308,7 @@ let instantiate_hint env sigma p = { p with code = { p.code with obj = code } } let hints_path_atom_eq h1 h2 = match h1, h2 with -| PathHints l1, PathHints l2 -> List.equal eq_gr l1 l2 +| PathHints l1, PathHints l2 -> List.equal GlobRef.equal l1 l2 | PathAny, PathAny -> true | _ -> false @@ -365,7 +365,7 @@ let path_seq p p' = let rec path_derivate hp hint = let rec derivate_atoms hints hints' = match hints, hints' with - | gr :: grs, gr' :: grs' when eq_gr gr gr' -> derivate_atoms grs grs' + | gr :: grs, gr' :: grs' when GlobRef.equal gr gr' -> derivate_atoms grs grs' | [], [] -> PathEpsilon | [], hints -> PathEmpty | grs, [] -> PathAtom (PathHints grs) @@ -448,7 +448,7 @@ let subst_path_atom subst p = | PathAny -> p | PathHints grs -> let gr' gr = fst (subst_global subst gr) in - let grs' = List.smartmap gr' grs in + let grs' = List.Smart.map gr' grs in if grs' == grs then p else PathHints grs' let rec subst_hints_path subst hp = @@ -474,28 +474,28 @@ module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t -val find : global_reference -> t -> search_entry +val find : GlobRef.t -> t -> search_entry val map_none : secvars:Id.Pred.t -> t -> full_hint list -val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list +val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list val map_existential : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_eauto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list 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 -> hint_mode array list -> full_hint list -> unit) -> t -> unit +val remove_one : GlobRef.t -> t -> t +val remove_list : GlobRef.t list -> t -> t +val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool val transparent_state : t -> transparent_state val set_transparent_state : t -> transparent_state -> t val add_cut : hints_path -> t -> t -val add_mode : global_reference -> hint_mode array -> t -> t +val add_mode : GlobRef.t -> hint_mode array -> t -> t val cut : t -> hints_path val unfolds : t -> Id.Set.t * Cset.t -val fold : (global_reference option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> +val fold : (GlobRef.t option -> hint_mode array list -> full_hint list -> 'a -> 'a) -> t -> 'a -> 'a end = @@ -510,7 +510,7 @@ struct hintdb_map : search_entry Constr_map.t; (* A list of unindexed entries starting with an unfoldable constant or with no associated pattern. *) - hintdb_nopat : (global_reference option * stored_data) list; + hintdb_nopat : (GlobRef.t option * stored_data) list; hintdb_name : string option; } @@ -654,7 +654,7 @@ struct 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 + let remove_sdl p sdl = List.Smart.filter p sdl let remove_he st p se = let sl1' = remove_sdl p se.sentry_nopat in @@ -664,9 +664,9 @@ struct let remove_list grs db = let filter (_, h) = - match h.name with PathHints [gr] -> not (List.mem_f eq_gr gr grs) | _ -> true in + match h.name with PathHints [gr] -> not (List.mem_f GlobRef.equal gr grs) | _ -> true in let hintmap = Constr_map.map (remove_he db.hintdb_state filter) db.hintdb_map in - let hintnopat = List.smartfilter (fun (ge, sd) -> filter sd) db.hintdb_nopat in + let hintnopat = List.Smart.filter (fun (ge, sd) -> filter sd) db.hintdb_nopat in { db with hintdb_map = hintmap; hintdb_nopat = hintnopat } let remove_one gr db = remove_list [gr] db @@ -876,7 +876,7 @@ let fresh_global_or_constr env sigma poly cr = let isgr, (c, ctx) = match cr with | IsGlobRef gr -> - let (c, ctx) = Universes.fresh_global_instance env gr in + let (c, ctx) = UnivGen.fresh_global_instance env gr in true, (EConstr.of_constr c, ctx) | IsConstr (c, ctx) -> false, (c, ctx) in @@ -1015,9 +1015,9 @@ type hint_action = | CreateDB of bool * transparent_state | AddTransparency of evaluable_global_reference list * bool | AddHints of hint_entry list - | RemoveHints of global_reference list + | RemoveHints of GlobRef.t list | AddCut of hints_path - | AddMode of global_reference * hint_mode array + | AddMode of GlobRef.t * hint_mode array let add_cut dbname path = let db = get_db dbname in @@ -1065,8 +1065,8 @@ let subst_autohint (subst, obj) = in if gr' == gr then gr else gr' in let subst_hint (k,data as hint) = - let k' = Option.smartmap subst_key k in - let pat' = Option.smartmap (subst_pattern subst) data.pat in + let k' = Option.Smart.map subst_key k in + let pat' = Option.Smart.map (subst_pattern subst) data.pat in let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in let code' = match data.code.obj with | Res_pf (c,t,ctx) -> @@ -1104,13 +1104,13 @@ let subst_autohint (subst, obj) = let action = match obj.hint_action with | CreateDB _ -> obj.hint_action | AddTransparency (grs, b) -> - let grs' = List.smartmap (subst_evaluable_reference subst) grs in + let grs' = List.Smart.map (subst_evaluable_reference subst) grs in if grs == grs' then obj.hint_action else AddTransparency (grs', b) | AddHints hintlist -> - let hintlist' = List.smartmap subst_hint hintlist in + let hintlist' = List.Smart.map subst_hint hintlist in if hintlist' == hintlist then obj.hint_action else AddHints hintlist' | RemoveHints grs -> - let grs' = List.smartmap (subst_global_reference subst) grs in + let grs' = List.Smart.map (subst_global_reference subst) grs in if grs == grs' then obj.hint_action else RemoveHints grs' | AddCut path -> let path' = subst_hints_path subst path in @@ -1226,7 +1226,7 @@ type hints_entry = | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * hint_mode list + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument let default_prepare_hint_ident = Id.of_string "H" diff --git a/tactics/hints.mli b/tactics/hints.mli index 1811150c2..c7de10a2a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -12,7 +12,6 @@ open Util open Names open EConstr open Environ -open Globnames open Decl_kinds open Evd open Misctypes @@ -25,13 +24,13 @@ open Vernacexpr exception Bound -val decompose_app_bound : evar_map -> constr -> global_reference * constr array +val decompose_app_bound : evar_map -> constr -> GlobRef.t * constr array type debug = Debug | Info | Off val secvars_of_hyps : ('c, 't) Context.Named.pt -> Id.Pred.t -val empty_hint_info : 'a hint_info_gen +val empty_hint_info : 'a Typeclasses.hint_info_gen (** Pre-created hint databases *) @@ -51,7 +50,7 @@ type 'a hints_path_atom_gen = (* For forward hints, their names is the list of projections *) | PathAny -type hints_path_atom = global_reference hints_path_atom_gen +type hints_path_atom = GlobRef.t hints_path_atom_gen type hint_db_name = string type 'a with_metadata = private { @@ -81,7 +80,7 @@ type 'a hints_path_gen = | PathEpsilon type pre_hints_path = Libnames.reference hints_path_gen -type hints_path = global_reference hints_path_gen +type hints_path = GlobRef.t hints_path_gen val normalize_path : hints_path -> hints_path val path_matches : hints_path -> hints_path_atom list -> bool @@ -91,15 +90,15 @@ val pp_hints_path_atom : ('a -> Pp.t) -> 'a hints_path_atom_gen -> Pp.t val pp_hints_path : hints_path -> Pp.t val pp_hint_mode : hint_mode -> Pp.t val glob_hints_path_atom : - Libnames.reference hints_path_atom_gen -> Globnames.global_reference hints_path_atom_gen + Libnames.reference hints_path_atom_gen -> GlobRef.t hints_path_atom_gen val glob_hints_path : - Libnames.reference hints_path_gen -> Globnames.global_reference hints_path_gen + Libnames.reference hints_path_gen -> GlobRef.t hints_path_gen module Hint_db : sig type t val empty : ?name:hint_db_name -> transparent_state -> bool -> t - val find : global_reference -> t -> search_entry + val find : GlobRef.t -> t -> search_entry (** All hints which have no pattern. * [secvars] represent the set of section variables that @@ -107,27 +106,27 @@ module Hint_db : val map_none : secvars:Id.Pred.t -> t -> full_hint list (** All hints associated to the reference *) - val map_all : secvars:Id.Pred.t -> global_reference -> t -> full_hint list + val map_all : secvars:Id.Pred.t -> GlobRef.t -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments, _not_ using the discrimination net. *) val map_existential : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments and using the discrimination net. *) - val map_eauto : evar_map -> secvars:Id.Pred.t -> (global_reference * constr array) -> constr -> t -> full_hint list + val map_eauto : evar_map -> secvars:Id.Pred.t -> (GlobRef.t * constr array) -> constr -> t -> full_hint list (** All hints associated to the reference, respecting modes if evars appear in the arguments. *) val map_auto : evar_map -> secvars:Id.Pred.t -> - (global_reference * constr array) -> constr -> t -> full_hint list + (GlobRef.t * constr array) -> constr -> t -> full_hint list 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 -> + val remove_one : GlobRef.t -> t -> t + val remove_list : GlobRef.t list -> t -> t + val iter : (GlobRef.t option -> hint_mode array list -> full_hint list -> unit) -> t -> unit val use_dn : t -> bool @@ -144,10 +143,10 @@ type hint_db = Hint_db.t type hnf = bool -type hint_info = (patvar list * constr_pattern) hint_info_gen +type hint_info = (patvar list * constr_pattern) Typeclasses.hint_info_gen type hint_term = - | IsGlobRef of global_reference + | IsGlobRef of GlobRef.t | IsConstr of constr * Univ.ContextSet.t type hints_entry = @@ -157,7 +156,7 @@ type hints_entry = | HintsCutEntry of hints_path | HintsUnfoldEntry of evaluable_global_reference list | HintsTransparencyEntry of evaluable_global_reference list * bool - | HintsModeEntry of global_reference * hint_mode list + | HintsModeEntry of GlobRef.t * hint_mode list | HintsExternEntry of hint_info * Genarg.glob_generic_argument val searchtable_map : hint_db_name -> hint_db @@ -171,7 +170,7 @@ val searchtable_add : (hint_db_name * hint_db) -> unit val create_hint_db : bool -> hint_db_name -> transparent_state -> bool -> unit -val remove_hints : bool -> hint_db_name list -> global_reference list -> unit +val remove_hints : bool -> hint_db_name list -> GlobRef.t list -> unit val current_db_names : unit -> String.Set.t @@ -264,7 +263,7 @@ val rewrite_db : hint_db_name val pr_searchtable : env -> evar_map -> Pp.t val pr_applicable_hint : unit -> Pp.t -val pr_hint_ref : env -> evar_map -> global_reference -> Pp.t +val pr_hint_ref : env -> evar_map -> GlobRef.t -> Pp.t val pr_hint_db_by_name : env -> evar_map -> hint_db_name -> Pp.t val pr_hint_db_env : env -> evar_map -> Hint_db.t -> Pp.t val pr_hint_db : Hint_db.t -> Pp.t diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index b012a7ecd..b8f1ed720 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -294,13 +294,13 @@ let match_with_equation env sigma t = let (hdapp,args) = destApp sigma t in match EConstr.kind sigma hdapp with | Ind (ind,u) -> - if eq_gr (IndRef ind) glob_eq then + if GlobRef.equal (IndRef ind) glob_eq then Some (build_coq_eq_data()),hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if eq_gr (IndRef ind) glob_identity then + else if GlobRef.equal (IndRef ind) glob_identity then Some (build_coq_identity_data()),hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if eq_gr (IndRef ind) glob_jmeq then + else if GlobRef.equal (IndRef ind) glob_jmeq then Some (build_coq_jmeq_data()),hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 0697d0f19..f04cda123 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -144,7 +144,7 @@ val is_matching_sigma : Environ.env -> evar_map -> constr -> bool (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) -val match_eqdec : Environ.env -> evar_map -> constr -> bool * Globnames.global_reference * constr * constr * constr +val match_eqdec : Environ.env -> evar_map -> constr -> bool * GlobRef.t * constr * constr * constr (** Match a negation *) val is_matching_not : Environ.env -> evar_map -> constr -> bool diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 62ead57f3..21520f5d2 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -53,7 +53,7 @@ let subst_one_scheme subst (ind,const) = (subst_ind subst ind,subst_constant subst const) let subst_scheme (subst,(kind,l)) = - (kind,Array.map (subst_one_scheme subst) l) + (kind,Array.Smart.map (subst_one_scheme subst) l) let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> @@ -123,7 +123,7 @@ let define internal id c p univs = let fd = declare_constant ~internal in let id = compute_name internal id in let ctx = UState.minimize univs in - let c = Universes.subst_opt_univs_constr (UState.subst ctx) c in + let c = UnivSubst.nf_evars_and_universes_opt_subst (fun _ -> None) (UState.subst ctx) c in let univs = if p then Polymorphic_const_entry (UState.context ctx) else Monomorphic_const_entry (UState.context_set ctx) diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 5e81e2d4b..6c7db26c7 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -492,11 +492,13 @@ module New = struct Proofview.tclINDEPENDENT (Proofview.tclPROGRESS t) (* Select a subset of the goals *) - let tclSELECT = function - | Vernacexpr.SelectNth i -> Proofview.tclFOCUS i i - | Vernacexpr.SelectList l -> Proofview.tclFOCUSLIST l - | Vernacexpr.SelectId id -> Proofview.tclFOCUSID id - | Vernacexpr.SelectAll -> fun tac -> tac + let tclSELECT = let open Goal_select in function + | SelectNth i -> Proofview.tclFOCUS i i + | SelectList l -> Proofview.tclFOCUSLIST l + | SelectId id -> Proofview.tclFOCUSID id + | SelectAll -> anomaly ~label:"tclSELECT" Pp.(str "SelectAll not allowed here") + | SelectAlreadyFocused -> + anomaly ~label:"tclSELECT" Pp.(str "SelectAlreadyFocused not allowed here") (* Check that holes in arguments have been resolved *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 340d8fbf3..cbaf691f1 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -135,7 +135,7 @@ val elimination_sort_of_hyp : Id.t -> goal sigma -> Sorts.family val elimination_sort_of_clause : Id.t option -> goal sigma -> Sorts.family val pf_with_evars : (goal sigma -> Evd.evar_map * 'a) -> ('a -> tactic) -> tactic -val pf_constr_of_global : Globnames.global_reference -> (constr -> tactic) -> tactic +val pf_constr_of_global : GlobRef.t -> (constr -> tactic) -> tactic (** Tacticals defined directly in term of Proofview *) @@ -223,7 +223,7 @@ module New : sig val tclCOMPLETE : 'a tactic -> 'a tactic val tclSOLVE : unit tactic list -> unit tactic val tclPROGRESS : unit tactic -> unit tactic - val tclSELECT : Vernacexpr.goal_selector -> 'a tactic -> 'a tactic + val tclSELECT : Goal_select.t -> 'a tactic -> 'a tactic val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic val tclDELAYEDWITHHOLES : bool -> 'a delayed_open -> ('a -> unit tactic) -> unit tactic @@ -268,5 +268,5 @@ module New : sig val elim_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic val case_on_ba : (branch_assumptions -> unit Proofview.tactic) -> branch_args -> unit Proofview.tactic - val pf_constr_of_global : Globnames.global_reference -> constr Proofview.tactic + val pf_constr_of_global : GlobRef.t -> constr Proofview.tactic end diff --git a/tactics/tactics.ml b/tactics/tactics.ml index aae4bc088..a42e4b44b 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -198,32 +198,40 @@ end let convert x y = convert_gen Reduction.CONV x y let convert_leq x y = convert_gen Reduction.CUMUL x y -let clear_dependency_msg env sigma id = function +let clear_in_global_msg = function + | None -> mt () + | Some ref -> str " implicitly in " ++ Printer.pr_global ref + +let clear_dependency_msg env sigma id err inglobal = + let pp = clear_in_global_msg inglobal in + match err with | Evarutil.OccurHypInSimpleClause None -> - Id.print id ++ str " is used in conclusion." + Id.print id ++ str " is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> - Id.print id ++ strbrk " is used in hypothesis " ++ Id.print id' ++ str"." + Id.print id ++ strbrk " is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> str "Cannot remove " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." -let error_clear_dependency env sigma id err = - user_err (clear_dependency_msg env sigma id err) +let error_clear_dependency env sigma id err inglobal = + user_err (clear_dependency_msg env sigma id err inglobal) -let replacing_dependency_msg env sigma id = function +let replacing_dependency_msg env sigma id err inglobal = + let pp = clear_in_global_msg inglobal in + match err with | Evarutil.OccurHypInSimpleClause None -> - str "Cannot change " ++ Id.print id ++ str ", it is used in conclusion." + str "Cannot change " ++ Id.print id ++ str ", it is used" ++ pp ++ str " in conclusion." | Evarutil.OccurHypInSimpleClause (Some id') -> str "Cannot change " ++ Id.print id ++ - strbrk ", it is used in hypothesis " ++ Id.print id' ++ str"." + strbrk ", it is used" ++ pp ++ str " in hypothesis " ++ Id.print id' ++ str"." | Evarutil.EvarTypingBreak ev -> str "Cannot change " ++ Id.print id ++ strbrk " without breaking the typing of " ++ Printer.pr_existential env sigma ev ++ str"." -let error_replacing_dependency env sigma id err = - user_err (replacing_dependency_msg env sigma id err) +let error_replacing_dependency env sigma id err inglobal = + user_err (replacing_dependency_msg env sigma id err inglobal) (* This tactic enables the user to remove hypotheses from the signature. * Some care is taken to prevent him from removing variables that are @@ -239,13 +247,12 @@ let clear_gen fail = function let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let concl = Proofview.Goal.concl gl in - let evdref = ref sigma in - let (hyps, concl) = - try clear_hyps_in_evi env evdref (named_context_val env) concl ids - with Evarutil.ClearDependencyError (id,err) -> fail env sigma id err + let (sigma, hyps, concl) = + try clear_hyps_in_evi env sigma (named_context_val env) concl ids + with Evarutil.ClearDependencyError (id,err,inglobal) -> fail env sigma id err inglobal in let env = reset_with_named_context hyps env in - Proofview.tclTHEN (Proofview.Unsafe.tclEVARS !evdref) + Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun sigma -> Evarutil.new_evar env sigma ~principal:true concl end) @@ -423,11 +430,10 @@ let get_previous_hyp_position env sigma id = let clear_hyps2 env sigma ids sign t cl = try - let evdref = ref (Evd.clear_metas sigma) in - let (hyps,t,cl) = Evarutil.clear_hyps2_in_evi env evdref sign t cl ids in - (hyps, t, cl, !evdref) - with Evarutil.ClearDependencyError (id,err) -> - error_replacing_dependency env sigma id err + let sigma = Evd.clear_metas sigma in + Evarutil.clear_hyps2_in_evi env sigma sign t cl ids + with Evarutil.ClearDependencyError (id,err,inglobal) -> + error_replacing_dependency env sigma id err inglobal let internal_cut_gen ?(check=true) dir replace id t = Proofview.Goal.enter begin fun gl -> @@ -439,7 +445,7 @@ let internal_cut_gen ?(check=true) dir replace id t = let sign',t,concl,sigma = if replace then let nexthyp = get_next_hyp_position env sigma id (named_context_of_val sign) in - let sign',t,concl,sigma = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in + let sigma,sign',t,concl = clear_hyps2 env sigma (Id.Set.singleton id) sign t concl in let sign' = insert_decl_in_named_context sigma (LocalAssum (id,t)) nexthyp sign' in sign',t,concl,sigma else @@ -557,20 +563,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> end end -let warning_nameless_fix = - CWarnings.create ~name:"nameless-fix" ~category:"deprecated" Pp.(fun () -> - str "fix/cofix without a name are deprecated, please use the named version.") - -let fix ido n = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_fix id n [] 0 - end - | Some id -> - mutual_fix id n [] 0 +let fix id n = mutual_fix id n [] 0 let rec check_is_mutcoind env sigma cl = let b = whd_all env sigma cl in @@ -613,16 +606,7 @@ let mutual_cofix f others j = Proofview.Goal.enter begin fun gl -> end end -let cofix ido = match ido with - | None -> - warning_nameless_fix (); - Proofview.Goal.enter begin fun gl -> - let name = Proof_global.get_current_proof_name () in - let id = new_fresh_id Id.Set.empty name gl in - mutual_cofix id [] 0 - end - | Some id -> - mutual_cofix id [] 0 +let cofix id = mutual_cofix id [] 0 (**************************************************************) (* Reduction and conversion tactics *) @@ -971,6 +955,11 @@ let rec intro_then_gen name_flag move_flag force_flag dep_flag tac = | LetIn (name,b,t,u) when not dep_flag || not (noccurn sigma 1 u) -> let name = find_name false (LocalDef (name,b,t)) name_flag gl in build_intro_tac name move_flag tac + | Evar ev when force_flag -> + let sigma, t = Evardefine.define_evar_as_product sigma ev in + Tacticals.New.tclTHEN + (Proofview.Unsafe.tclEVARS sigma) + (intro_then_gen name_flag move_flag force_flag dep_flag tac) | _ -> begin if not force_flag then Proofview.tclZERO (RefinerError (env, sigma, IntroNeedsProduct)) (* Note: red_in_concl includes betaiotazeta and this was like *) @@ -1974,24 +1963,22 @@ let on_the_bodies = function exception DependsOnBody of Id.t option let check_is_type env sigma ty = - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - !evdref + let sigma, _ = Typing.sort_of env sigma ty in + sigma with e when CErrors.noncritical e -> raise (DependsOnBody None) let check_decl env sigma decl = let open Context.Named.Declaration in let ty = NamedDecl.get_type decl in - let evdref = ref sigma in try - let _ = Typing.e_sort_of env evdref ty in - let _ = match decl with - | LocalAssum _ -> () - | LocalDef (_,c,_) -> Typing.e_check env evdref c ty + let sigma, _ = Typing.sort_of env sigma ty in + let sigma = match decl with + | LocalAssum _ -> sigma + | LocalDef (_,c,_) -> Typing.check env sigma c ty in - !evdref + sigma with e when CErrors.noncritical e -> let id = NamedDecl.get_id decl in raise (DependsOnBody (Some id)) @@ -3007,8 +2994,24 @@ let unfold_body x = end end +let warn_cannot_remove_as_expected = + CWarnings.create ~name:"cannot-remove-as-expected" ~category:"tactics" + (fun (id,inglobal) -> + let pp = match inglobal with + | None -> mt () + | Some ref -> str ", it is used implicitly in " ++ Printer.pr_global ref in + str "Cannot remove " ++ Id.print id ++ pp ++ str ".") + +let clear_for_destruct ids = + Proofview.tclORELSE + (clear_gen (fun env sigma id err inglobal -> raise (ClearDependencyError (id,err,inglobal))) ids) + (function + | ClearDependencyError (id,err,inglobal),_ -> warn_cannot_remove_as_expected (id,inglobal); Proofview.tclUNIT () + | e -> iraise e) + (* Either unfold and clear if defined or simply clear if not a definition *) -let expand_hyp id = Tacticals.New.tclTRY (unfold_body id) <*> clear [id] +let expand_hyp id = + Tacticals.New.tclTRY (unfold_body id) <*> clear_for_destruct [id] (*****************************) (* High-level induction *) @@ -3424,7 +3427,7 @@ let cook_sign hyp0_opt inhyps indvars env sigma = type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; params: rel_context; (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (* number of parameters *) predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) @@ -3786,7 +3789,10 @@ let specialize_eqs id = let ty = Tacmach.New.pf_get_hyp_typ id gl in let evars = ref (Proofview.Goal.sigma gl) in let unif env evars c1 c2 = - compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2 + compare_upto_variables !evars c1 c2 && + (match Evarconv.conv env !evars c1 c2 with + | Some sigma -> evars := sigma; true + | None -> false) in let rec aux in_eqs ctx acc ty = match EConstr.kind !evars ty with @@ -3811,7 +3817,8 @@ let specialize_eqs id = | _ -> if in_eqs then acc, in_eqs, ctx, ty else - let e = e_new_evar (push_rel_context ctx env) evars t in + let sigma, e = Evarutil.new_evar (push_rel_context ctx env) !evars t in + evars := sigma; aux false (LocalDef (na,e,t) :: ctx) (mkApp (lift 1 acc, [| mkRel 1 |])) b) | t -> acc, in_eqs, ctx, ty in @@ -4338,7 +4345,7 @@ let check_expected_type env sigma (elimc,bl) elimt = let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in let (_,u,_) = destProd sigma cl.cl_concl in - fun t -> Evarconv.e_cumul env (ref sigma) t u + fun t -> Option.has_some (Evarconv.cumul env sigma t u) let check_enough_applied env sigma elim = (* A heuristic to decide whether the induction arg is enough applied *) @@ -4929,9 +4936,9 @@ let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let evd, ctx, concl = (* FIXME: should be done only if the tactic succeeds *) - let evd, nf = nf_evars_and_universes !evdref in + let evd = Evd.minimize_universes !evdref in let ctx = Evd.universe_context_set evd in - evd, ctx, nf concl + evd, ctx, Evarutil.nf_evars_universes evd concl in let concl = EConstr.of_constr concl in let solve_tac = tclCOMPLETE (tclTHEN (tclDO (List.length sign) intro) tac) in diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 7809dbf48..ddf78b1d4 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -16,7 +16,6 @@ open Proof_type open Evd open Clenv open Redexpr -open Globnames open Pattern open Unification open Misctypes @@ -42,9 +41,9 @@ val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic val convert_hyp_no_check : named_declaration -> unit Proofview.tactic val mutual_fix : Id.t -> int -> (Id.t * int * constr) list -> int -> unit Proofview.tactic -val fix : Id.t option -> int -> unit Proofview.tactic +val fix : Id.t -> int -> unit Proofview.tactic val mutual_cofix : Id.t -> (Id.t * constr) list -> int -> unit Proofview.tactic -val cofix : Id.t option -> unit Proofview.tactic +val cofix : Id.t -> unit Proofview.tactic val convert : constr -> constr -> unit Proofview.tactic val convert_leq : constr -> constr -> unit Proofview.tactic @@ -177,7 +176,7 @@ val change : val pattern_option : (occurrences * constr) list -> goal_location -> unit Proofview.tactic val reduce : red_expr -> clause -> unit Proofview.tactic -val unfold_constr : global_reference -> unit Proofview.tactic +val unfold_constr : GlobRef.t -> unit Proofview.tactic (** {6 Modification of the local context. } *) @@ -253,7 +252,7 @@ val apply_delayed_in : type elim_scheme = { elimc: constr with_bindings option; elimt: types; - indref: global_reference option; + indref: GlobRef.t option; params: rel_context; (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *) nparams: int; (** number of parameters *) predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *) diff --git a/tactics/term_dnet.ml b/tactics/term_dnet.ml index 753c608ad..611799990 100644 --- a/tactics/term_dnet.ml +++ b/tactics/term_dnet.ml @@ -37,7 +37,7 @@ struct type 't t = | DRel | DSort - | DRef of global_reference + | DRef of GlobRef.t | DCtx of 't * 't (* (binding list, subterm) = Prods and LetIns *) | DLambda of 't * 't | DApp of 't * 't (* binary app *) |