diff options
| author | herbelin | 2001-07-24 16:33:42 +0000 |
|---|---|---|
| committer | herbelin | 2001-07-24 16:33:42 +0000 |
| commit | 12978666bf34dad8e5ec1207cc9e0b45d348dbb0 (patch) | |
| tree | 82c84d7512202d6f343a66a9d8853b1c6f91d06c | |
| parent | 9ecb3d8a50b7b7f3a79a945a00f445b9a7d89c33 (diff) | |
Suppression de l'affichage du non-reparsable 'Local constraint change'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1865 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/refiner.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index cfb5e64f92..ab7a4958ce 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -674,8 +674,8 @@ let extract_pftreestate pts = [< 'sTR "Attempt to save an incomplete proof" >]; let env = Global.env_of_context pts.tpf.goal.evar_hyps in strong whd_betaiotaevar env (ts_it pts.tpfsigma) pfterm - (*** - local_strong (whd_ise (ts_it pts.tpfsigma)) pfterm + (*** + local_strong (Evarutil.whd_ise (ts_it pts.tpfsigma)) pfterm ***) (* Focus on the first leaf proof in a proof-tree state *) @@ -797,7 +797,9 @@ let pr_rule = function | Prim r -> pr_prim_rule r | Tactic texp -> hOV 0 (pr_tactic texp) | Context ctxt -> pr_ctxt ctxt - | Local_constraints lc -> [< 'sTR"Local constraint change" >] + | Local_constraints lc -> + (* This is internal tactic and cannot be replayed at user-level *) + [< (* 'sTR"Local constraint change" *) >] exception Different |