diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 10 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 4 |
2 files changed, 7 insertions, 7 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 9cc6f9de93..9b5fca4da1 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -668,11 +668,11 @@ let __eps__ = id_of_string "_eps_" let new_state_var typ state = let id = pf_get_new_id __eps__ state.gls in - state.gls<- - {state.gls with it = - {state.gls.it with evar_hyps = - Environ.push_named_context_val (id,None,typ) - state.gls.it.evar_hyps}}; + let {it=gl ; sigma=sigma} = state.gls in + let new_hyps = + Environ.push_named_context_val (id,None,typ) (Goal.V82.hyps sigma gl) in + let gls = Goal.V82.new_goal_with sigma gl new_hyps in + state.gls<- gls; id let complete_one_class state i= diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 4e6ea8022e..ccfa2a0a70 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -204,9 +204,9 @@ let rec make_prb gls depth additionnal_terms = neg_hyps:=(cid,nh):: !neg_hyps | `Rule patts -> add_quant state id true patts | `Nrule patts -> add_quant state id false patts - end) (Environ.named_context_of_val gls.it.evar_hyps); + end) (Environ.named_context_of_val (Goal.V82.hyps gls.sigma gls.it)); begin - match atom_of_constr env sigma gls.it.evar_concl with + match atom_of_constr env sigma (pf_concl gls) with `Eq (t,a,b) -> add_disequality state Goal a b | `Other g -> List.iter |