diff options
| author | Pierre-Marie Pédrot | 2015-02-15 18:17:04 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-15 18:17:04 +0100 |
| commit | d7691de7184b4cdcfd48fd762011569cde5523c5 (patch) | |
| tree | 9c9e14226b070fc2a5cf4c216c4f8c634de20855 /plugins | |
| parent | eed12bddc3e6f6f9192c909a8b8f82859080f3a1 (diff) | |
| parent | aed3c876d422f4dcc0296fd4949148c697f37b1d (diff) | |
Merge branch 'v8.5'
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 439b1a5c01..a77b552e01 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 <> Vernacexpr.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 eb5221fd69..04347537f2 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 0c7b0a0b08..b9d7e0d909 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 5558556e2d..b1cbea51c8 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); *) |