From d9530632321c0b470ece6337cda2cf54d02d61eb Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 17 Jul 2017 12:57:43 +0200 Subject: 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. --- checker/environ.mli | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'checker/environ.mli') diff --git a/checker/environ.mli b/checker/environ.mli index 754c295d2..8e8d0fd49 100644 --- a/checker/environ.mli +++ b/checker/environ.mli @@ -46,7 +46,7 @@ val check_constraints : Univ.constraints -> env -> bool (* Constants *) val lookup_constant : constant -> env -> Cic.constant_body val add_constant : constant -> Cic.constant_body -> env -> env -val constant_type : env -> constant puniverses -> constant_type Univ.constrained +val constant_type : env -> constant puniverses -> constr Univ.constrained type const_evaluation_result = NoBody | Opaque | IsProj exception NotEvaluableConst of const_evaluation_result val constant_value : env -> constant puniverses -> constr -- cgit v1.2.3