aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-23 16:16:46 +0000
committerGravatar msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-03-23 16:16:46 +0000
commit0714753208a4c9c85c33f72f05245674a842eba2 (patch)
treeda716d88d20865c0f0a0f60817444cfd99e86b76
parentcdc52320d764eb7cd005e2b535bc1c1dab59bbb5 (diff)
- Fix solve_simpl_eqn which was cheking instances types in the wrong environment sometimes.
- Remove compilation warning in classes.ml due to (as yet) unused code. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13924 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--pretyping/evarutil.ml44
-rw-r--r--theories/Vectors/VectorDef.v15
-rw-r--r--toplevel/classes.ml16
3 files changed, 27 insertions, 48 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index b88ea03e1..1df6a3d4e 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1295,24 +1295,6 @@ let status_changed lev (pbty,_,t1,t2) =
(try ExistentialSet.mem (head_evar t1) lev with NoHeadEvar -> false) or
(try ExistentialSet.mem (head_evar t2) lev with NoHeadEvar -> false)
-(* Util *)
-
-let check_instance_type conv_algo pbty env evd ev1 t2 =
- let t2 = nf_evar evd t2 in
- if has_undefined_evars_or_sorts evd t2 then
- (* May contain larger constraints than needed: don't want to
- commit to an equal solution while only subtyping is requested *)
- evd
- else
- let typ2 = Retyping.get_type_of env evd (refresh_universes t2) in
- if isEvar typ2 then (* Don't want to commit too early too *) evd
- else
- let typ1 = existential_type evd ev1 in
- let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
- if b then evd else
- user_err_loc (fst (evar_source (fst ev1) evd),"",
- str "Unable to find a well-typed instantiation")
-
(* Tries to solve problem t1 = t2.
* Precondition: t1 is an uninstantiated evar
* Returns an optional list of evars that were instantiated, or None
@@ -1334,19 +1316,23 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
else
add_conv_pb (Reduction.CUMUL,env,t2,mkEvar ev1) evd
| _ ->
- let evd = check_instance_type conv_algo pbty env evd ev1 t2 in
let evd = evar_define ~choose env ev1 t2 evd in
let evi = Evd.find evd evk1 in
- if occur_existential evd evi.evar_concl then
- let evenv = evar_unfiltered_env evi in
- let evc = nf_evar evd evi.evar_concl in
- match evi.evar_body with
- | Evar_defined body ->
- let ty = nf_evar evd (Retyping.get_type_of evenv evd body) in
- add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
- | Evar_empty -> (* Resulted in a constraint *)
- evd
- else evd
+ let evenv = evar_unfiltered_env evi in
+ let evc = nf_evar evd evi.evar_concl in
+ match evi.evar_body with
+ | Evar_defined body ->
+ let ty = nf_evar evd (Retyping.get_type_of evenv evd body) in
+ if occur_existential evd evi.evar_concl
+ || occur_existential evd ty
+ then add_conv_pb (Reduction.CUMUL,evenv,ty,evc) evd
+ else
+ let evd,b = conv_algo evenv evd Reduction.CUMUL ty evc in
+ if b then evd else
+ user_err_loc (fst (evar_source (fst ev1) evd),"",
+ str "Unable to find a well-typed instantiation")
+ | Evar_empty -> (* Resulted in a constraint *)
+ evd
in
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
List.fold_left
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index d26af7876..cac37ae28 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -38,11 +38,7 @@ Definition rectS {A} (P:forall {n}, t A (S n) -> Type)
(bas: forall a: A, P (a :: []))
(rect: forall a {n} (v: t A (S n)), P v -> P (a :: v)) :=
fix rectS_fix {n} (v: t A (S n)) : P v :=
- match v in t _ n' return match n' return t _ n' -> Type with
- | 0 => fun _ => ID
- | S n => fun v => P v
- end v
- with
+ match v with
|nil => @id
|cons a 0 v =>
match v as vnn in t _ nn
@@ -67,9 +63,7 @@ fix rect2_fix {n} (v1:t A n):
match v1 as v1' in t _ n1
return forall v2 : t B n1, P v1' v2 with
|[] => fun v2 =>
- match v2 as v2' in t _ n2
- return match n2 as n2' return t B n2' -> Type with
- |0 => fun v2 => P [] v2 |S _ => fun _ => @ID end v2' with
+ match v2 with
|[] => bas
|_ :: _ => @id
end
@@ -89,15 +83,14 @@ end.
(** A vector of length [0] is [nil] *)
Definition case0 {A} (P:t A 0 -> Type) (H:P (nil A)) v:P v :=
-match v as v0 in t _ n return match n return t _ n -> Type with 0 => fun v => P v | S n => fun v => ID end v0 with
+match v with
|[] => H
- | _ => @id
end.
(** A vector of length [S _] is [cons] *)
Definition caseS {A} (P : forall n, t A (S n) -> Type)
(H : forall h {n} t, @P n (h :: t)) {n} v : P n v :=
-match v as v0 in t _ n return match n return t _ n -> Type with 0 => fun v => ID | S n => fun v => P n v end v0 with
+match v with
|[] => @id (* Why needed ? *)
|h :: t => H h t
end.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 4f1df4bb9..7786b200b 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -310,7 +310,7 @@ let rec declare_subclasses gr (rels, (tc, args)) =
add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
declare_subclasses (ConstRef cst) cl
| None -> ()
- in () (* List.iter declare_proj projs *)
+ in List.iter declare_proj projs
let context l =
let env = Global.env() in
@@ -328,9 +328,9 @@ let context l =
(ParameterEntry (t,None), IsAssumption Logical)
in
match class_of_constr t with
- | Some (rels, (tc, args) as cl) ->
- add_instance (Typeclasses.new_instance tc None false (ConstRef cst));
- declare_subclasses (ConstRef cst) cl
+ | Some (rels, (tc, args) as _cl) ->
+ add_instance (Typeclasses.new_instance tc None false (ConstRef cst))
+ (* declare_subclasses (ConstRef cst) cl *)
| None -> ()
else (
let impl = List.exists
@@ -338,9 +338,9 @@ let context l =
match x with ExplByPos (_, Some id') -> id = id' | _ -> false) impls
in
Command.declare_assumption false (Local (* global *), Definitional) t
- [] impl (* implicit *) None (* inline *) (dummy_loc, id);
- match class_of_constr t with
- | None -> ()
- | Some tc -> declare_subclasses (VarRef id) tc)
+ [] impl (* implicit *) None (* inline *) (dummy_loc, id))
+(* match class_of_constr t with *)
+(* | None -> () *)
+(* | Some tc -> declare_subclasses (VarRef id) tc) *)
in List.iter fn (List.rev ctx)