Imported Upstream version 8.2~beta3+dfsgupstream/8.2.beta3+dfsg

1 files changed, 10 insertions, 3 deletions

diff --git a/contrib/subtac/subtac_command.mli b/contrib/subtac/subtac_command.mli
index 846e06cf..27520867 100644
--- a/contrib/subtac/subtac_command.mli
+++ b/contrib/subtac/subtac_command.mli
@@ -14,18 +14,18 @@ val interp_gen :
   evar_defs ref ->
   env ->
   ?impls:full_implicits_env ->
-  ?allow_soapp:bool ->
+  ?allow_patvar:bool ->
   ?ltacvars:ltac_sign ->
   constr_expr -> constr
 val interp_constr :
   evar_defs ref ->
   env -> constr_expr -> constr
-val interp_type :
+val interp_type_evars :
   evar_defs ref ->
   env ->
   ?impls:full_implicits_env ->
   constr_expr -> constr
-val interp_casted_constr :
+val interp_casted_constr_evars :
   evar_defs ref ->
   env ->
   ?impls:full_implicits_env ->
@@ -38,5 +38,12 @@ val interp_constr_judgment :
   constr_expr -> unsafe_judgment
 val list_chop_hd : int -> 'a list -> 'a list * 'a * 'a list
 
+val interp_binder :     Evd.evar_defs ref ->
+    Environ.env -> Names.name -> Topconstr.constr_expr -> Term.constr
+
+
 val build_recursive :
   (fixpoint_expr * decl_notation) list -> bool -> unit
+
+val build_corecursive :
+  (cofixpoint_expr * decl_notation) list -> bool -> unit