Permalink
Browse files

- Move Ring/Field back to Type. It was silently putting R in Set due …

…to the definition of ring_morph.

- Rework inference of universe levels for inductive definitions.
- Make fold_left/right polymorphic on both levels A and B (the list's type). They don't have to be
at the same level.
  • Loading branch information...
1 parent 1360b14 commit c0fa398bbc7a764bdf66036f1fba11b2f2360077 @mattam82 mattam82 committed Dec 19, 2012
View
8 plugins/micromega/EnvRing.v
@@ -30,15 +30,15 @@ Section MakeRingPol.
Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
(* Coefficients *)
- Variable C: Set.
+ Variable C: Type.
Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
Variable ceqb : C->C->bool.
Variable phi : C -> R.
Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi.
(* Power coefficients *)
- Variable Cpow : Set.
+ Variable Cpow : Type.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -108,7 +108,7 @@ Section MakeRingPol.
- (Pinj i (Pc c)) is (Pc c)
*)
- Inductive Pol : Set :=
+ Inductive Pol : Type :=
| Pc : C -> Pol
| Pinj : positive -> Pol -> Pol
| PX : Pol -> positive -> Pol -> Pol.
@@ -929,7 +929,7 @@ Qed.
(** Definition of polynomial expressions *)
- Inductive PExpr : Set :=
+ Inductive PExpr : Type :=
| PEc : C -> PExpr
| PEX : positive -> PExpr
| PEadd : PExpr -> PExpr -> PExpr
View
8 plugins/micromega/RingMicromega.v
@@ -49,15 +49,15 @@ Notation "x < y" := (rlt x y).
(* Assume we have a type of coefficients C and a morphism from C to R *)
-Variable C : Set.
+Variable C : Type.
Variables cO cI : C.
Variables cplus ctimes cminus: C -> C -> C.
Variable copp : C -> C.
Variables ceqb cleb : C -> C -> bool.
Variable phi : C -> R.
(* Power coefficients *)
-Variable E : Set. (* the type of exponents *)
+Variable E : Type. (* the type of exponents *)
Variable pow_phi : N -> E.
Variable rpow : R -> E -> R.
@@ -139,7 +139,7 @@ Qed.
(* Begin Micromega *)
-Definition PolC := Pol C : Set. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
+Definition PolC := Pol C. (* polynomials in generalized Horner form, defined in Ring_polynom or EnvRing *)
Definition PolEnv := Env R. (* For interpreting PolC *)
Definition eval_pol (env : PolEnv) (p:PolC) : R :=
Pphi rplus rtimes phi env p.
@@ -286,7 +286,7 @@ destruct o' ; rewrite H1 ; now rewrite (Rplus_0_l sor).
now apply (Rplus_nonneg_nonneg sor).
Qed.
-Inductive Psatz : Set :=
+Inductive Psatz : Type :=
| PsatzIn : nat -> Psatz
| PsatzSquare : PolC -> Psatz
| PsatzMulC : PolC -> Psatz -> Psatz
View
10 plugins/setoid_ring/Field_theory.v
@@ -48,7 +48,7 @@ Section AlmostField.
Let rinv_l := AFth.(AFinv_l).
(* Coefficients *)
- Variable C: Set.
+ Variable C: Type.
Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
Variable ceqb : C->C->bool.
Variable phi : C -> R.
@@ -109,7 +109,7 @@ Hint Resolve lem1 lem2 lem3 lem4 lem5 lem6 lem7 lem8 lem9 lem10
lem11 lem12 lem13 lem14 lem15 lem16 SRinv_ext.
(* Power coefficients *)
- Variable Cpow : Set.
+ Variable Cpow : Type.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -605,7 +605,7 @@ Qed.
(* The input: syntax of a field expression *)
-Inductive FExpr : Set :=
+Inductive FExpr : Type :=
FEc: C -> FExpr
| FEX: positive -> FExpr
| FEadd: FExpr -> FExpr -> FExpr
@@ -633,7 +633,7 @@ Strategy expand [FEeval].
(* The result of the normalisation *)
-Record linear : Set := mk_linear {
+Record linear : Type := mk_linear {
num : PExpr C;
denum : PExpr C;
condition : list (PExpr C) }.
@@ -856,7 +856,7 @@ destruct n.
trivial.
Qed.
-Record rsplit : Set := mk_rsplit {
+Record rsplit : Type := mk_rsplit {
rsplit_left : PExpr C;
rsplit_common : PExpr C;
rsplit_right : PExpr C}.
View
8 plugins/setoid_ring/Ring_polynom.v
@@ -27,15 +27,15 @@ Section MakeRingPol.
Variable ARth : almost_ring_theory rO rI radd rmul rsub ropp req.
(* Coefficients *)
- Variable C: Set.
+ Variable C: Type.
Variable (cO cI: C) (cadd cmul csub : C->C->C) (copp : C->C).
Variable ceqb : C->C->bool.
Variable phi : C -> R.
Variable CRmorph : ring_morph rO rI radd rmul rsub ropp req
cO cI cadd cmul csub copp ceqb phi.
(* Power coefficients *)
- Variable Cpow : Set.
+ Variable Cpow : Type.
Variable Cp_phi : N -> Cpow.
Variable rpow : R -> Cpow -> R.
Variable pow_th : power_theory rI rmul req Cp_phi rpow.
@@ -110,7 +110,7 @@ Section MakeRingPol.
- (Pinj i (Pc c)) is (Pc c)
*)
- Inductive Pol : Set :=
+ Inductive Pol : Type :=
| Pc : C -> Pol
| Pinj : positive -> Pol -> Pol
| PX : Pol -> positive -> Pol -> Pol.
@@ -908,7 +908,7 @@ Section MakeRingPol.
(** Definition of polynomial expressions *)
- Inductive PExpr : Set :=
+ Inductive PExpr : Type :=
| PEc : C -> PExpr
| PEX : positive -> PExpr
| PEadd : PExpr -> PExpr -> PExpr
View
4 theories/FSets/FSetPositive.v
@@ -161,7 +161,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
Section Fold.
- Variables B : Type.
+ Variable B : Type.
Variable f : positive -> B -> B.
(** the additional argument, [i], records the current path, in
@@ -759,7 +759,7 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
Proof. intros. rewrite diff_spec. split; assumption. Qed.
(** Specification of [fold] *)
-
+
Lemma fold_1: forall s (A : Type) (i : A) (f : elt -> A -> A),
fold f s i = fold_left (fun a e => f e a) (elements s) i.
Proof.
View
8 theories/Lists/List.v
@@ -830,7 +830,7 @@ End ListOps.
(************)
Section Map.
- Variables A B : Type.
+ Variables (A : Type) (B : Type).
Variable f : A -> B.
Fixpoint map (l:list A) : list B :=
@@ -940,7 +940,7 @@ Qed.
(************************************)
Section Fold_Left_Recursor.
- Variables A B : Type.
+ Variables (A : Type) (B : Type).
Variable f : A -> B -> A.
Fixpoint fold_left (l:list B) (a0:A) : A :=
@@ -978,7 +978,7 @@ Qed.
(************************************)
Section Fold_Right_Recursor.
- Variables A B : Type.
+ Variables (A : Type) (B : Type).
Variable f : B -> A -> A.
Variable a0 : A.
@@ -1165,7 +1165,7 @@ End Fold_Right_Recursor.
(******************************************************)
Section ListPairs.
- Variables A B : Type.
+ Variables (A : Type) (B : Type).
(** [split] derives two lists from a list of pairs *)
View
6 theories/ZArith/Zcomplements.v
@@ -53,11 +53,11 @@ Theorem Z_lt_abs_rec :
forall n:Z, P n.
Proof.
intros P HP p.
- set (Q := fun z => 0 <= z -> P z * P (- z) : Set).
- cut (Q (Z.abs p)); [ intros | apply (Z_lt_rec Q); auto with zarith ].
+ set (Q := fun z => 0 <= z -> P z * P (- z)).
+ cut (Q (Z.abs p)); [ intros H | apply (Z_lt_rec Q); auto with zarith ].
elim (Zabs_dec p); intro eq; rewrite eq;
elim H; auto with zarith.
- intros; subst Q.
+ intros x H; subst Q.
split; apply HP.
rewrite Z.abs_eq; auto; intros.
elim (H (Z.abs m)); intros; auto with zarith.
View
11 toplevel/command.ml
@@ -416,11 +416,16 @@ let interp_mutual_inductive (paramsl,indl) notations poly finite =
let evd = consider_remaining_unif_problems env_params !evdref in
evdref := Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env_params evd;
(* Compute renewed arities *)
- let arities = inductive_levels env_ar_params evdref arities constructors in
- let nf = e_nf_evars_and_universes evdref in
+ let nf = e_nf_evars_and_universes evdref in
+ let arities = List.map nf arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
+ let _ = List.iter (fun ty -> make_conclusion_flexible evdref ty) arities in
+ let arities = inductive_levels env_ar_params evdref arities constructors in
+ let nf' = e_nf_evars_and_universes evdref in
+ let nf x = nf' (nf x) in
+ let arities = List.map nf' arities in
+ let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
let ctx_params = Sign.map_rel_context nf ctx_params in
- let arities = List.map nf arities in
let evd = !evdref in
List.iter (check_evars env_params Evd.empty evd) arities;
Sign.iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;

0 comments on commit c0fa398

Please sign in to comment.