diff options
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index ce4e1b28..c68cfffe 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: evd.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: evd.mli 13902 2011-03-10 15:50:24Z msozeau $ i*) (*i*) open Util @@ -177,7 +177,7 @@ val existential_opt_value : evar_map -> existential -> constr option val subst_evar_defs_light : substitution -> evar_map -> evar_map (* spiwack: this function seems to somewhat break the abstraction. *) -val evars_reset_evd : evar_map -> evar_map -> evar_map +val evars_reset_evd : ?with_conv_pbs:bool -> evar_map -> evar_map -> evar_map (* spiwack: [is_undefined_evar] should be considered a candidate |