diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:12:52 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-19 11:12:52 +0100 |
| commit | eaff61e0a19fcf6ebc2a9a8ae17327413274c67b (patch) | |
| tree | acbbc416ad78bf8520893405c04855c600909576 /plugins/cc | |
| parent | 073b92396a68be30f77c80960a58ca562bb01f49 (diff) | |
| parent | 68935660fbfdec2e357e123ed999073ed3b8fc26 (diff) | |
Merge PR #6771: [engine] Remove ghost parameter from `Proofview.Goal.t`
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/cctac.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 8642df684..7f8f60e46 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -187,7 +187,7 @@ let make_prb gls depth additionnal_terms = let open Tacmach.New in let env=pf_env gls in let sigma=project gls in - let state = empty depth {it = Proofview.Goal.goal (Proofview.Goal.assume gls); sigma } in + let state = empty depth {it = Proofview.Goal.goal gls; sigma } in let pos_hyps = ref [] in let neg_hyps =ref [] in List.iter |