From bae7532aaf4fc4ca0f637cb6e53f6b4b80c7cb75 Mon Sep 17 00:00:00 2001 From: filliatr Date: Wed, 3 May 2000 20:44:42 +0000 Subject: diverses modifs pour ocamlweb git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@408 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/pretyping.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 9bd4827636..f46f9ddb3d 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -12,7 +12,7 @@ open Evarutil (*i*) (* Raw calls to the inference machine of Trad: boolean says if we must fail - on unresolved evars, or replace them by Metas ; the unsafe_judgment list + on unresolved evars, or replace them by Metas ; the [unsafe_judgment] list allows us to extend env with some bindings *) val ise_resolve : bool -> 'a evar_map -> (int * constr) list -> env -> (identifier * unsafe_judgment) list -> -- cgit v1.2.3