diff options
| author | Pierre-Marie Pédrot | 2020-02-14 23:48:57 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-02-14 23:48:57 +0100 |
| commit | 4de476c53d85be4dd266cfe5fd5f2ddec9163a5b (patch) | |
| tree | 1f8cb4ea4350ee9dfef0d65a90aebdd3d939c1d5 /vernac | |
| parent | bdc8e29d806ab7e9bbd0491bf237890b7934795a (diff) | |
| parent | 0f58738351db02f30ac43ec52517c54b315d5886 (diff) | |
Merge PR #11557: Use thunks to univ instead of lazy constr for template typing
Reviewed-by: ppedrot
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/assumptions.ml | 3 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.ml | 2 | ||||
| -rw-r--r-- | vernac/record.ml | 2 |
3 files changed, 3 insertions, 4 deletions
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml index fb61a1089f..46f616c4ff 100644 --- a/vernac/assumptions.ml +++ b/vernac/assumptions.ml @@ -239,7 +239,6 @@ and traverse_inductive (curr, data, ax2ty) mind obj = in (* Build the context of all arities *) let arities_ctx = - let global_env = Global.env () in let instance = let open Univ in Instance.of_array @@ -250,7 +249,7 @@ and traverse_inductive (curr, data, ax2ty) mind obj = in Array.fold_left (fun accu oib -> let pspecif = ((mib, oib), instance) in - let ind_type = Inductive.type_of_inductive global_env pspecif in + let ind_type = Inductive.type_of_inductive pspecif in let indr = oib.mind_relevance in let ind_name = Name oib.mind_typename in Context.Rel.add (Context.Rel.Declaration.LocalAssum (make_annot ind_name indr, ind_type)) accu) diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 6bdb3159cf..bdf8511cce 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -178,7 +178,7 @@ let build_beq_scheme mode kn = (* current inductive we are working on *) let cur_packet = mib.mind_packets.(snd (fst ind)) in (* Inductive toto : [rettyp] := *) - let rettyp = Inductive.type_of_inductive env ((mib,cur_packet),u) in + let rettyp = Inductive.type_of_inductive ((mib,cur_packet),u) in (* split rettyp in a list without the non rec params and the last -> e.g. Inductive vec (A:Set) : nat -> Set := ... will do [nat] *) let rettyp_l = quick_chop nparrec (deconstruct_type rettyp) in diff --git a/vernac/record.ml b/vernac/record.ml index 27bd390714..3e44cd85cc 100644 --- a/vernac/record.ml +++ b/vernac/record.ml @@ -622,7 +622,7 @@ let add_inductive_class env sigma ind = let env = push_context ~strict:false (Univ.AUContext.repr univs) env in let env = push_rel_context ctx env in let inst = Univ.make_abstract_instance univs in - let ty = Inductive.type_of_inductive env ((mind, oneind), inst) in + let ty = Inductive.type_of_inductive ((mind, oneind), inst) in let r = Inductive.relevance_of_inductive env ind in { cl_univs = univs; cl_impl = GlobRef.IndRef ind; |