summaryrefslogtreecommitdiff
path: root/plugins/ltac/extraargs.mli
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
committerGravatar Benjamin Barenblat <bbaren@debian.org>2018-12-29 14:31:27 -0500
commit9043add656177eeac1491a73d2f3ab92bec0013c (patch)
tree2b0092c84bfbf718eca10c81f60b2640dc8cab05 /plugins/ltac/extraargs.mli
parenta4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff)
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'plugins/ltac/extraargs.mli')
-rw-r--r--plugins/ltac/extraargs.mli84
1 files changed, 84 insertions, 0 deletions
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
new file mode 100644
index 00000000..e5a4f090
--- /dev/null
+++ b/plugins/ltac/extraargs.mli
@@ -0,0 +1,84 @@
+(************************************************************************)
+(* * 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 *)
+(* * (see LICENSE file for the text of the license) *)
+(************************************************************************)
+
+open Tacexpr
+open Names
+open Constrexpr
+open Glob_term
+open Misctypes
+
+val wit_orient : bool Genarg.uniform_genarg_type
+val orient : bool Pcoq.Gram.entry
+val pr_orient : bool -> Pp.t
+
+val wit_rename : (Id.t * Id.t) Genarg.uniform_genarg_type
+
+val occurrences : (int list or_var) Pcoq.Gram.entry
+val wit_occurrences : (int list or_var, int list or_var, int list) Genarg.genarg_type
+val pr_occurrences : int list or_var -> Pp.t
+val occurrences_of : int list -> Locus.occurrences
+
+val wit_natural : int Genarg.uniform_genarg_type
+
+val wit_glob :
+ (constr_expr,
+ Tacexpr.glob_constr_and_expr,
+ Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
+
+val wit_lglob :
+ (constr_expr,
+ Tacexpr.glob_constr_and_expr,
+ Tacinterp.interp_sign * glob_constr) Genarg.genarg_type
+
+val wit_lconstr :
+ (constr_expr,
+ Tacexpr.glob_constr_and_expr,
+ EConstr.t) Genarg.genarg_type
+
+val wit_casted_constr :
+ (constr_expr,
+ Tacexpr.glob_constr_and_expr,
+ EConstr.t) Genarg.genarg_type
+
+val glob : constr_expr Pcoq.Gram.entry
+val lglob : constr_expr Pcoq.Gram.entry
+
+type 'id gen_place= ('id * Locus.hyp_location_flag,unit) location
+
+type loc_place = lident gen_place
+type place = Id.t gen_place
+
+val wit_hloc : (loc_place, loc_place, place) Genarg.genarg_type
+val hloc : loc_place Pcoq.Gram.entry
+val pr_hloc : loc_place -> Pp.t
+
+val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry
+val wit_by_arg_tac :
+ (raw_tactic_expr option,
+ glob_tactic_expr option,
+ Geninterp.Val.t option) Genarg.genarg_type
+
+val pr_by_arg_tac :
+ (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
+ raw_tactic_expr option -> Pp.t
+
+val test_lpar_id_colon : unit Pcoq.Gram.entry
+
+val wit_test_lpar_id_colon : (unit, unit, unit) Genarg.genarg_type
+
+(** Spiwack: Primitive for retroknowledge registration *)
+
+val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry
+val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type
+
+val wit_in_clause :
+ (lident Locus.clause_expr,
+ lident Locus.clause_expr,
+ Id.t Locus.clause_expr) Genarg.genarg_type