diff options
| author | Gaëtan Gilbert | 2020-04-16 16:33:43 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-04-16 16:33:43 +0200 |
| commit | 0754dfc001218a8124609418e58896ef18d6b6cf (patch) | |
| tree | cc635dc3916971d0615924367cc314226148d55a /plugins/funind/gen_principle.ml | |
| parent | 35e363f988e941e710b4e24cd638233383275bd7 (diff) | |
| parent | 38aa25757957e9e9f879509605f06ada5992ca36 (diff) | |
Merge PR #11999: [proof] Merge `Proof_global` into `Declare`
Reviewed-by: Matafou
Ack-by: SkySkimmer
Reviewed-by: ppedrot
Diffstat (limited to 'plugins/funind/gen_principle.ml')
| -rw-r--r-- | plugins/funind/gen_principle.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/plugins/funind/gen_principle.ml b/plugins/funind/gen_principle.ml index df147b3aa6..eec78391af 100644 --- a/plugins/funind/gen_principle.ml +++ b/plugins/funind/gen_principle.ml @@ -191,7 +191,7 @@ let prepare_body {Vernacexpr.binders} rt = let fun_args, rt' = chop_rlambda_n n rt in (fun_args, rt') -let build_functional_principle ?(opaque = Proof_global.Transparent) +let build_functional_principle ?(opaque = Declare.Transparent) (evd : Evd.evar_map ref) old_princ_type sorts funs _i proof_tac hook = (* First we get the type of the old graph principle *) let mutr_nparams = @@ -233,9 +233,10 @@ let build_functional_principle ?(opaque = Proof_global.Transparent) (* let dur1 = System.time_difference tim1 tim2 in *) (* Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *) (* end; *) - let open Proof_global in - let {entries} = - Lemmas.pf_fold (close_proof ~opaque ~keep_body_ucst_separate:false) lemma + let {Declare.entries} = + Lemmas.pf_fold + (Declare.close_proof ~opaque ~keep_body_ucst_separate:false) + lemma in match entries with | [entry] -> (entry, hook) @@ -1394,7 +1395,7 @@ let make_scheme evd (fas : (Constr.pconstant * Sorts.family) list) : | None -> raise Not_found | Some finfos -> finfos in - let open Proof_global in + let open Declare in match finfos.equation_lemma with | None -> Transparent (* non recursive definition *) | Some equation -> @@ -1550,7 +1551,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) fst @@ Lemmas.by (Proofview.V82.tactic (proving_tac i)) lemma in let () = - Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent + Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None in let finfo = @@ -1621,7 +1622,7 @@ let derive_correctness (funs : Constr.pconstant list) (graphs : inductive list) lemma) in let () = - Lemmas.save_lemma_proved ~lemma ~opaque:Proof_global.Transparent + Lemmas.save_lemma_proved ~lemma ~opaque:Declare.Transparent ~idopt:None in let finfo = |