diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-14 18:35:04 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-02-14 18:50:58 +0100 |
| commit | 4a53151f846476f2fbe038a4ecb8e84256a26ba9 (patch) | |
| tree | 8b37e319015557cbec25b6058d366e4abbc74c94 /plugins | |
| parent | 9c5db70b891bf6c3e173a31d4e8761e586c7814a (diff) | |
Abstract: "Qed export ident, .., ident" to preserve v8.4 behavior
Of course such proofs cannot be processed asynchronously
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/derive/derive.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/functional_principles_proofs.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/invfun.ml | 2 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 8 |
4 files changed, 7 insertions, 7 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 439b1a5c0..711a8aaf0 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -55,7 +55,7 @@ let start_deriving f suchthat lemma = | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> - opaque , f_def , lemma_def + opaque <> Transparent , f_def , lemma_def | _ -> assert false in (** The opacity of [f_def] is adjusted to be [false], as it diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml index eb5221fd6..04347537f 100644 --- a/plugins/funind/functional_principles_proofs.ml +++ b/plugins/funind/functional_principles_proofs.ml @@ -989,7 +989,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num = lemma_type (Lemmas.mk_hook (fun _ _ -> ())); ignore (Pfedit.by (Proofview.V82.tactic prove_replacement)); - Lemmas.save_proof (Vernacexpr.Proved(false,None)) + Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))) diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index 0c7b0a0b0..b9d7e0d90 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -1022,7 +1022,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic = -let do_save () = Lemmas.save_proof (Vernacexpr.Proved(false,None)) +let do_save () = Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))) (* [derive_correctness make_scheme functional_induction funs graphs] create correctness and completeness diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 5558556e2..b1cbea51c 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -60,7 +60,7 @@ let declare_fun f_id kind ?(ctx=Univ.UContext.empty) value = let ce = definition_entry ~univs:ctx value (*FIXME *) in ConstRef(declare_constant f_id (DefinitionEntry ce, kind));; -let defined () = Lemmas.save_proof (Vernacexpr.Proved (false,None)) +let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None))) let def_of_const t = match (kind_of_term t) with @@ -1247,9 +1247,9 @@ let build_new_goal_type () = let is_opaque_constant c = let cb = Global.lookup_constant c in match cb.Declarations.const_body with - | Declarations.OpaqueDef _ -> true - | Declarations.Undef _ -> true - | Declarations.Def _ -> false + | Declarations.OpaqueDef _ -> Vernacexpr.Opaque None + | Declarations.Undef _ -> Vernacexpr.Opaque None + | Declarations.Def _ -> Vernacexpr.Transparent let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) = (* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *) |