diff options
Diffstat (limited to 'pretyping/evarconv.mli')
| -rw-r--r-- | pretyping/evarconv.mli | 22 |
1 files changed, 10 insertions, 12 deletions
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 28b960bb9..2e52fb12b 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -1,26 +1,24 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) +(*********************************************************************** + v * The Coq Proof Assistant / The Coq Development Team + <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud + \VV/ ************************************************************* + // * This file is distributed under the terms of the + * GNU Lesser General Public License Version 2.1 + ***********************************************************************) (*i $Id$ i*) -(*i*) open Term open Sign open Environ open Reductionops open Evd -(*i*) -(* returns exception Reduction.NotConvertible if not unifiable *) +(** returns exception Reduction.NotConvertible if not unifiable *) val the_conv_x : env -> constr -> constr -> evar_map -> evar_map val the_conv_x_leq : env -> constr -> constr -> evar_map -> evar_map -(* The same function resolving evars by side-effect and +(** The same function resolving evars by side-effect and catching the exception *) val e_conv : env -> evar_map ref -> constr -> constr -> bool val e_cumul : env -> evar_map ref -> constr -> constr -> bool @@ -32,7 +30,7 @@ val evar_eqappr_x : env -> evar_map -> conv_pb -> constr * constr list -> constr * constr list -> evar_map * bool -(*i*) +(**/**) val consider_remaining_unif_problems : env -> evar_map -> evar_map |