diff options
| author |  Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 12:34:30 +0100 |
|---|---|---|
| committer | Matej Kosik <m4tej.kosik@gmail.com> | 2016-01-11 12:34:30 +0100 |
| commit | 78bad016e389cd78635d40281bfefd7136733b7e (patch) | |
| tree | 51f90da34d2444734868d7954412ac08ddc0f5c6 /tactics/equality.ml | |
| parent | f8eb2ed4ddbe2199187696f51c42734014f4d9d0 (diff) | |
| parent | 9d991d36c07efbb6428e277573bd43f6d56788fc (diff) | |
merge
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 1854b4120..ac41c9464 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1574,7 +1574,7 @@ let unfold_body x = Proofview.Goal.enter { enter = begin fun gl -> (** We normalize the given hypothesis immediately. *) let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in - let (_, xval, _) = Context.lookup_named x hyps in + let (_, xval, _) = Context.Named.lookup x hyps in let xval = match xval with | None -> errorlabstrm "unfold_body" (pr_id x ++ str" is not a defined hypothesis.") @@ -1656,7 +1656,7 @@ let subst_one_var dep_proof_ok x = (** [is_eq_x] ensures nf_evar on its side *) let hyps = Proofview.Goal.hyps gl in let test hyp _ = is_eq_x gl varx hyp in - Context.fold_named_context test ~init:() hyps; + Context.Named.fold_outside test ~init:() hyps; errorlabstrm "Subst" (str "Cannot find any non-recursive equality over " ++ pr_id x ++ str".") |