diff options
| author | herbelin | 2004-08-24 11:09:20 +0000 |
|---|---|---|
| committer | herbelin | 2004-08-24 11:09:20 +0000 |
| commit | 27e6bc5c07e7da16d1cd5ab9a627bcd50b112b9e (patch) | |
| tree | b145b26755270d7cad25f4a915e99978359fb93d /pretyping/termops.mli | |
| 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
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 0f454c2779..255e8a056b 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 |