diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-17 12:57:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-07-26 15:17:12 +0200 |
| commit | d9530632321c0b470ece6337cda2cf54d02d61eb (patch) | |
| tree | dd8ef37eddb9a3244c85e7cf042c5168edc95e12 /checker/typeops.ml | |
| parent | 906b48ff401f22be6059a6cdde8723b858102690 (diff) | |
Removing template polymorphism for definitions.
The use of template polymorphism in constants was quite limited, as it
only applied to definitions that were exactly inductive types without any
parameter whatsoever. Furthermore, it seems that following the introduction
of polymorphic definitions, the code path enforced regular polymorphism as
soon as the type of a definition was given, which was in practice almost
always.
Removing this feature had no observable effect neither on the test-suite,
nor on any development that we monitor on Travis. I believe it is safe to
assume it was nowadays useless.
Diffstat (limited to 'checker/typeops.ml')
| -rw-r--r-- | checker/typeops.ml | 25 |
1 files changed, 2 insertions, 23 deletions
diff --git a/checker/typeops.ml b/checker/typeops.ml index f2cbfec7d..9f39d588a 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -69,35 +69,16 @@ let judge_of_relative env n = (* Type of constants *) - -let type_of_constant_type_knowing_parameters env t paramtyps = - match t with - | RegularArity t -> t - | TemplateArity (sign,ar) -> - let ctx = List.rev sign in - let ctx,s = instantiate_universes env ctx ar paramtyps in - mkArity (List.rev ctx,s) - -let type_of_constant_knowing_parameters env cst paramtyps = - let ty, cu = constant_type env cst in - type_of_constant_type_knowing_parameters env ty paramtyps, cu - -let type_of_constant_type env t = - type_of_constant_type_knowing_parameters env t [||] - -let judge_of_constant_knowing_parameters env (kn,u as cst) paramstyp = +let judge_of_constant env (kn,u as cst) = let _cb = try lookup_constant kn env with Not_found -> failwith ("Cannot find constant: "^Constant.to_string kn) in - let ty, cu = type_of_constant_knowing_parameters env cst paramstyp in + let ty, cu = constant_type env cst in let () = check_constraints cu env in ty -let judge_of_constant env cst = - judge_of_constant_knowing_parameters env cst [||] - (* Type of an application. *) let judge_of_apply env (f,funj) argjv = @@ -276,8 +257,6 @@ let rec execute env cstr = match f with | Ind ind -> judge_of_inductive_knowing_parameters env ind jl - | Const cst -> - judge_of_constant_knowing_parameters env cst jl | _ -> (* No template polymorphism *) execute env f |