diff options
| -rw-r--r-- | pretyping/cases.ml | 12 | ||||
| -rw-r--r-- | pretyping/program.ml | 20 | ||||
| -rw-r--r-- | pretyping/program.mli | 4 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 35 | ||||
| -rw-r--r-- | vernac/indschemes.mli | 2 |
5 files changed, 43 insertions, 30 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c2c8065a9..56f5d521a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -2223,14 +2223,14 @@ let build_ineqs evdref prevpatterns pats liftsign = (Some ([], 0, 0, [])) eqnpats pats in match acc with None -> c - | Some (sign, len, _, c') -> - let conj = it_mkProd_or_LetIn (mk_coq_not (mk_coq_and c')) - (lift_rel_context liftsign sign) - in - conj :: c) + | Some (sign, len, _, c') -> + let sigma, conj = mk_coq_and !evdref c' in + let sigma, neg = mk_coq_not sigma conj in + let conj = it_mkProd_or_LetIn neg (lift_rel_context liftsign sign) in + evdref := sigma; conj :: c) [] prevpatterns in match diffs with [] -> None - | _ -> Some (mk_coq_and diffs) + | _ -> Some (let sigma, conj = mk_coq_and !evdref diffs in evdref := sigma; conj) let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let i = ref 0 in diff --git a/pretyping/program.ml b/pretyping/program.ml index 8769c5659..2fa3facb3 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -9,7 +9,6 @@ open CErrors open Util -let init_constant dir s () = Universes.constr_of_global @@ Coqlib.coq_reference "Program" dir s let init_reference dir s () = Coqlib.coq_reference "Program" dir s let papp evdref r args = @@ -39,20 +38,25 @@ let coq_eq_rect = init_reference ["Init"; "Logic"] "eq_rect" let coq_JMeq_ind = init_reference ["Logic";"JMeq"] "JMeq" let coq_JMeq_refl = init_reference ["Logic";"JMeq"] "JMeq_refl" -let coq_not = init_constant ["Init";"Logic"] "not" -let coq_and = init_constant ["Init";"Logic"] "and" +let coq_not = init_reference ["Init";"Logic"] "not" +let coq_and = init_reference ["Init";"Logic"] "and" -let delayed_force c = EConstr.of_constr (c ()) +let new_global sigma gr = + let open Sigma in + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c -let mk_coq_not x = EConstr.mkApp (delayed_force coq_not, [| x |]) +let mk_coq_not sigma x = + let sigma, notc = new_global sigma (coq_not ()) in + sigma, EConstr.mkApp (notc, [| x |]) let unsafe_fold_right f = function hd :: tl -> List.fold_right f tl hd | [] -> invalid_arg "unsafe_fold_right" -let mk_coq_and l = - let and_typ = delayed_force coq_and in - unsafe_fold_right +let mk_coq_and sigma l = + let sigma, and_typ = new_global sigma (coq_and ()) in + sigma, unsafe_fold_right (fun c conj -> EConstr.mkApp (and_typ, [| c ; conj |])) l diff --git a/pretyping/program.mli b/pretyping/program.mli index 94a7bdcb6..8439b9528 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference val coq_JMeq_ind : unit -> global_reference val coq_JMeq_refl : unit -> global_reference -val mk_coq_and : constr list -> constr -val mk_coq_not : constr -> constr +val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr +val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index f57b1bba0..a678d20bb 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -453,11 +453,19 @@ let fold_left' f = function [] -> invalid_arg "fold_left'" | hd :: tl -> List.fold_left f hd tl +let new_global sigma gr = + let open Sigma in + let Sigma (c, sigma, _) = Evarutil.new_global (Sigma.Unsafe.of_evar_map sigma) gr + in Sigma.to_evar_map sigma, c + +let mk_coq_and sigma = new_global sigma (Coqlib.build_coq_and ()) +let mk_coq_conj sigma = new_global sigma (Coqlib.build_coq_conj ()) + let build_combined_scheme env schemes = - let defs = List.map (fun cst -> (* FIXME *) - let evd, c = Evd.fresh_constant_instance env (Evd.from_env env) cst in - (c, Typeops.type_of_constant_in env c)) schemes in -(* let nschemes = List.length schemes in *) + let evdref = ref (Evd.from_env env) in + let defs = List.map (fun cst -> + let evd, c = Evd.fresh_constant_instance env !evdref cst in + evdref := evd; (c, Typeops.type_of_constant_in env c)) schemes in let find_inductive ty = let (ctx, arity) = decompose_prod ty in let (_, last) = List.hd ctx in @@ -471,26 +479,27 @@ let build_combined_scheme env schemes = let (c, t) = List.hd defs in let ctx, ind, nargs = find_inductive t in (* Number of clauses, including the predicates quantification *) - let prods = nb_prod Evd.empty (EConstr.of_constr t) - (nargs + 1) (** FIXME *) in - let coqand = Universes.constr_of_global @@ Coqlib.build_coq_and () in - let coqconj = Universes.constr_of_global @@ Coqlib.build_coq_conj () in + let prods = nb_prod !evdref (EConstr.of_constr t) - (nargs + 1) in + let sigma, coqand = mk_coq_and !evdref in + let sigma, coqconj = mk_coq_conj sigma in + let () = evdref := sigma in let relargs = rel_vect 0 prods in let concls = List.rev_map - (fun (cst, t) -> (* FIXME *) + (fun (cst, t) -> mkApp(mkConstU cst, relargs), snd (decompose_prod_n prods t)) defs in let concl_bod, concl_typ = fold_left' (fun (accb, acct) (cst, x) -> - mkApp (coqconj, [| x; acct; cst; accb |]), - mkApp (coqand, [| x; acct |])) concls + mkApp (EConstr.to_constr !evdref coqconj, [| x; acct; cst; accb |]), + mkApp (EConstr.to_constr !evdref coqand, [| x; acct |])) concls in let ctx, _ = list_split_rev_at prods (List.rev_map (fun (x, y) -> LocalAssum (x, y)) ctx) in let typ = List.fold_left (fun d c -> Term.mkProd_wo_LetIn c d) concl_typ ctx in let body = it_mkLambda_or_LetIn concl_bod ctx in - (body, typ) + (!evdref, body, typ) let do_combined_scheme name schemes = let csts = @@ -501,9 +510,9 @@ let do_combined_scheme name schemes = with Not_found -> user_err Pp.(pr_qualid (snd qualid) ++ str " is not declared.")) schemes in - let body,typ = build_combined_scheme (Global.env ()) csts in + let sigma,body,typ = build_combined_scheme (Global.env ()) csts in let proof_output = Future.from_val ((body,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in - ignore (define (snd name) UserIndividualRequest Evd.empty proof_output (Some typ)); + ignore (define (snd name) UserIndividualRequest sigma proof_output (Some typ)); fixpoint_message None [snd name] (**********************************************************************) diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index e5d79fd51..0f559d2bd 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -40,7 +40,7 @@ val do_scheme : (Id.t located option * scheme) list -> unit (** Combine a list of schemes into a conjunction of them *) -val build_combined_scheme : env -> constant list -> constr * types +val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types val do_combined_scheme : Id.t located -> Id.t located list -> unit |