From 2d747797c427818cdf85d0a0d701c7c9b0106b82 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 20 Oct 2015 16:12:39 +0200 Subject: Proofview.Goal.sigma returns an indexed evarmap. --- 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 35178aa1e..8c15f54af 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -385,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p = let identity = Universes.constr_of_global (Lazy.force _I) in (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in let outtype = mkSort outtype in let pred=mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in -- cgit v1.2.3