From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- plugins/ssr/ssrcommon.ml | 43 ++++++++++++++++++++++--------------------- 1 file changed, 22 insertions(+), 21 deletions(-) (limited to 'plugins/ssr/ssrcommon.ml') diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml index 82cae439..c94039a6 100644 --- a/plugins/ssr/ssrcommon.ml +++ b/plugins/ssr/ssrcommon.ml @@ -181,10 +181,9 @@ let option_assert_get o msg = (** Constructors for rawconstr *) open Glob_term open Globnames -open Misctypes open Decl_kinds -let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None) +let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, Namegen.IntroAnonymous, None) let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else [] let rec isRHoles cl = match cl with @@ -254,7 +253,7 @@ let interp_refine ist gl rc = let interp_open_constr ist gl gc = - let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Misctypes.NoBindings) in + let (sigma, (c, _)) = Tacinterp.interp_open_constr_with_bindings ist (pf_env gl) (project gl) (gc, Tactypes.NoBindings) in (project gl, (sigma, c)) let interp_term ist gl (_, c) = snd (interp_open_constr ist gl c) @@ -423,12 +422,12 @@ let mk_anon_id t gl_ids = (set s i (Char.chr (Char.code (get s i) + 1)); s) in Id.of_bytes (loop (n - 1)) -let convert_concl_no_check t = Tactics.convert_concl_no_check t Term.DEFAULTcast -let convert_concl t = Tactics.convert_concl t Term.DEFAULTcast +let convert_concl_no_check t = Tactics.convert_concl_no_check t DEFAULTcast +let convert_concl t = Tactics.convert_concl t DEFAULTcast let rename_hd_prod orig_name_ref gl = match EConstr.kind (project gl) (pf_concl gl) with - | Term.Prod(_,src,tgt) -> + | Prod(_,src,tgt) -> Proofview.V82.of_tactic (convert_concl_no_check (EConstr.mkProd (!orig_name_ref,src,tgt))) gl | _ -> CErrors.anomaly (str "gentac creates no product") @@ -504,16 +503,17 @@ let nf_evar sigma t = EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t)) let pf_abs_evars2 gl rigid (sigma, c0) = - let c0 = EConstr.to_constr sigma c0 in + let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in let sigma0, ucst = project gl, Evd.evar_universe_context sigma in let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in - let dc = CList.firstn n (evar_filtered_context evi) in + let concl = EConstr.Unsafe.to_constr evi.evar_concl in + let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in - let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in + let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma t in let rec put evlist c = match Constr.kind c with | Evar (k, a) -> @@ -569,11 +569,12 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let nenv = env_size (pf_env gl) in let abs_evar n k = let evi = Evd.find sigma k in - let dc = CList.firstn n (evar_filtered_context evi) in + let concl = EConstr.Unsafe.to_constr evi.evar_concl in + let dc = EConstr.Unsafe.to_named_context (CList.firstn n (evar_filtered_context evi)) in let abs_dc c = function | NamedDecl.LocalDef (x,b,t) -> mkNamedLetIn x b t (mkArrow t c) | NamedDecl.LocalAssum (x,t) -> mkNamedProd x t c in - let t = Context.Named.fold_inside abs_dc ~init:evi.evar_concl dc in + let t = Context.Named.fold_inside abs_dc ~init:concl dc in nf_evar sigma0 (nf_evar sigma t) in let rec put evlist c = match Constr.kind c with | Evar (k, a) -> @@ -581,7 +582,7 @@ let pf_abs_evars_pirrel gl (sigma, c0) = let n = max 0 (Array.length a - nenv) in let k_ty = Retyping.get_sort_family_of - (pf_env gl) sigma (EConstr.of_constr (Evd.evar_concl (Evd.find sigma k))) in + (pf_env gl) sigma (Evd.evar_concl (Evd.find sigma k)) in let is_prop = k_ty = InProp in let t = abs_evar n k in (k, (n, t, is_prop)) :: put evlist t | _ -> Constr.fold put evlist c in @@ -746,7 +747,7 @@ let pf_mkSsrConst name gl = let pf_fresh_global name gl = let sigma, env, it = project gl, pf_env gl, sig_it gl in let sigma,t = Evd.fresh_global env sigma name in - t, re_sig it sigma + EConstr.Unsafe.to_constr t, re_sig it sigma let mkProt t c gl = let prot, gl = pf_mkSsrConst "protect_term" gl in @@ -802,7 +803,7 @@ let rec is_name_in_ipats name = function | IPatId id :: tl -> id = name || is_name_in_ipats name tl | IPatAbstractVars ids :: tl -> CList.mem_f Id.equal name ids || is_name_in_ipats name tl - | (IPatCase l | IPatDispatch l | IPatInj l) :: tl -> + | (IPatCase l | IPatDispatch (_,l) | IPatInj l) :: tl -> List.exists (is_name_in_ipats name) l || is_name_in_ipats name tl | (IPatView _ | IPatAnon _ | IPatSimpl _ | IPatRewrite _ | IPatTac _ | IPatNoop) :: tl -> is_name_in_ipats name tl | [] -> false @@ -857,10 +858,10 @@ open Util (** Constructors for constr_expr *) let mkCProp loc = CAst.make ?loc @@ CSort GProp let mkCType loc = CAst.make ?loc @@ CSort (GType []) -let mkCVar ?loc id = CAst.make ?loc @@ CRef (CAst.make ?loc @@ Ident id, None) +let mkCVar ?loc id = CAst.make ?loc @@ CRef (qualid_of_ident ?loc id, None) let rec mkCHoles ?loc n = - if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) -let mkCHole loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None) + if n <= 0 then [] else (CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None)) :: mkCHoles ?loc (n - 1) +let mkCHole loc = CAst.make ?loc @@ CHole (None, Namegen.IntroAnonymous, None) let mkCLambda ?loc name ty t = CAst.make ?loc @@ CLambdaN ([CLocalAssum([CAst.make ?loc name], Default Explicit, ty)], t) let mkCArrow ?loc ty t = CAst.make ?loc @@ @@ -983,7 +984,7 @@ let applyn ~with_evars ?beta ?(with_shelve=false) n t gl = if not (EConstr.Vars.closed0 sigma ty) then raise dependent_apply_error; let m = Evarutil.new_meta () in - loop (meta_declare m (EConstr.Unsafe.to_constr ty) sigma) bo ((EConstr.mkMeta m)::args) (n-1) + loop (meta_declare m ty sigma) bo ((EConstr.mkMeta m)::args) (n-1) | _ -> assert false in loop sigma t [] n in pp(lazy(str"Refiner.refiner " ++ Printer.pr_econstr_env (pf_env gl) (project gl) t)); @@ -1219,7 +1220,7 @@ let genclrtac cl cs clr = (fun type_err gl -> tclTHEN (tclTHEN (Proofview.V82.of_tactic (Tactics.elim_type (EConstr.of_constr - (Universes.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) + (UnivGen.constr_of_global @@ Coqlib.build_coq_False ())))) (old_cleartac clr)) (fun gl -> raise type_err) gl)) (old_cleartac clr) @@ -1444,7 +1445,7 @@ let tclINTRO_ANON = tclINTRO ~id:None ~conclusion:return let tclRENAME_HD_PROD name = Goal.enter begin fun gl -> let convert_concl_no_check t = - Tactics.convert_concl_no_check t Term.DEFAULTcast in + Tactics.convert_concl_no_check t DEFAULTcast in let concl = Goal.concl gl in let sigma = Goal.sigma gl in match EConstr.kind sigma concl with @@ -1503,7 +1504,7 @@ let tclOPTION o d = let tacIS_INJECTION_CASE ?ty t = begin tclOPTION ty (tacTYPEOF t) >>= fun ty -> tacREDUCE_TO_QUANTIFIED_IND ty >>= fun ((mind,_),_) -> - tclUNIT (Globnames.eq_gr (Globnames.IndRef mind) (Coqlib.build_coq_eq ())) + tclUNIT (GlobRef.equal (GlobRef.IndRef mind) (Coqlib.build_coq_eq ())) end let tclWITHTOP tac = Goal.enter begin fun gl -> -- cgit v1.2.3