From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 1 Apr 2017 02:36:16 +0200 Subject: Using delayed universe instances in EConstr. The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step. --- plugins/cc/cctac.ml | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'plugins/cc') diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index c9c904e35..2d9dec095 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -66,6 +66,7 @@ let rec decompose_term env sigma t= decompose_term env sigma b) | Construct c -> let (((mind,i_ind),i_con),u)= c in + let u = EInstance.kind sigma u in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in let (oib,_)=Global.lookup_inductive (canon_ind) in @@ -75,9 +76,11 @@ let rec decompose_term env sigma t= ci_nhyps=nargs-oib.mind_nparams} | Ind c -> let (mind,i_ind),u = c in + let u = EInstance.kind sigma u in let canon_mind = mind_of_kn (canonical_mind mind) in let canon_ind = canon_mind,i_ind in (Symb (Constr.mkIndU (canon_ind,u))) | Const (c,u) -> + let u = EInstance.kind sigma u in let canon_const = constant_of_kn (canonical_con c) in (Symb (Constr.mkConstU (canon_const,u))) | Proj (p, c) -> @@ -408,7 +411,8 @@ let build_term_to_complete uf meta pac = let real_args = List.map (fun i -> constr_of_term (term uf i)) pac.args in let dummy_args = List.rev (List.init pac.arity meta) in let all_args = List.rev_append real_args dummy_args in - applist (mkConstructU cinfo.ci_constr, all_args) + let (kn, u) = cinfo.ci_constr in + applist (mkConstructU (kn, EInstance.make u), all_args) let cc_tactic depth additionnal_terms = Proofview.Goal.enter { enter = begin fun gl -> -- cgit v1.2.3