Centralisation prod_name and co dans Environ; mkLambda_string dans Term

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@437 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 0 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 51406b1e08..7320b8be89 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -164,6 +164,9 @@ val mkCast : constr -> constr -> constr
 (* Constructs the product $(x:t_1)t_2$. $x$ may be anonymous. *)
 val mkProd : name -> constr -> constr -> constr
 
+(* [mkProd_string s t c] constructs the product $(s:t)c$ *)
+val mkProd_string : string -> constr -> constr -> constr
+
 (* non-dependant product $t_1 \rightarrow t_2$ *)
 val mkArrow : constr -> constr -> constr
 
@@ -174,6 +177,9 @@ val mkNamedProd : identifier -> constr -> constr -> constr
 val mkLambda : name -> constr -> constr -> constr
 val mkNamedLambda : identifier -> constr -> constr -> constr
 
+(* [mkLambda_string s t c] constructs $[s:t]c$ *)
+val mkLambda_string : string -> constr -> constr -> constr
+
 (* If $a = [| t_1; \dots; t_n |]$, constructs the application 
    $(t_1~\dots~t_n)$. *)
 val mkAppL : constr array -> constr