From b98e5c6662e4e6ef3b9ba8da6da9cb1fda63e2a8 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Wed, 18 Apr 2012 14:47:37 +0000
Subject: Adds a comment: precondition on Evd.add

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15204 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evd.mli | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 5e596e0de2..bfdbf5e716 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -149,6 +149,8 @@ val is_empty : evar_map -> bool
     there are uninstantiated evars in [sigma]. *)
 val has_undefined : evar_map -> bool
 
+(** [add sigma ev info] adds [ev] with evar info [info] in sigma.
+    Precondition: ev must not preexist in [sigma]. *)
 val add : evar_map -> evar -> evar_info -> evar_map
 
 val find : evar_map -> evar -> evar_info
-- 
cgit v1.2.3