diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-12 18:12:45 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-12-15 19:18:41 +0100 |
| commit | 9aa416c0c66ad7e14c4704898b74b99237d81c78 (patch) | |
| tree | 7b2519a4aa91a80c6c2c6e463389b13bbc5fa47e /pretyping/evarconv.mli | |
| parent | 4fec6bdf0ad0f49c98a82538c5caf4511ba5e95c (diff) | |
Documenting check_record + changing a possibly undefined int into int option.
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index f559db253..dd9c622dc 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -48,7 +48,7 @@ val check_conv_record : env -> evar_map -> * constr * constr list * (constr Stack.t * constr Stack.t) * (constr Stack.t * types Stack.t) * (constr Stack.t * types Stack.t) * constr * - (int * constr) + (int option * constr) (** Try to solve problems of the form ?x[args] = c by second-order matching, using typing to select occurrences *) |