diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-07 19:28:25 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2004-09-07 19:28:25 +0000 |
| commit | d331f7f1ac0ec2ed12d458597d558a1988db1ba6 (patch) | |
| tree | 0e5addad213aeb1d647a0411285754e8a9cb23f6 /tactics/inv.ml | |
| parent | 11104cdcb1e53cd83768d2ce9858829b457e2d65 (diff) | |
deuxieme vague de modifs: evar_defs fonctionnel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index e74fc05a9..7c4456b3d 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -445,9 +445,8 @@ let rewrite_equations_tac (gene, othin) id neqns names ba = let raw_inversion inv_kind indbinding id status names gl = let env = pf_env gl and sigma = project gl in let c = mkVar id in - let (wc,kONT) = startWalk gl in let t = strong_prodspine (pf_whd_betadeltaiota gl) (pf_type_of gl c) in - let indclause = mk_clenv_from wc (c,t) in + let indclause = mk_clenv_from (rc_of_glsigma gl) (c,t) in let indclause' = clenv_constrain_with_bindings indbinding indclause in let newc = clenv_instance_template indclause' in let ccl = clenv_instance_template_type indclause' in |