diff options
| author | Maxime Dénès | 2017-11-23 17:36:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-23 17:36:03 +0100 |
| commit | 915554785ffed11370f5d700d11a8b5614408096 (patch) | |
| tree | 4b5b4120c896cf99c863fab4fd5e1ec22af20d53 /engine/proofview.ml | |
| parent | ebe133a0df0656de82a566c4f1673257f60f7c0c (diff) | |
| parent | 9f47342d890dc3ef7f4950004513a47d940af5ca (diff) | |
Merge PR #6186: [api] Miscellaneous consolidation.
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 598358c472..3b945c87f9 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 = |