diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-28 23:51:42 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-01-28 23:51:42 +0000 |
| commit | e521ccb7d16b7e2192a0c0d6bc046534a4466848 (patch) | |
| tree | 1616a21eb4cb88bef2fcae0830d666bec2e02ab0 /pretyping | |
| parent | bd23886243736ba75a584c475b7da521571c646d (diff) | |
documentation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@288 85f007b7-540e-0410-9357-904b9bb8a0f7
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 972109d2f..6672a3d4b 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 f29f79c61..f4c39fdb3 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 036cd53f0..3f9ec1555 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 |