diff options
| author | barras | 2004-09-10 22:49:32 +0000 |
|---|---|---|
| committer | barras | 2004-09-10 22:49:32 +0000 |
| commit | 8089ee3421c4228fbf606f24ed49b33d6ec3145b (patch) | |
| tree | af7706aa547c4ed2113b9f231da1dc47f2c67455 /tactics/setoid_replace.ml | |
| parent | 112e6dced6dad495857a71c7a822f90d7d93d7d9 (diff) | |
simplification de clenv
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6096 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/setoid_replace.ml')
| -rw-r--r-- | tactics/setoid_replace.ml | 9 |
1 files changed, 4 insertions, 5 deletions
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml index 7961a7dc93..905ca60b45 100644 --- a/tactics/setoid_replace.ml +++ b/tactics/setoid_replace.ml @@ -961,9 +961,9 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl = Clenv.clenv_wtactic (fun evd-> fst (Unification.w_unify_to_subterm (pf_env gl) (c1,but) evd)) cl in - let c1 = Clenv.clenv_instance_term cl' c1 in - let c2 = Clenv.clenv_instance_term cl' c2 in - (lft2rgt,Clenv.clenv_instance_template cl'), c1, c2 + let c1 = Clenv.clenv_nf_meta cl' c1 in + let c2 = Clenv.clenv_nf_meta cl' c2 in + (lft2rgt,Clenv.clenv_value cl'), c1, c2 in let input_relation = relation_of_hypothesis_and_term_to_rewrite gl hyp c1 in let marked_but = mark_occur c1 but in @@ -979,8 +979,7 @@ let relation_rewrite c1 c2 (lft2rgt,cl) gl = let general_s_rewrite lft2rgt c gl = let ctype = pf_type_of gl c in let eqclause = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in - let (equiv, args) = - decompose_app (Clenv.clenv_instance_template_type eqclause) in + let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in let rec get_last_two = function | [c1;c2] -> (c1, c2) | x::y::z -> get_last_two (y::z) |