diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-19 08:11:07 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-11-22 11:33:57 +0100 |
| commit | 88afd8a9853c772b6b1681c7ae208e55e7daacbe (patch) | |
| tree | 7561c915ee289a94ea29ff5538fbafa004f4e901 /engine/proofview.ml | |
| parent | 23f0f5fe6b510d2ab91a2917eb895faa479d9fcf (diff) | |
[api] Deprecate Term destructors, move to Constr
We mirror the structure of EConstr and move the destructors from `Term`
to `Constr`.
This is a step towards having a single module for `Constr`.
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index 598358c47..3b945c87f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1200,7 +1200,7 @@ module V82 = struct { Evd.it = comb ; sigma = solution } let top_goals initial { solution=solution; } = - let goals = CList.map (fun (t,_) -> fst (Term.destEvar (EConstr.Unsafe.to_constr t))) initial in + let goals = CList.map (fun (t,_) -> fst (Constr.destEvar (EConstr.Unsafe.to_constr t))) initial in { Evd.it = goals ; sigma=solution; } let top_evars initial = |