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
---
 tactics/equality.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics/equality.ml')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 38dc8f58e4..f9834f5229 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -821,7 +821,7 @@ let swap_equands gls eqn =
 let swapEquandsInConcl gls =
   let (lbeq,(t,e1,e2)) = find_eq_data_decompose (pf_concl gls) in
   let sym_equal = lbeq.sym in
-  refine (applist(sym_equal,[t;e2;e1;mkMeta (Clenv.new_meta())])) gls
+  refine (applist(sym_equal,[t;e2;e1;Evarutil.mk_new_meta()])) gls
 
 let swapEquandsInHyp id gls =
   ((tclTHENS (cut_replacing id (swap_equands gls (pf_get_hyp_typ gls id)))
@@ -880,8 +880,8 @@ let bareRevSubstInConcl lbeq body (t,e1,e2) gls =
     else
       (build_non_dependent_rewrite_predicate (t,e1,e2)  body  gls)
   in
-  refine (applist(eq_elim,[t;e1;p;mkMeta(Clenv.new_meta());
-                           e2;mkMeta(Clenv.new_meta())])) gls
+  refine (applist(eq_elim,[t;e1;p;Evarutil.mk_new_meta();
+                           e2;Evarutil.mk_new_meta()])) gls
 
 (* [subst_tuple_term dep_pair B]
 
-- 
cgit v1.2.3