diff options
| -rw-r--r-- | checker/subtyping.ml | 2 | ||||
| -rw-r--r-- | checker/typeops.ml | 4 | ||||
| -rw-r--r-- | doc/refman/RefMan-cic.tex | 12 | ||||
| -rw-r--r-- | doc/refman/RefMan-pre.tex | 2 | ||||
| -rw-r--r-- | engine/universes.mli | 2 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 2 | ||||
| -rw-r--r-- | kernel/typeops.ml | 4 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 4 | ||||
| -rw-r--r-- | pretyping/typing.ml | 3 | ||||
| -rw-r--r-- | proofs/logic.ml | 2 | ||||
| -rw-r--r-- | test-suite/failure/proofirrelevance.v | 5 | ||||
| -rw-r--r-- | test-suite/success/Case19.v | 2 |
12 files changed, 21 insertions, 23 deletions
diff --git a/checker/subtyping.ml b/checker/subtyping.ml index 7eae9b831..a290b240d 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -113,7 +113,7 @@ let check_inductive env mp1 l info1 mib2 spec2 subst1 subst2= in let check_inductive_type env t1 t2 = - (* Due to sort-polymorphism in inductive types, the conclusions of + (* Due to template polymorphism, the conclusions of t1 and t2, if in Type, are generated as the least upper bounds of the types of the constructors. diff --git a/checker/typeops.ml b/checker/typeops.ml index 02d801741..1396d56df 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -275,13 +275,11 @@ let rec execute env cstr = let j = match f with | Ind ind -> - (* Sort-polymorphism of inductive types *) judge_of_inductive_knowing_parameters env ind jl | Const cst -> - (* Sort-polymorphism of constant *) judge_of_constant_knowing_parameters env cst jl | _ -> - (* No sort-polymorphism *) + (* No template polymorphism *) execute env f in let jl = Array.map2 (fun c ty -> c,ty) args jl in diff --git a/doc/refman/RefMan-cic.tex b/doc/refman/RefMan-cic.tex index b9c17d814..fdd272581 100644 --- a/doc/refman/RefMan-cic.tex +++ b/doc/refman/RefMan-cic.tex @@ -79,8 +79,8 @@ An algebraic universe $u$ is either a variable (a qualified identifier with a number) or a successor of an algebraic universe (an expression $u+1$), or an upper bound of algebraic universes (an expression $max(u_1,...,u_n)$), or the base universe (the expression -$0$) which corresponds, in the arity of sort-polymorphic inductive -types (see Section \ref{Sort-polymorphism-inductive}), +$0$) which corresponds, in the arity of template polymorphic inductive +types (see Section \ref{Template-polymorphism}), to the predicative sort {\Set}. A graph of constraints between the universe variables is maintained globally. To ensure the existence of a mapping of the universes to the positive integers, the graph of @@ -977,8 +977,8 @@ Inductive exType (P:Type->Prop) : Type := %is recursive or not. We shall write the type $(x:_R T)C$ if it is %a recursive argument and $(x:_P T)C$ if the argument is not recursive. -\paragraph[Sort-polymorphism of inductive types.]{Sort-polymorphism of inductive types.\index{Sort-polymorphism of inductive types}} -\label{Sort-polymorphism-inductive} +\paragraph[Template polymorphism.]{Template polymorphism.\index{Template polymorphism}} +\label{Template-polymorphism} Inductive types declared in {\Type} are polymorphic over their arguments in {\Type}. @@ -1120,6 +1120,10 @@ Check (fun (A:Prop) (B:Set) => prod A B). Check (fun (A:Type) (B:Prop) => prod A B). \end{coq_example} +\Rem Template polymorphism used to be called ``sort-polymorphism of +inductive types'' before universe polymorphism (see +Chapter~\ref{Universes-full}) was introduced. + \subsection{Destructors} The specification of inductive definitions with arities and constructors is quite natural. But we still have to say how to use an diff --git a/doc/refman/RefMan-pre.tex b/doc/refman/RefMan-pre.tex index f36969e82..0441f952d 100644 --- a/doc/refman/RefMan-pre.tex +++ b/doc/refman/RefMan-pre.tex @@ -529,7 +529,7 @@ intensive computations. Christine Paulin implemented an extension of inductive types allowing recursively non uniform parameters. Hugo Herbelin implemented -sort-polymorphism for inductive types. +sort-polymorphism for inductive types (now called template polymorphism). Claudio Sacerdoti Coen improved the tactics for rewriting on arbitrary compatible equivalence relations. He also generalized rewriting to diff --git a/engine/universes.mli b/engine/universes.mli index 932de941a..83ca1ea60 100644 --- a/engine/universes.mli +++ b/engine/universes.mli @@ -223,7 +223,7 @@ val refresh_constraints : UGraph.t -> universe_context_set -> universe_context_s val pr_universe_opt_subst : universe_opt_subst -> Pp.std_ppcmds -(** {6 Support for old-style sort-polymorphism } *) +(** {6 Support for template polymorphism } *) val solve_constraints_system : universe option array -> universe array -> universe array -> universe array diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index c8ceb064d..d0fdf9fda 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -117,7 +117,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2 let mib2 = Declareops.subst_mind_body subst2 mib2 in let check_inductive_type cst name env t1 t2 = - (* Due to sort-polymorphism in inductive types, the conclusions of + (* Due to template polymorphism, the conclusions of t1 and t2, if in Type, are generated as the least upper bounds of the types of the constructors. diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7d9a2aac0..dbc0dcb73 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -367,15 +367,13 @@ let rec execute env cstr = let ft = match kind_of_term f with | Ind ind when Environ.template_polymorphic_pind ind env -> - (* Template sort-polymorphism of inductive types *) let args = Array.map (fun t -> lazy t) argst in type_of_inductive_knowing_parameters env ind args | Const cst when Environ.template_polymorphic_pconstant cst env -> - (* Template sort-polymorphism of constants *) let args = Array.map (fun t -> lazy t) argst in type_of_constant_knowing_parameters env cst args | _ -> - (* Full or no sort-polymorphism *) + (* No template polymorphism *) execute env f in diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index c26e7458e..e6c0075c5 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -478,8 +478,8 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 = (* We eta-expand (hence possibly modifying the original term!) *) (* and look for a coercion c:u1->t1 s.t. fun x:u1 => v' (c x)) *) (* has type forall (x:u1), u2 (with v' recursively obtained) *) - (* Note: we retype the term because sort-polymorphism may have *) - (* weaken its type *) + (* Note: we retype the term because template polymorphism may have *) + (* weakened its type *) let name = match name with | Anonymous -> Name Namegen.default_dependent_ident | _ -> name in diff --git a/pretyping/typing.ml b/pretyping/typing.ml index c2a030bcd..00535adb7 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -313,14 +313,13 @@ let rec execute env evdref cstr = let j = match EConstr.kind !evdref f with | Ind (ind, u) when EInstance.is_empty u && Environ.template_polymorphic_ind ind env -> - (* Sort-polymorphism of inductive types *) make_judge f (inductive_type_knowing_parameters env !evdref (ind, u) jl) | Const (cst, u) when EInstance.is_empty u && Environ.template_polymorphic_constant cst env -> - (* Sort-polymorphism of inductive types *) make_judge f (constant_type_knowing_parameters env !evdref (cst, u) jl) | _ -> + (* No template polymorphism *) execute env evdref f in e_judge_of_apply env evdref j jl diff --git a/proofs/logic.ml b/proofs/logic.ml index 9ab8c34d8..54345abd9 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -374,7 +374,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm = let (acc',hdty,sigma,applicand) = if is_template_polymorphic env sigma (EConstr.of_constr f) then let ty = - (* Template sort-polymorphism of definition and inductive types *) + (* Template polymorphism of definitions and inductive types *) let firstmeta = Array.findi (fun i x -> occur_meta sigma (EConstr.of_constr x)) l in let args, _ = Option.cata (fun i -> CArray.chop i l) (l, [||]) firstmeta in type_of_global_reference_knowing_parameters env sigma (EConstr.of_constr f) (Array.map EConstr.of_constr args) diff --git a/test-suite/failure/proofirrelevance.v b/test-suite/failure/proofirrelevance.v index b62f9b686..bb9579d48 100644 --- a/test-suite/failure/proofirrelevance.v +++ b/test-suite/failure/proofirrelevance.v @@ -1,6 +1,5 @@ -(* This was working in version 8.1beta (bug in the Sort-polymorphism - of inductive types), but this is inconsistent with classical logic - in Prop *) +(* This was working in version 8.1beta (bug in template polymorphism), + but this is inconsistent with classical logic in Prop *) Inductive bool_in_prop : Type := hide : bool -> bool_in_prop with bool : Type := true : bool | false : bool. diff --git a/test-suite/success/Case19.v b/test-suite/success/Case19.v index c29e52978..e59828def 100644 --- a/test-suite/success/Case19.v +++ b/test-suite/success/Case19.v @@ -1,5 +1,5 @@ (* This used to fail in Coq version 8.1 beta due to a non variable - universe (issued by the inductive sort-polymorphism) being sent by + universe (issued by template polymorphism) being sent by pretyping to the kernel (bug #1182) *) Variable T : Type. |