diff options
| author | barras | 2004-09-12 11:38:09 +0000 |
|---|---|---|
| committer | barras | 2004-09-12 11:38:09 +0000 |
| commit | 34bc13e0ef3642244fe77fe8a8a7869fbc8d2fca (patch) | |
| tree | 1b681cce520d8ba260651969ee96d0fb313ef166 /tactics/equality.ml | |
| parent | 5cd3851617123736fafa3b81688bb63d850b9dd4 (diff) | |
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
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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] |