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 --- vernac/auto_ind_decl.ml | 54 ++++++++++++++++++++++++------------------------- 1 file changed, 27 insertions(+), 27 deletions(-) (limited to 'vernac/auto_ind_decl.ml') diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 0404d015..3bf3925b 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -24,7 +24,8 @@ open Globnames open Inductiveops open Tactics open Ind_tables -open Misctypes +open Namegen +open Tactypes open Proofview.Notations module RelDecl = Context.Rel.Declaration @@ -54,20 +55,20 @@ exception EqUnknown of string exception UndefinedCst of string exception InductiveWithProduct exception InductiveWithSort -exception ParameterWithoutEquality of global_reference +exception ParameterWithoutEquality of GlobRef.t exception NonSingletonProp of inductive exception DecidabilityMutualNotSupported exception NoDecidabilityCoInductive -let constr_of_global g = lazy (Universes.constr_of_global g) +let constr_of_global g = lazy (UnivGen.constr_of_global g) (* Some pre declaration of constant we are going to use *) let bb = constr_of_global Coqlib.glob_bool -let andb_prop = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop +let andb_prop = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_prop let andb_true_intro = fun _ -> - Universes.constr_of_global + UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb_true_intro let tt = constr_of_global Coqlib.glob_true @@ -76,9 +77,9 @@ let ff = constr_of_global Coqlib.glob_false let eq = constr_of_global Coqlib.glob_eq -let sumbool () = Universes.constr_of_global (Coqlib.build_coq_sumbool ()) +let sumbool () = UnivGen.constr_of_global (Coqlib.build_coq_sumbool ()) -let andb = fun _ -> Universes.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb +let andb = fun _ -> UnivGen.constr_of_global (Coqlib.build_bool_type()).Coqlib.andb let induct_on c = induction false None c None None @@ -186,10 +187,10 @@ let build_beq_scheme mode kn = *) let compute_A_equality rel_list nlist eqA ndx t = let lifti = ndx in - let sigma = Evd.empty (** FIXME *) in let rec aux c = - let (c,a) = Reductionops.whd_betaiota_stack Evd.empty c in - match EConstr.kind sigma c with + let (c,a) = Reductionops.whd_betaiota_stack Evd.empty EConstr.(of_constr c) in + let (c,a) = EConstr.Unsafe.(to_constr c, List.map to_constr a) in + match Constr.kind c with | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants | Var x -> let eid = Id.of_string ("eq_"^(Id.to_string x)) in @@ -198,7 +199,7 @@ let build_beq_scheme mode kn = with Not_found -> raise (ParameterWithoutEquality (VarRef x)) in mkVar eid, Safe_typing.empty_private_constants - | Cast (x,_,_) -> aux (EConstr.applist (x,a)) + | Cast (x,_,_) -> aux (Term.applist (x,a)) | App _ -> assert false | Ind ((kn',i as ind'),u) (*FIXME: universes *) -> if MutInd.equal kn kn' then mkRel(eqA-nlist-i+nb_ind-1), Safe_typing.empty_private_constants @@ -213,8 +214,8 @@ let build_beq_scheme mode kn = List.fold_left Safe_typing.concat_private eff (List.rev effs) in let args = - Array.append - (Array.of_list (List.map (fun x -> lift lifti (EConstr.Unsafe.to_constr x)) a)) eqa in + Array.append + (Array.of_list (List.map (fun x -> lift lifti x) a)) eqa in if Int.equal (Array.length args) 0 then eq, eff else mkApp (eq, args), eff with Not_found -> raise(EqNotFound (ind', fst ind)) @@ -224,10 +225,9 @@ let build_beq_scheme mode kn = | Lambda _-> raise (EqUnknown "abstraction") | LetIn _ -> raise (EqUnknown "let-in") | Const (kn, u) -> - let u = EConstr.EInstance.kind sigma u in (match Environ.constant_opt_value_in env (kn, u) with | None -> raise (ParameterWithoutEquality (ConstRef kn)) - | Some c -> aux (EConstr.applist (EConstr.of_constr c,a))) + | Some c -> aux (Term.applist (c,a))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") | Case _ -> raise (EqUnknown "match") @@ -271,7 +271,7 @@ let build_beq_scheme mode kn = nparrec (nparrec+3+2*nb_cstr_args) (nb_cstr_args+ndx+1) - (EConstr.of_constr cc) + cc in eff := Safe_typing.concat_private eff' !eff; Array.set eqs ndx @@ -408,9 +408,9 @@ let do_replace_lb mode lb_scheme_key aavoid narg p q = lb_type_of_p >>= fun (lb_type_of_p,eff) -> Proofview.tclEVARMAP >>= fun sigma -> let lb_args = Array.append (Array.append - (Array.map (fun x -> x) v) - (Array.map (fun x -> do_arg sigma x 1) v)) - (Array.map (fun x -> do_arg sigma x 2) v) + v + (Array.Smart.map (fun x -> do_arg sigma x 1) v)) + (Array.Smart.map (fun x -> do_arg sigma x 2) v) in let app = if Array.is_empty lb_args then lb_type_of_p else mkApp (lb_type_of_p,lb_args) in @@ -479,9 +479,9 @@ let do_replace_bl mode bl_scheme_key (ind,u as indu) aavoid narg lft rgt = user_err err_msg in let bl_args = Array.append (Array.append - (Array.map (fun x -> x) v) - (Array.map (fun x -> do_arg sigma x 1) v)) - (Array.map (fun x -> do_arg sigma x 2) v ) + v + (Array.Smart.map (fun x -> do_arg sigma x 1) v)) + (Array.Smart.map (fun x -> do_arg sigma x 2) v ) in let app = if Array.is_empty bl_args then bl_t1 else mkApp (bl_t1,bl_args) @@ -543,7 +543,7 @@ let eqI ind l = and e, eff = try let c, eff = find_scheme beq_scheme_kind ind in mkConst c, eff with Not_found -> user_err ~hdr:"AutoIndDecl.eqI" - (str "The boolean equality on " ++ MutInd.print (fst ind) ++ str " is needed."); + (str "The boolean equality on " ++ Printer.pr_inductive (Global.env ()) ind ++ str " is needed."); in (if Array.equal Constr.equal eA [||] then e else mkApp(e,eA)), eff (**********************************************************************) @@ -643,7 +643,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]). | App (c,ca) -> ( match EConstr.kind sigma c with | Ind (indeq, u) -> - if eq_gr (IndRef indeq) Coqlib.glob_eq + if GlobRef.equal (IndRef indeq) Coqlib.glob_eq then Tacticals.New.tclTHEN (do_replace_bl mode bl_scheme_key ind @@ -871,7 +871,7 @@ let compute_dec_goal ind lnamesparrec nparrec = create_input ( mkNamedProd n (mkFullInd ind (2*nparrec)) ( mkNamedProd m (mkFullInd ind (2*nparrec+1)) ( - mkApp(sumbool(),[|eqnm;mkApp (Universes.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) + mkApp(sumbool(),[|eqnm;mkApp (UnivGen.constr_of_global @@ Coqlib.build_coq_not(),[|eqnm|])|]) ) ) ) @@ -931,7 +931,7 @@ let compute_dec_tact ind lnamesparrec nparrec = (* left *) Tacticals.New.tclTHENLIST [ simplest_left; - apply (EConstr.of_constr (mkApp(blI,Array.map(fun x->mkVar x) xargs))); + apply (EConstr.of_constr (mkApp(blI,Array.map mkVar xargs))); Auto.default_auto ] ; @@ -947,7 +947,7 @@ let compute_dec_tact ind lnamesparrec nparrec = assert_by (Name freshH3) (EConstr.of_constr (mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))) (Tacticals.New.tclTHENLIST [ - apply (EConstr.of_constr (mkApp(lbI,Array.map (fun x->mkVar x) xargs))); + apply (EConstr.of_constr (mkApp(lbI,Array.map mkVar xargs))); Auto.default_auto ]); Equality.general_rewrite_bindings_in true -- cgit v1.2.3