diff options
| author | Hugo Herbelin | 2015-11-21 00:17:21 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-12-05 10:01:21 +0100 |
| commit | 6899d3aa567436784a08af4e179c2ef1fa504a02 (patch) | |
| tree | 41ff9881c85242d2f58eb59364be3d8fa14e851c /toplevel | |
| parent | e7f7fc3e0582867975642fcaa7bd42140c61cd99 (diff) | |
Moving extended_rel_vect/extended_rel_list to the kernel.
It will later be used to fix a bug and improve some code.
Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/auto_ind_decl.ml | 1 | ||||
| -rw-r--r-- | toplevel/class.ml | 1 | ||||
| -rw-r--r-- | toplevel/record.ml | 6 |
3 files changed, 5 insertions, 3 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml index e99b609b6c..98686fb1b7 100644 --- a/toplevel/auto_ind_decl.ml +++ b/toplevel/auto_ind_decl.ml @@ -15,6 +15,7 @@ open Util open Pp open Term open Vars +open Context open Termops open Declarations open Names diff --git a/toplevel/class.ml b/toplevel/class.ml index da6624032f..22baa5e61c 100644 --- a/toplevel/class.ml +++ b/toplevel/class.ml @@ -12,6 +12,7 @@ open Pp open Names open Term open Vars +open Context open Termops open Entries open Environ diff --git a/toplevel/record.ml b/toplevel/record.ml index dc2c9264b8..3a75004b08 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -244,8 +244,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field let ctx = Univ.instantiate_univ_context mib.mind_universes in let indu = indsp, u in let r = mkIndU (indsp,u) in - let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in - let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) + let rp = applist (r, Context.extended_rel_list 0 paramdecls) in + let paramargs = Context.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*) let x = Name binder_name in let fields = instantiate_possibly_recursive_type indu paramdecls fields in let lifted_fields = Termops.lift_rel_context 1 fields in @@ -353,7 +353,7 @@ open Typeclasses let declare_structure finite poly ctx id idbuild paramimpls params arity template fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign = let nparams = List.length params and nfields = List.length fields in - let args = Termops.extended_rel_list nfields params in + let args = Context.extended_rel_list nfields params in let ind = applist (mkRel (1+nparams+nfields), args) in let type_constructor = it_mkProd_or_LetIn ind fields in let binder_name = |