diff options
| author | herbelin | 2005-01-21 17:24:37 +0000 |
|---|---|---|
| committer | herbelin | 2005-01-21 17:24:37 +0000 |
| commit | b7af7027d15afa2dee1695792a2658f0df392956 (patch) | |
| tree | bebcce8f9fbb305d0bd9aa203ec843677665323b /pretyping | |
| parent | accec4fc961d85ef21e73e690dedc36ce4c25f46 (diff) | |
Compatibilité ocamlweb pour cible doc
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6621 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/evd.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index fff6808d19..435efa4998 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -105,10 +105,10 @@ val map_clb : (constr -> constr) -> clbinding -> clbinding (* Unification state *) type evar_defs -(* Substitution is not applied to the evar_map *) +(* Substitution is not applied to the [evar_map] *) val subst_evar_defs : substitution -> evar_defs -> evar_defs -(* create an evar_defs with empty meta map: *) +(* create an [evar_defs] with empty meta map: *) val create_evar_defs : evar_map -> evar_defs val evars_of : evar_defs -> evar_map val evars_reset_evd : evar_map -> evar_defs -> evar_defs @@ -139,7 +139,7 @@ val get_conv_pbs : evar_defs -> (evar_constraint -> bool) -> (* Metas *) val meta_list : evar_defs -> (metavariable * clbinding) list val meta_defined : evar_defs -> metavariable -> bool -(* [meta_fvalue] raises Not_found if meta not in map or Anomaly if +(* [meta_fvalue] raises [Not_found] if meta not in map or [Anomaly] if meta has no value *) val meta_fvalue : evar_defs -> metavariable -> constr freelisted val meta_ftype : evar_defs -> metavariable -> constr freelisted |