diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-24 11:09:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-08-24 11:09:20 +0000 |
| commit | 27e6bc5c07e7da16d1cd5ab9a627bcd50b112b9e (patch) | |
| tree | b145b26755270d7cad25f4a915e99978359fb93d | |
| parent | f80495d7457b6e2358eb06c566f1c0f253d2252a (diff) | |
Ajout nom standard mkLambda_name pour lambda_name (et idem pour prod)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6030 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 |