diff options
author | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 12:36:19 +0000 |
---|---|---|
committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-06-21 12:36:19 +0000 |
commit | 9024a91b59b9ecfb94e68b3748f2a9a66adcf515 (patch) | |
tree | 44d3483d8ec18b2f8bba7a0a348632edbfad465c /interp/constrarg.mli | |
parent | 47cbc272e79db52cc96dfe3d4d1cd4b978e4fa2a (diff) |
Cutting the dependency of Genarg in constr_expr, glob_constr
related types. This will ultimately allow putting genargs into
these ASTs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16600 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrarg.mli')
-rw-r--r-- | interp/constrarg.mli | 79 |
1 files changed, 79 insertions, 0 deletions
diff --git a/interp/constrarg.mli b/interp/constrarg.mli new file mode 100644 index 000000000..548bd6690 --- /dev/null +++ b/interp/constrarg.mli @@ -0,0 +1,79 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(** Generic arguments based on [constr]. We put them here to avoid a dependency + of Genarg in [constr]-related interfaces. *) + +open Loc +open Pp +open Names +open Term +open Libnames +open Globnames +open Glob_term +open Genredexpr +open Pattern +open Constrexpr +open Tacexpr +open Term +open Misctypes +open Evd +open Genarg + +(** FIXME: nothing to do there. *) +val loc_of_or_by_notation : ('a -> Loc.t) -> 'a or_by_notation -> Loc.t + +(** {5 Additional generic arguments} *) + +val wit_int_or_var : int or_var uniform_genarg_type + +val wit_intro_pattern : intro_pattern_expr located uniform_genarg_type + +val wit_ident : Id.t uniform_genarg_type + +val wit_pattern_ident : Id.t uniform_genarg_type + +val wit_ident_gen : bool -> Id.t uniform_genarg_type + +val wit_var : (Id.t located, Id.t located, Id.t) genarg_type + +val wit_ref : (reference, global_reference located or_var, global_reference) genarg_type + +val wit_quant_hyp : quantified_hypothesis uniform_genarg_type + +val wit_genarg : (raw_generic_argument, glob_generic_argument, typed_generic_argument) genarg_type + +val wit_sort : (glob_sort, glob_sort, sorts) genarg_type + +val wit_constr : (constr_expr, glob_constr_and_expr, constr) genarg_type + +val wit_constr_may_eval : + ((constr_expr,reference or_by_notation,constr_expr) may_eval, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval, + constr) genarg_type + +val wit_open_constr_gen : bool -> (open_constr_expr, open_glob_constr, open_constr) genarg_type + +val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type + +val wit_casted_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type + +val wit_constr_with_bindings : + (constr_expr with_bindings, + glob_constr_and_expr with_bindings, + constr with_bindings sigma) genarg_type + +val wit_bindings : + (constr_expr bindings, + glob_constr_and_expr bindings, + constr bindings sigma) genarg_type + +val wit_red_expr : + ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen, + (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen, + (constr,evaluable_global_reference,constr_pattern) red_expr_gen) genarg_type |