diff options
-rw-r--r-- | CHANGES | 2 | ||||
-rw-r--r-- | pretyping/cases.ml | 2 | ||||
-rw-r--r-- | pretyping/coercion.ml | 10 | ||||
-rw-r--r-- | pretyping/typeclasses.ml | 3 | ||||
-rw-r--r-- | pretyping/typeclasses.mli | 1 | ||||
-rw-r--r-- | tactics/class_tactics.ml4 | 19 | ||||
-rw-r--r-- | test-suite/bugs/closed/shouldsucceed/2083.v | 2 | ||||
-rw-r--r-- | test-suite/success/ProgramWf.v | 4 | ||||
-rw-r--r-- | theories/Classes/Morphisms.v | 2 | ||||
-rw-r--r-- | toplevel/classes.ml | 2 | ||||
-rw-r--r-- | toplevel/command.ml | 11 | ||||
-rw-r--r-- | toplevel/g_obligations.ml4 | 8 | ||||
-rw-r--r-- | toplevel/obligations.ml | 44 | ||||
-rw-r--r-- | toplevel/obligations.mli | 6 | ||||
-rw-r--r-- | toplevel/vernacentries.ml | 4 |
15 files changed, 86 insertions, 34 deletions
@@ -4,6 +4,8 @@ Changes from V8.4 Tactics - Tactics btauto, a reflexive boolean tautology solver. +- "Solve Obligations using" changed to "Solve Obligations with", + consistent with "Proof with". Changes from V8.4beta to V8.4 ============================= diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 0f7705317..871f161ab 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -337,6 +337,8 @@ let coerce_row typing_fun evdref env pats (tomatch,(_,indopt)) = let loc = Some (loc_of_glob_constr tomatch) in let tycon,realnames = find_tomatch_tycon evdref env loc indopt in let j = typing_fun tycon env evdref tomatch in + let evd, j = Coercion.inh_coerce_to_base (loc_of_glob_constr tomatch) env !evdref j in + evdref := evd; let typ = nf_evar !evdref j.uj_type in let t = try try_find_ind env !evdref typ realnames diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 2b93a5fca..327745616 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -219,8 +219,11 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr) let (evs, t) = Evarutil.define_evar_as_lambda env !isevars (k,args) in isevars := evs; let (n, dom, rng) = destLambda t in - let (domk, args) = destEvar dom in - isevars := define domk a !isevars; + let dom = whd_evar !isevars dom in + if isEvar dom then + let (domk, args) = destEvar dom in + isevars := define domk a !isevars; + else (); t, rng | _ -> raise NoSubtacCoercion in @@ -228,8 +231,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr) let env' = push_rel (make_name "x", None, a) env in let c2 = coerce_unify env' b b' in match c1, c2 with - None, None -> - None + | None, None -> None | _, _ -> Some (fun x -> diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 8fe06539c..be335ac91 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -480,9 +480,10 @@ let mark_resolvability_undef b evi = let mark_resolvability b evi = assert (evi.evar_body = Evar_empty); - mark_resolvability_undef false evi + mark_resolvability_undef b evi let mark_unresolvable evi = mark_resolvability false evi +let mark_resolvable evi = mark_resolvability true evi let mark_resolvability b sigma = Evd.fold_undefined (fun ev evi evs -> diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index 3d36168fd..67336b340 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -85,6 +85,7 @@ val instance_constructor : typeclass -> constr list -> constr option * types val is_resolvable : evar_info -> bool val mark_unresolvable : evar_info -> evar_info val mark_unresolvables : evar_map -> evar_map +val mark_resolvable : evar_info -> evar_info val mark_resolvables : evar_map -> evar_map val is_class_evar : evar_map -> evar_info -> bool diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4 index 4a850db66..125ef94dc 100644 --- a/tactics/class_tactics.ml4 +++ b/tactics/class_tactics.ml4 @@ -635,6 +635,23 @@ let has_undefined p oevd evd = snd (p oevd ev evi)) evd false +(** Revert the resolvability status of evars after resolution, + potentially unprotecting some evars that were set unresolvable + just for this call to resolution. *) + +let revert_resolvability oevd evd = + Evd.fold_undefined + (fun ev evi evm -> + try + if not (Typeclasses.is_resolvable evi) then + let evi' = Evd.find_undefined oevd ev in + if Typeclasses.is_resolvable evi' then + Evd.add evm ev (Typeclasses.mark_resolvable evi) + else evm + else evm + with Not_found -> evm) + evd evd + (** If [do_split] is [true], we try to separate the problem in several components and then solve them separately *) @@ -645,7 +662,7 @@ let resolve_all_evars debug m env p oevd do_split fail = let in_comp comp ev = if do_split then Intset.mem ev comp else true in let rec docomp evd = function - | [] -> evd + | [] -> revert_resolvability oevd evd | comp :: comps -> let p = select_and_update_evars p oevd (in_comp comp) in try diff --git a/test-suite/bugs/closed/shouldsucceed/2083.v b/test-suite/bugs/closed/shouldsucceed/2083.v index a6ce4de0f..5f17f7af3 100644 --- a/test-suite/bugs/closed/shouldsucceed/2083.v +++ b/test-suite/bugs/closed/shouldsucceed/2083.v @@ -15,7 +15,7 @@ Program Fixpoint check_n (n : nat) (P : { i | i < n } -> bool) (p : nat) Require Import Omega. -Solve Obligations using program_simpl ; auto with *; try omega. +Solve Obligations with program_simpl ; auto with *; try omega. Next Obligation. apply H. simpl. omega. diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v index 00a13aed0..f8d3ad2c3 100644 --- a/test-suite/success/ProgramWf.v +++ b/test-suite/success/ProgramWf.v @@ -100,6 +100,6 @@ Next Obligation. simpl in *; intros. apply H. simpl. omega. Qed. -Program Fixpoint check_n' (n : nat) (m : nat | m = n) (p : nat) (q : nat | q = p) +Program Fixpoint check_n' (n : nat) (m : {m:nat | m = n}) (p : nat) (q:{q : nat | q = p}) {measure (p - n) p} : nat := - _. + _.
\ No newline at end of file diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index e0d7a3d7a..8e491b1b8 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -224,7 +224,7 @@ Hint Extern 4 (subrelation (inverse _) _) => class_apply @subrelation_symmetric : typeclass_instances. (** The complement of a relation conserves its proper elements. *) -Set Printing All. + Program Definition complement_proper `(mR : Proper (A -> A -> Prop) (RA ==> RA ==> iff) R) : Proper (RA ==> RA ==> iff) (complement R) := _. diff --git a/toplevel/classes.ml b/toplevel/classes.ml index ceaab3d0f..9d259eee1 100644 --- a/toplevel/classes.ml +++ b/toplevel/classes.ml @@ -280,7 +280,7 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props match term with | Some t -> let obls, _, constr, typ = - Obligations.eterm_obligations env id !evars evm 0 t termtype + Obligations.eterm_obligations env id !evars 0 t termtype in obls, Some constr, typ | None -> [||], None, termtype in diff --git a/toplevel/command.ml b/toplevel/command.ml index 0b4e9daa1..3657c5d5a 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -141,9 +141,9 @@ let do_definition ident k bl red_option c ctypopt hook = | Some t -> t | None -> Retyping.get_type_of env evd c in - let evm = Obligations.non_instanciated_map env (ref evd) evd in + Obligations.check_evars env evd; let obls, _, c, cty = - Obligations.eterm_obligations env ident evd evm 0 c typ + Obligations.eterm_obligations env ident evd 0 c typ in ignore(Obligations.add_definition ident ~term:c cty ~implicits:imps ~kind:k ~hook obls) else let ce = check_definition def in @@ -282,6 +282,7 @@ let interp_mutual_inductive (paramsl,indl) notations finite = (* Instantiate evars and check all are resolved *) let evd = consider_remaining_unif_problems env_params !evdref in + let evd = Typeclasses.mark_resolvables evd in let evd = Typeclasses.resolve_typeclasses ~onlyargs:false ~fail:true env_params evd in let sigma = evd in let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map (nf_evar sigma) cl,impsl)) constructors in @@ -714,9 +715,9 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = in let fullcoqc = Evarutil.nf_evar !isevars def in let fullctyp = Evarutil.nf_evar !isevars typ in - let evm = Obligations.non_instanciated_map env isevars !isevars in + Obligations.check_evars env !isevars; let evars, _, evars_def, evars_typ = - Obligations.eterm_obligations env recname !isevars evm 0 fullcoqc fullctyp + Obligations.eterm_obligations env recname !isevars 0 fullcoqc fullctyp in ignore(Obligations.add_definition recname ~term:evars_def evars_typ evars ~hook) @@ -885,7 +886,7 @@ let do_program_recursive fixkind fixl ntns = Termops.it_mkNamedProd_or_LetIn typ rec_sign in let evars, _, def, typ = - Obligations.eterm_obligations env id evd (Evd.undefined_evars evd) + Obligations.eterm_obligations env id evd (List.length rec_sign) (nf_evar evd def) (nf_evar evd typ) in (id, def, typ, imps, evars) diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4 index 9840814b1..7f5991d38 100644 --- a/toplevel/g_obligations.ml4 +++ b/toplevel/g_obligations.ml4 @@ -46,6 +46,8 @@ open Pcoq open Prim open Constr +let sigref = mkRefC (Qualid (Pp.dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) + GEXTEND Gram GLOBAL: withtac; @@ -53,6 +55,12 @@ GEXTEND Gram [ [ "with"; t = Tactic.tactic -> Some t | -> None ] ] ; + + Constr.closed_binder: + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in + [LocalRawAssum ([id], default_binder_kind, typ)] + ] ]; END diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 529228d01..589403882 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -44,17 +44,17 @@ let succfix (depth, fixrels) = let mkMetas n = list_tabulate (fun _ -> Evarutil.mk_new_meta ()) n -let non_instanciated_map env evd evm = - List.fold_left - (fun evm (key, evi) -> - let (loc,k) = evar_source key !evd in - match k with - | QuestionMark _ -> Evd.add evm key evi - | ImplicitArg (_,_,false) -> Evd.add evm key evi - | _ -> - Pretype_errors.error_unsolvable_implicit loc env - evm (Evarutil.nf_evar_info evm evi) k None) - Evd.empty (Evarutil.non_instantiated evm) +let check_evars env evm = + List.iter + (fun (key, evi) -> + let (loc,k) = evar_source key evm in + match k with + | QuestionMark _ + | ImplicitArg (_,_,false) -> () + | _ -> + Pretype_errors.error_unsolvable_implicit loc env + evm (Evarutil.nf_evar_info evm evi) k None) + (Evd.undefined_list evm) type oblinfo = { ev_name: int * identifier; @@ -223,11 +223,12 @@ let map_evar_info f evi = evar_concl = f evi.evar_concl; evar_body = map_evar_body f evi.evar_body } -let eterm_obligations env name isevars evm fs ?status t ty = +let eterm_obligations env name evm fs ?status t ty = (* 'Serialize' the evars *) let nc = Environ.named_context env in let nc_len = Sign.named_context_length nc in - let evl = List.rev (to_list evm) in + let evm = Evarutil.nf_evar_map_undefined evm in + let evl = List.rev (Evarutil.non_instantiated evm) in let evl = List.map (fun (id, ev) -> (id, ev, evar_dependencies evm id)) evl in let sevl = sort_dependencies evl in let evl = List.map (fun (id, ev, _) -> id, ev) sevl in @@ -250,7 +251,7 @@ let eterm_obligations env name isevars evm fs ?status t ty = | Some t -> t, trunc_named_context fs hyps, fs | None -> evtyp, hyps, 0 in - let loc, k = evar_source id isevars in + let loc, k = evar_source id evm in let status = match k with QuestionMark o -> Some o | _ -> status in let status, chop = match status with | Some (Define true as stat) -> @@ -984,3 +985,18 @@ let next_obligation n tac = try array_find (fun x -> x.obl_body = None && deps_remaining obls x.obl_deps = []) obls with Not_found -> anomaly "Could not find a solvable obligation." in solve_obligation prg i tac + + +let init_program () = + Coqlib.check_required_library ["Coq";"Init";"Datatypes"]; + Coqlib.check_required_library ["Coq";"Init";"Specif"]; + Coqlib.check_required_library ["Coq";"Program";"Tactics"] + + +let set_program_mode c = + if c then + if !Flags.program_mode then () + else begin + init_program (); + Flags.program_mode := true; + end diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli index 1758082e8..16c00ce8f 100644 --- a/toplevel/obligations.mli +++ b/toplevel/obligations.mli @@ -29,7 +29,7 @@ val declare_definition_ref : Entries.definition_entry -> Impargs.manual_implicits -> global_reference declaration_hook -> global_reference) ref -val non_instanciated_map : env -> evar_map ref -> evar_map -> evar_map +val check_evars : env -> evar_map -> unit val mkMetas : int -> constr list @@ -38,7 +38,7 @@ val sort_dependencies : (int * evar_info * Intset.t) list -> (int * evar_info * (* env, id, evars, number of function prototypes to try to clear from evars contexts, object and type *) -val eterm_obligations : env -> identifier -> evar_map -> evar_map -> int -> +val eterm_obligations : env -> identifier -> evar_map -> int -> ?status:obligation_definition_status -> constr -> types -> (identifier * types * hole_kind located * obligation_definition_status * Intset.t * tactic option) array @@ -115,3 +115,5 @@ val admit_obligations : Names.identifier option -> unit exception NoObligations of Names.identifier option val explain_no_obligations : Names.identifier option -> Pp.std_ppcmds + +val set_program_mode : bool -> unit diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 20c9531fe..c727cc918 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1579,8 +1579,8 @@ let interp c = match c with let interp c = let mode = Flags.is_program_mode () in - let flag = mode || !program_flag in - Flags.program_mode := flag; + (try Obligations.set_program_mode !program_flag + with e -> program_flag := false; raise e); interp c; check_locality (); program_flag := false; Flags.program_mode := mode |