From 68935660fbfdec2e357e123ed999073ed3b8fc26 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 11 Feb 2018 16:00:04 +0100 Subject: [engine] Remove ghost parameter from `Proofview.Goal.t` In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code. --- plugins/cc/cctac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/cc') 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 -- cgit v1.2.3