diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-04 16:58:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-05-04 16:58:20 +0000 |
| commit | 783bdffba901a29027878f41e10b6bcfe406100f (patch) | |
| tree | 9c06d41adc21f0306e612d0897eb80667c0bf8b4 /toplevel/himsg.ml | |
| parent | ffafed95378e41b4c0ad57ab1c5664d3387a11d9 (diff) | |
Nettoyage de l'interface de Pfedit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@415 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/himsg.ml')
| -rw-r--r-- | toplevel/himsg.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 8b1fc69f3..079ad7ed1 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -310,7 +310,7 @@ let explain_refiner_cannot_unify m n = 'sTR"with"; 'bRK(1,1) ; pn >] let explain_refiner_cannot_generalize ty = - [< 'sTR "cannot find a generalisation of the goal with type : "; + [< 'sTR "Cannot find a well-typed generalisation of the goal with type : "; prterm ty >] let explain_refiner_not_well_typed c = |