diff options
| author | Pierre-Marie Pédrot | 2016-04-13 16:31:01 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-04 13:47:12 +0200 |
| commit | 5da0f107cb3332d5cd87fc352aef112f6b74fc97 (patch) | |
| tree | 854d373e13b6ef39017e6bc2dd6d0c7e14a006cd /engine/geninterp.mli | |
| parent | a6de02fcfde76f49b10d8481a2423692fa105756 (diff) | |
Moving Ftactic and Geninterp to the engine folder.
Diffstat (limited to 'engine/geninterp.mli')
| -rw-r--r-- | engine/geninterp.mli | 27 |
1 files changed, 27 insertions, 0 deletions
diff --git a/engine/geninterp.mli b/engine/geninterp.mli new file mode 100644 index 0000000000..0992db7a29 --- /dev/null +++ b/engine/geninterp.mli @@ -0,0 +1,27 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Interpretation functions for generic arguments. *) + +open Names +open Genarg + +module TacStore : Store.S + +type interp_sign = { + lfun : Val.t Id.Map.t; + extra : TacStore.t } + +type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t + +val interp : ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun + +val generic_interp : (glob_generic_argument, Val.t) interp_fun + +val register_interp0 : + ('raw, 'glb, 'top) genarg_type -> ('glb, 'top) interp_fun -> unit |