diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/interface/blast.ml | 1 | ||||
| -rw-r--r-- | contrib/interface/xlate.ml | 21 | ||||
| -rw-r--r-- | contrib/subtac/subtac.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_classes.ml | 5 | ||||
| -rw-r--r-- | contrib/subtac/subtac_classes.mli | 1 | ||||
| -rw-r--r-- | contrib/subtac/subtac_pretyping_F.ml | 6 |
6 files changed, 27 insertions, 11 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index 82fbe9c691..7cc43e4ce8 100644 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -467,6 +467,7 @@ let rec search_gen decomp n db_list local_db extra_sign goal = try [make_apply_entry (pf_env g') (project g') (true,false) + None (mkVar hid,htyp)] with Failure _ -> [] in diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index db8963554b..4d28a22a98 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1727,7 +1727,7 @@ let rec xlate_vernac = CT_id_ne_list(n1, names), dblist) | HintsExtern (n, c, t) -> CT_hint_extern(CT_int n, xlate_formula c, xlate_tactic t, dblist) - | HintsResolve l | HintsImmediate l -> + | HintsImmediate l -> let f1, formulas = match List.map xlate_formula l with a :: tl -> a, tl | _ -> failwith "" in @@ -1744,6 +1744,23 @@ let rec xlate_vernac = HintsResolve _ -> CT_hints_resolve(l', dblist) | HintsImmediate _ -> CT_hints_immediate(l', dblist) | _ -> assert false) + | HintsResolve l -> + let f1, formulas = match List.map xlate_formula (List.map snd l) with + a :: tl -> a, tl + | _ -> failwith "" in + let l' = CT_formula_ne_list(f1, formulas) in + if local then + (match h with + HintsResolve _ -> + CT_local_hints_resolve(l', dblist) + | HintsImmediate _ -> + CT_local_hints_immediate(l', dblist) + | _ -> assert false) + else + (match h with + HintsResolve _ -> CT_hints_resolve(l', dblist) + | HintsImmediate _ -> CT_hints_immediate(l', dblist) + | _ -> assert false) | HintsUnfold l -> let n1, names = match List.map loc_qualid_to_ct_ID l with n1 :: names -> n1, names @@ -2083,7 +2100,7 @@ let rec xlate_vernac = (* TypeClasses *) | VernacDeclareInstance _|VernacContext _| - VernacInstance (_, _, _)|VernacClass (_, _, _, _, _) -> + VernacInstance (_, _, _, _)|VernacClass (_, _, _, _, _) -> xlate_error "TODO: Type Classes commands" | VernacResetName id -> CT_reset (xlate_ident (snd id)) diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index e9c2ed4e52..2d1be640b1 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -148,8 +148,8 @@ let subtac (loc, command) = | VernacAssumption (stre,nl,l) -> vernac_assumption env isevars stre l nl - | VernacInstance (sup, is, props) -> - ignore(Subtac_classes.new_instance sup is props) + | VernacInstance (sup, is, props, pri) -> + ignore(Subtac_classes.new_instance sup is props pri) | VernacCoFixpoint (l, b) -> let _ = trace (str "Building cofixpoint") in diff --git a/contrib/subtac/subtac_classes.ml b/contrib/subtac/subtac_classes.ml index e439021635..a2184a557e 100644 --- a/contrib/subtac/subtac_classes.ml +++ b/contrib/subtac/subtac_classes.ml @@ -100,7 +100,7 @@ let type_class_instance_params isevars env id n ctx inst subst = let substitution_of_constrs ctx cstrs = List.fold_right2 (fun c (na, _, _) acc -> (na, c) :: acc) cstrs ctx [] -let new_instance ctx (instid, bk, cl) props = +let new_instance ctx (instid, bk, cl) props pri = let env = Global.env() in let isevars = ref (Evd.create_evar_defs Evd.empty) in let bound = Implicit_quantifiers.ids_of_list (Termops.ids_of_context env) in @@ -211,11 +211,10 @@ let new_instance ctx (instid, bk, cl) props = let hook cst = let inst = { is_class = k; - is_name = id; + is_pri = pri; is_impl = cst; } in - Classes.add_instance_hint id; Impargs.declare_manual_implicits false (ConstRef cst) false imps; Typeclasses.add_instance inst in diff --git a/contrib/subtac/subtac_classes.mli b/contrib/subtac/subtac_classes.mli index 12a6e29549..c621f1516f 100644 --- a/contrib/subtac/subtac_classes.mli +++ b/contrib/subtac/subtac_classes.mli @@ -36,4 +36,5 @@ val new_instance : Topconstr.local_binder list -> typeclass_constraint -> binder_def_list -> + int option -> identifier diff --git a/contrib/subtac/subtac_pretyping_F.ml b/contrib/subtac/subtac_pretyping_F.ml index 5bcbf4db6c..730b12605e 100644 --- a/contrib/subtac/subtac_pretyping_F.ml +++ b/contrib/subtac/subtac_pretyping_F.ml @@ -572,11 +572,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | IsType -> (pretype_type empty_valcon env isevars lvar c).utj_val in let evd,_ = consider_remaining_unif_problems env !isevars in - let evd = nf_evar_defs evd in let evd = Typeclasses.resolve_typeclasses ~onlyargs:true ~all:false env (evars_of evd) evd in - let c' = nf_evar (evars_of evd) c' in - isevars := evd; - c' + isevars:=evd; + nf_evar (evars_of !isevars) c' (* TODO: comment faire remonter l'information si le typage a resolu des variables du sigma original. il faudrait que la fonction de typage |