From 34bc13e0ef3642244fe77fe8a8a7869fbc8d2fca Mon Sep 17 00:00:00 2001
From: barras
Date: Sun, 12 Sep 2004 11:38:09 +0000
Subject: inclusion de meta_map dans evar_defs

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

(limited to 'pretyping/unification.mli')

diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 02d1918bed..d3007e69df 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -18,19 +18,19 @@ open Evd
 open Evarutil
 (*i*)
 
-type maps = evar_defs * meta_map
-
-val w_Declare : env -> evar -> types -> maps -> maps
-val w_Define : evar -> constr -> maps -> maps
+val w_Declare : env -> evar -> types -> evar_defs -> evar_defs
+val w_Define : evar -> constr -> evar_defs -> evar_defs
 
 (* The "unique" unification fonction *)
 val w_unify :
-  bool -> env -> Reductionops.conv_pb -> constr -> constr -> maps -> maps
+  bool -> env -> Reductionops.conv_pb -> constr -> constr ->
+  evar_defs -> evar_defs
 
 (* [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
    subterm of [t]. Constraints are added to [m] and the matched
    subterm of [t] is also returned. *)
-val w_unify_to_subterm : env -> constr * constr -> maps -> maps * constr
+val w_unify_to_subterm :
+  env -> constr * constr -> evar_defs -> evar_defs * constr
 
 (*i This should be in another module i*)
 
-- 
cgit v1.2.3