Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 60 insertions, 0 deletions

diff --git a/plugins/subtac/subtac_command.mli b/plugins/subtac/subtac_command.mli
new file mode 100644
index 00000000..304aa139
--- /dev/null
+++ b/plugins/subtac/subtac_command.mli
@@ -0,0 +1,60 @@
+open Pretyping
+open Evd
+open Environ
+open Term
+open Topconstr
+open Names
+open Libnames
+open Pp
+open Vernacexpr
+open Constrintern
+
+val interp_gen :
+  typing_constraint ->
+  evar_map ref ->
+  env ->
+  ?impls:full_internalization_env ->
+  ?allow_patvar:bool ->
+  ?ltacvars:ltac_sign ->
+  constr_expr -> constr
+val interp_constr :
+  evar_map ref ->
+  env -> constr_expr -> constr
+val interp_type_evars :
+  evar_map ref ->
+  env ->
+  ?impls:full_internalization_env ->
+  constr_expr -> constr
+val interp_casted_constr_evars :
+  evar_map ref ->
+  env ->
+  ?impls:full_internalization_env ->
+  constr_expr -> types -> constr
+val interp_open_constr :
+  evar_map ref -> env -> constr_expr -> constr
+val interp_constr_judgment :
+  evar_map ref ->
+  env ->
+  constr_expr -> unsafe_judgment
+val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
+
+val interp_binder :     Evd.evar_map ref ->
+    Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
+
+
+val telescope :
+  (Names.name * 'a option * Term.types) list ->
+  Term.types * (Names.name * Term.types option * Term.types) list *
+    Term.constr
+
+val build_wellfounded :
+           Names.identifier * 'a * Topconstr.local_binder list *
+           Topconstr.constr_expr * Topconstr.constr_expr ->
+           Topconstr.constr_expr ->
+           Topconstr.constr_expr -> 'b -> 'c -> Subtac_obligations.progress
+
+val build_recursive :
+  (fixpoint_expr * decl_notation list) list -> bool -> unit
+
+val build_corecursive :
+  (cofixpoint_expr * decl_notation list) list -> bool -> unit