diff options
Diffstat (limited to 'plugins/derive')
| -rw-r--r-- | plugins/derive/Derive.v | 2 | ||||
| -rw-r--r-- | plugins/derive/derive.ml | 25 | ||||
| -rw-r--r-- | plugins/derive/derive.mli | 12 | ||||
| -rw-r--r-- | plugins/derive/g_derive.ml4 | 13 |
4 files changed, 26 insertions, 26 deletions
diff --git a/plugins/derive/Derive.v b/plugins/derive/Derive.v index 0d5a93b034..d1046ae79b 100644 --- a/plugins/derive/Derive.v +++ b/plugins/derive/Derive.v @@ -1 +1 @@ -Declare ML Module "derive_plugin".
\ No newline at end of file +Declare ML Module "derive_plugin". diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml index 19d23c0e43..480819ebe1 100644 --- a/plugins/derive/derive.ml +++ b/plugins/derive/derive.ml @@ -1,17 +1,19 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open API +open Constr open Context.Named.Declaration -let map_const_entry_body (f:Term.constr->Term.constr) (x:Safe_typing.private_constants Entries.const_entry_body) +let map_const_entry_body (f:constr->constr) (x:Safe_typing.private_constants Entries.const_entry_body) : Safe_typing.private_constants Entries.const_entry_body = - Future.chain ~pure:true x begin fun ((b,ctx),fx) -> + Future.chain x begin fun ((b,ctx),fx) -> (f b , ctx) , fx end @@ -38,9 +40,8 @@ let start_deriving f suchthat lemma = let f_type = EConstr.Unsafe.to_constr f_type in let ef = EConstr.Unsafe.to_constr ef in let env' = Environ.push_named (LocalDef (f, ef, f_type)) env in - let evdref = ref sigma in - let suchthat = Constrintern.interp_type_evars env' evdref suchthat in - TCons ( env' , !evdref , suchthat , (fun sigma _ -> + let sigma, suchthat = Constrintern.interp_type_evars env' sigma suchthat in + TCons ( env' , sigma , suchthat , (fun sigma _ -> TNil sigma)))))) in @@ -60,7 +61,7 @@ let start_deriving f suchthat lemma = | Proved (opaque, None, obj) -> match Proof_global.(obj.entries) with | [_;f_def;lemma_def] -> - opaque <> Vernacexpr.Transparent , f_def , lemma_def + opaque <> Proof_global.Transparent , f_def , lemma_def | _ -> assert false in (** The opacity of [f_def] is adjusted to be [false], as it @@ -68,7 +69,7 @@ let start_deriving f suchthat lemma = let f_def = { f_def with Entries.const_entry_opaque = false } in let f_def = Entries.DefinitionEntry f_def , Decl_kinds.(IsDefinition Definition) in let f_kn = Declare.declare_constant f f_def in - let f_kn_term = Term.mkConst f_kn in + let f_kn_term = mkConst f_kn in (** In the type and body of the proof of [suchthat] there can be references to the variable [f]. It needs to be replaced by references to the constant [f] declared above. This substitution diff --git a/plugins/derive/derive.mli b/plugins/derive/derive.mli index 7ea64a5288..06ff9c48cf 100644 --- a/plugins/derive/derive.mli +++ b/plugins/derive/derive.mli @@ -1,13 +1,13 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open API - (** [start_deriving f suchthat lemma] starts a proof of [suchthat] (which can contain references to [f]) in the context extended by [f:=?x]. When the proof ends, [f] is defined as the value of [?x] diff --git a/plugins/derive/g_derive.ml4 b/plugins/derive/g_derive.ml4 index ce9129bcfe..a59324149c 100644 --- a/plugins/derive/g_derive.ml4 +++ b/plugins/derive/g_derive.ml4 @@ -1,16 +1,15 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) -open API open Stdarg -(*i camlp4deps: "grammar/grammar.cma" i*) - DECLARE PLUGIN "derive_plugin" let classify_derive_command _ = Vernacexpr.(VtStartProof ("Classic",Doesn'tGuaranteeOpacity,[]),VtLater) |