diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evarconv.mli | 3 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 2 | ||||
| -rw-r--r-- | pretyping/retyping.mli | 6 |
3 files changed, 7 insertions, 4 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 972109d2f1..6672a3d4b0 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -15,7 +15,7 @@ val the_conv_x : env -> 'a evar_defs -> constr -> constr -> bool val the_conv_x_leq : env -> 'a evar_defs -> constr -> constr -> bool -(* For debugging *) +(*i For debugging *) val solve_pb : env -> 'a evar_defs -> conv_pb * constr * constr -> bool @@ -26,3 +26,4 @@ val evar_conv_x : val evar_eqappr_x : env -> 'a evar_defs -> conv_pb -> constr * constr list -> constr * constr list -> bool +(*i*) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f29f79c617..f4c39fdb3c 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -11,7 +11,7 @@ open Reduction (*i*) (* This modules provides useful functions for unification algorithms. - * Used in Trad and Progmach + * Used in Trad and Progmach. * This interface will have to be improved. *) val filter_unique : 'a list -> 'a list diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 036cd53f0b..3f9ec15552 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -1,12 +1,12 @@ (* $Id$ *) +(*i*) open Names open Term open Evd open Environ - -type metamap = (int * constr) list +(*i*) (* This family of functions assumes its constr argument is known to be well-typable. It does not type-check, just recompute the type @@ -14,6 +14,8 @@ type metamap = (int * constr) list either produces a wrong result or raise an anomaly. Use with care. It doesn't handle predicative universes too. *) +type metamap = (int * constr) list + val get_type_of : env -> 'a evar_map -> constr -> constr val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr val get_sort_of : env -> 'a evar_map -> constr -> sorts |