diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-12 16:58:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-12 16:59:53 +0200 |
| commit | e4aa9817115b3d27eb7fca8fed86ffe397b868ad (patch) | |
| tree | efa8a3250bffa0a6fd7ac7d8c0f07ee17bc53734 | |
| parent | 5dc8187aa8e6b481338035a022fec4025a25eb33 (diff) | |
While we don't have a clean alternative to Clenvtac, add a primitive
for tclEVARS which might solve existing goals.
| -rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
| -rw-r--r-- | proofs/proofview.ml | 3 | ||||
| -rw-r--r-- | proofs/proofview.mli | 6 | ||||
| -rw-r--r-- | test-suite/typeclasses/deftwice.v | 9 |
4 files changed, 18 insertions, 2 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 94731b039..99ea2300c 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.ml @@ -123,7 +123,7 @@ let unify ?(flags=fail_quick_unif_flags) m = let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in try let evd' = w_unify env evd CONV ~flags m n in - Proofview.V82.tclEVARS evd' + Proofview.V82.tclEVARSADVANCE evd' with e when Errors.noncritical e -> (** This is Tacticals.tclFAIL *) Proofview.tclZERO (FailError (0, lazy (Errors.print e))) diff --git a/proofs/proofview.ml b/proofs/proofview.ml index bc6ce4fc6..a97add1ce 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -804,6 +804,9 @@ module V82 = struct let tclEVARS evd = Proof.modify (fun ps -> { ps with solution = evd }) + let tclEVARSADVANCE evd = + Proof.modify (fun ps -> { solution = evd; comb = undefined evd ps.comb }) + let tclEVARUNIVCONTEXT ctx = Proof.modify (fun ps -> { ps with solution = Evd.set_universe_context ps.solution ctx }) diff --git a/proofs/proofview.mli b/proofs/proofview.mli index 3b2dd7ccd..94969f3a5 100644 --- a/proofs/proofview.mli +++ b/proofs/proofview.mli @@ -334,8 +334,12 @@ module V82 : sig (* normalises the evars in the goals, and stores the result in solution. *) val nf_evar_goals : unit tactic - + + (* Assumes the new evar_map does not change existing goals *) val tclEVARS : Evd.evar_map -> unit tactic + + (* Assumes the new evar_map might be solving some existing goals *) + val tclEVARSADVANCE : Evd.evar_map -> unit tactic (* Set the evar universe context *) val tclEVARUNIVCONTEXT : Evd.evar_universe_context -> unit tactic diff --git a/test-suite/typeclasses/deftwice.v b/test-suite/typeclasses/deftwice.v new file mode 100644 index 000000000..439782c9e --- /dev/null +++ b/test-suite/typeclasses/deftwice.v @@ -0,0 +1,9 @@ +Class C (A : Type) := c : A -> Type. + +Record Inhab (A : Type) := { witness : A }. + +Instance inhab_C : C Type := Inhab. + +Variable full : forall A (X : C A), forall x : A, c x. + +Definition truc {A : Type} : Inhab A := (full _ _ _).
\ No newline at end of file |