diff options
Diffstat (limited to 'pretyping/termops.ml')
| -rw-r--r-- | pretyping/termops.ml | 7 |
1 files changed, 5 insertions, 2 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) |