summaryrefslogtreecommitdiff
path: root/vernac/auto_ind_decl.ml
diff options
context:
space:
mode:
Diffstat (limited to 'vernac/auto_ind_decl.ml')
-rw-r--r--vernac/auto_ind_decl.ml54
1 files changed, 27 insertions, 27 deletions
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
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 17:34:14 +0000