diff options
| -rw-r--r-- | pretyping/termops.ml | 7 | ||||
| -rw-r--r-- | pretyping/termops.mli | 8 |
2 files changed, 12 insertions, 3 deletions
diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 7aea3b484..7c4739b48 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -667,8 +667,11 @@ let named_hd env a = function let named_hd_type env a = named_hd env (body_of_type a) -let prod_name env (n,a,b) = mkProd (named_hd_type env a n, a, b) -let lambda_name env (n,a,b) = mkLambda (named_hd_type env a n, a, b) +let mkProd_name env (n,a,b) = mkProd (named_hd_type env a n, a, b) +let mkLambda_name env (n,a,b) = mkLambda (named_hd_type env a n, a, b) + +let lambda_name = mkLambda_name +let prod_name = mkProd_name let prod_create env (a,b) = mkProd (named_hd_type env a Anonymous, a, b) let lambda_create env (a,b) = mkLambda (named_hd_type env a Anonymous, a, b) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 0f454c277..255e8a056 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -126,8 +126,14 @@ val id_of_name_using_hdchar : env -> types -> name -> identifier val named_hd : env -> types -> name -> name val named_hd_type : env -> types -> name -> name -val prod_name : env -> name * types * types -> constr + +val mkProd_name : env -> name * types * types -> types +val mkLambda_name : env -> name * types * constr -> constr + +(* Deprecated synonyms of mkProd_name and mkLambda_name *) +val prod_name : env -> name * types * types -> types val lambda_name : env -> name * types * constr -> constr + val prod_create : env -> types * types -> constr val lambda_create : env -> types * constr -> constr val name_assumption : env -> rel_declaration -> rel_declaration |