diff options
| author | Pierre Boutillier | 2014-10-08 19:39:08 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-10-08 22:11:34 +0200 |
| commit | 8ab64e4e53cfc3f316795790c92093c3ba8d199a (patch) | |
| tree | 301123854796312a06418e539330dfce9120d9e3 | |
| parent | 827a2bba4c9342a50c47ce257b40cb395518be6f (diff) | |
fix make mlidoc
| -rw-r--r-- | pretyping/reductionops.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index a2b7e6f3fd..ed635c0640 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -261,7 +261,7 @@ val is_trans_conv : transparent_state -> env -> evar_map -> constr -> constr -> val is_trans_conv_leq : transparent_state -> env -> evar_map -> constr -> constr -> bool val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr -> constr -> bool -(** [check_conv} Checks universe constraints only. +(** [check_conv] Checks universe constraints only. pb defaults to CUMUL and ts to a full transparent state. *) val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool |