diff options
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index adc0e6daa..b290a5e5f 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) +(*i $Id$ i*) open Util open Pp @@ -16,7 +16,6 @@ open Sign open Environ (* Universes *) -(*val set_module : Names.dir_path -> unit*) val new_univ : unit -> Univ.universe val new_sort_in_family : sorts_family -> sorts val new_Type : unit -> types @@ -139,7 +138,7 @@ val named_hd_type : env -> types -> name -> name val mkProd_name : env -> name * types * types -> types val mkLambda_name : env -> name * types * constr -> constr -(* Deprecated synonyms of mkProd_name and mkLambda_name *) +(* Deprecated synonyms of [mkProd_name] and [mkLambda_name] *) val prod_name : env -> name * types * types -> types val lambda_name : env -> name * types * constr -> constr |