diff options
| -rw-r--r-- | pretyping/evarutil.ml | 44 | ||||
| -rw-r--r-- | theories/Vectors/VectorDef.v | 15 | ||||
| -rw-r--r-- | toplevel/classes.ml | 16 |
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) |