diff options
| author | Pierre-Marie Pédrot | 2014-01-08 09:06:58 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-01-10 17:46:36 +0100 |
| commit | 6058cdf5e70822e4501c61dfd969e4746c01145b (patch) | |
| tree | 08a86366100937b2f91742807c3ad76ec0848048 /tactics | |
| parent | a6ca35c30199f3ccf0ebb7d9b200190e345c4d50 (diff) | |
Exporting the full pretyper options in Goal.constr_of_raw.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/extratactics.ml4 | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index 031cbc7c5d..a1e57fd3c4 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -322,8 +322,6 @@ END (* Refine *) -let refine_tac = Tactics.New.refine - let refine_red_flags = Genredexpr.Lazy { Genredexpr.rBeta=true; @@ -341,7 +339,10 @@ let refine_tac (ist, c) = let constrvars = Tacinterp.extract_ltac_constr_values ist env in let vars = (constrvars, ist.Geninterp.lfun) in let c = Goal.Refinable.make begin fun h -> - Goal.Refinable.constr_of_raw h true true vars c + Goal.bind Goal.concl (fun concl -> + let flags = Pretyping.all_no_fail_flags in + let tycon = Pretyping.OfType concl in + Goal.Refinable.constr_of_raw h tycon flags vars c) end in Proofview.Goal.lift c >>= fun c -> Proofview.tclSENSITIVE (Goal.refine c) <*> |